Rust自动证明代理

90%正确率

首个针对Rust代码自动生成形式化正确性证明的多代理系统，显著超越现有基于LLM的代码验证方法。

Yang, Chenyuan · Xuheng, Li · Misu, Md Rakib Hossain · Yao, Jianan · Cui, Weidong · 宫叶云 · Hawblitzel, Chris · Lahiri, Shuvendu K. · Lorch, Jacob R. · Lu, Shuai · 杨帆 · Zhou, Ziqiao · Lu, Shan

Proceedings of the ACM on Programming Languages 2025

参数信息

证明成功率
90 %
任务完成时间或调用次数
50 %
完成时间阈值
30 seconds
LLM调用次数阈值
3
证明任务数量
150

技术优势

无需人工干预

通过多代理网络模拟人类专家的证明构建过程，自动生成、优化和调试证明，大幅减少人工参与。

高效省时

超过一半的任务在30秒内或3次LLM调用内完成，显著降低验证时间成本。

适用范围广

在基于现有代码生成基准和验证基准构建的150个非平凡证明任务上取得高成功率，覆盖多种代码类型。

应用场景