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
• 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

• LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
  Large Language Models (LLMs) exhibit strong informal mathematical reasoning but struggle to generate verifiable proofs in formal languages like Lean.<n>We present LEAP, an agentic framework that enables general-purpose foundation models to achieve state-of-the-art performance on automated formal theorem proving.
  arXiv  Detail & Related papers  (2026-06-02T08:16:42Z)
• On Improving Neurosymbolic Learning by Exploiting the Representation Space [54.16389421332958]
  We study the problem of learning neural classifiers in a neurosymbolic setting where the hidden gold labels of input instances must satisfy a logical formula.<n>One challenge is that the space of label combinations can grow exponentially, making learning difficult.<n>We propose a technique that prunes this space by exploiting the intuition that instances with similar latent representations are likely to share the same label.
  arXiv  Detail & Related papers  (2026-02-08T13:56:47Z)
• MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics [51.65118519899584]
  We introduce MathlibLemma, the first LLM-based multi-agent system to automate the discovery and formalization of mathematical folklore lemmas.<n>We further construct the MathlibLemma benchmark, a suite of 4,028 type-checked Lean statements spanning a broad range of mathematical domains.
  arXiv  Detail & Related papers  (2026-01-30T15:24:42Z)
• SciML Agents: Write the Solver, Not the Solution [69.5021018644143]
  We introduce two new datasets: a diagnostic dataset of adversarial "misleading" problems; and a large-scale benchmark of 1,000 diverse ODE tasks.<n>We evaluate open- and closed-source LLM models along two axes: (i) unguided versus guided prompting with domain-specific knowledge; and (ii) off-the-shelf versus fine-tuned variants.<n>Preliminary results indicate that careful prompting and fine-tuning can yield a specialized LLM agent capable of reliably solving simple ODE problems.
  arXiv  Detail & Related papers  (2025-09-12T02:53:57Z)
• Towards Reliable Proof Generation with LLMs: A Neuro-Symbolic Approach [14.213719696233934]
  Large language models (LLMs) struggle with formal domains that require rigorous logical deduction and symbolic reasoning.<n>We propose a neuro-symbolic approach that combines LLMs' generative strengths with structured components to overcome this challenge.
  arXiv  Detail & Related papers  (2025-05-20T15:13:32Z)
• 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)
• MathFimer: Enhancing Mathematical Reasoning by Expanding Reasoning Steps through Fill-in-the-Middle Task [49.355810887265925]
  We introduce MathFimer, a novel framework for mathematical reasoning step expansion.<n>We develop a specialized model, MathFimer-7B, on our carefully curated NuminaMath-FIM dataset.<n>We then apply these models to enhance existing mathematical reasoning datasets by inserting detailed intermediate steps into their solution chains.
  arXiv  Detail & Related papers  (2025-02-17T11:22:24Z)
• Token Assorted: Mixing Latent and Text Tokens for Improved Language Model Reasoning [44.84219266082269]
  Large Language Models (LLMs) excel at reasoning and planning when trained on chainof-thought (CoT) data.<n>We propose a hybrid representation of the reasoning process, where we partially abstract away the initial reasoning steps using latent discrete tokens.
  arXiv  Detail & Related papers  (2025-02-05T15:33:00Z)
• 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)
• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
  Logical reasoning is an important task for artificial intelligence with potential impacts on science, mathematics, and society. In this work, we reformulating such tasks as modular neurosymbolic programming, which we call LINC. We observe significant performance gains on FOLIO and a balanced subset of ProofWriter for three different models in nearly all experimental conditions we evaluate.
  arXiv  Detail & Related papers  (2023-10-23T17:58:40Z)
• 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.