Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911666011111424 |
|---|---|
| author | Di, Nongyu Chen, Tianyu Lu, Shan Lu, Shuai Gong, Yeyun Cheng, Peng Lorch, Jacob R. Yao, Yuan Ma, Xiaoxing |
| author_facet | Di, Nongyu Chen, Tianyu Lu, Shan Lu, Shuai Gong, Yeyun Cheng, Peng Lorch, Jacob R. Yao, Yuan Ma, Xiaoxing |
| contents | Large Language Models (LLMs) are widely used for code generation. However, the correctness of code generated by LLMs remains a concern. A potential remedy to this concern is to have LLMs generate formal correctness proofs along with such code. However, compared with code generation, code-proof generation requires much higher reasoning capability and has much less existing data to learn from. In this paper, we present VeruSyn, a data synthesis pipeline for Verus, a state-of-the-art verification tool for system software written in Rust. Through self-synthesis and tutorial-based synthesis, VeruSyn achieves much larger scale and Verus-feature coverage than previous data-synthesis techniques designed for Verus; VeruSyn also supplements its dataset with long-chain-of-thought (CoT) data through agent trajectory synthesis. With VeruSyn, we synthesize the largest set of Verus verified programs: 6.9 million Rust programs, each with a formal specification and a proof that it meets that specification. This dataset lets us create a fine-tuned Qwen2.5-Coder-32B-Instruct model with appealing cost-proof tradeoff compared with state-of-the-art commercial models like Claude Sonnet 4.5. It also significantly outperforms models like o4-mini and previously proposed research models. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_04910 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set Di, Nongyu Chen, Tianyu Lu, Shan Lu, Shuai Gong, Yeyun Cheng, Peng Lorch, Jacob R. Yao, Yuan Ma, Xiaoxing Software Engineering Large Language Models (LLMs) are widely used for code generation. However, the correctness of code generated by LLMs remains a concern. A potential remedy to this concern is to have LLMs generate formal correctness proofs along with such code. However, compared with code generation, code-proof generation requires much higher reasoning capability and has much less existing data to learn from. In this paper, we present VeruSyn, a data synthesis pipeline for Verus, a state-of-the-art verification tool for system software written in Rust. Through self-synthesis and tutorial-based synthesis, VeruSyn achieves much larger scale and Verus-feature coverage than previous data-synthesis techniques designed for Verus; VeruSyn also supplements its dataset with long-chain-of-thought (CoT) data through agent trajectory synthesis. With VeruSyn, we synthesize the largest set of Verus verified programs: 6.9 million Rust programs, each with a formal specification and a proof that it meets that specification. This dataset lets us create a fine-tuned Qwen2.5-Coder-32B-Instruct model with appealing cost-proof tradeoff compared with state-of-the-art commercial models like Claude Sonnet 4.5. It also significantly outperforms models like o4-mini and previously proposed research models. |
| title | Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set |
| topic | Software Engineering |
| url | https://arxiv.org/abs/2602.04910 |