Learning to Prove from Synthetic Theorems

• URL: http://arxiv.org/abs/2006.11259v1
• Date: Fri, 19 Jun 2020 17:48:09 GMT
• Title: Learning to Prove from Synthetic Theorems
• Authors: Eser Ayg\"un, Zafarali Ahmed, Ankit Anand, Vlad Firoiu, Xavier Glorot, Laurent Orseau, Doina Precup, Shibl Mourad
• Abstract summary: A major challenge in applying machine learning to automated theorem proving is the scarcity of training data. We propose an approach that relies on training with synthetic theorems, generated from a set of axioms. We show that such theorems can be used to train an automated prover and that the learned prover transfers successfully to human-generated theorems.
• Score: 41.74768503409581
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: A major challenge in applying machine learning to automated theorem proving is the scarcity of training data, which is a key ingredient in training successful deep learning models. To tackle this problem, we propose an approach that relies on training with synthetic theorems, generated from a set of axioms. We show that such theorems can be used to train an automated prover and that the learned prover transfers successfully to human-generated theorems. We demonstrate that a prover trained exclusively on synthetic theorems can solve a substantial fraction of problems in TPTP, a benchmark dataset that is used to compare state-of-the-art heuristic provers. Our approach outperforms a model trained on human-generated problems in most axiom sets, thereby showing the promise of using synthetic data for this task.

Related papers

• Training Nonlinear Transformers for Chain-of-Thought Inference: A Theoretical Generalization Analysis [82.51626700527837]
  Chain-of-shift (CoT) is an efficient method that enables the reasoning ability of large language models by augmenting the query using examples with multiple intermediate steps. We show that despite the theoretical success of CoT, it fails to provide an accurate generalization when CoT does.
  arXiv  Detail & Related papers  (2024-10-03T03:12:51Z)
• Discovering Interpretable Physical Models using Symbolic Regression and Discrete Exterior Calculus [55.2480439325792]
  We propose a framework that combines Symbolic Regression (SR) and Discrete Exterior Calculus (DEC) for the automated discovery of physical models. DEC provides building blocks for the discrete analogue of field theories, which are beyond the state-of-the-art applications of SR to physical problems. We prove the effectiveness of our methodology by re-discovering three models of Continuum Physics from synthetic experimental data.
  arXiv  Detail & Related papers  (2023-10-10T13:23:05Z)
• Learning to Guide a Saturation-Based Theorem Prover [9.228237801323042]
  TRAIL is a deep learning-based approach to theorem proving that characterizes core elements of saturation-based theorem proving within a neural framework. To the best of our knowledge, TRAIL is the first reinforcement learning-based approach to exceed the performance of a state-of-the-art traditional theorem prover.
  arXiv  Detail & Related papers  (2021-06-07T18:35:57Z)
• Training a First-Order Theorem Prover from Synthetic Data [50.23600875138756]
  A major challenge in applying machine learning to automated theorem proving is the scarcity of training data. We propose an approach that relies on training purely with synthetically generated theorems, without any human data aside from axioms. Our neural prover outperforms the state-of-the-art E-prover on this synthetic data in both time and search steps.
  arXiv  Detail & Related papers  (2021-03-05T17:01:34Z)
• Proof Artifact Co-training for Theorem Proving with Language Models [4.934817254755007]
  PACT (bf Proof bf Artifact bf Co-bf Training) is a general methodology for extracting self-supervised data from kernel-level proof terms for co-training. We instrument Lean with a neural theorem prover driven by a Transformer language model and show that PACT improves theorem proving success rate on a held-out suite of test theorems from 32% to 48%.
  arXiv  Detail & Related papers  (2021-02-11T18:59:24Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  This work is motivated by the possibility that a major limitation of automated theorem provers compared to humans might be addressable via generation from language models. We present an automated prover and proof assistant, GPT-f, for the Metamath formalization language, and analyze its performance.
  arXiv  Detail & Related papers  (2020-09-07T19:50:10Z)
• IsarStep: a Benchmark for High-level Mathematical Reasoning [20.96474618260995]
  We present a benchmark for high-level mathematical reasoning and study the reasoning capabilities of neural sequence-to-sequence models. We build a non-synthetic dataset from the largest repository of proofs written by human experts in a theorem prover.
  arXiv  Detail & Related papers  (2020-06-13T21:09:23Z)
• Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
  We 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.
  arXiv  Detail & Related papers  (2020-02-17T16:06:02Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.