PaperlayerView exact revision on arXiv

Source-linked AI summary

HyperTree Proof Search for Neural Theorem Proving

Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, Timothée Lacroix

arXiv:2205.11491v1cs.CLcs.AI

TL;DR

Formal theorem proving remains difficult because proofs are complex to verify and formalization requires substantial effort. The paper introduces HTPS with online training for neural proof search and evaluates it across three environments. The approach reaches state-of-the-art results, including 82.6% on held-out set.mm theorems and 58.6% on miniF2F-valid.

  • Problem

    Formal mathematics is difficult to adopt because formalization resembles programming and requires substantial effort and expertise.

  • Method

    The paper combines HTPS, an MCTS-inspired proof-search algorithm, with an online training procedure for policy and critic models.

  • Results

    The approach achieves state-of-the-art performance, proving 82.6% of held-out set.mm theorems and 58.6% on miniF2F-valid in Lean.

  • Takeaways & Limitations

    Online training provides large speed-ups over expert iteration and supports policy and critic generalization to completely new domains.

  • Takeaways & Limitations

    The search assumes a policy model initialized by supervised fine-tuning on an environment-specific dataset, while the critic begins untrained.

Abstract

from arXiv · show

We propose an online training procedure for a transformer-based automated theorem prover. Our approach leverages a new search algorithm, HyperTree Proof Search (HTPS), inspired by the recent success of AlphaZero. Our model learns from previous proof searches through online training, allowing it to generalize to domains far from the training distribution. We report detailed ablations of our pipeline's main components by studying performance on three environments of increasing complexity. In particular, we show that with HTPS alone, a model trained on annotated proofs manages to prove 65.4% of a held-out set of Metamath theorems, significantly outperforming the previous state of the art of 56.5% by GPT-f. Online training on these unproved theorems increases accuracy to 82.6%. With a similar computational budget, we improve the state of the art on the Lean-based miniF2F-curriculum dataset from 31% to 42% proving accuracy.

1 Introduction

The paper targets the difficulty and limited adoption of formal mathematical proofs by developing an automated prover that searches for tactic sequences without human interaction. It introduces HTPS, a simpler Equations environment, and an extensive multi-environment study reporting strong proving results.

  • Formal proofs have become increasingly complex, limiting verification to specialists and allowing errors to remain undiscovered.
  • Formal mathematics remains difficult to adopt because it resembles programming code, requires substantial expertise, and can be laborious even for simple statements.The formalization of the Kepler conjecture took over 20 person years.
  • The prover generates tactics from goals, recursively expands resulting subgoals, and seeks a proof hypertree whose leaves are empty sets.The resulting search graph can grow exponentially, making branch prioritization critical.
  • HTPS is a new MCTS-inspired search algorithm for finding proofs in unbalanced hypergraphs.
  • Equations is a new environment for prototyping and understanding model and proof-search behavior.
  • The study ablates data selection, critic targets, and online training versus expert iteration across three theorem-proving environments.
  • 82.6% of held-out set.mm theorems and 58.6% of miniF2F-valid theorems are proved, achieving state-of-the-art performance on analyzed environments.

2 Related work

The paper builds on classical automated theorem proving, neural theorem provers, language-model reasoning, and MCTS-based game search. It distinguishes its approach through HTPS, proof-search-derived training data, and online training rather than expert iteration.

  • Classical theorem provers are efficient for simpler logics but insufficient for theorems written in modern proof assistants.
  • Recent neural theorem provers achieve strong results on held-out Metamath and Lean sets, while this work differs in search, data extraction, and online training.The paper reports improved performance and faster training from these differences.
  • Language models have shown strong performance on formal tasks including expression simplification, differential equations, symbolic regression, and mathematical-property prediction.
  • AlphaZero combines neural policy guidance with learned evaluations in MCTS, motivating theorem proving as a related search problem over proof states.

3 Proving environments

