Sasha Rush 用 Lean 形式化验证 JAX 机器学习代码

普林斯顿 NLP 学者 Sasha Rush 发布 Provably Correct Tensor Puzzles，将流行的 Tensor Puzzles 升级为「可证明正确」版本。他构建了一个 Jax-Lean 转译器，能把 JAX 代码翻译到 Lean 定理证明器中，从而对张量谜题乃至任意 Python 机器学习代码进行形式化验证，让 ML 代码的正确性获得严格的数学证明。

2026-10-09 ~ 2026-10-09 · 2 条相关

• srush 构建 Jax-Lean 转译器，形式化验证张量谜题与任意 JAX 代码 — srush_nlp · 2026-10-09
• srush 发布 Provably Correct Tensor Puzzles,用 Lean 形式化验证 ML 代码 — srush_nlp · 2026-10-09