Formal Mathematics Statement Curriculum Learning

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

177 citations recorded by the source corpus.

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.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Natural Language Processing, Prompting & Reasoning

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Natural Language Processing

In Prompting & Reasoning

Citations in the corpus

Solving Quantitative Reasoning Problems with Language Models (2022, background): “Previous work trained language models to predict mathematical expressions [34, 31, 32, 35, 36, 37, 38, 39].”
Llemma: An Open Language Model For Mathematics (2023, background): “…of strong mathematical reasoning are upstream of a number of research topics, such as reward modeling (Uesato et al., 2022; Lightman et al., 2023), reinforcement learning for reasoning (Polu et al., 2022; Lample et al., 2022), and algorithmic reasoning (Zhou et al., 2022; Zhang et al., 2023).”
STaR: Bootstrapping Reasoning With Reasoning (2022, background): “[16] builds off of ExIt for formal reasoning, while [22] applies iterated learning to visual question answering using modular networks which can be combined compositionally.”
PaLM-E: An Embodied Multimodal Language Model (2023, background): “, 2022), math problem solving (Lewkowycz et al., 2022; Polu et al., 2022), and code writing (Chen et al.”
Contrastive Distillation Is a Sample-Efficient Self-Supervised Loss Policy for Transfer Learning (2022, unknown): “This is also the case for iterative self-learning approaches like expert iteration (Anthony et al., 2017; Polu et al., 2022), which required 2000 A100 GPU-days for training as well as hand-engineered features.”
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models (2023, methodology): “Existing tool [19] is limited: 21.1% of the ground truth proofs are misjudged as incorrect, due to issues with how they construct the proof environment, which distorts the reported performance and produces unreliable feedback when used in reinforcement learning.”
A Survey of Large Language Models (2023, unknown): “As a typical approach, existing work on ATP utilizes LLMs to aid the search for proofs using an interactive theorem prover (ITP), such as Lean and Metamath [364, 365].”
Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers (2022, methodology): “The second is the Isabelle fraction of the MiniF2F dataset [Zheng et al., 2022] under an Apache license.”
A Review on Language Models as Knowledge Bases (2022, background): “Such tasks include: commonsense (Da et al., 2021), natural language inference (Bowman et al., 2015), mathematical (Saxton et al., 2019; Polu et al., 2022), rule-based (Clark et al., 2020), inductive (Misra, 2021) and abductive reasoning (Bhagavatula et al., 2020).”
A Survey of Deep Learning for Mathematical Reasoning (2022, unknown): “, 2022) provides a dataset of proof-steps from Lean’s mathematical library along with auxiliary tasks, while Lean-Gym (Polu et al., 2022) provides an interactive REPL.”
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs (2022, methodology): “We perform experiments to generate formal proofs of problems from the miniF2F dataset (Zheng et al., 2022) and show that a large portion of theorems can be proved automatically with this method.”
A Survey on Pretrained Language Models for Neural Code Intelligence (2022, methodology): “synthesis models have been used to solve linear algebra problems, math word problems, and perform automated proof search (Tang et al., 2021; Drori and Verma, 2021; Polu et al., 2022).”
HyperTree Proof Search for Neural Theorem Proving (2022, methodology): “Following [9], we also evaluate the pass@k by running k proof searches on the evaluated statements with the policy and critic obtained by online training.”
RT-2: Vision-Language-Action Models Transfer Web Knowledge to Robotic Control (2023, background): “…for a wide range of downstream tasks: large language models can enable not only fluent text generation [1, 2, 3] but emergent problem-solving [4, 5, 6] and creative generation of prose [7, 2] and code [8], while vision-language models enable open-vocabulary visual recognition [9, 10, 11] and can…”