The paper evaluates its methods in Metamath, Lean, and the simpler Equations environment, which differ in automation, expressivity, proof representation, and available training data. Equations specifically tests generalization from synthetic proofs to complex out-of-domain identities.

  • Metamath: Metamath uses string substitution over the 30k-theorem set.mm database, with tactics represented by theorem labels and necessary substitutions.
  • Metamath: Metamath’s simplicity makes it a useful algorithmic test bed, but its lack of automation produces larger, harder-to-interpret proofs.
  • Lean: Lean provides stronger automation through tactics such as ring, norm_num, and linarith, but its states may contain dependent subgoals linked by metavariables.
  • Lean: Lean proof terms are checked by the kernel after each tactic application, with metavariables replaced by lambda abstractions for checking.
  • Equations: Equations restricts expressivity to mathematical expressions and simple rules, making goals and tactics easier to understand and debugging more interpretable.
  • Equations: Equations training uses randomly generated synthetic theorems and proofs, while Identities contains 160 manually created mathematical expressions without provided proofs.
  • Equations: Because synthetic theorems differ substantially from Identities, the split evaluates generalization to complex, out-of-domain data.

4 HyperTree Proof Search

HTPS searches for proofs in hypergraphs by repeatedly selecting partial proof hypertrees, expanding unexpanded goals, and back-propagating values. Its hypergraph-aware search evaluates tactics by whether all resulting subgoals can be solved.

  • Proof search: HTPS grows a proof hypergraph from the root goal until it finds a hypertree whose leaves are empty sets.Proof search interacts with the learned models and theorem-proving environment to construct this hypertree.
  • HTPS procedure: Each iteration selects a hypertree using a search policy, expands its unexpanded leaves with valid tactics, and back-propagates node values.The three steps repeat until a proof is found or the expansion budget is exceeded.
  • Selection: The search policy balances tactic priors with critic estimates using visit counts and Q = W/N, addressing exponential hypergraph growth.Higher visit counts increase confidence in estimated tactic values relative to the policy prior.
  • Hypergraph search: Unlike path-based MCTS, HTPS builds partial proof hypertrees whose leaves may include multiple solved or unexpanded subgoals.This reflects the requirement that every subgoal produced by a tactic must be proved.
  • Back-propagation: Node values are 1 for solved goals, 0 for invalid goals, and critic estimates otherwise; parent values multiply the values of their children.The method assumes subgoal solvability is independent for this computation.

5 Online training from proof searches

The paper turns proof search into an online training loop for shared policy and critic transformers. Asynchronous provers generate samples while distributed trainers update and synchronize the models.

  • Online training: Asynchronous proof searches continuously generate training data while trainers update models, coupling data extraction and learning online.Provers periodically retrieve the latest model versions from the trainers.
  • Model objectives: The shared-weight encoder-decoder models use a tactic objective for policy generation and a critic objective for goal solvability estimation.The policy predicts tactics from goals, while the critic decodes PROVABLE or UNPROVABLE probabilities.
  • Training data: Successful searches provide minimal-proof goal-tactic pairs as policy samples, with minimality defined by environment-specific proof cost.Metamath and Equations use proof steps, whereas Lean uses tactic CPU time.
  • Training data: Critic samples include solved, invalid, and sufficiently visited nodes with targets based on solved status or final estimated action values.Solved and invalid nodes receive targets 1 and 0, respectively.
  • Training procedure: Training samples are stored in separate finite queues, sampled uniformly, and combined with continued sampling from supervised tasks.The two training objectives are weighted equally.
  • Training pipeline: The pipeline bootstraps policy learning through pretraining and environment-specific supervised fine-tuning before online training of both models.The critic is initially untrained, while the policy must already produce coherent tactics.

6 Experiments

Experiments establish environment-specific supervised training and evaluate online learning across Metamath, Lean, and Equations settings. The protocol also examines transductive learning from unproved statements and reports pass rates.

  • Experimental setup: The experiments evaluate supervised training, pretraining, model architecture, and proof performance across three theorem-proving environments.The section describes datasets, tokenization, pretraining, architecture, and evaluation methodology.
  • Experimental setup: Starting online training from a non-trivial policy is critical because a randomly initialized model would not produce valid tactics.The policy is first fine-tuned on a supervised dataset specific to each environment.
  • Metamath: Metamath uses 37,091 set.mm theorems with dependency-aware random train-validation-test splits and 1,000 validation and test theorems.The dependency DAG prevents validation or test theorems from being used to prove other held-out theorems.
  • Metamath: Metamath tokenization stops tactic decoding at the End Of Useful token and omits predictable substitutions to reduce decoding time and invalid substitutions.The model outputs the rule label and only substitutions that cannot be inferred syntactically.
  • Lean: Lean supervision combines 24k Mathlib theorems, 144k goal-tactic pairs, proof-artifact data, fixed software versions, and an additional converted synthetic task.The setup is designed to facilitate experimentation and reproducibility.
  • Evaluation: The transductive protocol measures how many unproved statements can be learned during training and reports cumulative pass rate alongside pass@k.Cumulative pass rate is the proportion solved at least once during online training.

