PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Albert Q. Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Wu, Mateja Jamnik

arXiv:2205.10893v1cs.AI

TL;DR

Language models struggle to select useful premises from the huge volumes of facts in theorem-proving libraries. Thor assigns premise selection to hammers while leaving other tasks to language models, improving results across PISA and MiniF2F with a much smaller computational budget than expert iteration on MiniF2F.

  • Problem

    Language models struggle to reason over the large volumes of facts and definitions needed for premise selection, an important task in finding proofs.

    Source: §1 · p. 1, §2.1 · p. 3

  • Method

    Thor combines language models with automated theorem provers through hammers, using the hammer for premise selection and language models for other tasks.

    Source: §1 · p. 2

  • Results

    PISA success rises from 39.0% to 57.0%, Thor solves 8.2% of problems neither standalone system solves, and MiniF2F success rises from 29.6% to 29.9% with far less computation.

    Source: §1 · p. 2, Contributions · p. 2

  • Takeaways & Limitations

    The results demonstrate that selecting a suitable premise-selection subsystem can benefit the performance of the overall reasoning system.

    Source: §1 · p. 2

    Evaluation covers only Isabelle, and current Thor admits only premise-selection tools that use a hammer to generate valid ITP proof steps.

    Source: §6 · pp. 9–10

Abstract

from arXiv · show

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.

1 Introduction

Thor addresses language models’ difficulty selecting premises from large libraries by assigning that task to hammers while language models handle the other tasks. Its Isabelle/Sledgehammer instance improves results on PISA and MiniF2F.

1 Introduction

  • Language models struggle to reason over thousands of facts and their definitions in text, while premise selection is essential for discovering many proofs.The introduction describes hammers as using external provers to find proof-relevant premises.Source: §1 · p. 1

Contributions

  • PISA success rises from 39.0% to 57.0%, Thor solves 8.2% of problems neither language models nor Sledgehammer solve alone, and MiniF2F rises from 29.6% to 29.9% with far less computation.On MiniF2F, the comparison is with the expert-iteration result reported by Polu et al. [2022].Source: §1 · p. 2, Contributions · p. 2
  • Thor’s premise-selection subsystem can benefit the performance of the overall reasoning system.The framework marks successful hammer applications in training data and invokes the hammer when the model emits a special token.Source: §1 · p. 2
  • Thor integrates language models and automated theorem provers through hammers, assigning premise selection to the hammer method.The paper instantiates the framework with Isabelle and Sledgehammer.Source: Contributions · p. 2, §1 · p. 2

2 Background

The background contrasts ATPs and ITPs, explains why premise selection is difficult for language models, and describes how hammers connect ATP reasoning with ITP proof checking.

2.1 Automated and Interactive Theorem Proving

  • ITPs support diverse, sound formalizations, while ATPs target well-defined problems; large formal libraries make finding useful premises difficult.The paper models ITP proving as successive proof-state transformations until all goals are discharged.Source: §2.1 · pp. 2–3

2.2 Language Models for Theorem Proving

  • Language models predict proof steps from text, but premise selection is difficult because libraries and premise contexts can exceed their capacity.The Archive of Formal Proofs has over 200,000 theorems; premise-selection steps advance proofs 1.9% of the time, versus 28.2% for steps without premises.Source: §2.2 · p. 3

2.3 Hammers

  • Hammers send goals and candidate premises to external ATPs, select useful premises from successful proofs, and reconstruct proofs within the ITP kernel.External ATPs act as premise relevance filters rather than trusted oracles.Source: §2.3 · pp. 3–4

3 Thor

Thor integrates language models with hammers to address premise selection. Its protocol labels successful hammer applications in training data and invokes the hammer when the model predicts its special token.

3 Thor

  • During preprocessing, Thor changes the target output to <hammer> <EOS> when the hammer succeeds and otherwise keeps the original output.The procedure is applied across training datapoints; at evaluation, the token triggers the hammer method.Source: §3 · pp. 4–5
  • Thor’s protocol uses training examples to teach a heuristic for when to invoke a hammer and is straightforward to implement in hammer-enabled ITPs.At evaluation, the hammer is called when the model outputs <hammer> <EOS>.Source: §3 · p. 5
  • For ITPs with traces of hammer-generated steps, deployment adds little computational cost beyond language-model training.The paper estimates 7,400 CPU hours to preprocess one large proof corpus for a year’s submissions, a one-time, shareable process.Source: §3 · p. 5

4 Experiment

The experiments evaluate Thor on Isabelle across PISA and MiniF2F, testing whether it complements language models and Sledgehammer and how design choices affect results. Thor improves proof success on both benchmarks, with gains comparable to expert iteration on MiniF2F at much lower computational cost.

4 Experiment

  • The evaluation asks whether Thor solves problems neither component solves alone, improves premise selection, and how context, sampling diversity, and premise-selection training affect performance.The study instantiates Thor for Isabelle, chosen for Sledgehammer’s maturity and the size of its Archive of Formal Proofs.Source: §4 · p. 5

