Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving

• URL: http://arxiv.org/abs/2401.11898v1
• Date: Mon, 22 Jan 2024 12:49:08 GMT
• Title: Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving
• Authors: Salwa Tabet Gonzalez (University of Strasbourg), Predrag Jani\v{c}i\'c (University of Belgrade), Julien Narboux (University of Strasbourg)
• Abstract summary: We propose a framework for completing incomplete conjectures and incomplete proofs. The framework can turn a conjecture with missing assumptions into a proper theorem. Also, the proposed framework can help in completing a proof sketch into a human-readable and machine-checkable proof.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Conjecturing and theorem proving are activities at the center of mathematical practice and are difficult to separate. In this paper, we propose a framework for completing incomplete conjectures and incomplete proofs. The framework can turn a conjecture with missing assumptions and with an under-specified goal into a proper theorem. Also, the proposed framework can help in completing a proof sketch into a human-readable and machine-checkable proof. Our approach is focused on synthetic geometry, and uses coherent logic and constraint solving. The proposed approach is uniform for all three kinds of tasks, flexible and, to our knowledge, unique such approach.

Related papers

• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  This work proposes Alchemy, a framework for data synthesis that constructs formal theorems through symbolic mutation. For each candidate theorem in Mathlib, we identify all invocable theorems that can be used to rewrite or apply to it. As a result, our method increases the number of theorems in Mathlib by an order of magnitude, from 110k to 6M.
  arXiv  Detail & Related papers  (2024-10-21T08:04:21Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  We present Lean-STaR, a framework for training language models to produce informal thoughts prior to each step of a proof. Lean-STaR achieves state-of-the-art results on the miniF2F-test benchmark within the Lean theorem proving environment.
  arXiv  Detail & Related papers  (2024-07-14T01:43:07Z)
• 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)
• Autoformalizing Euclidean Geometry [74.72212706513318]
  We introduce a neuro-symbolic framework for autoformalizing Euclidean geometry. One challenge is that informal proofs rely on diagrams, leaving gaps in texts that are hard to formalize. We provide automatic semantic evaluation for autoformalized theorem statements.
  arXiv  Detail & Related papers  (2024-05-27T14:35:10Z)
• Towards Automated Readable Proofs of Ruler and Compass Constructions [0.0]
  We show how our triangle construction solver ArgoTriCS can cooperate with automated theorem provers for first order logic and coherent logic. These proofs currently rely on many high-level lemmas and our goal is to have them all formally shown from the basic axioms of geometry.
  arXiv  Detail & Related papers  (2024-01-22T12:48:51Z)
• Plan, Verify and Switch: Integrated Reasoning with Diverse X-of-Thoughts [65.15322403136238]
  We propose XoT, an integrated problem solving framework by prompting LLMs with diverse reasoning thoughts. For each question, XoT always begins with selecting the most suitable method then executes each method iteratively. Within each iteration, XoT actively checks the validity of the generated answer and incorporates the feedback from external executors.
  arXiv  Detail & Related papers  (2023-10-23T07:02:20Z)
• A Measure-Theoretic Axiomatisation of Causality [55.6970314129444]
  We argue in favour of taking Kolmogorov's measure-theoretic axiomatisation of probability as the starting point towards an axiomatisation of causality. Our proposed framework is rigorously grounded in measure theory, but it also sheds light on long-standing limitations of existing frameworks.
  arXiv  Detail & Related papers  (2023-05-19T13:15:48Z)
• ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics [7.607254619341369]
  We introduce ProofNet, a benchmark for autoformalization and formal proving of undergraduate-level mathematics. The ProofNet benchmarks consists of 371 examples, each consisting of a formal theorem statement in Lean 3. We report baseline results on statement autoformalization via in-context learning.
  arXiv  Detail & Related papers  (2023-02-24T03:28:46Z)
• TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning [6.764610878007278]
  We propose a novel approach to interactive theorem-proving (ITP) using deep reinforcement learning. We formulate the process of ITP as a Markov decision process (MDP) in which each state represents a set of potential derivation paths. We show that the framework provides comparable performance to that of the approaches that use human experts.
  arXiv  Detail & Related papers  (2021-02-19T06:08:39Z)
• 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)
• Geometric Formulation for Discrete Points and its Applications [0.0]
  We introduce a novel formulation for geometry on discrete points. It is based on a universal differential calculus, which gives a geometric description of a discrete set by the algebra of functions.
  arXiv  Detail & Related papers  (2020-02-07T01:12:57Z)

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.