7 Results

The evaluation compares Evariste with supervised and prior systems across Lean, Metamath, and Equations, while ablations isolate contributions from online training, proof-search data, critic targets, and search-parameter sampling.

  • Main Results: 58.6% cumulative pass rate was obtained on miniF2F-valid, while miniF2F-test reached 41% pass@64 versus 36.6% for GPT-f.The Lean evaluation used statements from miniF2F-valid during online training.
  • Main Results: 82.6% cumulative pass rate on Metamath valid statements improved substantially over the supervised model’s 61% pass@8.The supervised model plateaued at 66%, whereas Evariste continued improving beyond 74% after seven days.
  • Main Results: 65.6% pass@32 on Metamath test theorems increased by 10% from the supervised model’s 55.8%.The supervised model achieved 65.4% on validation and 61.2% on test, compared with GPT-f’s 56.5% and 56.2% after expert iteration.
  • Main Results: 91.3% cumulative pass rate on Equations Identities contrasted with a supervised model that never exceeded 36%.HTPS also found proofs requiring 82 and 117 proof steps, supporting search in large proof graphs and adaptation to out-of-domain identities.
  • Ablations: Learning only minimal proofs reached 78.1% on Equations versus 40.6% when learning from all proofs, while root-minimal proofs reached 68.6% pass@8 on Metamath validation.The ablation selected proof-derived goal-tactic pairs using minimality criteria appropriate to each environment.
  • Ablations: Randomly sampling HTPS hyper-parameters outperformed fixed parameters, reaching 78.1% versus 73.8% on Equations Identities.The comparison also reported better performance on the Metamath test set.

8 Conclusion

The paper introduces HTPS with online training and reports state-of-the-art results across multiple theorem-proving environments. Online training improves speed and supports generalization, but fully proving datasets such as miniF2F remains elusive.

  • 8 Conclusion: HTPS combines an AlphaZero-inspired proof-search algorithm with an online training procedure.The pipeline is evaluated across multiple theorem-proving environments.
  • 8 Conclusion: Online training provides large speed-ups over expert iteration and enables generalization of policy and critic models to completely new domains.The conclusion frames online training as learning from proof-search-generated data.
  • 8 Conclusion: Fully proving datasets like miniF2F remains elusive despite large numbers of attempts per theorem.The authors state that proof-search data from currently available corpora will likely be insufficient in the long term.
  • 8 Conclusion: Automated generation of new theorems is identified as a likely future milestone for supplying exploration and additional training data.This follows the stated limitation of manually annotated formal datasets and existing proof-search corpora.

A Proof search in more details

The proof search represents theorem proving as hypergraph exploration, combining tactic policies, value estimates, and solved or invalid node propagation. HTPS adapts search policies and backups to the requirement that every subgoal of a tactic must be proved.

  • Hypergraph representation: A hypergraph represents goals as nodes, tactics as edges, and tactic-generated subgoals as children.A hypertree is an acyclic hypergraph, and proofs are hypertrees whose leaves are solved nodes.
  • Node status: Solved and invalid statuses are maintained recursively: a goal is solved through a tactic whose children are all solved, while invalidity propagates when every tactic has an invalid child.The procedures MaintainSolved and MaintainInvalid update these sets as the hypergraph grows.
  • Search procedure: Proof search repeatedly expands expandable subtrees, backs up value estimates, and stops when the root is proved or the expansion budget is exhausted.Expandable subtrees contain at least one unexpanded or invalid leaf.
  • Search policy: PUCT and a prior-regularized policy balance model priors with value estimates, with πRP performing better on Equations and PUCT performing better on Metamath and Lean.Virtual counts reduce the value of repeatedly selected solving tactics, encouraging exploration of already solved subtrees.
  • Expansion: During expansion, the policy proposes tactics, the proving environment filters valid tactics, and valid tactic-child relations are added to the hypergraph.A tactic that solves a goal creates no subgoals; if no tactic is valid, the goal is marked invalid.

