TorchLean:用 Lean 4 形式化神经网络与 GPU 执行验证
srush_nlp · x · 2026-09-16
Caltech 等 团队发布 TorchLean，一个用 Lean 4 编写的神经网络形式化代码库，入选 ICML 2026 AI4Math Workshop Spotlight。作者 Sasha Rush 提及此前的 Lean Verified Transformers 项目——用 Lean 从零证明一系列 Transformer 不变量，并推测对现实世界代码做同样事情的难度。
TorchLean 主要贡献：
- 类型化张量与层 API：可直接在 Lean 中编写神经网络程序，显式建模张量布局、预处理、编译边界、浮点运算与模型导出等接口。
- 完整运行时：PyTorch 风格 API、通过带 op 标签的 SSA/DAG 图 IR 支持即时与编译执行、反向模式自动微分、优化器。
- CUDA/GPU 后端：原生 kernel、CPU stub、Compute Sanitizer 检查与 Nsight profiling 钩子。
- 显式信任边界：覆盖外部 FFI、PyTorch 导入/导出、Python/Julia/Arb oracle、α,β-CROWN 证书与 CUDA kernel。
- Float32/IEEE-754 语义与验证：支持 IBP 及 CROWN/LiRPA 风格验证。
- 模型动物园：涵盖 MLP、CNN、ResNet、ViT、GPT-2、Mamba/SSM、扩散模型、MAE 自监督、强化学习、PINNs 与 3D 几何证书 demo。
「研究」频道最新
- Greg Brockman 官宣:OpenAI 在又一个千禧年数学难题上取得重大进展 — scaling01 · 2026-09-16
- OmegAMP 预印本:生成式 AI 可编程设计抗菌肽,204 条实验验证含体内疗效 — AllThingsApx · 2026-09-16
- Agent 基准新增真实故障任务:缓存令牌冒充用户 40 分钟 — Kind-Atmosphere9655 · 2026-09-16
- 千禧年大奖难题之争:OpenAI 疑与含 Anthropic 研究者的团队赛跑解 Navier-Stokes — thursdai_pod · 2026-09-16
- MICAFlow 论文发布：快速稳健的 MRI 预处理管线打通科研与临床 — bttyeo · 2026-09-16
- 自进化研究智能体 Épi 数日刷出 120 项纪录，改写 Klarner 常数上界 — my_cat_can_code · 2026-09-16