PaperlayerView exact revision on arXiv

Source-linked AI summary

ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving

Wenqian Ye, Ziwei Guan, Eric Xie, Bohan Liu, Shivani Modi, Buyun Zhang, Ellie Dingqiao Wen, Henry Kautz, Aidong Zhang

arXiv:2608.26334v1cs.AI

TL;DR

Existing neural theorem provers do not fully preserve verified progress across problems and often rely on sparse whole-proof feedback. ProofEvolve evolves Lean-verified partial proof DAGs with neural variation proposals, graded verified closure, and persistent typed schemas, achieving the highest average solve rate across three competition-level benchmarks.

  • Problem

    Existing systems either embed proof experience in model parameters, keep intermediate deductions within the current problem, or rely heavily on sparse whole-proof feedback.

  • Method

    ProofEvolve evolves explicit verified partial AND-OR proof DAGs, ranks them by kernel-grounded verified closure, and reuses kernel-checked schemas through typed recombination.

  • Results

    ProofEvolve achieves the highest average solve rate among evaluated systems across three competition-level Lean benchmarks.

  • Takeaways & Limitations

    Verified results from incomplete attempts can be preserved and made available for later proofs without weakening formal soundness.

  • Takeaways & Limitations

    Schema recombination remains sound only when Lean accepts a typed instantiation; mismatched retrieval fails without changing the trusted proof state.

Abstract

from arXiv · show

Automated theorem proving offers a natural foundation for recursive self-improvement in scientific discovery. However, existing neural provers do not fully preserve this recursive structure, where the learning process should be self-improving over time. Existing methods either embed proof experience into model parameters through expensive weight updates, or keep verified intermediate deductions only within the current problem. In addition, these methods also heavily rely on sparse whole-proof feedback, even when unsuccessful partial attempts contain useful discoveries. To close the gap, we propose ProofEvolve, a neuro-symbolic framework that evolves explicit, formally verified symbolic proof structures with neural models to decisively expand the knowledge boundary. In this framework, the neural model proposes variation operators, including decompositions, repairs, and schema recombinations. The symbolic Lean kernel verifies every proof transition. Over the evolution loops, ProofEvolve computes verified closure over the resulting proof directed acyclic graphs (DAGs). Within each problem, ProofEvolve evolves partial AND-OR proof DAGs in a behaviorally indexed archive. Across problems, kernel-checked schema extraction adds newly proved sub-DAGs to a persistent schema library. Proof DAGs inherit the solved results through typed schema recombination, with every residual premise exposed as a new subgoal. This evolutionary process preserves verified results from incomplete attempts and makes them available for later proofs without weakening formal soundness. Across three competition-level Lean benchmarks, ProofEvolve achieves the highest average solve rate among the evaluated proof systems.

1 Introduction

ProofEvolve addresses limitations in neural theorem proving by preserving verified partial structures within and across problems. It combines neural variation proposals with Lean-checked evolution, graded closure, and reusable theorem schemas, achieving the highest average solve rate across three competition-level Lean benchmarks.

  • Motivation: Proofs can yield reusable lemmas, hidden structures, and hypotheses beyond their stated conclusions, including through unsuccessful attempts.The paper motivates theorem proving as a route to cumulative scientific reasoning with formal correctness guarantees.
  • Limitations: Current systems mainly store experience in model parameters or reuse intermediate lemmas only within the current target.Training-based methods require another training cycle for later problems, while agentic memory remains target-specific.
  • Limitations: Useful verified structures from partial proofs are rarely inherited across searches, although small textual mutations can invalidate otherwise valuable complete proofs.The paper therefore argues for evolving verified partial structures rather than complete proof texts alone.
  • ProofEvolve: ProofEvolve uses neural proposals for decomposition, repair, and schema recombination, while Lean 4 verifies every proof transition.A behaviorally indexed archive retains diverse partial proof DAGs and ranks them by verified closure over proved subgoals.
  • ProofEvolve: Typed schema recombination instantiates closed sub-DAGs at matching goals, exposes residual premises as subgoals, and expands later search spaces.Across problems, kernel-checked extraction adds reusable theorem schemas to a persistent library.
  • Results: 57.8% average solve rate compares with 50.5% for LEAP and 45.9% for Hilbert across the evaluated benchmarks.On 744 disjoint Lean Workbook theorems, the prover’s own verified proofs improve solve rate by about four points over zero-shot, while random retrieval adds nothing.

