TorchLean 获 AI for Math 基金资助，用 Lean 形式化验证神经网络

AnimaAnandkumar · x · 2026-10-07

Caltech 团队（含 Anima Anandkumar）的 TorchLean 项目入选 2026 年 AI for Math Fund 资助名单。该基金由 XTX Markets 出资，本轮共 1710 万美元、累计承诺 3510 万美元，从 50 个国家 400+ 申请中选出 22 个获奖者。

TorchLean 是一个 Lean 4 代码库，用于神经网络的形式化规范、执行与验证，已覆盖自动微分、浮点语义、验证乃至 GPU 执行，并在主流 ML 栈中发现了多处 bug 与语义不一致； major 公司和美国国家实验室团队已开始用它做 ML 验证。下一步目标是形式化验证 GPU 执行与 kernel 验证。