Self-evolving Lean proof agents reach 45.1% on miniF2F with coevolving benchmarks
omarsar0 · x · 2026-07-22
A paper on self-modifying Lean proof agents argues that agents should co-evolve with their benchmarks instead of optimizing against a fixed test set.
- The system uses a small trusted runtime around a fully mutable workspace covering workflow, prompts, and tools.
- Between generations, the current champion updates the task distribution with a mastery-throttled curriculum, adding harder proof obligations only after the current level is mastered.
- A single-anchor recalibration reruns the champion on the updated benchmark so scores stay comparable as difficulty rises.
- All success is grounded in a Lean verifier: a result only counts if it produces verified proofs under a trusted snapshot.
- Over 15 generations, the best coevolving agent reaches 45.1% held-out solve rate on miniF2F, versus 12.7% for the seed and 32.0% for the best fixed-benchmark agent.
The paper argues that verifier-grounded self-evolution can improve formal proof workflows while avoiding reward hacking.
More from AGI Musings
- AI Safety Researcher Warns Current Crisis Could Lead to Loss of Control, Proposes 3 Fixes — LuizaJarovsky · 2026-10-26
- Ben Thompson's 'The End of the Internet': when creation goes free, winners go small — tushaarmehtaa · 2026-10-26
- Revolut CEO: China's 9/9/6 work culture makes it unbeatable — only 2 of 140 startups survived — davidsenra · 2026-10-26
- AI Is Redistributing Technical Power Inside Companies, Not Just Creating New Roles — mdancho84 · 2026-10-26
- Two New Papers Quantify AI's Impact on India's Labour Market With PLFS Data — ravi_iitm · 2026-10-26
- AI thinking is to human thought what planes are to bird flight — js_craft_hq · 2026-10-26