論文の概要: Can LLM Aid in Solving Constraints with Inductive Definitions?
- arxiv url: http://arxiv.org/abs/2603.03668v2
- Date: Thu, 12 Mar 2026 08:30:51 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-03-13 14:46:25.401529
- Title: Can LLM Aid in Solving Constraints with Inductive Definitions?
- Title（参考訳）: LLMは帰納的定義による制約の解決に有効か?
- Authors: Weizhi Feng, Shidong Shen, Jiaxiang Liu, Taolue Chen, Fu Song, Zhilin Wu,
- Abstract要約: 本研究では,構造的プロンプトを利用して大規模言語モデル(LLM)を抽出し,帰納的定義の推論に必要な補助補題を生成する。
本稿では,LLMと制約解法を相乗的に統合するニューロシンボリックアプローチを提案する。
実験結果から,本手法は最先端のSMTおよびCHCソルバを改良し,帰納的定義を含む約25%の証明タスクを解くことができることがわかった。
- 参考スコア（独自算出の注目度）: 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.
- Abstract（参考訳）: 帰納的(あるいは再帰的)定義を含む制約を解決することは難しい。
最先端のSMT/CHCソルバと一階述語論理プロバーは、特に抽象データ型を含む場合、そのような制約を解決するための限定的なサポートしか提供しない。
本研究では,構造化プロンプトを利用して大規模言語モデル(LLM)を抽出し,これらの帰納的定義を推論するために必要な補助補題を生成する。
さらに,LLMを制約解法と相乗的に統合するニューロシンボリックアプローチを提案し,LLMは予測を反復的に生成し,解法は目標を証明するための妥当性と有用性を確認する。
本稿では,代用データ型と再帰関係に基づく制約を含む多種多様なベンチマークスイートに対するアプローチを評価する。
実験結果から,本手法は最先端のSMTとCHCの解法を改良し,帰納的定義を含む約25%の証明タスクを解き,その有効性を示した。
関連論文リスト
- Matrix as Plan: Structured Logical Reasoning with Feedback-Driven Replanning [9.431480849387595]
Chain-of-Thoughtプロンプトは、Large Language Models(LLMs)の推論能力を高めることが示されている。
ニューロシンボリック法は、外部の解法を通して形式的正しさを強制することによって、このギャップに対処する。
行列ベースの計画を持つ構造化CoTフレームワークであるMatrixCoTを提案する。
論文 参考訳（メタデータ） (2026-01-15T06:12:00Z) - LLM-Guided Quantified SMT Solving over Uninterpreted Functions [10.767268261124515]
非線形実算術上の非解釈関数 (UF) の量子式は、Satifiability Modulo Theories (SMT) の解法に根本的な課題をもたらす。
本稿では,UFインスタンス化のセマンティックガイダンスを提供するために,大規模言語モデルを活用するフレームワークであるAquaForteを紹介する。
提案手法は,制約分離によって計算式を前処理し,構造化プロンプトを用いてLLMから数学的推論を抽出し,従来のSMTアルゴリズムと統合する。
論文 参考訳（メタデータ） (2026-01-08T07:40:37Z) - Syzygy of Thoughts: Improving LLM CoT with the Minimal Free Resolution [59.39066657300045]
CoT(Chain-of-Thought)は、問題を逐次ステップに分解することで、大きな言語モデル(LLM)の推論を促進する。
思考のシジー(Syzygy of Thoughts, SoT)は,CoTを補助的,相互関連的な推論経路を導入して拡張する新しいフレームワークである。
SoTはより深い論理的依存関係をキャプチャし、より堅牢で構造化された問題解決を可能にする。
論文 参考訳（メタデータ） (2025-04-13T13:35:41Z) - InductionBench: LLMs Fail in the Simplest Complexity Class [53.70978746199222]
大規模言語モデル(LLM)は推論において顕著に改善されている。
帰納的推論(inductive reasoning)は、観測されたデータから基礎となるルールを推測するものであり、まだ探索されていない。
本稿では, LLMの帰納的推論能力を評価するための新しいベンチマークであるインジェクションベンチを紹介する。
論文 参考訳（メタデータ） (2025-02-20T03:48:00Z) - Argumentation Computation with Large Language Models : A Benchmark Study [6.0682923348298194]
大規模言語モデル(LLM)は、ニューロシンボリックコンピューティングにおいて大きな進歩を遂げた。
我々は,様々な抽象的論証セマンティクスの拡張を決定する上でのLLMの能力を検討することを目的とする。
論文 参考訳（メタデータ） (2024-12-21T18:23:06Z) - Distilling Algorithmic Reasoning from LLMs via Explaining Solution Programs [2.3020018305241337]
大きな言語モデルの推論能力を改善する効果的な方法として、明確な推論経路を蒸留する手法が登場している。
本稿では, LLM から推論能力を抽出する手法を提案する。
提案実験は,ReasonerがCoderによるプログラム実装をより効果的にガイドできることを示す。
論文 参考訳（メタデータ） (2024-04-11T22:19:50Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。