Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Lemmas: Generation, Selection, Application

Michael Rawson, Christoph Wernhard, Zsolt Zombori, Wolfgang Bibel

TL;DR

This work tackles improving automated theorem proving by exploiting lemmas within condensed detachment (CD) problems. It introduces SGCD, a Structure Generating Theorem Prover that enumerates proof structures as $D$-terms and couples this with machine learning-based lemma utility models (both linear and graph neural networks) to generate and select useful lemmas before search, thereby guiding proof search. The approach yields substantial gains across both CM-CT and RS provers, including a remarkable automatic proof of Meredith's single axiom LCL073-1, showcasing the value of leveraging proof structure in ATP. Overall, the study demonstrates that explicit handling of proof structures and external lemma provisioning can close parts of the gap between different proving paradigms and opens avenues for generalizing lemma-based strategies to broader first-order theories.

Abstract

Noting that lemmas are a key feature of mathematics, we engage in an investigation of the role of lemmas in automated theorem proving. The paper describes experiments with a combined system involving learning technology that generates useful lemmas for automated theorem provers, demonstrating improvement for several representative systems and solving a hard problem not solved by any system for twenty years. By focusing on condensed detachment problems we simplify the setting considerably, allowing us to get at the essence of lemmas and their role in proof search.

Lemmas: Generation, Selection, Application

TL;DR

This work tackles improving automated theorem proving by exploiting lemmas within condensed detachment (CD) problems. It introduces SGCD, a Structure Generating Theorem Prover that enumerates proof structures as -terms and couples this with machine learning-based lemma utility models (both linear and graph neural networks) to generate and select useful lemmas before search, thereby guiding proof search. The approach yields substantial gains across both CM-CT and RS provers, including a remarkable automatic proof of Meredith's single axiom LCL073-1, showcasing the value of leveraging proof structure in ATP. Overall, the study demonstrates that explicit handling of proof structures and external lemma provisioning can close parts of the gap between different proving paradigms and opens avenues for generalizing lemma-based strategies to broader first-order theories.

Abstract

Noting that lemmas are a key feature of mathematics, we engage in an investigation of the role of lemmas in automated theorem proving. The paper describes experiments with a combined system involving learning technology that generates useful lemmas for automated theorem provers, demonstrating improvement for several representative systems and solving a hard problem not solved by any system for twenty years. By focusing on condensed detachment problems we simplify the setting considerably, allowing us to get at the essence of lemmas and their role in proof search.
Paper Structure (31 sections, 5 equations, 4 figures, 11 tables)

This paper contains 31 sections, 5 equations, 4 figures, 11 tables.

Table of Contents

  1. Introduction
  2. Structure of the Paper.
  3. Background and Related Work
  4. Machine Learning for ATP
  5. Condensed Detachment: Proofs as Terms
  6. Condensed Detachment for ATP and Lemmas
  7. SGCD --- Structure Generating Theorem Proving
  8. Improving a Prover via Learned Lemma Selection
  9. Base Prover.
  10. Utility Model Training.
  11. Candidate Lemma Generation.
  12. Evaluated Prover.
  13. Learning-Based Experiments
  14. Improving the Base Prover.
  15. Learned Lemmas to Enhance other Provers.
  16. ...and 16 more sections

Figures (4)

  • Figure 1: The nested loops of the SGCD theorem proving method.
  • Figure 2: The D-term of our proof of LCL073-1 represented by factor equations.
  • Figure 3: Our proof of LCL073-1 in the notation of Meredith meredith:notes:1963cwwb:article. For each factor of the overall D-term the argument term of its MGT is there shown in Łu-ka-sie-wicz's notation.
  • Figure 4: Our proof of LCL073-1 with the ATP-oriented notation for formulas and D-terms of the paper, arranged such that it mimics Meredith's notation.