Conjectures, Tests and Proofs: An Overview of Theory Exploration
- URL: http://arxiv.org/abs/2109.03721v1
- Date: Tue, 7 Sep 2021 01:57:07 GMT
- Title: Conjectures, Tests and Proofs: An Overview of Theory Exploration
- Authors: Moa Johansson (Chalmers University of Technology), Nicholas Smallbone
(Chalmers University of Technology)
- Abstract summary: We give a brief overview of a theory exploration system called QuickSpec.
QuickSpec is able to automatically discover interesting conjectures about a given set of functions.
It has been successfully applied to generate lemmas for automated inductive theorem proving.
- Score: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: A key component of mathematical reasoning is the ability to formulate
interesting conjectures about a problem domain at hand. In this paper, we give
a brief overview of a theory exploration system called QuickSpec, which is able
to automatically discover interesting conjectures about a given set of
functions. QuickSpec works by interleaving term generation with random testing
to form candidate conjectures. This is made tractable by starting from small
sizes and ensuring that only terms that are irreducible with respect to already
discovered conjectures are considered. QuickSpec has been successfully applied
to generate lemmas for automated inductive theorem proving as well as to
generate specifications of functional programs. We give an overview of typical
use-cases of QuickSpec, as well as demonstrating how to easily connect it to a
theorem prover of the user's choice.
Related papers
- Learning Formal Mathematics From Intrinsic Motivation [34.986025832497255]
Minimo is an agent that learns to pose problems for itself (conjecturing) and solve them (theorem proving)
We combine methods for constrained decoding and type-directed synthesis to sample valid conjectures from a language model.
Our agent targets generating hard but provable conjectures - a moving target, since its own theorem proving ability also improves as it trains.
arXiv Detail & Related papers (2024-06-30T13:34:54Z) - ATG: Benchmarking Automated Theorem Generation for Generative Language Models [83.93978859348313]
Humans can develop new theorems to explore broader and more complex mathematical results.
Current generative language models (LMs) have achieved significant improvement in automatically proving theorems.
This paper proposes an Automated Theorem Generation benchmark that evaluates whether an agent can automatically generate valuable (and possibly brand new) theorems.
arXiv Detail & Related papers (2024-05-05T02:06:37Z) - Machine learning and information theory concepts towards an AI
Mathematician [77.63761356203105]
The current state-of-the-art in artificial intelligence is impressive, especially in terms of mastery of language, but not so much in terms of mathematical reasoning.
This essay builds on the idea that current deep learning mostly succeeds at system 1 abilities.
It takes an information-theoretical posture to ask questions about what constitutes an interesting mathematical statement.
arXiv Detail & Related papers (2024-03-07T15:12:06Z) - Considerations on Approaches and Metrics in Automated Theorem
Generation/Finding in Geometry [0.0]
We present and discuss different approaches for the automatic discovery of geometric theorems (and properties)
We will argue that judging whether a theorem prover is able to produce interesting theorems remains a non deterministic task.
arXiv Detail & Related papers (2024-01-22T12:51:19Z) - Mathematical conjecture generation using machine intelligence [0.0]
We focus on strict inequalities of type f g and associate them with a vector space.
We develop a structural understanding of this conjecture space by studying linear automorphisms of this manifold.
We propose an algorithmic pipeline to generate novel conjectures using geometric gradient descent.
arXiv Detail & Related papers (2023-06-12T17:58:38Z) - TheoremQA: A Theorem-driven Question Answering dataset [100.39878559382694]
GPT-4's capabilities to solve these problems are unparalleled, achieving an accuracy of 51% with Program-of-Thoughts Prompting.
TheoremQA is curated by domain experts containing 800 high-quality questions covering 350 theorems.
arXiv Detail & Related papers (2023-05-21T17:51:35Z) - Connes implies Tsirelson: a simple proof [91.3755431537592]
We show that the Connes embedding problem implies the synchronous Tsirelson conjecture.
We also give a different construction of Connes' algebra $mathcalRomega$ appearing in the Connes embedding problem.
arXiv Detail & Related papers (2022-09-16T13:59:42Z) - Who Finds the Short Proof? An Exploration of variants of Boolos' Curious
Inference using Higher-order Automated Theorem Provers [62.997667081978825]
We report on an exploration of variants of Boolos' curious inference using higher-order automated theorem provers.
Surprisingly, only a single shorthand notation still had to be provided by hand.
All higher-order lemmas required for obtaining short proof are automatically discovered by the computer.
arXiv Detail & Related papers (2022-08-14T16:31:04Z) - Optimal Measurement Structures for Contextuality Applications [4.407033774951362]
The Kochen-Specker (KS) theorem is a corner-stone result in the foundations of quantum mechanics.
Recently specific substructures termed $01$-gadgets were shown to exist within KS proofs.
We show these gadgets and their generalizations provide an optimal toolbox for contextuality applications.
arXiv Detail & Related papers (2022-06-27T09:34:36Z) - Prove-It: A Proof Assistant for Organizing and Verifying General
Mathematical Knowledge [0.0]
We introduce Prove-It, a Python-based general-purpose interactive theorem-proving assistant.
Prove-It uses a highly-flexible Jupyter notebook-based user interface that documents interactions and proof steps.
Current development and future work includes promising applications to quantum circuit manipulation and quantum algorithm verification.
arXiv Detail & Related papers (2020-12-20T18:15:12Z) - 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.