PaperlayerView exact revision on arXiv

Source-linked AI summary

Formal Mathematics Statement Curriculum Learning

Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, Ilya Sutskever

arXiv:2202.01344v1cs.LGcs.AI

TL;DR

Formal mathematics presents difficult proof-search and curriculum-learning problems because its action space is infinite and it lacks direct self-play. The paper applies expert iteration, interleaving proof search with learning and using varied formal statements, to learn increasingly difficult problems. It achieves state-of-the-art miniF2F performance while remaining limited in chaining long reasoning sequences.

  • Problem

    Formal mathematics combines an infinite action space with no direct self-play setup, making naive reinforcement-learning approaches unlikely to succeed.

  • Method

    Expert iteration interleaves proof search with learning and uses automatically or manually curated formal statements of varied difficulty as auxiliary curriculum data.

  • Results

    The method solves increasingly difficult problem curricula and achieves state-of-the-art on miniF2F, reaching 47.3% pass@64 on miniF2F-valid and 36.6% on miniF2F-test.

  • Takeaways & Limitations

    The results suggest that missing self-play can be compensated for with curated formal statement sets, which are cheaper to formalize than full proofs.

  • Takeaways & Limitations

    The models generally cannot chain more than 2 or 3 non-trivial reasoning steps, limiting consistent performance on challenging olympiad problems.

Abstract

from arXiv · show

We explore the use of expert iteration in the context of language modeling applied to formal mathematics. We show that at same compute budget, expert iteration, by which we mean proof search interleaved with learning, dramatically outperforms proof search only. We also observe that when applied to a collection of formal statements of sufficiently varied difficulty, expert iteration is capable of finding and solving a curriculum of increasingly difficult problems, without the need for associated ground-truth proofs. Finally, by applying this expert iteration to a manually curated set of problem statements, we achieve state-of-the-art on the miniF2F benchmark, automatically solving multiple challenging problems drawn from high school olympiads.

1. Introduction

Formal mathematics offers a game-like setting for studying reasoning, but its infinite action space and lack of direct self-play create distinct challenges. The paper addresses these challenges with expert iteration and varied auxiliary statements, achieving state-of-the-art on miniF2F.

  • Motivation: Formal mathematics provides automatically verifiable proof trajectories and broader potential significance than comparable game reasoning.The paper highlights possible applications including software verification.
  • Challenges: The domain combines an extremely large search space with an infinite action space requiring complex tactics and generated mathematical terms.Actions may include witnesses, cuts, and exogenous mathematical terms.
  • Challenges: Formal mathematics lacks direct self-play because provers face statements rather than opponents and hard statements offer no obvious intermediate targets.This asymmetry blocks naive transfer of symmetric self-play algorithms from two-player games.
  • Approach: Expert iteration uses auxiliary problem statements of varied difficulty, without requiring proofs, to produce a curriculum of increasingly difficult problems.The method works with automatically generated and manually curated auxiliary distributions.
  • Results: The approach achieves state-of-the-art performance on the miniF2F benchmark using manually curated problem statements.The benchmark contains formalized competition problems and is used as a test bed for the methodology.
  • Contributions: The paper identifies expert iteration, synthetic inequality generation, and fixed-budget comparisons against proof search only among its contributions.It also presents lean-gym and studies curriculum learning from generated statements.

2. Related Work

The work builds on prior systems for language-model theorem proving, Lean proof training, and the miniF2F benchmark, while situating further related work in an appendix.

  • Prior work: The paper extends GPT-f, PACT, and the miniF2F benchmark in its formal mathematics experiments.GPT-f supplies tactic generation, PACT studies Lean and co-training, and miniF2F provides the benchmark.
  • Prior work: Additional related work is presented in Appendix A.

3. Formal Environment

