用大模型辅助证明递归定义约束，提升求解成功率约25%。
Can LLM Aid in Solving Constraints with Inductive Definitions?
- 通过结构化提示让大模型生成推理所需的辅助命题
- 在代数数据类型和递推关系上使求解率提升约25%
- 适合需要形式化验证的程序分析与自动推理研究者
涉及归纳（即递归）定义的约束求解极具挑战性。当前最先进的SMT/CHC求解器和一阶逻辑证明器对这类约束支持有限，尤其在处理抽象数据类型时。本文提出一种神经符号方法：利用结构化提示引导大语言模型（LLM）生成辅助引理，用于推理归纳定义；同时设计迭代机制，由大模型生成猜想，约束求解器验证其有效性与助益性。我们在涵盖代数数据类型与递推关系的多样化基准集上评估该方法，实验结果表明，相比现有方法，本方案显著提升了状态机求解器的表现，在涉及归纳定义的证明任务中多解决约25%的问题，验证了其有效性。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。