Automated Planning Techniques for Elementary Proofs in Abstract Algebra

• URL: http://arxiv.org/abs/2312.06490v1
• Date: Mon, 11 Dec 2023 16:17:43 GMT
• Title: Automated Planning Techniques for Elementary Proofs in Abstract Algebra
• Authors: Alice Petrov, Christian Muise
• Abstract summary: We investigate the use of planning to construct elementary proofs in abstract algebra. We implement basic implications, equalities, and rules in both deterministic and non-deterministic domains. The success of this initial implementation suggests that the well-established techniques seen in automated planning are applicable to the relatively newer field of automated theorem proving.
• Score: 5.379968204052965
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: This paper explores the application of automated planning to automated theorem proving, which is a branch of automated reasoning concerned with the development of algorithms and computer programs to construct mathematical proofs. In particular, we investigate the use of planning to construct elementary proofs in abstract algebra, which provides a rigorous and axiomatic framework for studying algebraic structures such as groups, rings, fields, and modules. We implement basic implications, equalities, and rules in both deterministic and non-deterministic domains to model commutative rings and deduce elementary results about them. The success of this initial implementation suggests that the well-established techniques seen in automated planning are applicable to the relatively newer field of automated theorem proving. Likewise, automated theorem proving provides a new, challenging domain for automated planning.

Related papers

• Unifying Tree Search Algorithm and Reward Design for LLM Reasoning: A Survey [92.71325249013535]
  Deliberative tree search is a cornerstone of Large Language Model (LLM) research.<n>This paper introduces a unified framework that deconstructs search algorithms into three core components.
  arXiv  Detail & Related papers  (2025-10-11T03:29:18Z)
• LLM-Generated Heuristics for AI Planning: Do We Even Need Domain-Independence Anymore? [87.71321254733384]
  Large language models (LLMs) can generate planning approaches tailored to specific planning problems. LLMs can achieve state-of-the-art performance on some standard IPC domains. We discuss whether these results signify a paradigm shift and how they can complement existing planning approaches.
  arXiv  Detail & Related papers  (2025-01-30T22:21:12Z)
• Learning Quantitative Automata Modulo Theories [17.33092604696224]
  We present QUINTIC, an active learning algorithm, wherein the learner infers a valid automaton through deductive reasoning. Our evaluations utilize theory of rationals in order to learn summation, discounted summation, product, and classification quantitative automata.
  arXiv  Detail & Related papers  (2024-11-15T21:51:14Z)
• 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)
• A Hybrid System for Systematic Generalization in Simple Arithmetic Problems [70.91780996370326]
  We propose a hybrid system capable of solving arithmetic problems that require compositional and systematic reasoning over sequences of symbols. We show that the proposed system can accurately solve nested arithmetical expressions even when trained only on a subset including the simplest cases.
  arXiv  Detail & Related papers  (2023-06-29T18:35:41Z)
• Reformulation Techniques for Automated Planning: A Systematic Review [4.83420384410068]
  A cornerstone of domain-independent planning is the separation between planning logic and the knowledge model. Over the past decades, significant research effort has been devoted to the design of reformulation techniques. We present a systematic review of the large body of work on reformulation techniques for classical planning.
  arXiv  Detail & Related papers  (2023-01-24T15:33:37Z)
• Structural Analysis of Branch-and-Cut and the Learnability of Gomory Mixed Integer Cuts [88.94020638263467]
  The incorporation of cutting planes within the branch-and-bound algorithm, known as branch-and-cut, forms the backbone of modern integer programming solvers. We conduct a novel structural analysis of branch-and-cut that pins down how every step of the algorithm is affected by changes in the parameters defining the cutting planes added to the input integer program. Our main application of this analysis is to derive sample complexity guarantees for using machine learning to determine which cutting planes to apply during branch-and-cut.
  arXiv  Detail & Related papers  (2022-04-15T03:32:40Z)
• Goal Agnostic Planning using Maximum Likelihood Paths in Hypergraph World Models [1.370633147306388]
  We present a hypergraph-based machine learning algorithm, a datastructure--driven maintenance method, and a planning algorithm based on a probabilistic application of Dijkstra's algorithm. We prove that the algorithm determines optimal solutions within the problem space, mathematically bound learning performance, and supply a mathematical model analyzing system state progression through time.
  arXiv  Detail & Related papers  (2021-10-18T16:22:33Z)
• Refining Labelled Systems for Modal and Constructive Logics with Applications [0.0]
  This thesis serves as a means of transforming the semantics of a modal and/or constructive logic into an 'economical' proof system. The refinement method connects two proof-theoretic paradigms: labelled and nested sequent calculi. The introduced refined labelled calculi will be used to provide the first proof-search algorithms for deontic STIT logics.
  arXiv  Detail & Related papers  (2021-07-30T08:27:15Z)
• Induction and Exploitation of Subgoal Automata for Reinforcement Learning [75.55324974788475]
  We present ISA, an approach for learning and exploiting subgoals in episodic reinforcement learning (RL) tasks. ISA interleaves reinforcement learning with the induction of a subgoal automaton, an automaton whose edges are labeled by the task's subgoals. A subgoal automaton also consists of two special states: a state indicating the successful completion of the task, and a state indicating that the task has finished without succeeding.
  arXiv  Detail & Related papers  (2020-09-08T16:42:55Z)
• 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)
• A General Framework for Consistent Structured Prediction with Implicit Loss Embeddings [113.15416137912399]
  We propose and analyze a novel theoretical and algorithmic framework for structured prediction. We study a large class of loss functions that implicitly defines a suitable geometry on the problem. When dealing with output spaces with infinite cardinality, a suitable implicit formulation of the estimator is shown to be crucial.
  arXiv  Detail & Related papers  (2020-02-13T10:30:04Z)

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.