TorchLean 代码库现已开放！TorchLean 是一个用于验证神经网络软件的 Lean 4 框架。它支持带类型的张量、可运行的训练、图中间表示、经验证的反向模式自动微分、Float32/IEEE 语义、CROWN/IBP 风格的验证、证书检查、PyTorch 互操作以及 CUDA/GPU 执行。根据我们最初帖子收到的反馈与评论，我们大幅扩展了 TorchLean：神经算子/FNO、扩散模型、GPT 风格的文本模型、GPT-2 风格的运行、Mamba/状态空间模型、强化学习、3D 视觉证书、Bug Zoo 案例研究、PyTorch 互操作等等。项目页面：https://lean-dojo.github.io/TorchLean/ 代码库：https://github.com/lean-dojo/TorchLean… @Robertljg, Jennifer Cruden, Will Adkisson, Xiangru Zhong, @huan_zhang12 @caltech #MachineLearning #ScientificComputing #Lean #FormalVerification

TorchLean

来源：https://lean-dojo.github.io/TorchLean/ TorchLean 在 Lean 4 中对神经网络基础设施进行了形式化，连接了带类型的张量和层规约、可运行的训练示例、图中间表示语义、浮点契约、CUDA 信任边界以及可供 Lean 检查器审查的工件。

其目标是在现代机器学习工作流与形式化推理之间架设一座实用的桥梁：模型可以被执行、降阶、审查、从 PyTorch 风格的管线导入，并根据明确的数学契约进行检查。

TorchLean 为你提供什么

TorchLean 概览：带类型的张量、共享图中间表示、经验证的反向模式自动微分、IEEE-754 语义、证书检查、PyTorch 往返、CUDA 信任边界、逼近定理以及 Lean 验证。

它适合的位置

TorchLean 处于人们已经在使用的软件与他们希望信任的证明工件之间。该项目使用 Lean 4（https://lean-lang.org/）编写，并在能使模型代码更易读的地方采用 PyTorch 风格的接口。对于 Python 生态，请参阅官方 PyTorch 文档（https://pytorch.org/docs/stable/index.html）；对于 Lean 本身，请从 Lean 文档（https://lean-lang.org/documentation/）开始。

论文 / 引用

@misc{george2026torchleanformalizingneuralnetworks,
      title={TorchLean: Formalizing Neural Networks in Lean},
      author={Robert Joseph George and Jennifer Cruden and Xiangru Zhong and Huan Zhang and Anima Anandkumar},
      year={2026},
      eprint={2602.22631},
      archivePrefix={arXiv},
      primaryClass={cs.MS},
      url={https://arxiv.org/abs/2602.22631},
}