Can LLM Aid in Solving Constraints with Inductive Definitions?

Weizhi Feng; Shidong Shen; Jiaxiang Liu; Taolue Chen; Fu Song; Zhilin Wu

cs.LOMar 4, 2026

Can LLM Aid in Solving Constraints with Inductive Definitions?

Authors: Weizhi Feng, Shidong Shen, Jiaxiang Liu, Taolue Chen, Fu Song, Zhilin Wu

Organizations: Key Laboratory of System Software (Chinese Academy of Sciences), Institute of Software, Chinese Academy of Sciences, Beijing, China · University of Chinese Academy of Sciences, Beijing, China · Birkbeck, University of London, United Kingdom · Nanjing Institute of Software Technology, Nanjing, China

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.

Figures & tables

Benchmark	Total	LLM4Ind		cvc5		Vampire		Racer
Benchmark	Total	<1200s	<360s	<1200s	<360s	<1200s	<360s	<1200s	<360s
StandardDT	241	212	200	150	150	160	160	N/A	N/A
StandardDTLIA	168	134	127	76	76	58	56	40	40
AutoProofBM	141	65	61	34	34	3	3	N/A	N/A
IndBen	156	114	104	34	34	122	118	N/A	N/A
Total	706	525	492	293	293	343	337	40	40

Table 1: Comparison with baseline SMT solvers

Benchmark	Qwen		DeepSeek		Gemini		GPT-5
Benchmark	LLM4Ind	Naive	LLM4Ind	Naive	LLM4Ind	Naive	LLM4Ind	Naive
StandardDT	212	160	206	153	206	155	212	180
StandardDTLIA	134	88	131	90	119	91	144	106
AutoProofBM	65	42	63	43	68	49	67	46
IndBen	114	89	121	79	126	76	129	118
Total	525	379	521	365	514	371	552	450

Table 2: Results of LLM4Ind using different LLMs and naive prompt strategy

Benchmark	W. filter				W.o. filter				Avg time (s)
Benchmark	R1	R2	R3	Avg	R1	R2	R3	Avg	W. filter	W.o. filter
StandardDT	212	211	207	210	204	203	209	205.3	83.91	67.26
StandardDTLIA	134	137	135	135.3	134	139	134	135.7	97.53	112.05
AutoProofBM	65	61	64	63.3	60	64	64	62.7	99.10	103.61
IndBen	114	111	111	112	113	106	111	110	168.92	178.64
Total	525	520	517	520.7	511	512	518	513.7	107.59	107.37

Table 3: Results of LLM4Ind with and without filter over three runs

Benchmark	T = 0.1			T = 0.5			T = 0.9			T = 1.3
Benchmark	R1	R2	R3	R1	R2	R3	R1	R2	R3	R1	R2	R3
StandardDT	211	206	210	207	209	207	212	211	207	208	209	210
StandardDTLIA	135	139	135	136	138	138	134	137	135	140	136	135
AutoProof	60	62	62	61	62	61	65	61	64	60	60	65
IndBen	114	108	114	110	107	113	114	111	111	119	113	112
Total	520	515	521	514	516	519	525	520	517	527	518	522

Table 4: Results of LLM4Ind with different sampling temperatures

Benchmark	Total	LLM4Ind -V		cvc5		Vampire		Racer
Benchmark	Total	<1200s	<360s	<1200s	<360s	<1200s	<360s	<1200s	<360s
StandardDT	241	214	206	150	150	160	160	N/A	N/A
StandardDTLIA	168	80	73	76	76	58	56	40	40
AutoProofBM	141	19	16	34	34	3	3	N/A	N/A
IndBen	156	140	140	34	34	122	118	N/A	N/A
Total	706	453	435	293	293	343	337	40	40

Table 5: Comparison with baseline SMT solvers (Vampire backend)

Appendix figures & tables1 asset

Supplementary material from the paper’s appendix.

Appendix

Automated Theorem Proving

Automated theorem proving develops algorithms and AI systems that construct or check formal proofs in mathematics, logic, and software.

See all 159 papers

Formalize, Don't Optimize: The Heuristic Trap in LLM-Generated Combinatorial Solvers
May 12, 2026Haoyu Wang, Yuliang Song, Tao Li +5Large Language Model-Guided Optimization LLM-Based Program Synthesis
University of Pennsylvania · University of Toronto · Google DeepMind +1
Hypothesis Frontier: Verifier Guided LLM and Symbolic Search for First-Order Induction
Aug 11, 2026Serafim BatzoglouSymbolic Reasoning LLM-Based Program Synthesis
Independent Researcher
ReaComp: Compiling LLM Reasoning into Symbolic Solvers for Efficient Program Synthesis
May 6, 2026Atharva Naik, Yash Mathur, Prakam +2Symbolic Reasoning LLM-Based Program Synthesis
Carnegie Mellon University · Independent Researcher

May 12, 2026J/K move · Enter open · S save

Formalize, Don't Optimize: The Heuristic Trap in LLM-Generated Combinatorial Solvers

Haoyu Wang, Yuliang Song, Tao Li, Zhiwei Deng+4

University of Pennsylvania · University of Toronto · Google DeepMind+1

Large Language Model-Guided Optimization LLM-Based Program Synthesis Combinatorial Optimization Natural Language to Optimization Modeling Constraint Programming

Open paper AskPDF arXiv

Large Language Models (LLMs) struggle to solve complex combinatorial problems through direct reasoning, so recent neuro-symbolic systems increasingly use them to synthesize executable solvers. A central design question is how the LLM should represent the solver, and whether it should also attempt to optimize search. We introduce CP-SynC-XL, a benchmark of 100 combinatorial problems (4,577 instances), and evaluate three solver-construction paradigms: native algorithmic search (Python), constraint modeling through a Python solver API (Python + OR-Tools), and declarative constraint modeling (MiniZinc + OR-Tools). We find a consistent representational divergence: Python + OR-Tools attains the highest correctness across LLMs, while MiniZinc + OR-Tools has lower absolute coverage despite using the same OR-Tools back-end. Native Python is the most likely to return a schema-valid solution that fails verification, whereas solver-backed paths preserve higher conditional fidelity. On the heuristic axis, prompting for search optimization yields only small median speed-ups (1.03-1.12x) and a strongly bimodal effect: many instances slow down, and correctness drops sharply on a long tail of problems. A paired code-level audit traces these regressions to a recurring heuristic trap. Under an efficiency-oriented prompt, the LLM may replace complete search with local approximations (Python), inject unverified bounds (Python + OR-Tools), or add redundant declarative machinery that overwhelms or over-constrains the model (MiniZinc + OR-Tools). These findings support a conservative design principle for LLM-generated combinatorial solvers: use the LLM primarily to formalize variables, constraints, and objectives for verified solvers, and separately check any LLM-authored search optimization before use.

Abstract

Automated Theorem Proving

Explore similar work

Formalize, Don't Optimize: The Heuristic Trap in LLM-Generated Combinatorial Solvers

Hypothesis Frontier: Verifier Guided LLM and Symbolic Search for First-Order Induction

ReaComp: Compiling LLM Reasoning into Symbolic Solvers for Efficient Program Synthesis