論文の概要: 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は帰納的定義による制約の解決に有効か?
• 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%の証明タスクを解き,その有効性を示した。

関連論文リスト

• HintMR: Eliciting Stronger Mathematical Reasoning in Small Language Models [10.405512438256467]
  小型言語モデル(SLM)は複雑な数学的推論に苦しむことが多い。 我々は,多段階の数学的問題解決を通じてSLMを段階的にガイドするヒント支援推論フレームワークを導入する。
  論文  参考訳（メタデータ） (2026-04-14T03:09:26Z)
• On the Paradoxical Interference between Instruction-Following and Task Solving [50.75960598434753]
  次の命令は、大規模言語モデル(LLM)を、タスクの実行方法に関する明示的な制約を指定することで、人間の意図と整合させることを目的としている。 我々は,LLMのタスク解決能力にパラドックス的に干渉する命令に従うという,直感に反する現象を明らかにした。 本稿では,タスク解決に追従する命令の干渉を定量化する指標として,SUSTAINSCOREを提案する。
  論文  参考訳（メタデータ） (2026-01-29T17:48:56Z)
• 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)
• Computational Thinking Reasoning in Large Language Models [69.28428524878885]
  計算思考モデル(CTM)は、計算思考パラダイムを大規模言語モデル(LLM)に組み込んだ新しいフレームワークである。 ライブコード実行は推論プロセスにシームレスに統合され、CTMが計算によって考えることができる。 CTMは、精度、解釈可能性、一般化可能性の観点から、従来の推論モデルとツール拡張ベースラインを上回っている。
  論文  参考訳（メタデータ） (2025-06-03T09:11:15Z)
• 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)
• The Curse of CoT: On the Limitations of Chain-of-Thought in In-Context Learning [56.574829311863446]
  CoT(Chain-of-Thought)プロンプトは,大規模言語モデル(LLM)における推論能力の向上によって広く認識されている。 我々は、CoTとその推論変異が、様々なモデルスケールやベンチマークの複雑さに対して、直接応答を一貫して過小評価していることを実証する。 パターンベースICLにおけるCoTの性能を駆動する明示的単純推論の基本的なハイブリッド機構を明らかにする。
  論文  参考訳（メタデータ） (2025-04-07T13:51:06Z)
• 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)
• Enhancing Chain-of-Thoughts Prompting with Iterative Bootstrapping in Large Language Models [81.01397924280612]
  大規模言語モデル (LLM) は、ステップ・バイ・ステップ・チェーン・オブ・シークレット (CoT) をデモンストレーションとして組み込むことで、様々な推論タスクにおいて高い効果的な性能を達成することができる。 本稿では,イターCoT (Iterative bootstrapping in Chain-of-Thoughts Prompting) を導入する。
  論文  参考訳（メタデータ） (2023-04-23T13:54:39Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。