Research map / Large language models / Agents, code and math
Automated Proof Generation for Rust Code via Self-Evolution
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes SAFE, a self-evolving framework that synthesizes Verus specifications and proofs for Rust code, fine-tuning open LLMs (DeepSeekCoder-33B) on verifier-filtered proofs plus self-debugging data, reaching 52.52% on VerusBench versus GPT-4o's 14.39%.
Problem
Automated proof generation for Rust code in the Verus verifier is limited by severe scarcity of Verus programs, specifications, and proofs, so data-hungry fine-tuning approaches used for Lean and F* do not directly apply.
Approach
A self-evolving loop in which GPT-4o bootstraps data, then fine-tuned open models generate specifications (filtered by test-based correctness/completeness scores via Verus) and proofs (filtered by the Verus verifier); incorrect proofs paired with verifier errors and later correct proofs form self-debugging training data.
Key results
- On VerusBench, SAFE with DeepSeekCoder reaches 43.17% Accuracy@1 by direct generation versus GPT-4o's 11.51%; SAFE+ reaches 70.50% Accuracy@100.
- Accuracy@2 with self-debugging (SAFE+) on VerusBench reaches 52.52% for LLaMa3.1 versus GPT-4o's 14.39%.
- On CodeNet-Test, SAFE with DeepSeekCoder reaches 43.83% Accuracy@1 versus GPT-4o's 0.28%.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| fine-tune DeepSeekCoder with SAFE self-evolution for direct proof generation | DeepSeekCoder-33B-Instruct · VerusBench | Accuracy@1: 9.35 -> 43.17 | Helped |
| fine-tune DeepSeekCoder with SAFE self-evolution for direct proof generation | DeepSeekCoder-33B-Instruct · CodeNet-Test | Accuracy@1: 0.21 -> 43.83 | Helped |
| apply self-debugging to an initial proof | SAFE DeepSeekCoder · VerusBench | Accuracy@2: 46.76 -> 49.64 | Helped |
| apply self-debugging to an initial proof | SAFE DeepSeekCoder · CodeNet-Test | Accuracy@2: 44.74 -> 48.43 | Helped |
| continue self-evolution from Round 1 to Round 2 (ablation) | SAFE DeepSeekCoder · VerusBench | Accuracy@1: 32.37 -> 42.45 | Helped |
| continue self-evolution from Round 2 to Round 3 (ablation) | SAFE DeepSeekCoder · VerusBench | Accuracy@10: 49.64 -> 53.96 | Helped |
| train using low-quality specifications only instead of selected high-quality specifications (ablation) | SAFE DeepSeekCoder · VerusBench | Accuracy@1: 43.17 -> 17.27 | Hurt |
| mix low-quality specifications with high-quality specifications (ablation) | SAFE DeepSeekCoder · VerusBench | Accuracy@1: 43.17 -> 30.22 | Hurt |
| use self-debugging instead of direct generation at Accuracy@2 | SAFE LLaMa3.1 · VerusBench | Accuracy@2: 48.20 -> 52.52 | Helped |
| use self-debugging instead of direct generation at Accuracy@2 | SAFE LLaMa3.1 · CodeNet-Test | Accuracy@2: 45.34 -> 48.50 | Helped |
Surprising findings
- Training only on low-quality specification data drops SV accuracy@1 to 0%, showing that specification quality matters more than quantity.
- Increasing self-debugging rounds beyond one hardly improves accuracy (under 1%), and sampling helps more in generation than in debugging.
Limitations
- Focuses on small single-function Rust programs; scaling to large projects with cross-function dependencies is untested.
- About 20.86% of VerusBench programs remain unproved even at Accuracy@100, e.g., those requiring reveal features absent from training data.
- Self-debugging gains saturate after one round of debugging.
Experimental setup
Datasets: MBPP training split CodeNet training Rust programs VerusBench SV-COMP-2021 translated tasks MBPP-DFY-153
Benchmarks: VerusBench CodeNet-Test
Metrics: Accuracy@1 Accuracy@2 Accuracy@10 Accuracy@100
Baselines: GPT-4o DeepSeekCoder-33B-Instruct Llama3.1-8B-Instruct
Builds on: expert iteration self-training Verus DeepSeekCoder
Closest papers by meaning
- AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement (ICML 2025 · similarity 0.88)
- CLEVER: A Curated Benchmark for Formally Verified Code Generation (NeurIPS 2025 · similarity 0.86)
- Verify0: Can AI Agents Build Formally Verified Software Repositories? (NeurIPS 2026 · similarity 0.86)
- Synthetic Programming Elicitation for Text-to-Code in Very Low-Resource Programming and Formal Languages (NeurIPS 2024 · similarity 0.85)
- Teaching Large Language Models to Self-Debug (ICLR 2024 · similarity 0.84)
- APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · similarity 0.84)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.