4.2 Datasets and Environment

  • PISA contains 2.49 million datapoints, while the Isabelle MiniF2F benchmark contains 488 high-school competition problems; PISA evaluation samples 3,000 test theorems.MiniF2F’s problems are formalised in Lean, Metamath, and Isabelle.Source: §4.2 · p. 6

4.3 Thor Against an Ensemble of a Language Model and Sledgehammer

  • 57.0% of PISA/test problems were proved by Thor, versus 48.8% by the union of the language model and Sledgehammer alone.The language model and Sledgehammer individually proved 39.0% and 25.7%; Thor solved 8.2% that neither could solve alone.Source: Table 1 · p. 6, §4.3 · p. 7
  • Thor found several times more proofs than the language model when proofs required more premises, and its advantage increased with ground-truth premise count.For proofs requiring zero or one premise, the systems performed similarly.Source: §4.3 · p. 7, Figure 2 · p. 7

4.4 The Effect of Learning How to Select Premises

  • 55.4% success on PISA/test for a variant that learned both when and how to select premises was 1.6% below base Thor.The variant invoked Sledgehammer when the model emitted a Sledgehammer keyword.Source: §4.4 · p. 7, Table 2 · p. 8

4.5 The Effect of the Proof Context

  • 53.6% of PISA/test theorems were proved without the most recent proof-step context, 3.4% fewer than by base Thor.The authors describe this context as crucial for Thor’s optimal performance.Source: §4.5 · p. 8

4.6 The Effect of the Sequence Sampling Diversity

  • 55.7% success with sampling temperature T = 1.0 was 1.3% below Thor’s result with T = 1.2.The authors suggest more diverse sampling can improve Thor’s performance.Source: §4.6 · p. 8

4.7 Comparing Thor with Expert Iteration

  • 29.9% of MiniF2F test problems were proved by Thor, versus 29.6% after expert iteration, with Thor’s improvement comparable at much lower computational cost.Thor raises the language model’s success rate by 5.7%; expert iteration raises PACT’s by 5.0%.Source: Table 3 · p. 8, §4.7 · p. 9

5 Related Work

Earlier language-model theorem provers applied model outputs directly to interactive theorem provers, while Thor explicitly combines language models with symbolic reasoning tools for premise selection. The paper situates hammers among several alternative premise-selection approaches.

5 Related Work

  • Thor is presented as the first system to explicitly hybridise language models and automated theorem provers for theorem proving.Earlier systems iteratively sampled a language model and applied its output directly to the interactive theorem prover.Source: §5 · p. 9
  • Premise-selection alternatives include symbolic ranking methods, machine-learning systems, and deep-learning approaches, any of which may suit future Thor versions.Examples include SInE, SRASS, MaLARea, and deep-learning methods.Source: §5 · p. 9

6 Discussion

The discussion presents Thor as an efficient way to combine language models and automated theorem provers, while noting limits on supported premise-selection tools and evaluation beyond Isabelle.

6 Discussion

  • Thor with Isabelle increased automatically proved theorems, remains computationally efficient, and can be combined with expert iteration or proof artifact co-training.The authors describe these approaches as having no contradictions and being easily incorporated with Thor.Source: §6 · p. 9
  • Thor currently supports only automated theorem provers that use hammers to generate valid proof steps directly in the interactive theorem prover.Other premise-selection approaches that do not directly generate proof steps are outside the current version's scope.Source: §6 · pp. 9–10
  • Experiments tested Thor only with Isabelle because of computational costs, leaving its improvement on other interactive theorem provers untested.The authors identify instantiating Thor with other theorem provers as future work.Source: §6 · p. 10
  • The authors argue that Thor's performance, computational efficiency, and convenient deployment give scope to tool hybridisation in automated reasoning and AI.They describe tool hybridisation as promising for impact in both fields.Source: §6 · p. 10

A Appendix

The appendix presents examples of lemmas solved by Thor alone, illustrating proof traces across tree, matrix, and linear-algebra results.

A Appendix

  • The appendix's examples are lemmas solved by Thor only.They include results about columns of a matrix, tree measures, and a linear map's kernel.Source: A Appendix · p. 13
  • For cols_upt_k, Thor unfolds the definition and simplifies the goal before Sledgehammer discharges the remaining subgoals.The lemma equates columns through index k+1 with the columns through k plus column k+1, provided k+1 is below the matrix's column count.Source: A Appendix · p. 13
  • For size_del_max, Thor uses structural induction, simplifies split product cases, and finishes the remaining goal with Sledgehammer.The lemma states that deleting the maximum from a non-leaf weight-balanced tree reduces its size by one.Source: A Appendix · p. 13
  • For t_list_of_B_log_bound, Thor relates a Braun tree's t_list_of_B measure to its size, using induction, case analysis, and Sledgehammer.The bound is 3 * (nlog2 (size t + 1) + 1) * size t, where nlog2 is the ceiling of log base 2.Source: A Appendix · p. 13
  • For inj_imp_Ker0, Thor proves that injectivity on V's carrier makes the kernel equal to the zero singleton, then closes the final goal with Sledgehammer.The proof applies equality and subset introduction before unfolding the kernel definition and simplifying.Source: A Appendix · p. 14

Related papers

Loading 2205.10893v1…