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

cs.AIAug 26, 2026

ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving

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

Organizations: University of Virginia · Meta AI

Abstract

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.

Figures & tables

Figure 1: Overview of ProofEvolve. Within a target, a proof DAG archive preserves structurally diverse candidates and ranks them by verified closure

\rho

, computed from kernel-accepted subgoals. Across targets, checked extraction adds newly proved results to a persistent schema library, and typed recombination instantiates them in later DAGs while exposing all residual premises as subgoals.

Inference-only models
Method	Putnam (%)	IMO-Lean (%)	Combi (%)	Avg. (%)
Claude Haiku 4.5 ( Anthropic, 2025 )	$0.0$	$0.0$	$3.3$	$1.1$
Claude Sonnet 4.6 ( Anthropic, 2026b )	$0.0$	$0.0$	$6.7$	$2.2$
Claude Opus 4.8 ( Anthropic, 2026a )	$0.0$	$0.0$	$10.0$	$3.3$
Gemini 3.1 Pro ( Google DeepMind, 2026 )	$0.0$	$3.3$	$10.0$	$4.4$
DeepSeek-Prover-V2-671B ( Ren et al., 2025 )	$7.0$	$0.0$	$10.0$	$5.7$

Table 1: Main comparison. Mean solve rate (%) over three independent runs on PutnamBench ( Tsoukalas et al., 2024 ) , IMO-LeanProofBench ( Luong et al., 2025 ) , and CombiBench ( Liu et al., 2025 ) .

Figure 2: Closure trajectories

Figure 5: Per-difficulty ablation: every variation operator contributes more on the harder Advanced split than on the Basic split. Error bars show the run-to-run standard deviation across independent reruns.

Figure 6: Test-time budget scaling (a) Kernel-verified transitions per target across seeds; (b) Union of distinct targets solved across seeds and configuration. In (a) : Qwen3.5 think

\circ

/ instant

\square

; Qwen3.6 instant

\Diamond

/ think

\triangle

; GLM-5.1

+

; Kimi-K2.6

\times

; gpt-oss med

\triangledown

/ low

\times

Panel of Figure 7 — Figure 7: Library size, at $K{=}8$

Appendix figures & tables6 assets

Supplementary material from the paper’s appendix.

Appendix

Model	Developer	Engine	TP	Mode	temp.	top- $p$	top- $k$
Kimi-K2.6	Moonshot AI	SGLang	$8$	instant	$0.6$	$0.95$	–
Qwen3.5-397B-A17B-FP8	Alibaba	vLLM	$4$	instant	$0.7$	$0.80$	$20$
				thinking	$0.6$	$0.95$	$20$
Qwen3.6-35B-A3B	Alibaba	vLLM	$1$	instant	$0.7$	$0.80$	$20$
				thinking	$1.0$	$0.95$	$20$
GLM-5.1-FP8	Z.ai	SGLang	$8$	instant	$1.0$	–	–

Appendix

Table 2: Self-hosted fixed-weight models and their serving and decoding settings. TP denotes tensor parallelism per replica, and dashes mark parameters left at their vendor defaults. Qwen instant modes use a presence penalty of

1.5

, compared with

0

in thinking mode. For gpt-oss-120b, we vary the reasoning effort.

Budget	Model calls	Lean calls	Tokens	Wall (s)
$0.25\times$	$3$	$15$	$100$ K	$450$
$0.5\times$	$6$	$30$	$200$ K	$900$
$1\times$	$12$	$60$	$400$ K	$1{,}800$
$2\times$	$24$	$120$	$800$ K	$3{,}600$

Appendix

Table 3: Per-target composite budget profiles. Each row gives four hard caps. “Tokens” is the combined input

+

output allowance; the per-call output cap remains

32{,}768

Model	Mode	$0.25\times$	$0.5\times$	$1\times$	$2\times$
Qwen3.5-397B	thinking	1.44/1.15/1.18	2.35/1.96/2.08	3.80/3.66/3.73	6.41/6.15/6.59
Qwen3.5-397B	instant	0.82/0.78/0.85	1.19/1.02/1.23	1.64/1.78/1.67	2.26/2.37/2.37
Qwen3.6-35B	instant	0.48/0.51/0.41	0.70/0.89/0.75	1.35/1.58/1.57	2.27/2.67/2.65
Qwen3.6-35B	thinking	0.50/0.51/0.53	0.81/0.82/0.75	1.31/1.32/1.31	2.21/2.19/2.17
GLM-5.1	instant	1.05/0.95/1.06	1.72/1.44/1.63	2.57/2.63/2.78	4.26/4.27/4.29
Kimi-K2.6	instant	0.97/0.89/0.98	1.38/1.20/1.31	1.95/2.12/2.17	3.20/2.94/3.11

Appendix

Table 4: Mean kernel-verified transitions per target, with entries ordered as seed 19 / seed 36 / seed 65 . Figure 6 a plots the target-weighted mean across the three seeds. These counts measure cumulative verified search activity, not unique proofs or solve rates.

Model	Mode	$0.25\times$	$0.5\times$	$1\times$	$2\times$
Qwen3.5-397B	thinking	$3$	$4$	$5$	$9$
Qwen3.5-397B	instant	$3$	$3$	$3$	$6$
Qwen3.6-35B	instant	$3$	$3$	$4$	$3$
Qwen3.6-35B	thinking	$4$	$3$	$3$	$4$
GLM-5.1	instant	$3$	$4$	$5$	$3$
Kimi-K2.6	instant	$3$	$7$	$9$	$11$

