通过扩大种子训练集规模，降低 Rust 系统证明合成的成本
软件工程
2026-05-12 v3
摘要
大型语言模型（LLM）在代码生成领域得到广泛应用，但由 LLM 生成的代码正确性仍是关切。其潜在解决方案是让 LLM 在生成代码的同时也生成形式化正确性证明。然而，与代码生成相比，代码-证明生成所需的推理能力更高，且现有学习数据更少。本文提出了 VeruSyn，一套用于 Verus（一种针对用 Rust 编写的系统软件的前沿级验证工具）的数据合成管道。通过自我合成和教程式合成，VeruSyn 实现了规模和 Verus 功能覆盖面均远超面向 Verus 的现有数据合成技术；VeruSyn 还通过智能体轨迹合成补充了长链思维（CoT）数据。借助 VeruSyn，我们合成了最大规模的 Verus 验证程序集合：690 万个 Rust 程序，每个程序都包含形式化规范及其满足该规范的证明。该数据集使我们能够创建一款在成本-证明权衡上优于 Claude Sonnet 4.5 等最先进商业模型的微调 Qwen2.5-Coder-32B-Instruct 模型，同时显著优于 o4-mini 和此前提出的研究模型。
引用
@article{arxiv.2602.04910,
title = {Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set},
author = {Nongyu Di and Tianyu Chen and Shan Lu and Shuai Lu and Yeyun Gong and Peng Cheng and Jacob R. Lorch and Yuan Yao and Xiaoxing Ma},
journal= {arXiv preprint arXiv:2602.04910},
year = {2026}
}