Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers

By Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzyg'o'zd'z, Piotr Milo's, Yuhuai Wu, Mateja Jamnik. 2022

144 citations recorded by the source corpus.

In theorem proving, the task of selecting useful premises from a large library to unlock the proof of a given conjecture is crucially important. This presents a challenge for all theorem provers, especially the ones based on language models, due to their relative inability to reason over huge volumes of premises in text form. This paper introduces Thor, a framework integrating language models and automated theorem provers to overcome this difficulty. In Thor, a class of methods called hammers that leverage the power of automated theorem provers are used for premise selection, while all other tasks are designated to language models. Thor increases a language model's success rate on the PISA dataset from $39\%$ to $57\%$, while solving $8.2\%$ of problems neither language models nor automated theorem provers are able to solve on their own. Furthermore, with a significantly smaller computational budget, Thor can achieve a success rate on the MiniF2F dataset that is on par with the best existing methods. Thor can be instantiated for the majority of popular interactive theorem provers via a straightforward protocol we provide.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Natural Language Processing, Program Analysis & Verification

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 Program Analysis & Verification

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, methodology): “This includes synthesizing proofs via tactic prediction (Polu & Sutskever, 2020; Han et al., 2022; Lample et al., 2022; Jiang et al., 2022), autoformalization (Wu et al., 2022; Jiang et al., 2023), and integrated tools (Welleck & Saha, 2023).”
Autoformalization with Large Language Models (2022, methodology): “In evaluation, whenever the special token is emitted, Thor invokes the proof method Sledgehammer [36] in Isabelle with a 30 second timeout.”
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs (2022, methodology): “Language models for proof search Finally, we include baselines which are representative of state-of-the-art neural theorem proving in Isabelle, speciﬁcally Thor (Jiang et al., 2022) and Thor with expert iteration on autoformalized data (Wu et al., 2022).”
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].”
Baldur: Whole-Proof Generation and Repair with Large Language Models (2023, methodology): “While comparisons across different neural theorem provers are hard in general, we can compare to Thor [32], one of the strongest approaches available.”
ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics (2023, methodology): “An alternative approach is to use language models to guide formal proof-search in an interactive theorem prover (ITP) [Yang and Deng, 2019, Polu and Sutskever, 2020, Polu et al., 2022, Jiang et al., 2022a].”
Teaching Algorithmic Reasoning via In-context Learning (2022, background): “In addition to this class of benchmarks, formal mathematics in the form of theorem-proofs (Rabe et al., 2020; Li et al., 2020; Polu and Sutskever, 2020; Welleck et al., 2021; Jiang et al., 2022; Wu et al., 2022) has been considered extensively.”
A Survey of Deep Learning for Mathematical Reasoning (2022, unknown): “Thor (Jiang et al., 2022a) pre-trains a language model on the GitHub + arXiv subsets of The Pile (Gao et al.”
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models (2023, methodology): “…dimensions: proof search algorithms for assembling model-generated steps into complete proofs [17, 21]; overcoming data scarcity through reinforcement learning (RL) [17, 19, 36, 37] or synthetic/auxiliary data [16, 38–40]; as well as outsourcing some proof goals to classical provers [18, 41–43].”