编程智能体能否用 Lean 4 形式化验证真实 Rust 代码的行为？

HN Code LLM Research 发布日期待确认

i5h 基准测试

每道题都对应某个开源 Rust 应用的一项性质：它的安全相关逻辑（访问控制、输入校验、解析）被移植到 i5h，再提取成 Lean 4。智能体会拿到移植后的 Rust 代码、提取出的 Lean 代码以及一份规格说明，然后证明该性质成立。点击任意题目，可以查看上游原版 Rust、移植版本、两者如何互相校验、Lean 代码，以及各模型写出的证明。

仍在进行中

本基准测试还在测评中。下面的结果是阶段性快照：并非每个模型都跑完了所有题目，数字后续还会变化。

i5h 是什么

i5h 是一个 Rust Web 框架，它的应用逻辑可以在 Lean 4 中证明正确。

1. Rust：构建处理函数与状态变更
   用 Rust 的一个子集编写，由 axum 提供服务，配合 PostgreSQL 事务。

2. Aeneas：提取
   Aeneas 把那段 Rust 翻译成 Lean 4 定义，因此 Lean 里的代码就是真正运行的代码，而不是它的某种模型。

3. Lean 4：证明
   授权、租户隔离等不变量，变成关于这些定义的定理。

这个基准测试要问的是：编码智能体能否在真实代码上完成最后一步——把已有开源应用的逻辑移植到 i5h 之后的那一步。

方法

一道题是怎么造出来的，以及怎样才算解出它。

1. Rust：上游代码
   某开源应用的访问控制、输入校验和解析代码，锁定在某个固定提交（commit）上。

2. Rust：i5h 移植版
   逐个函数移植。字符串变成字节切片，迭代器变成循环；每一处改动都记录在移植版的偏差文件里。

3. Lean 4：提取出的模型
   Aeneas 提取移植后的代码。手写的规格说明把要证的性质表述成一条定理。

4. 智能体：尝试证明
   无网络；提供 i5h 的 Lean 库和相关技能；限时 40 分钟，若中途停止可恢复一次。

5. 评分器：是否通过？
   证明能通过构建，命题未被改动，且只用到 propext、Classical.choice 和 Quot.sound。

差分测试。 上游版本和 i5h 移植版在相同的随机输入上运行，必须返回相同结果。一个故意改坏的移植版必须无法通过。

没有提供给 agent。下面是基准测试自带的参考证明。每个任务下方展示的是模型写出、且评分器认可的证明。

应用程序

统计上游代码行数时，不计空行、注释和属性。

模型

已解决任务占已尝试任务的比例。各模型跑的任务不完全相同；每根柱子旁边标注的是任务数量。分钟数和成本只统计模型成功解决的任务。每行 Rust 代码的成本，按这些任务在标价下的花费计算，再除以这些性质所涉及操作的上游代码行数。

查看原文