2 Related Work

Prior work combines neural proof generation, agentic decomposition, retrieval, tree search, and evolutionary selection. ProofEvolve distinguishes itself by combining kernel-grounded verified closure with typed schema recombination during inference, without modifying model parameters.

  • Neural theorem proving: Neural theorem provers learn policies for tactic generation or proof completion, often combined with retrieval, tree search, synthetic proofs, fine-tuning, or reinforcement learning.The related systems include GPT-f, PACT, AlphaProof, and other learned proposal methods.
  • Agentic systems: Agentic systems structure proof search through decomposition, retrieval, repeated tactic execution, verifier feedback, and intermediate-lemma sharing.LEAP uses an AND-OR proof DAG to share lemmas across branches, while other systems recursively decompose or repair goals.
  • Evolutionary search: Evolutionary program search alternates language-model generation with automatic evaluation and selection, while MAP-Elites preserves diverse candidates across behavioral niches.Related approaches also expand lemma libraries, retrain retrievers, distill strategies, or modify agent code.
  • ProofEvolve: ProofEvolve combines verified closure and typed schema recombination so kernel-accepted partial proof structures are selected and newly closed sub-DAGs reused across problems.The framework performs this recursive improvement during inference without modifying the model.

3 Preliminaries

The preliminaries model Lean proofs as finite acyclic AND-OR DAGs whose nodes are tactic states and whose accepted hyperedges are kernel-checked proof constructors. Acyclic assembly supports reusable closed fragments while open goals remain available for further search.

  • Reusable structures: ProofEvolve retains each partial result rather than discarding it, allowing closed fragments from incomplete attempts to accumulate and transfer verified work.This retention property underpins later inheritance and recombination across searches.
  • Lean verification: Lean verification accepts a proof term only when it elaborates in the fixed environment without unresolved placeholders and has the target type.The kernel provides the formal verification condition for proof artifacts.
  • Proof DAGs: A proof attempt is a finite acyclic AND-OR DAG rooted at the target tactic state, with nodes representing tactic states.Accepted hyperedges connect a source obligation to the child obligations needed to construct it.
  • Proof DAGs: Alternative edges represent different proof steps, whereas every child of one hyperedge must be discharged; zero-child edges provide checked closing witnesses.DAG extensions preserve existing nodes, edges, labels, and edge realizers.
  • Proof assembly: Acyclicity makes proof assembly well founded, and a closed internal sub-DAG becomes a typed result even when its root remains open.The resulting fragment can be reused while the surrounding proof continues searching.

4 Neuro-Symbolic Evolution for Formal Automated Theorem Proving

