Self-Modifying Lean Proof Agents with Verifier-Grounded Benchmark Coevolution

• URL: http://arxiv.org/abs/2607.17352v1
• Date: Sun, 19 Jul 2026 17:26:59 GMT
• Title: Self-Modifying Lean Proof Agents with Verifier-Grounded Benchmark Coevolution
• Abstract summary: We present a self-evolving Lean proof agent in which a small fixed workspace wraps a fully mutable proof workflow, prompts, and tools.<n>Unlike most self-evolving systems, which optimize against a fixed external benchmark, our system coevolves the agent and its benchmark.<n>The best coevolving agent reaches a 45.1% held-out solve rate, versus 12.7% for the seed and 32.0% for the best fixed-benchmark agent.
• Score: 20.44043749792232
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Designing effective Lean proof agents is a central challenge in formal mathematical reasoning. Beyond building stronger provers, recent work emphasizes the workflow around Lean: how an agent decomposes proof obligations, uses tools and compiler feedback, diagnoses failures, repairs proofs, and maintains structured proof context. Motivated by code-level self-evolving agents, we study whether such workflows can be evolved rather than hand-designed. We present a self-evolving Lean proof agent in which a small fixed, trusted runtime wraps a fully mutable workspace: the proof workflow, prompts, and tools. Unlike most self-evolving systems, which optimize against a fixed external benchmark, our system coevolves the agent and its benchmark. Between generations, the highest-scoring agent (the champion) revises the active task distribution through a mastery-throttled curriculum update that introduces harder proof obligations only after the current level is mastered, and a single-anchor recalibration re-runs the champion on the updated benchmark to keep scores comparable as difficulty rises. All evolution stays inside a Lean-grounded verification loop: however the agent rewrites itself, a success counts only when its behavior yields Lean-verified proofs under a trusted snapshot, and each attempt must emit a machine-readable, Lean-grounded proof context whose representation may evolve but whose groundedness is enforced. We run the coevolving trajectory and a fixed-benchmark baseline for 15 active generations and compare them on a held-out miniF2F test split. The best coevolving agent reaches a 45.1% held-out solve rate, versus 12.7% for the seed and 32.0% for the best fixed-benchmark agent, showing that verifier-grounded self-evolution can improve Lean proof workflows under a coevolving benchmark.

Related papers

• HarnessEvolve: Learning from Reference Trajectories for Reliable Agent Self-Evolution [11.431479238875712]
  We introduce HarnessEvolve, a self-evolving framework that learns from reference trajectories to achieve reliable agent self-evolution.<n>We conduct extensive experiments on several benchmarks spanning open-domain and enterprise scenarios, using different models and agent frameworks.<n>Results demonstrate that HarnessEvolve consistently outperforms state-of-the-art baselines across all benchmarks and settings.
  arXiv  Detail & Related papers  (2026-09-01T07:31:18Z)
• TTHE: Test-Time Harness Evolution [50.26245555541721]
  Existing approaches optimize such harnesses before deployment, searching training or development data for a fixed agent workflow that is then frozen at test time.<n>We ask whether the harness can instead be optimized during evaluation itself, using only the unlabeled execution traces the agent produces on the test inputs.<n>During evaluation, TTHE maintains a population of candidate harnesses and refines them through an agentic proposer that reasons over their execution traces.<n>A judge then commits an improved harness from execution-derived proxy signals, and the selected program persists to govern subsequent inputs.
  arXiv  Detail & Related papers  (2026-07-09T05:53:39Z)
• EvoAgentBench: Benchmarking Agent Self-Evolution via Ability Transfer [25.657960361149833]
  EvoAgentBench is a benchmark for agent self-evolution via Ability-guided transfer.<n>Every test task is backed by verified training-side Ability support.
  arXiv  Detail & Related papers  (2026-07-06T15:17:09Z)