The paper uses Lean as its formal environment, extracts proof data from mathlib and related artifacts, and introduces lean-gym to make proof-search iteration easier.

  • 3. Formal Environment: Lean is selected as the formal environment because its high-level tactics benefit neural theorem proving.
  • 3. Formal Environment: Lean proofs are typically 10x shorter than Metamath proofs on the miniF2F-related comparison.
  • 3.1. lean-gym: PACT’s Lean-runtime search interface makes changing and iterating on proof search difficult for cluster-wide parallelized workloads.The search procedure is programmed in Lean, which is not designed for such I/O-intensive tasks.
  • 3.1. lean-gym: lean-gym provides a simple standard-input/output REPL interface over Lean.The implementation is intended to address limitations of coupling search procedures directly to the Lean runtime.
  • 3.2. Proof datasets extraction: The paper extracts human tactic proof steps from mathlib into a tactic dataset.
  • 3.2. Proof datasets extraction: It also extracts additional proof artifacts into the mix1 and mix2 datasets.
  • 3.2. Proof datasets extraction: Statements are partitioned into mathlib-train, mathlib-valid, and mathlib-test using the split proposed in prior work.The associated tactic and artifact dataset splits are aligned with these statement splits.

4. Expert Iteration

The paper develops expert iteration for formal mathematics by alternating proof search with model training, using proofstep and proofsize objectives to improve search. Across mathlib and miniF2F, iterative training improves pass rates, outperforms search-only scaling, and shortens discovered proofs.

  • Expert iteration: Expert iteration trains models on proofs they previously sampled, enabling repeated cycles of proof search and model improvement.Each iteration samples proof searches, filters successful searches into a dataset, and fine-tunes the base model.
  • Training objectives: The proofstep objective generates a Lean tactic from the current tactic state and declaration name, while the proofsize objective predicts a bucket for proof length.The declaration name provides a weak signal about the current declaration’s library context, and proofsize buckets guide search toward shorter proofs.
  • Bootstrapping: Bootstrapping initializes θ0 with proofstep training, then uses sampled mathlib-train proofs to construct proofstep and proofsize training data for θ1.The initial model is fine-tuned on mathlib tactic data and proof artifacts; sampled proofs add deduplicated proofsteps and proofsize tuples.
  • Expert iteration on mathlib-train: 56.3% pass@1 for θ1 on mathlib-valid rises to 62.6% for θ9, while later iterations also improve transfer to out-of-distribution miniF2F-valid statements.The improvement follows a clear logarithmic scaling pattern on mathlib-valid, and miniF2F transfer becomes stronger at later iterations.
  • Compute scaling: At fixed compute, expert iteration outperforms proof search alone, with a substantially higher scaling exponent than increasing test-time search attempts.The comparison uses cumulative pass rates for the normal loop and a sampling-only loop that skips retraining.
  • Expert iteration on mathlib-train: 17,390 statements proved at iteration 1 increases to 19,476 at iteration 9, while average proof length decreases from 4.8 to 4.0.These gains occur even though ground-truth proofs are available for the mathlib-train statements.

5. Statement curriculum learning

Expert iteration learns an intrinsic curriculum from synthetic inequality statements of varied difficulty, eventually solving harder problems without seed proofs for those difficulty levels. At fixed compute, it outperforms proof search without interleaved retraining.

  • Synthetic curriculum: Expert iteration uses synthetic inequality statements whose composition depth ND and expression complexity NS control difficulty.The generator composes inequalities from established theorems, including AM-GM, Cauchy-Schwarz, Bernoulli, Young, and Hölder.
  • Synthetic curriculum: The curriculum contains 5,600 statements without proofs, covering 100 statements for each combination of 0 ≤ NS ≤ 7 and 0 ≤ ND ≤ 6.A small separately formalized set of low-difficulty statements is used for bootstrapping.
  • Expert iteration: Each iteration searches statements, filters successful proofs into training data, and fine-tunes the model before the next iteration.The synthetic setup combines mathlib-train and synth-ineq, with models additionally trained on synth-ineq-train.
  • Results: Expert iteration closes 6 statements at difficulty ND = 6 without any seed ground-truth proof at that level.The sample-only loop remains at zero for ND = 6, even when the number of attempts is scaled.
  • Results: The results show that expert iteration can learn a curriculum and develop capabilities for highly challenging composed inequalities without ground-truth proofs.This conclusion concerns the synthetic synth-ineq dataset and the emergence of solutions at difficult levels.

6. Targeting miniF2F