ProofEvolve combines neural structural proposals with Lean-kernel verification to evolve proof DAGs, score partial progress, preserve diversity, and transfer verified schemas across targets. Its invariants ensure accepted proof states, extracted schemas, and returned proofs remain kernel-validated.

  • 4.1 Overview: ProofEvolve separates neural proposals from symbolic transitions: the model proposes edits and retrieval supplies premises, while only kernel-verified changes update trusted state.The operational state includes target-local DAG archives, a persistent schema library, and rejected proposals with Lean errors.
  • 4.2 Neural Proof Proposal: Accepted proposals extend DAGs with typed, kernel-checked edges; rejected proposals leave the proof archives and schema library unchanged.Decompositions expose typed intermediate obligations, and proposal-time holes become explicit child states before acceptance.
  • 4.2 Neural Proof Proposal: Verified closure converts binary root verification into graded fitness by evaluating proved internal obligations over the acyclic proof DAG.Alternative edges use a maximum, while conjunctive obligations use weighted child values, yielding ρ(D) ∈ [0, 1].
  • 4.2 Neural Proof Proposal: The archive preserves structural diversity by storing at most one DAG per behavioral descriptor and using verified closure to select stronger occupants.Descriptors encode binned depth, dominant tactic family, and schema-index region; ties favor the incumbent.
  • 4.2 Neural Proof Proposal: Frontier scheduling prioritizes the open state whose hypothetical closure would provide the largest structural gain.The priority is computed by counterfactually setting a frontier state's value to one in the closure recursion.
  • 4.3 Symbolic Knowledge Inheritance: Kernel-checked schema extraction abstracts newly closed states into quantified reusable schemas whose used hypotheses become explicit premises.Extraction follows the winning extension and returns no schema when generalization or the kernel judgment fails.
  • 4.3 Symbolic Knowledge Inheritance: Schema application uses typed substitutions, local witnesses, and residual child states, so Lean accepts recombination only after checking the complete instantiated realizer.Persistent schemas therefore enter later proofs as kernel-checked transformations rather than unchecked textual insertions.
  • 4.4 Theoretical analysis: Under the formal assumptions, accepted edges, closed nodes, extracted schemas, and returned proofs satisfy Lean-kernel judgments throughout execution.The schema library grows monotonically, and Corollary 1 establishes E; Γ0 ⊢K p : T for every returned proof.

5 Experiments

ProofEvolve is evaluated on competition-level Lean benchmarks, with kernel verification applied uniformly to solutions. Experiments examine verified-closure dynamics, operator contributions, budget scaling, and cross-problem proof reuse.

  • 5.2 Main results: ProofEvolve achieves the highest average solve rate at 57.8%, ahead of LEAP at 50.5% and Hilbert at 45.9%.
  • 5.2 Main results: 71.2% on PutnamBench leads LEAP by 6.5 points, while IMO-LeanProofBench reaches 53.3% against LEAP’s 36.7%.On CombiBench, LEAP and ProofEvolve are within one point at 50.0% and 49.0%, respectively.
  • 5.3 Dynamics of verified closure ρ: Verified closure ρ rises as Lean certifies intermediate subgoals, whereas failed runs plateau below one and binary pass/fail remains zero.A solved proof DAG shows ρ increasing step by step as lemma nodes are certified before root closure.
  • 5.4 Ablation study: On 60 IMO-LeanProofBench problems, the full system solves 32 on average, compared with 11 without decomposition.The full system solves 22 Basic and 10 Advanced problems; removing decomposition solves 9 Basic and 2 Advanced.
  • 5.5 Test-time budget scaling: Seven of eight open-weight configurations produce more kernel-verified transitions per target as the per-target budget grows.Low-effort gpt-oss-120b is the exception and remains flat across budgets.
  • 5.6 Old Proofs, New Theorems: Verified Reuse Across Problems: 19.8% of synthetic compositional targets are solved with a growing library versus 7.3% when the library resets, a 2.7× difference.Recombination remains sound because Lean accepts a typed schema instantiation only when it discharges the subgoal.
  • 5.6 Old Proofs, New Theorems: Verified Reuse Across Problems: At K=8, relevant retrieval raises solve rate from 49.5% to 53.4%, while random retrieval reaches 49.6%.The evaluation covers 744 screened Lean Workbook theorems disjoint from the source stream.

6 Conclusion

ProofEvolve evolves explicit, formally verified proof structures rather than relying only on complete proof texts. Its pipeline uses kernel-grounded closure, archived proof DAGs, and extracted schemas to preserve and reuse verified work.

  • 6 Conclusion: ProofEvolve represents partial proofs as AND-OR DAGs and ranks them using kernel-grounded verified closure.
  • 6 Conclusion: Neural models propose decompositions, repairs, and schema recombinations, while Lean 4 verifies every proof transition.
  • 6 Conclusion: The algorithm extracts kernel-checked schemas from accepted transitions and updates the target archive after each valid step.
  • 6 Conclusion: A completed DAG returns a proof only when verified closure reaches 1 and Lean checks the assembled result against the target.