• The Red Queen Gödel Machine: Co-Evolving Agents and Their Evaluators [17.44053709945519]
  Self-improving agents are state-of-the-art (SOTA) on agentic coding benchmarks and have recently been extended to general domains.<n>We introduce the Red Queen Godel Machine (RQGM), an evolutionary framework for self-improvement under non-stationary utilities.<n>We show that the RQGM improves test pass rate over the prior SOTA by adding a complementary agent-as-a-judge code-review signal.<n>We then turn to scientific paper writing and reviewing, and Olympiad-level proof writing and grading, where the RQGM improves performance over prior self-improving agents
  arXiv  Detail & Related papers  (2026-06-24T18:38:26Z)
• Self-evolving LLM agents with in-distribution Optimization [60.05867547965365]
  Large Language Models (LLMs) have recently emerged as powerful controllers for interactive agents in complex environments.<n>We propose Q-Evolve, a self-evolving framework for LLM agents that unifies automatic process-reward labeling and policy learning.<n>We evaluate our method on AlfWorld, WebShop, and ScienceWorld, showing Q-Evolve outperforms strong baselines in sample efficiency, robustness, and overall task performance.
  arXiv  Detail & Related papers  (2026-06-05T15:09:52Z)
• AgentV-RL: Scaling Reward Modeling with Agentic Verifier [63.55502685076245]
  Verifiers have been demonstrated to enhance LLM reasoning via test-time scaling (TTS)<n>We propose Agentic Verifier, a framework that transforms reward modeling into a multi-turn, tool-augmented deliberative process.<n>We show that Agentic Verifier yields consistent performance gains under both parallel and sequential TTS.
  arXiv  Detail & Related papers  (2026-04-17T12:27:36Z)
• FRESCO: Benchmarking and Optimizing Re-rankers for Evolving Semantic Conflict in Retrieval-Augmented Generation [73.22935457705057]
  We introduce FRESCO, a benchmark for evaluating re-rankers in temporally dynamic contexts.<n>By pairing recency-seeking queries with historical Wikipedia revisions, FRESCO tests whether re-rankers can prioritize factually recent evidence while maintaining semantic relevance.<n>Our evaluation reveals a consistent failure mode across existing re-rankers: a strong bias toward older, semantically rich documents, even when they are factually obsolete.
  arXiv  Detail & Related papers  (2026-04-14T17:04:25Z)
• CoVerRL: Breaking the Consensus Trap in Label-Free Reasoning via Generator-Verifier Co-Evolution [52.691495954442985]
  CoVerRL is a framework where a single model alternates between generator and verifier roles, with each capability bootstrapping the other.<n> Experiments across Qwen and Llama model families demonstrate that CoVerRL outperforms label-free baselines by 4.7-5.9% on mathematical reasoning benchmarks.<n>Self-verification accuracy improves from around 55% to over 85%, confirming that both capabilities genuinely co-evolve.
  arXiv  Detail & Related papers  (2026-03-18T14:38:55Z)
• AgentDevel: Reframing Self-Evolving LLM Agents as Release Engineering [8.201374511929538]
  AgentDevel is a release engineering pipeline that iteratively runs the current agent.<n>It produces implementation-blind, symptom-level quality signals from execution traces.<n>It aggregates dominant symptom patterns and produces auditable engineering specifications.
  arXiv  Detail & Related papers  (2026-01-08T05:49:01Z)
• Towards Self-Evolving Benchmarks: Synthesizing Agent Trajectories via Test-Time Exploration under Validate-by-Reproduce Paradigm [60.36837655498119]
  We propose a Trajectory-based validated-by-Reproducing Agent-benchmark Complexity Evolution framework.<n>This framework takes an original task from an existing benchmark and encourages agents to evolve it into a new task with higher difficulty.<n>Experiments on the GAIA benchmark demonstrate that the TRACE framework consistently enhances task complexity while improving the reliability of correctness.
  arXiv  Detail & Related papers  (2025-10-01T01:52:52Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.