Can LLM Aid in Solving Constraints with Inductive Definitions?
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2026
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866914387406618624 |
|---|---|
| author | Feng, Weizhi Shen, Shidong Liu, Jiaxiang Chen, Taolue Song, Fu Wu, Zhilin |
| author_facet | Feng, Weizhi Shen, Shidong Liu, Jiaxiang Chen, Taolue Song, Fu Wu, Zhilin |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_03668 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Can LLM Aid in Solving Constraints with Inductive Definitions? Feng, Weizhi Shen, Shidong Liu, Jiaxiang Chen, Taolue Song, Fu Wu, Zhilin Logic in Computer Science Artificial Intelligence 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. |
| title | Can LLM Aid in Solving Constraints with Inductive Definitions? |
| topic | Logic in Computer Science Artificial Intelligence |
| url | https://arxiv.org/abs/2603.03668 |