A manually formalized curriculum of contest-style exercises is added to expert iteration to address miniF2F's distribution shift from mathlib. The resulting model transfers to miniF2F and achieves reported state-of-the-art pass rates while solving challenging olympiad-derived problems.

  • Curriculum construction: The miniF2F curriculum contains 327 manually formalized statements from contest textbooks and MATH, with no overlap with miniF2F validation or test statements.The set targets the out-of-distribution character of miniF2F relative to generic mathlib statements.
  • Curriculum construction: The full curriculum combines mathlib-train, synth-ineq, and miniF2F-curriculum, using 8 proof-search attempts per miniF2F-curriculum statement.Mathlib-train and synth-ineq use one attempt per statement.
  • Transfer to miniF2F: 100 of the 327 miniF2F-curriculum statements are closed by the end of expert iteration, indicating limited density in the manually curated set.The figure comparison accounts for the greater compute used by the full curriculum.
  • Transfer to miniF2F: Steady miniF2F-valid improvement in both pass@1 and pass@8 indicates transfer beyond the statements composing the curriculum.The authors describe this as effective transfer among miniF2F-curriculum, synth-ineq, and miniF2F-valid.
  • Results: 47.3% on miniF2F-valid and 36.6% on miniF2F-test are reported using 64 attempts, improving on the previous state of the art.The results include 26 AMC12, 6 AIME, and 2 IMO-adapted problems.
  • Results: The models also exceed 75% pass rate on mathlib validation and test using 64 attempts.The authors describe this as a new state of the art on mathlib as well.

7. Discussion

The discussion identifies compute allocation, model scaling, and proof-search depth as important constraints on the approach. Larger models improve pass@1 but may be less effective per fixed compute, while chaining several non-trivial reasoning steps remains difficult.

  • 7.1. Model Size: 774m parameters was the sole model size studied throughout the paper.The authors briefly experimented with other sizes but did not report those results.
  • 7.1. Model Size: Bigger models consistently achieve higher pass@1, but sampling more attempts from smaller models can yield better fixed-compute performance.The trade-off arises because larger models are more expensive to sample from.
  • 7.1. Model Size: The authors leave a more thorough study of model-size and compute-frontier dynamics for future work.They considered their selected model size a compelling trade-off for the available compute budget.
  • 7.1. Model Size: A full expert iteration with the 774m-parameter model required about 2000 A100 days, whereas one parallelized proof search required about 0.1 A100 hour.The proof-search configuration was a = 1, d = 512, and e = 8.
  • 7.2. Limitations: The models generally cannot chain more than 2 or 3 non-trivial mathematical reasoning steps under the proposed search procedure.This prevents them from consistently solving challenging olympiad problems, although they can generate cuts and witnesses.
  • 7.2. Limitations: Generated cuts are often shallow, involving only a few proofsteps and not necessarily changing the proof structure deeply.The authors identify deeper cut generation and search procedures that exploit it as future research directions.

8. Conclusion

The paper presents expert iteration for GPT-f and shows that varied formal statements can support a curriculum of increasingly difficult problems. It positions this statement-based approach as a way to compensate for the lack of self-play in formal mathematics.

  • 8. Conclusion: The paper presents an expert iteration procedure for GPT-f that solves a curriculum of increasingly difficult problems from sufficiently varied formal statements.The curriculum is obtained without requiring the associated statements to come with full proofs.
  • 8. Conclusion: Automatically and manually curated formal statement sets can compensate for the lack of self-play in formal mathematics.The paper notes that such statements are much cheaper to formalize than full proofs.
  • Related Work: Earlier deep-learning work on formal mathematics focused primarily on premise selection and proof guidance.DeepMath used CNNs and RNNs for premise usefulness prediction, while FormulaNet improved results with graph neural networks.
  • Related Work: HOList and related work used formal environments, exploration, skip-tree objectives, and Transformers to advance automated theorem proving.The paper cites these efforts alongside GPT-f as evidence for Transformer-based formal reasoning.

B. Lean-gym