Appendix

Table 5: Final kernel-verified outcomes across seeds

\{19,36,65\}

. A solve event is one run for a particular model, mode, seed, and target that returns a valid proof. Repeated solutions of the same target count separately. The last row counts target identifiers solved at least once. Budget columns correspond to separate runs rather than cumulative prefixes.

Target	Bench	Model (mode, budget)	Trans.	Calls	Lean	Representative mechanism
putnam_2012_a2	Putnam	Qwen3.5-397B (thinking, $2\times$ )	$7$	$17$	$40$	decomposition and derived identity lemma
putnam_1977_a5	Putnam	Qwen3.5-397B (thinking, $2\times$ )	$7$	$23$	$59$	ProofLib schema reuse
putnam_2001_a1	Putnam	Qwen3.5-397B (thinking, $2\times$ )	$3$	$5$	$21$	hypothesis instantiation and rewrite
putnam_1988_b1	Putnam	Qwen3.5-397B (thinking, $2\times$ )	$2$	$5$	$10$	explicit construction and ring
hackmath_4	Combi	Kimi-K2.6 (instant, $2\times$ )	$1$	$3$	$8$	IsLeast decomposition and pigeonhole
brualdi_ch1_10	Combi	Kimi-K2.6 (instant, $2\times$ )	$4$	$14$	$33$	order- $2$ impossibility via omega

Appendix

Table 6: The

11

distinct targets solved in the open-weight runs. For one representative run per target, “Trans.” gives kernel-verified transitions, “Calls” gives model calls, and “Lean” gives kernel calls. Every listed run reaches

\rho=1

. Medium-effort gpt-oss-120b also solves brualdi_ch14_33 and brualdi_ch7_7 . Appendix E gives the corresponding proofs.

Relevant retrieval, depth (full library)
Condition	Solve rate (%)	Lift (pp)
Zero-shot	$49.5\pm 0.7$	$0.0$
Random retrieval ( $K{=}8$ )	$49.6\pm 1.0$	$+0.1$
$K{=}8$	$53.4\pm 0.7$	$+3.9$
$K{=}16$	$54.1\pm 0.9$	$+4.6$
$K{=}32$	$52.9\pm 0.9$	$+3.4$

Appendix

Table 7: Solve rate on the

744

screened evaluation theorems. We report the mean over three independent runs, and the

\pm

figure is the run-to-run standard deviation of the solve rate . Lift is the paired difference from zero-shot, computed per run before rounding, so it need not equal the difference of the two rounded means.

Automated Theorem Proving

Automated theorem proving develops algorithms and AI systems that construct or check formal proofs in mathematics, logic, and software.

See all 162 papers

ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization
May 21, 2026Riyaz Ahuja, Tate Rowney, Jeremy Avigad +1LLM Self-Refinement Automated Theorem Proving
Carnegie Mellon University
Neuro-Symbolic Proof Generation for Scaling Systems Software Verification
Mar 20, 2026Baoding He, Zenan Li, Wei Sun +4Large Language Model-Guided Theorem Proving Automated Theorem Proving
State Key Laboratory of Novel Software Technology, Nanjing University, China · School of Computer Science, Nanjing University, China · Department of Computer Science, ETH Zurich, Switzerland +1
Discovering New Theorems via LLMs with In-Context Proof Learning in Lean
Sep 16, 2025Kazumi Kasaura, Naoto Onda, Yuta Oriike +3Automated Theorem Proving In-Context Learning
OMRON SINIC X Corporation · RIKEN AIP · AutoRes +7

May 21, 2026J/K move · Enter open · S save

ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization

Riyaz Ahuja, Tate Rowney, Jeremy Avigad, Sean Welleck

Carnegie Mellon University

LLM Self-Refinement Automated Theorem Proving Lean Theorem Proving Neuro-Symbolic Reasoning

Open paper AskPDF arXiv

Formal mathematics libraries are rapidly expanding, creating a growing need to refactor verified proofs for maintainability and to improve training data quality for neural provers. However, scalable proof optimization is hindered by heterogeneous and heuristically specified objectives, scarce data, and high training and inference costs. To overcome these challenges, we introduce ImProver 2, a neurosymbolic framework for automated proof optimization in Lean 4. ImProver 2 combines a data-efficient expert-iteration pipeline with a scaffold that exposes formal structure alongside lightweight informal abstractions. We further introduce a suite of metrics capturing structural proof properties. Using ImProver 2, we train a 7B-parameter model that outperforms orders-of-magnitude larger models within the same model family, and is competitive with mid-tier frontier models across metrics. We additionally demonstrate that our neurosymbolic scaffold significantly improves performance across both small and frontier models. We show that with proper scaffolding and training, small models can effectively restructure research-level proofs over complex and varied metrics, matching substantially larger systems and establishing proof optimization as a scalable, learnable task.

Abstract

Automated Theorem Proving

Explore similar work

ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization

Neuro-Symbolic Proof Generation for Scaling Systems Software Verification

Discovering New Theorems via LLMs with In-Context Proof Learning in Lean