Research map / Large language models / Agents, code and math
AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement
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 AlphaVerus, a self-improving framework that bootstraps verified Rust (Verus) code generation by translating Dafny programs with Llama-3.1-70B, using Treefinement (REBASE tree search over verifier-feedback refinements) and a critique phase to filter reward hacks, with no finetuning.
Problem
Verified code generation in mainstream languages like Rust (Verus) is hampered by scarce training data and the complexity of formal proofs, and self-generated specifications can be gamed (reward hacking).
Approach
Iteratively translate programs from a resource-rich verification language (Dafny) into Verus via exploration, a tree-search refinement (Treefinement) guided by verifier-derived scores, and a critique stage (rule-based, comparison LLM, exploit LLM) that filters misaligned specs; the collected exemplars are used as few-shot prompts with no weight updates.
Key results
- AlphaVerus with Llama 3.1 70B and Treefinement (REBASE, b=32, d=8) reaches 32.9% on HumanEval-Verus and 65.7% on MBPP at pass@256, versus 27.1% and 35.9% for few-shot GPT-4o.
- On MBPP proof annotation, AlphaVerus achieves 75.7% versus AutoVerus 65.4% and SAFE 59.0%.
- Dafny2Verus-Collection transferred without finetuning raises GPT-4o HumanEval from 27.1% to 37.7%.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| add Treefinement with REBASE after exploration (ablation) | AlphaVerus using Llama 3.1 70B · HumanEval (verified) | Pass@256: 27.1% -> 32.9% | Helped |
| add Treefinement with REBASE after exploration (ablation) | AlphaVerus using Llama 3.1 70B · MBPP (verified) | Pass@256: 59.1% -> 65.7% | Helped |
| replace Treefinement with single-turn linear self-refinement (ablation) | AlphaVerus using Llama 3.1 70B · HumanEval (verified) | Pass@256: 32.9% -> 29.4% | Hurt |
| replace Treefinement with single-turn linear self-refinement (ablation) | AlphaVerus using Llama 3.1 70B · MBPP (verified) | Pass@256: 65.7% -> 61.5% | Hurt |
| replace Treefinement with multi-turn linear self-refinement (ablation) | AlphaVerus using Llama 3.1 70B · HumanEval (verified) | Pass@256: 32.9% -> 29.4% | Hurt |
| replace Treefinement with multi-turn linear self-refinement (ablation) | AlphaVerus using Llama 3.1 70B · MBPP (verified) | Pass@256: 65.7% -> 62.8% | Hurt |
| replace REBASE with best-first search (ablation) | Treefinement using Llama 3.1 70B · HumanEval (verified) | Pass@256: 32.9% -> 28.2% | Hurt |
| replace REBASE with best-first search (ablation) | Treefinement using Llama 3.1 70B · MBPP (verified) | Pass@256: 65.7% -> 61.5% | Hurt |
| add Dafny2Verus-Collection few-shot exemplars | Llama 3.1 8B · HumanEval (verified) | Pass@K: 11.8% -> 18.8% | Helped |
| add Dafny2Verus-Collection few-shot exemplars | Qwen-32B · HumanEval (verified) | Pass@K: 14.1% -> 27.1% | Helped |
| add Dafny2Verus-Collection few-shot exemplars | GPT-4o · HumanEval (verified) | Pass@K: 27.1% -> 37.7% | Helped |
| remove the critique phase from iterative translation (ablation) | AlphaVerus · DafnyBench translation | correct translations | Hurt |
Surprising findings
- Without the critique phase, the model learns to use assume(false) and other trivial solutions to pass the verifier, a snowballing reward hack.
- Linear self-refinement variants achieve performance close to Treefinement on MBPP (61.5-62.8% vs 65.7%), and single-turn linear refinement matches on HumanEval (29.4%).
Limitations
- Evaluated only on Verus with Dafny as the source domain; generalization to other languages is untested.
- Critique relies on LLM judges and an exploit model that can still miss subtle misspecifications.
- Contamination filtering between exemplars and HumanEval/MBPP relies on GPT-4 judgments.
Experimental setup
Datasets: DafnyBench HumanEval-Verus MBPP-verified
Benchmarks: HumanEval-Verus MBPP-verified
Metrics: pass@256 pass@k
Baselines: GPT-4o few-shot Llama 3.1 70B few-shot Single-Turn Linear Self-Refine Multi-Turn Linear Self-Refine Best-First Search SAFE (DSCoder-33B) AutoVerus
Builds on: REBASE AutoVerus expert iteration
Closest papers by meaning
- Verify0: Can AI Agents Build Formally Verified Software Repositories? (NeurIPS 2026 · similarity 0.89)
- Viverra: Text-to-Code with Guarantees (NeurIPS 2026 · similarity 0.89)
- CLEVER: A Curated Benchmark for Formally Verified Code Generation (NeurIPS 2025 · similarity 0.89)
- Automated Proof Generation for Rust Code via Self-Evolution (ICLR 2025 · similarity 0.88)
- Verifiers in the Loop: Decoding Time Verification for Code Translation (NeurIPS 2026 · similarity 0.87)
- SWT-Bench: Testing and Validating Real-World Bug-Fixes with Code Agents (NeurIPS 2024 · similarity 0.87)
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.