Jax-Lean转译器

一项名为“Provably Correct Tensor Puzzles”的工作构建了Jax到Lean的转译器，用于对Python机器学习代码进行形式化验证。

该工作使用“张量谜题”作为测试用例来验证Jax-Lean转译器的正确性。

当前工作很可能仅覆盖确定性的、整数或精确有理数范围内的张量操作，浮点与随机性仍是待攻克的开放问题。

如果Jax-Lean转译器成熟，开发者可以在编写Jax代码的同时获得形式化保证，尤其适用于安全关键的AI应用。