PaperlayerView exact revision on arXiv

Source-linked AI summary

InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search

Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Zheng Yuan, Wenwei Zhang, Dahua Lin, Kai Chen

arXiv:2410.15700v2cs.AIcs.CL

TL;DR

Best-first theorem-proving search can struggle to find deep proofs because it relies on prover-internal tactic scores rather than preference information in search trajectories. The paper trains a critic to rank intermediate states and combines it with expert iteration; on miniF2F, the critic raises prover performance from 59.4% to 65.9% when combined with vanilla best-first search.

  • Problem

    Best-first search relies on prover-internal indicators such as tactic log probabilities, which can become unreliable for deeper proofs; InternLM2-StepProver found proofs of at most 8 tactics despite typical tree searches requiring 100 to 1,000 steps.

    Source: §1 · p. 1

  • Method

    A critic learns preference information from search trajectories, ranks intermediate proof states at runtime, and is refined alongside the prover through expert iteration.

    Source: §1 · p. 1, §5 · p. 8

  • Results

    65.9% versus 59.4% on miniF2F when critic-guided search is combined with vanilla best-first search.

    Source: §1 · p. 2

  • Takeaways & Limitations

    The authors report that critic-guided search can improve search depth and theorem-proving capability, and they release Lean-Workbook-Plus and searched proofs.

    Source: §1 · p. 2, §5 · p. 8

    The work mainly focuses on contest-level math problems, pays less attention to other theorem-proving scenarios, and lacks a stable metric for evaluating critic models.

    Source: Limitations · p. 8

Abstract

from arXiv · show

Large Language Models (LLMs) have emerged as powerful tools in mathematical theorem proving, particularly when utilizing formal languages such as LEAN. A prevalent proof method involves the LLM prover iteratively constructing the proof tactic by tactic, typically following a best-first search scheme. However, this method often ignores the critical preference information inside the existing tactic trajectories, hindering the search for deeper proofs. We propose an intuitive yet effective method, which utilizes a critic model to capture the preference information and to guide the search of the prover model at runtime. Given the prover-critic framework, a large-scale expert iteration with more than 20,000 CPU days is then applied to further fine-tune the prover and the critic. The trained InternLM2.5-StepProver critic significantly boosts the performance of the prover model (59.4% to 65.9%). We also analyze the impact of the critic on various aspects of the theorem proving process during expert iteration, providing insights into its effectiveness. We open-source our models and searched proofs at https://github.com/InternLM/InternLM-Math and https://huggingface.co/datasets/internlm/Lean-Workbook.

1. Introduction

The paper motivates critic-guided theorem proving as a way to use search-trajectory preferences to address difficulty finding deep proofs. It reports improved miniF2F performance and large-scale expert iteration, alongside analysis of proof and resource scaling.

1. Introduction

  • Search trajectories provide preference information for a critic that estimates state value and guides which proof states the prover explores.The authors collect roughly 8,000 preference pairs from InternLM2-StepProver search trajectories on its training sets.Source: §1 · p. 1
  • The authors conduct expert iteration on Lean-Workbook, reporting more than 20,000 CPU days of experimentation.They describe the work as an example of expert iteration on synthetic datasets.Source: §1 · pp. 1–2
  • 65.9% versus 59.4% on miniF2F when the critic is combined with vanilla best-first search, compared with the prover model without the critic.Without vanilla best-first search, the critic raises performance to 65.6%.Source: §1 · p. 2
  • The enlarged Lean-Workbook solution set is to be open-sourced.The paper also states that its models and searched proofs are open-sourced.Source: §1 · p. 2
  • The paper identifies a log-linear relationship between proved-problem counts and both proof length and computational resources.The authors present this relationship as an insight for resource allocation in future work.Source: §1 · p. 2

2. Methods

The methods use a critic to rank intermediate proof states, train it from preferences in search trajectories, and iteratively refine the prover and critic using verified proof trajectories. The prover prompt also includes the tactics leading to the current state.

2.1. Search Methods

  • Best-first search selects among unexpanded states using the average log probability of tactics along each state’s proof trajectory.The search generates candidate tactics for the selected state and derives new states from valid tactics.Source: §2.1 · p. 2
  • The critic scores intermediate Lean states to guide expansion, addressing best-first search’s reliance on tactic log probabilities, which the authors say often fails to find deep proofs.Figure 1 contrasts log-probability-based priority with critic-based reranking; higher critique scores indicate higher priority.Source: §2.1 · p. 2, Figure 1 · p. 3
  • The critic is trained with preference pairs: successful-path child states are preferred to their parents, and successful-path states are preferred to sibling states that did not lead to a proof.The path-pair construction assumes legal tactics on a successful path yield positive reward.Source: §2.1 · pp. 2–3

2.2. Expert Iteration

  • Expert iteration initializes the critic from InternLM2-StepProver search trajectories over theorem collections including miniF2F-train, mathlib, Lean-Workbook, and Lean-Github.Preference pairs sampled from successful search trajectories are used to train the prover, and the iterative procedure continues until critic-guided search surpasses vanilla methods on miniF2F-train.Source: §2 · p. 2, §2.2 · p. 3
  • Lean-Workbook iteration includes negated versions of formalized propositions, an initial scan capped at 10 iterations and 50 seconds per problem, and later rounds with budgets up to 2,000 iterations and 3,600 seconds.After each round, the prover and critic are retrained on expanded successful proof trajectories; the critic then prioritizes the top 50% of unproven statements it deems most likely solvable.Source: §2.2 · p. 3
  • The prover prompt adds a PROOF BEFORE field containing the tactics that led to the current state, supplementing the goal and proof-step context.The paper presents this change as intended to improve reasoning in deep search trees.Source: §2.2 · pp. 3–4, Figure 2 · p. 4

