# Can LLM Aid in Solving Constraints with Inductive Definitions?

arXiv: https://arxiv.org/abs/2603.03668 · HTML: https://mlsanity.com/paper/2603.03668/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 23 of its 58 references that are in the map.
- First posted on arXiv 4 Mar 2026.

## Builds on (most cited first, 23 of 23)

- [DeepSeek-Coder: When the Large Language Model Meets Programming -- The Rise of Code Intelligence](https://mlsanity.com/paper/2401.14196/) (2024)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [Hilbert: Recursively Building Formal Proofs with Informal Reasoning](https://mlsanity.com/paper/2509.22819/) (2025)
- [Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification](https://mlsanity.com/paper/2404.00762/) (2024)
- [Verus: Verifying Rust Programs using Linear Ghost Types (extended version)](https://mlsanity.com/paper/2303.05491/) (2023)
- [SpecGen: Automated Generation of Formal Program Specifications via Large Language Models](https://mlsanity.com/paper/2401.08807/) (2024)
- [AutoVerus: Automated Proof Generation for Rust Code](https://mlsanity.com/paper/2409.13082/) (2024)
- [Exploring the Impact of Temperature on Large Language Models:Hot or Cold?](https://mlsanity.com/paper/2506.07295/) (2025)
- [Chain-of-Thought in Neural Code Generation: From and For Lightweight Language Models](https://mlsanity.com/paper/2312.05562/) (2023)
- [SMT-based Model Checking for Recursive Programs](https://mlsanity.com/paper/1405.4028/) (2014)
- [Don't Complete It! Preventing Unhelpful Code Completion for Productive and Sustainable Neural Code Completion Systems](https://mlsanity.com/paper/2209.05948/) (2022)
- [When Neural Code Completion Models Size up the Situation: Attaining Cheaper and Faster Completion through Dynamic Model Inference](https://mlsanity.com/paper/2401.09964/) (2024)
- [Leveraging Large Language Models to Boost Dafny's Developers Productivity](https://mlsanity.com/paper/2401.00963/) (2024)
- [Mining Math Conjectures from LLMs: A Pruning Approach](https://mlsanity.com/paper/2412.16177/) (2024)
- [System FR as Foundations for Stainless](https://mlsanity.com/paper/1904.03482/) (2019)
- [Theory Exploration Powered By Deductive Synthesis](https://mlsanity.com/paper/2009.04826/) (2020)
- [LLM-Guided Quantified SMT Solving over Uninterpreted Functions](https://mlsanity.com/paper/2601.04675/) (2026)
- [Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates](https://mlsanity.com/paper/2004.07749/) (2020)
- [Formalizing Graph Trail Properties in Isabelle/HOL](https://mlsanity.com/paper/2103.03607/) (2021)
- [Solving Horn Clauses on Inductive Data Types Without Induction](https://mlsanity.com/paper/1804.09007/) (2018)
- [Proving Functional Program Equivalence via Directed Lemma Synthesis](https://mlsanity.com/paper/2405.11535/) (2024)
- [Large Lemma Miners: Can LLMs do Induction Proofs for Hardware?](https://mlsanity.com/paper/2511.02521/) (2025)

## Built on by (most cited first, 1 of 1)

- [Schwarz: Solver-Aware Agentic Program Verification](https://mlsanity.com/paper/2608.30803/) (2026)

## Abstract (arXiv)

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.