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

May 21, 2026

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

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.

Riyaz Ahuja, Tate Rowney, Jeremy Avigad +1

Carnegie Mellon University

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

Ask PDF

Mar 20, 2026

Neuro-Symbolic Proof Generation for Scaling Systems Software Verification

Formal verification via interactive theorem proving is increasingly used to ensure the correctness of critical systems, yet constructing large proof scripts remains highly manual and limits scalability. Advances in large language models (LLMs), especially in mathematical reasoning, make their integration into software verification increasingly promising. This paper introduces a neuro-symbolic proof generation framework designed to automate proof search for system-level verification projects. The framework performs a best-first tree search over proof states, repeatedly querying an LLM for the next candidate proof step. On the neural side, we fine-tune LLMs using datasets of proof state-step pairs; on the symbolic side, we incorporate a range of ITP tools to repair rejected steps, filter and rank proof states, and automatically discharge subgoals when search progress stalls. This synergy enables data-efficient LLM adaptation and semantics-informed pruning of the search space. We implement the framework on a new Isabelle REPL that exposes fine-grained proof states and automation tools, and evaluate it on the FVEL seL4 benchmark and additional Isabelle developments. On seL4, the system proves up to 77.6% of the theorems, substantially surpassing previous LLM-based approaches and standalone Sledgehammer, while solving significantly more multi-step proofs. Results across further Isabelle benchmarks demonstrate strong generalization, indicating a viable path toward scalable automated software verification.

Baoding He, Zenan Li, Wei Sun +4

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

Large Language Model-Guided Theorem Proving Automated Theorem Proving Formal Verification Interactive Theorem Proving Neuro-Symbolic Reasoning

Ask PDF

Sep 16, 2025

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

Large Language Models (LLMs) have demonstrated significant promise in formal theorem proving. In this study, we investigate the ability of LLMs to discover novel theorems and produce verified proofs. We propose a pipeline called Conjecturing-Proving Loop (CPL), which iteratively generates mathematical conjectures and attempts to prove them in Lean 4. A key feature of CPL is that each iteration conditions the LLM on previously generated theorems and their formal proofs, enabling parameter-free improvement of proof strategies via in-context learning. We provide both theoretical and experimental evidence that CPL increases the discovery rate of hard-to-prove theorems compared to frameworks that generate statements and proofs simultaneously. Moreover, our experiments show that reusing the LLM's own formally verified outputs as context consistently improves subsequent proof success, demonstrating the effectiveness of self-generated in-context learning for neural theorem proving. The source code is available at https://github.com/auto-res/ConjecturingProvingLoop.

Kazumi Kasaura, Naoto Onda, Yuta Oriike +3

OMRON SINIC X Corporation · RIKEN AIP · AutoRes +7

Automated Theorem Proving In-Context Learning Lean Theorem Proving Language Model Self-Improvement Large Language Model-Guided Theorem Proving

Ask PDF

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