3. Experiments and Results

Experiments report stronger miniF2F and ProofNet outcomes with hybrid critic-guided search, while critic-guided search finds deeper proofs. Expert iteration proves or disproves 17.0% of Lean-workbook-plus problems, and its resource analysis reveals substantial unresolved difficulty.

3.1. Benchmark Performance of InternLM2.5-StepProver

  • 69.6% miniF2F-Valid and 65.9% miniF2F-Test for hybrid search; on ProofNet, BF, CG, and hybrid solve 22.3%, 23.9%, and 27.0%.The miniF2F figures are reported alongside Table 1, and the ProofNet comparison alongside Table 2.Source: Table 1 · p. 5, §3.1 · p. 6, Table 2 · p. 7

3.2. Results of Expert Iteration

  • 17.0% of Lean-workbook-plus problems are proved or disproved, and the resulting statements, tactics, and states are released.The results are reported for Lean-workbook-plus.Source: §3.2 · p. 6, Table 3 · p. 7
  • 1.5% of CPU resources solve 17.0% of problems, while the remaining 98.5% yield no successful outcomes.The expert-iteration process consumed approximately 21,364 CPU days.Source: §3.2 · p. 6, Table 4 · p. 7
  • Proved-problem counts have a log-linear relationship with proof length and resources; above 10,000 seconds, BF finds fewer proofs while CG exceeds the trend.The paper reports that 83% of Lean-workbook problems remain unproven.Source: §3.2 · pp. 6–7
  • 4.44 tactics for CG versus 1.66 for BF on average; CG also finds proofs longer than 9 tactics.Figure 3 considers only the five shortest proofs for each solved problem.Source: Figure 3 · p. 4, §3.2 · p. 6, §3.1 · p. 6

4. Related Work

Prior theorem-proving work commonly combines tactic prediction with tree search, while other approaches generate complete proofs or translate informal proofs. The paper situates critic-guided search within work on process supervision and formal proof search.

4. Related Work

5. Conclusion

The paper presents critic-guided search and tandem expert iteration for formal theorem proving. On miniF2F-test, the reported pass rate rises from 54.5% to 65.9%.

5. Conclusion

  • 54.5% to 65.9%: critic-guided search raises the pass rate on miniF2F-test (p25).Source: §5 · p. 8
  • The critic reranks intermediate Lean states, with initial preference training from prior prover trajectories and tandem expert iteration on correct proof trajectories verified by the Lean solver.Source: §5 · p. 8
  • The paper introduces Lean-Workbook-Plus and reports that critic-guided search can further improve search depth.Source: §5 · p. 8
  • The authors say these advances offer concrete guidance for future developments in automated mathematical reasoning.Source: §5 · p. 8

Limitations

The work focuses mainly on contest-level mathematics and identifies both limited coverage of other theorem-proving scenarios and the absence of a stable critic-model evaluation metric.

Limitations

  • The study focuses mainly on contest-level math problems, so other automated theorem-proving scenarios receive less attention.Source: Limitations · p. 8
  • No stable metric for critic models makes critic-model iteration difficult.Source: Limitations · p. 8

A. Training details

The prover is based on InternLM-math-plus-7B, while the critic is initialized from InternLM2-Chat-1 8b-sft2. The training details include model fine-tuning, preference-pair construction, and critic evaluation.

A. Training details

  • The prover is built on InternLM-math-plus-7B and fine-tuned for two epochs with a global batch size of 512 and learning rate 2 × 10−5.Source: A. Training details · p. 11
  • Expert iteration generated 2.19 billion tokens; the final iteration took approximately 14 hours on 32 A800 GPUs.Source: A. Training details · p. 11
  • The critic is initialized from InternLM2-Chat-1 8b-sft2, fine-tuned for one epoch, and trained on preference pairs from miniF2F-valid, Mathlib, and Lean-Workbook-Plus.Source: A. Training details · p. 11
  • On 6,510 miniF2F-test preference pairs, the critic achieves 78.0% accuracy in predicting positive and negative pairs.Source: A. Training details · p. 11

B. Case studies

These case studies show the prover solving formalized problems through distinct proof strategies, including series-and-limit reasoning, Mathlib premises, and enumeration.

B. Case studies

  • For the modular divisibility problem, the prover constrains variable remainders and solves by enumeration, illustrating a distinction between formal and informal reasoning.The theorem states that (mn + m + n) mod 6 = 4 implies 12 | mn.Source: B. Case studies · p. 11
  • For mathd_algebra_31, the formalized series-and-limit problem differs from a risky informal substitution, yet the prover proves it without informal augmentation.The informal solution jumps from an equation to a substituted expression; the formal version uses series and limits.Source: B. Case studies · p. 12
  • On an undergraduate topology problem outside its fine-tuning distribution, it uses Mathlib premises to construct valid closure subsets.The example asks for neighborhoods of disjoint closed sets whose closures remain disjoint.Source: B. Case studies · p. 12

Related papers

Loading 2410.15700v2…