lean-gym provides a REPL interface for interacting with Lean proof states and tactics, enabling programmatic proof search and large-scale parallel execution. The section also describes the synthetic inequality data pipeline used for expert iteration experiments.

  • B. Lean-gym: lean-gym exposes an API for initializing searches from theorem declarations and applying tactics to tactic states.init-search returns a fresh search and tactic-state identifier, while run_tac returns an updated tactic state.
  • B. Lean-gym: Using lean-gym is equivalent to opening a Lean theorem, deleting its proof, and reconstructing it interactively.Its standard-input/output wrapper can be integrated from other programming languages with little code.
  • B. Lean-gym: lean-gym can access mathlib and miniF2F statements through Lean’s own library infrastructure.Loaded libraries are managed using leanpkg.toml.
  • B. Lean-gym: The stateful REPL scaled to thousands of cores and thousands of parallel proof searches, but its blocking interface prevents inner-proof-search parallelization.The authors note that the latter limitation could probably be removed in the future.
  • Pre-training Data: The updated WebMath pre-training mix up-weights high-quality mathematical content while avoiding overfitting and includes PACT mix2 directly.Including PACT mix2 avoids sequencing more than two pre-training phases for Lean models.
  • Synthetic Inequality Generator: The synthetic inequality generator has three phases: seed-expression generation, inequality composition, and simplification.Seed expressions track signs, known inequality theorems compose them, and Lean’s simp tactic performs final simplification.
  • Synthetic Inequality Generator: ND controls composition depth, while NS controls input-expression obfuscation and therefore contributes to generated-statement difficulty.The generator samples nn = 4 and randomly samples 2 ≤ nv ≤ 8 for each generation.

D.2. List of inequality composition theorems

The inequality generator composes existing inequalities through transformations and binary compositions using a listed set of theorem applications. The appendix gives a concrete generated theorem whose hypotheses and conclusion instantiate this composition process.

  • D.2. List of inequality composition theorems: One branch transforms the current composed inequality using a theorem from the listed composition rules.The list includes applications such as AddLeAdd, Bernoulli, Cauchy, Young, and DivLeDiv.
  • D.2. List of inequality composition theorems: The other branch composes the current inequality with a newly generated inequality using the listed composition theorems.This provides the second operation used to build increasingly complex inequalities.
  • D.2. List of inequality composition theorems: The theorem synthetic_ineq_nb_seed_var_4_depth_4_p_13 formalizes a depth-4 generated inequality over six positive real variables.Its assumptions state positivity for a through f, and its conclusion is a composed inequality ending with := sorry.

E. Example proofs from mathlib-train

This section presents proofs found by the models from mathlib-train and compares them with ground-truth versions. It also presents proofs from miniF2F datasets as evidence of capabilities emerging from the training procedure.

  • The section presents original model-found proofs from mathlib-train alongside their ground-truth versions.
  • The examples include proofs using case analysis, contradiction, induction, and Lean tactics such as simp and finish.
  • The section also presents proofs found on minif2f-{test,valid,curriculum} to demonstrate capabilities emerging from the training procedure.

F.1. Qualitative analysis of proofs

The qualitative analysis examines how the models solve formalized olympiad and contest problems, emphasizing tactic use, exogenous mathematical arguments, multi-step reasoning, and distinctive proof styles. Across examples, the models close problems with high-level tactics, generated witnesses, symbolic specialization, and concise machine-like proofs.

  • Computationally challenging problems: A large number of olympiad problems that are computationally challenging for humans become trivial for the models through Lean tactics.One example, mathd_numbertheory_447, is closed by refl.
  • High-level tactics: The models acquire advanced capabilities to leverage high-level tactics by providing exogenous arguments absent from the current tactic state.The cited tactics include linarith/nlinarith, norm_num, simp, and ring.
  • Multi-step reasoning: The models also produce multiple non-trivial reasoning steps involving witnesses, implication chaining, and context-specific exogenous terms.
  • Proof style: Model-generated proofs have a distinctive style, including machine-like one-liners that use high-level tactics differently from typical human formalizations.
  • Proof style: Search-generated proofs often interleave useful steps with extraneous proof steps such as hypothesis reversion, introduction, or no-op rewrites.This occurs despite a value-function bias toward shorter proofs.
  • imo_1961_p1: The model closes the system-of-equations problem by splitting cases, contraposing, and supplying crucial exogenous square-nonnegativity arguments to nlinarith.The arguments sq_nonneg (x - y) and sq_nonneg (y - z) are crucial in the final reasoning.
  • imo_1964_p2: The model closes an IMO problem in one line by supplying necessary exogenous arguments to nlinarith.Two of the listed final arguments can be omitted.
  • aime_1990_p15: The model closes a challenging AIME problem by providing crucial exogenous arguments to nlinarith, while other supplied arguments can be removed.The crucial arguments are sq_nonneg (x - y) and sq_nonneg (x + y - (2 : R)).
Loading 2202.01344v1…