B Proofs of Theoretical Results

The theoretical results establish that ProofEvolve preserves kernel-grounded proof state throughout finite executions. They also show that verified schemas accumulate monotonically and rejected proposals leave the schema library unchanged.

  • Theorem 1: Under the formal assumptions, every accepted edge has a checked realizer, every closed node has a valid proof, and every library schema is kernel-verified.
  • Proof of Theorem 1: Acyclicity supports the inner height induction used to establish valid proofs for closed nodes.
  • Proof of Theorem 1: The invariant proof proceeds by induction over transitions, distinguishing rejected proposals from kernel-accepted successor DAGs.Rejected steps update only the error store; accepted steps preserve old realizers and add a checked new edge.
  • Library monotonicity: If a transition rejects its proposal, the verified schema state remains unchanged: Σ_t+1 = Σ_t.
  • Library monotonicity: The schema library grows monotonically, with L_t ⊆ L_t+1 for every transition.

B.3 Validity of returned proofs

Returned ProofEvolve proofs are kernel-valid under Theorem 1’s assumptions. The validity argument relies on the return guard, Eq. (10), and Theorem 1(I2).

  • ProofEvolve returns a proof p only when it satisfies E; Γ0 ⊢K p : T.This is the stated validity guarantee for returned proofs under Theorem 1’s assumptions.
  • The validity result applies to proofs returned from an evolved DAG D′ ∈ Dn for target T with root r = (Γ0 ⊢ T).
  • The proof combines Algorithm 1’s return guard with Eq. (10) and Theorem 1(I2).

C Setup of Open-weight Models

The open-weight scaling study evaluates fixed targets, models, decoding settings, and Lean verification infrastructure under composite per-target budgets. The budgets jointly vary model calls, Lean calls, tokens, and wall-clock time.

  • Verification environment: All reported proofs elaborate in a frozen Lean 4 environment with a matched Mathlib commit and no unresolved metavariables or placeholders.The checks also exclude native_decide and include an independent #print axioms check.
  • Target set: The evaluation manifest contains 485 targets: 326 from PutnamBench, 60 from IMO-LeanProofBench, and 99 from CombiBench.Each target is scheduled with seeds 19, 36, and 65.
  • Serving infrastructure: Open-weight serving uses 8× NVIDIA B200 GPUs with dual-socket Intel Xeon hosts and approximately 3.9 TB RAM.
  • Verification environment: Proof verification uses Lean 4.29.1 with Mathlib commit 5e932f97 and pantograph 0.3.15.Claude Opus 4.8 proprietary baselines use vendor API inference plus local Lean kernel verification.
  • Decoding: Decoding parameters remain fixed across budget scales, with a 32,768-token per-call output cap.
  • Composite budget: Each composite budget jointly scales model calls, Lean calls, tokens, and wall-clock time relative to the 1× reference.The study therefore does not isolate any individual resource’s effect.

D Results of Test-Time Budget Scaling

As budgets increase, ProofEvolve generally records more verified search activity and more observed solve coverage, while the open-weight runs solve 11 distinct targets overall. All 139 recorded solve events were re-verified with zero false positives, but scaling curves have parser-related bias and do not establish per-model monotonicity.

  • Search activity: Seven of eight open-weight configurations produce more kernel-verified transitions per target as the budget grows.The low-reasoning gpt-oss-120b configuration is the exception and remains flat across budgets.
  • Limitations: Parser exits become more frequent in deeper searches, so recorded-outcome means may be biased upward at larger budgets.The curves are descriptive search activity rather than unbiased full-manifest estimates or proposal-efficiency measures.
  • Solves: Solve events rise from 28 at 0.25× to 44 at 2×, while the union of solved targets rises from 2 to 10.These are observed coverage counts from separate stochastic budget runs.
  • Solved-target inventory: Open-weight runs solve 11 distinct targets across all budgets and seeds: 4 from PutnamBench and 7 from CombiBench.None of the distinct solves comes from IMO-LeanProofBench.
  • Re-verification: 139 kernel-verified solve events have stored closing proofs, and re-verification finds 0 false positives.Every proof depends only on propext, Classical.choice, and Quot.sound, with no native_decide usage.
  • Verified substrate: The verified substrate contains 158 kernel-verified lemmas with no sorry occurrences and no axioms beyond the standard three.The library is inlined during re-verification so dependencies are checked transitively.

