lean-dojo/TorchLean

这是什么？

核心功能

• 01在 Lean 中编写形状可检查的张量与神经网络层
• 02通过 LibTorch 在 CPU 或 CUDA 上训练，自动微分由 TorchLean 自身实现
• 03通过 FloatLib 选择数值精度，支持 binary32 与 binary128 等格式
• 04提供区间边界传播、鲁棒性检查等验证流程
• 05支持 PyTorch 模型与 Jaxpr 图的导入导出

适用场景

• 证明神经网络的性质，例如在某输入区域内预测结果的鲁棒性
• 在明确假设下研究张量计算的数值误差与舍入行为
• 在 Lean 中训练小型模型，同时保证模型定义可直接用于证明
• 研究机器学习系统的形式化验证

快速上手

1. 1

   克隆仓库

   git clone https://github.com/lean-dojo/TorchLean.git
2. 2

   进入项目目录

   cd TorchLean
3. 3

   获取预编译缓存

   scripts/lake.sh exe cache get
4. 4

   构建并运行 CPU 快速入门示例

   scripts/lake.sh build && scripts/lake.sh exe torchlean quickstart_mlp --device cpu --steps 10

使用前须知

• !GPU 运行需要支持 CUDA 的 LibTorch SDK 和 NVIDIA GPU。
• !在 GPU 上，LibTorch/ATen 实现是 Lean 证明之外的外部信任边界。

标签

常见问题

TorchLean 是什么？

基于 Lean 4 的框架，用于神经网络的形式化规约、执行与形式验证，支持形状检查的张量与类 PyTorch 训练。 TorchLean 在 Lean 4 中将通用张量计算、机器学习和数学证明整合在一起。它的张量在类型层面检查形状，可用于线性代数和数值算法；同一套模型定义既能用于训练、图变换和证书检查，也能用于证明。

TorchLean 可以免费使用吗？用的什么许可证？

TorchLean 以 MIT 许可证开源。用于商业产品前，请先确认许可证条款。

TorchLean 还在维护吗？

活跃维护中。TorchLean 最近一次提交是在 2026年10月29日。

TorchLean 适合用来做什么？

证明神经网络的性质，例如在某输入区域内预测结果的鲁棒性 在明确假设下研究张量计算的数值误差与舍入行为 在 Lean 中训练小型模型，同时保证模型定义可直接用于证明 研究机器学习系统的形式化验证

TorchLean 怎么安装和运行？

克隆仓库: git clone https://github.com/lean-dojo/TorchLean.git 进入项目目录: cd TorchLean 获取预编译缓存: scripts/lake.sh exe cache get 构建并运行 CPU 快速入门示例: scripts/lake.sh build && scripts/lake.sh exe torchlean quickstart_mlp --device cpu --steps 10

在哪里获取 TorchLean？

源代码和安装说明在 GitHub 上：https://github.com/lean-dojo/TorchLean