B.5 Environment vulnerabilities due to initial numerical approximations

Approximate numerical verification made the Equations environment unsound, allowing the model to prove false statements. Restricting verification to rational expressions provides exact evaluation and avoids these approximation-based vulnerabilities.

  • Vulnerability: Approximate numerical verification let the model reach 100% accuracy while proving arbitrary statements in early Equations implementations.The environment was changed to restrict numerical verification to rational expressions.
  • Exponential example: The model derived 2 = 3 because NumPy rounded distinct exponential expressions to the same value, 0.0.It then applied injectivity of the exponential function to the incorrectly accepted equality.
  • Cosine example: The model derived 0̸ = 0 because NumPy approximated cos(π/2) as 6.123 × 10−17 rather than exactly zero.Repeated square-root transformations produced a value treated as non-zero under the environment threshold.
  • Propagation: Once 0̸ = 0 was accepted, the assertion rule using a multiplier C chosen as zero could establish arbitrary equalities.The rule requires A × C = B × C and C̸ = 0.
  • Synthetic data: Equations uses synthetic theorem generation because it lacks manually annotated proofs, with random-walk and graph-based procedures producing training data.Generated Equations theorems can also be translated to Lean using rules imported from Mathlib.

C Proof Search Hyper-Parameters

HTPS uses randomized decoding and search hyper-parameters because the evolving model can change which settings are effective. Evaluation samples from the same distributions while fixing expansion budgets for Lean and Metamath.

  • Parameter selection: HTPS hyper-parameters include policy-decoding settings and search settings whose optimal values may change as the model evolves.The paper motivates sampling rather than manually selecting a single fixed configuration.
  • Decoding parameters: Policy decoding samples the number of tactics, temperature, and length penalty from predefined distributions.The number of samples ranges over [8, 16, 32, 48], temperature over [0.8, 2.0], and length penalty over [0, 1.2].
  • Search parameters: Search settings sample the expansion budget, depth penalty, and exploration constant from predefined distributions.Expansion budgets range from 1000 to 10000, while exploration ranges from 0.01 to 100.
  • Evaluation: Evaluation uses the training-time distributions but fixes expansions to 5k in Lean and 10k in Metamath.This keeps the evaluation search budgets specified across runs.
  • Reproducibility: Experiments use fixed versions of Metamath, Lean, miniF2F, and Mathlib to compare models in the same setup.The paper records the corresponding repository commits and Lean version.

E Time vs Depth minimization

The Lean experiments compare minimizing proof depth-related behavior with minimizing total proof CPU time. CPU-time minimization favors faster tactics and yields a higher cumulative pass rate on miniF2F-valid.

  • Results: 50.4% of miniF2F-valid problems were solved after 3 days when minimizing total Lean proof CPU time.The passage reports a higher cumulative pass rate for this objective.
  • Proof time: Figure 12 reports average proof CPU time for different minimization objectives, with time-minimized training producing significantly lower average proof time.The comparison concerns proofs found by the model.
  • Tactic behavior: CPU-time minimization shifts tactic usage away from slow automation toward faster and simpler tactics.Table 10 compares tactic frequencies under the different minimization objectives.

F Example Lean proofs

This section presents two proofs found by the model in Lean-based miniF2F: one establishes a modular-arithmetic result, while the other exposes a statement error caused by natural-number subtraction.

  • Example proofs: The section illustrates examples of proofs found by the model, including both a valid proof and a proof invalidated by correcting the formalized statement.The second proof is no longer valid on the fixed statement.
  • Example proofs: The model proves that 2n + 1 is not divisible by 7 for every n ∈ N using modular arithmetic and strong induction.The proof uses 2n mod 7 + 1 ≠ 0, bounds the residue below 7, and applies 2n ≡ 2n+3 mod 7.
  • Example proofs: A second model-found proof is valid only for an erroneous statement whose natural-number subtraction encodes truncated subtraction.In Lean, (a : N) − (b : N) = (0 : N) when b ≥ a, so the hypothesis represents max(b + d − a, 0) + c.
Loading 2205.11491v1…