E.2 CombiBench

The section presents CombiBench proof examples in which Lean-verified proofs establish combinatorial, algebraic, and counting results through explicit formal constructions and tactics.

  • Counting and finite structures: 13 is the least group size that forces two people into the same month.The proof establishes membership using a cardinality argument and minimality by constructing an embedding for n ≤12.
  • Counting and finite structures: The proof of no order-2 magic square combines range, distinctness, row, column, and diagonal constraints before solving the integer system with omega.The theorem statement formalizes the impossibility of a 2 × 2 magic square.
  • Algebraic identities: gcd(F_m, F_n) = F_gcd(m,n) is proved by converting between N and Z formulations and applying a library identity.The proof uses the hypothesis d = Nat.gcd m n to connect the two formulations.
  • Algebraic identities: A permutation and its inverse have the same cycle type, proved with Equiv.Perm.cycleType_inv; all five models solve this target.The example requires only one transition and one call in the listed run.
  • Counting and finite structures: Kernel tactic decide verifies that 816 size-3 subsets of {1, . . . , 20} contain no consecutive elements.The proof explicitly avoids native_decide.
  • Combinatorial structures: A difference-set proof in Z21 supplies a multiplicity witness and verifies the result with kernel tactic decide rather than native_decide.The verified set is {0, 3, 4, 9, 11}.

F.8 Conditions, budget and compute

The evaluation compares retrieval conditions under fixed templates, one-attempt budgets, repeated runs, and substantial GPU compute.

  • Conditions and budget: Each theorem receives one attempt with no self-repair or second sample, while relevant retrieval uses K ∈{8, 16, 32, 64}.Library-size sweeps evaluate {1,000, 2,000, 4,000, full} at K=8, and random retrieval uses K=8.
  • Conditions and budget: Copy-rate analysis compares normalized accepted proof bodies with the eight proof bodies shown for each theorem.It counts cases where relevant retrieval closes a theorem that the corresponding zero-shot run leaves open.
  • Compute: 128 B200 GPUs build the library in about five hours, while a three-run sweep of one configuration takes about seven hours.The complete study uses a few thousand B200-GPU-hours across construction, sweeps, and leakage screening.

G Retrieval-to-Proof Traces on Lean Workbook

The traces illustrate how retrieved schemas support kernel-accepted proofs without requiring verbatim copying, while outcomes vary across retrieval conditions.

  • Trace evidence: 91.7% of the 351 theorems closed by relevant retrieval but left open by zero-shot do not reproduce any shown proof verbatim.This aggregate comparison supports retrieval as more than direct proof copying.
  • Example 1. A bound on [0, 1]: For the bound on [0, 1], the generated proof first establishes the product’s sign and then reuses the retrieved sq_nonneg(x −1/2) hint.Neither retrieved schema determines the sign, and the reference proof follows a different route.
  • Trace comparisons: The accepted proof’s route differs from the released reference proof, whose auxiliary inequalities do not appear in the accepted proof.For Example 2, six of the reference proof’s nine inequalities appear nowhere in the accepted proof.
  • Outcomes: Across three runs, zero-shot closes zero runs, relevant retrieval closes two, and random retrieval closes one.The same outcome is reported for both trace examples.
  • Example 2. A three-part symmetric conclusion: For the three-part symmetric conclusion, the accepted proof builds eleven named intermediate results and assembles the conjunction at the end.The target simultaneously requires bounds on x + y + z, xy + yz + zx, and xyz.
Loading 2608.26334v1…