Lemmanaid: Neuro-Symbolic Lemma Conjecturing

• URL: http://arxiv.org/abs/2504.04942v1
• Date: Mon, 07 Apr 2025 11:30:36 GMT
• Title: Lemmanaid: Neuro-Symbolic Lemma Conjecturing
• Authors: Yousef Alhessi, Sólrún Halla Einarsdóttir, George Granberry, Emily First, Moa Johansson, Sorin Lerner, Nicholas Smallbone,
• Abstract summary: We present the first steps towards a practical neuro-symbolic lemma conjecturing tool, Lemmanaid.<n>We train an LLM to generate lemma templates that describe the shape of a lemma, and use symbolic methods to fill in the details.<n>We compare Lemmanaid against an LLM trained to generate complete lemma statements as well as previous fully symbolic conjecturing methods.
• Score: 4.583367875081881
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: Automatically conjecturing useful, interesting and novel lemmas would greatly improve automated reasoning tools and lower the bar for formalizing mathematics in proof assistants. It is however a very challenging task for both neural and symbolic approaches. We present the first steps towards a practical neuro-symbolic lemma conjecturing tool, Lemmanaid, that combines Large Language Models (LLMs) and symbolic methods, and evaluate it on proof libraries for the Isabelle proof assistant. We train an LLM to generate lemma templates that describe the shape of a lemma, and use symbolic methods to fill in the details. We compare Lemmanaid against an LLM trained to generate complete lemma statements as well as previous fully symbolic conjecturing methods. Our results indicate that neural and symbolic techniques are complementary. By leveraging the best of both symbolic and neural methods we can generate useful lemmas for a wide range of input domains, facilitating computer-assisted theory development and formalization.

Related papers

• Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning [27.562284768743694]
  Large language models (LLMs) can prove mathematical theorems formally by generating proof steps within a proof system.<n>We introduce a neuro-symbolic tactic generator that synergizes the mathematical intuition learned by LLMs with domain-specific insights encoded by symbolic methods.<n>We evaluate our framework on 161 challenging inequalities from multiple mathematics competitions.
  arXiv  Detail & Related papers  (2025-02-19T15:54:21Z)
• Advanced Weakly-Supervised Formula Exploration for Neuro-Symbolic Mathematical Reasoning [18.937801725778538]
  We propose an advanced practice for neuro-symbolic reasoning systems to explore the intermediate labels with weak supervision from problem inputs and final outputs.<n>Our experiments on the Mathematics dataset illustrated the effectiveness of our proposals from multiple aspects.
  arXiv  Detail & Related papers  (2025-02-02T02:34:36Z)
• Neuro-Symbolic Data Generation for Math Reasoning [47.00099724151703]
  We develop an automated method for generating high-quality, supervised mathematical datasets.<n>The method carefully mutates existing math problems, ensuring both diversity and validity of the newly generated problems.<n> Empirical experiments demonstrate the high quality of data generated by the proposed method, and that the LLMs, specifically LLaMA-2 and Mistral, surpass their state-of-the-art counterparts.
  arXiv  Detail & Related papers  (2024-12-06T08:49:49Z)
• Converging Paradigms: The Synergy of Symbolic and Connectionist AI in LLM-Empowered Autonomous Agents [55.63497537202751]
  Article explores the convergence of connectionist and symbolic artificial intelligence (AI) Traditionally, connectionist AI focuses on neural networks, while symbolic AI emphasizes symbolic representation and logic. Recent advancements in large language models (LLMs) highlight the potential of connectionist architectures in handling human language as a form of symbols.
  arXiv  Detail & Related papers  (2024-07-11T14:00:53Z)
• A Recursive Bateson-Inspired Model for the Generation of Semantic Formal Concepts from Spatial Sensory Data [77.34726150561087]
  This paper presents a new symbolic-only method for the generation of hierarchical concept structures from complex sensory data. The approach is based on Bateson's notion of difference as the key to the genesis of an idea or a concept. The model is able to produce fairly rich yet human-readable conceptual representations without training.
  arXiv  Detail & Related papers  (2023-07-16T15:59:13Z)
• Explainable AI Insights for Symbolic Computation: A case study on selecting the variable ordering for cylindrical algebraic decomposition [0.0]
  This paper explores whether using explainable AI (XAI) techniques on such machine learning models can offer new insight for symbolic computation. We present a case study on the use of ML to select the variable ordering for cylindrical algebraic decomposition.
  arXiv  Detail & Related papers  (2023-04-24T15:05:04Z)
• Neuro-Symbolic Learning of Answer Set Programs from Raw Data [54.56905063752427]
  Neuro-Symbolic AI aims to combine interpretability of symbolic techniques with the ability of deep learning to learn from raw data. We introduce Neuro-Symbolic Inductive Learner (NSIL), an approach that trains a general neural network to extract latent concepts from raw data. NSIL learns expressive knowledge, solves computationally complex problems, and achieves state-of-the-art performance in terms of accuracy and data efficiency.
  arXiv  Detail & Related papers  (2022-05-25T12:41:59Z)
• Closed Loop Neural-Symbolic Learning via Integrating Neural Perception, Grammar Parsing, and Symbolic Reasoning [134.77207192945053]
  Prior methods learn the neural-symbolic models using reinforcement learning approaches. We introduce the textbfgrammar model as a textitsymbolic prior to bridge neural perception and symbolic reasoning. We propose a novel textbfback-search algorithm which mimics the top-down human-like learning procedure to propagate the error.
  arXiv  Detail & Related papers  (2020-06-11T17:42:49Z)
• Formal Synthesis of Lyapunov Neural Networks [61.79595926825511]
  We propose an automatic and formally sound method for synthesising Lyapunov functions. We employ a counterexample-guided approach where a numerical learner and a symbolic verifier interact to construct provably correct Lyapunov neural networks. Our method synthesises Lyapunov functions faster and over wider spatial domains than the alternatives, yet providing stronger or equal guarantees.
  arXiv  Detail & Related papers  (2020-03-19T17:21: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.