Can LLM Aid in Solving Constraints with Inductive Definitions?

• URL: http://arxiv.org/abs/2603.03668v2
• Date: Thu, 12 Mar 2026 08:30:51 GMT
• Title: Can LLM Aid in Solving Constraints with Inductive Definitions?
• Abstract summary: In this work, we leverage structured prompts to elicit Large Language Models (LLMs) to generate auxiliary lemmas that are necessary for reasoning about inductive definitions.<n>We propose a neuro-symbolic approach, which synergistically integrates LLMs with constraint solvers, while the solver checks their validity and usefulness for proving the goal.<n>The experimental results show that our approach can improve the state-of-the-art SMT and CHC solvers, solving considerably more (around 25%) proof tasks involving inductive definitions.
• Score: 6.956961686269943
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Solving constraints involving inductive (aka recursive) definitions is challenging. State-of-the-art SMT/CHC solvers and first-order logic provers provide only limited support for solving such constraints, especially when they involve, e.g., abstract data types. In this work, we leverage structured prompts to elicit Large Language Models (LLMs) to generate auxiliary lemmas that are necessary for reasoning about these inductive definitions. We further propose a neuro-symbolic approach, which synergistically integrates LLMs with constraint solvers: the LLM iteratively generates conjectures, while the solver checks their validity and usefulness for proving the goal. We evaluate our approach on a diverse benchmark suite comprising constraints originating from algebrai data types and recurrence relations. The experimental results show that our approach can improve the state-of-the-art SMT and CHC solvers, solving considerably more (around 25%) proof tasks involving inductive definitions, demonstrating its efficacy.

Related papers

• HintMR: Eliciting Stronger Mathematical Reasoning in Small Language Models [10.405512438256467]
  Small language models (SLMs) often struggle with complex mathematical reasoning.<n>We introduce a hint-assisted reasoning framework that incrementally guides SLMs through multi-step mathematical problem solving.
  arXiv  Detail & Related papers  (2026-04-14T03:09:26Z)
• On the Paradoxical Interference between Instruction-Following and Task Solving [50.75960598434753]
  Instruction following aims to align Large Language Models (LLMs) with human intent by specifying explicit constraints on how tasks should be performed.<n>We reveal a counterintuitive phenomenon: instruction following can paradoxically interfere with LLMs' task-solving capability.<n>We propose a metric, SUSTAINSCORE, to quantify the interference of instruction following with task solving.
  arXiv  Detail & Related papers  (2026-01-29T17:48:56Z)
• Matrix as Plan: Structured Logical Reasoning with Feedback-Driven Replanning [9.431480849387595]
  Chain-of-Thought prompting has been shown to enhance the reasoning capabilities of Large Language Models (LLMs)<n>Neuro-symbolic methods address this gap by enforcing formal correctness through external solvers.<n>We propose MatrixCoT, a structured CoT framework with a matrix-based plan.
  arXiv  Detail & Related papers  (2026-01-15T06:12:00Z)
• LLM-Guided Quantified SMT Solving over Uninterpreted Functions [10.767268261124515]
  Quantified formulas with Uninterpreted Functions (UFs) over non-linear real arithmetic pose fundamental challenges for Satisfiability Modulo Theories (SMT) solving.<n>We present AquaForte, a framework that leverages Large Language Models to provide semantic guidance for UF instantiation.<n>Our approach preprocesses formulas through constraint separation, uses structured prompts to extract mathematical reasoning from LLMs, and integrates the results with traditional SMT algorithms.
  arXiv  Detail & Related papers  (2026-01-08T07:40:37Z)
• Computational Thinking Reasoning in Large Language Models [69.28428524878885]
  Computational Thinking Model (CTM) is a novel framework that incorporates computational thinking paradigms into large language models (LLMs)<n>Live code execution is seamlessly integrated into the reasoning process, allowing CTM to think by computing.<n>CTM outperforms conventional reasoning models and tool-augmented baselines in terms of accuracy, interpretability, and generalizability.
  arXiv  Detail & Related papers  (2025-06-03T09:11:15Z)
• Syzygy of Thoughts: Improving LLM CoT with the Minimal Free Resolution [59.39066657300045]
  Chain-of-Thought (CoT) prompting enhances the reasoning of large language models (LLMs) by decomposing problems into sequential steps.<n>We propose Syzygy of Thoughts (SoT)-a novel framework that extends CoT by introducing auxiliary, interrelated reasoning paths.<n>SoT captures deeper logical dependencies, enabling more robust and structured problem-solving.
  arXiv  Detail & Related papers  (2025-04-13T13:35:41Z)
• The Curse of CoT: On the Limitations of Chain-of-Thought in In-Context Learning [56.574829311863446]
  Chain-of-Thought (CoT) prompting has been widely recognized for its ability to enhance reasoning capabilities in large language models (LLMs)<n>We demonstrate that CoT and its reasoning variants consistently underperform direct answering across varying model scales and benchmark complexities.<n>Our analysis uncovers a fundamental hybrid mechanism of explicit-implicit reasoning driving CoT's performance in pattern-based ICL.
  arXiv  Detail & Related papers  (2025-04-07T13:51:06Z)
• InductionBench: LLMs Fail in the Simplest Complexity Class [53.70978746199222]
  Large language models (LLMs) have shown remarkable improvements in reasoning.<n>Inductive reasoning, where one infers the underlying rules from observed data, remains less explored.<n>We introduce InductionBench, a new benchmark designed to evaluate the inductive reasoning ability of LLMs.
  arXiv  Detail & Related papers  (2025-02-20T03:48:00Z)
• Argumentation Computation with Large Language Models : A Benchmark Study [6.0682923348298194]
  Large language models (LLMs) have made significant advancements in neuro-symbolic computing.<n>We aim to investigate the capability of LLMs in determining the extensions of various abstract argumentation semantics.
  arXiv  Detail & Related papers  (2024-12-21T18:23:06Z)
• Distilling Algorithmic Reasoning from LLMs via Explaining Solution Programs [2.3020018305241337]
  Distilling explicit chain-of-thought reasoning paths has emerged as an effective method for improving the reasoning abilities of large language models. We propose a novel approach to distill reasoning abilities from LLMs by leveraging their capacity to explain solutions. Our experiments demonstrate that learning from explanations enables the Reasoner to more effectively guide program implementation by a Coder.
  arXiv  Detail & Related papers  (2024-04-11T22:19:50Z)
• Enhancing Chain-of-Thoughts Prompting with Iterative Bootstrapping in Large Language Models [81.01397924280612]
  Large language models (LLMs) can achieve highly effective performance on various reasoning tasks by incorporating step-by-step chain-of-thought (CoT) prompting as demonstrations. We introduce Iter-CoT (Iterative bootstrapping in Chain-of-Thoughts Prompting), an iterative bootstrapping approach for selecting exemplars and generating reasoning chains.
  arXiv  Detail & Related papers  (2023-04-23T13:54:39Z)

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.