AlphaVerus
A model translates programs into Verus, tree search repairs them with verifier feedback, and a filter keeps trustworthy results as examples.
The loop
- Proposes
Verus translations of programs (from Dafny) and repaired versions, from a Llama 3.1 70B model
- Judged by
The Verus verifier, plus a filter that rejects translations whose specification or program is misaligned
- Steers
Treefinement tree search fixes errors from verifier feedback; verified, filtered programs become prompt examples
Headline result
With Llama 3.1 70B and no model fine-tuning, verified-code generation reaches 32.9% on HumanEval-Verus and 65.7% on MBPP-verified (pass@256), versus 27.1% and 35.9% for GPT-4o and 11.8% and 26.9% for Llama 3.1 70B.
What this does not prove
HumanEval-Verus and MBPP-verified are small, hand-adapted benchmarks, and the task is generating code plus proofs from specifications. Verification proves code matches the specification, so the misalignment filter matters.
How it generalizes the harness
Verus judges validity, a tree of candidate repairs is searched, and a built-in filter guards against the model gaming the verifier.
Classification
| What it proposes | Program |
|---|---|
| Generative model | Llama 3.1 70B (frozen, no fine-tuning) |
| Algorithmic authority | Verus verifier with a misalignment filter |
| Feedback | Verifier errors |
| What gets updated | Prompt context and search tree |
| When it runs | At inference time |
| Validity | Formal (machine-checked) |
| Evidence | Experiments reported |
| Lineage | Original system |