Learning to Prove Theorems by Learning to Generate Theorems

By Mingzhe Wang, Jia Deng. 2020

59 citations recorded by the source corpus.

We consider the task of automated theorem proving, a key AI task. Deep learning has shown promise for training theorem provers, but there are limited human-written theorems and proofs available for supervised learning. To address this limitation, we propose to learn a neural generator that automatically synthesizes theorems and proofs for the purpose of training a theorem prover. Experiments on real-world tasks demonstrate that synthetic data from our approach improves the theorem prover and advances the state of the art of automated theorem proving in Metamath.

Subfields: Natural Language Processing

How researchers see this paper

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

In Natural Language Processing

Citations in the corpus

Generative Language Modeling for Automated Theorem Proving (2020, methodology): “mm as reported in MetaGenIL[25] (their methodology for benchmarking their solution is close to ours so the numbers are directly comparable); (ii) a 160m parameters trained from scratch on our raw dataset using the proofstep objective; and (iii) a 160m parameters trained from scratch on our augmented”
ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language (2020, background): “, (Polu and Sutskever, 2020; Wang and Deng, 2020), while ProofWriter performs inference with differing sets of rules expressed in natural language.”
Explaining Answers with Entailment Trees (2021, background): “Recent work in deductive reasoning has shown that transformers can generate formal proofs with high reliability, both in a formal setting (Polu and Sutskever, 2020; Wang and Deng, 2020) and with rules expressed in natural language (Saha 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].”
Solving olympiad geometry without human demonstrations (2024, methodology): “Synthetic data has long been recognized and used as an important ingredient in theorem proving 63–66 .”
Modelling High-Level Mathematical Reasoning in Mechanised Declarative Proofs (2020, methodology): “Statistical conjecture synthesis based on substitution has been explored in Metamath [47] and earlier in Mizar [12].”
INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving (2020, methodology): “MetaGen [32], a neural generator that synthesized theorems, was proposed for the training of an automatic theorem prover.”
Proof Artifact Co-training for Theorem Proving with Language Models (2021, methodology): “Holophrasm (Whalen, 2016), MetaGen (Wang & Deng, 2020), and GPT-f (Polu & Sutskever, 2020) all use RNNs or Transformers to generate proof steps.”