論文の概要: Provably Complete Generalized Planning with LLMs

• arxiv url: http://arxiv.org/abs/2609.27105v1
• Date: Tue, 22 Sep 2026 22:02:16 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-25 00:05:17.78658
• Title: Provably Complete Generalized Planning with LLMs
• Title（参考訳）: LLMによる多分完全汎用計画
• Abstract要約: 汎用プランニングは、計画ドメインのすべてのインスタンスを解決する計画を計算することを目的としている。 最近の研究では、そのような一般化された計画の自動生成とデバッグにLLMを使用している。 リーンにおける一般化計画の自動生成と,その相対的完全性を証明するためのアプローチを提案する。
• 参考スコア（独自算出の注目度）: 51.68151545319816
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Generalized planning aims to compute a plan that solves all instances of a planning domain. Recent work has used LLMs to automatically generate and debug such generalized plans in the form of Python programs and achieved perfect test data coverage for several domains. However, whether these generalized plans are actually complete, i.e. solve all instances of the domain, could only be determined by manual evaluation. Here, we present an approach for automatically generating generalized plans in Lean together with proofs of their completeness relative to a specification of the domain constraints provided as input. We introduce a semantic-preserving PDDL-to-Lean conversion, and use an LLM to generate both the generalized plan and the formal proof that it solves every instance satisfying the domain constraints. The correctness of the completeness proof is determined by Lean's kernel. We evaluate our approach on 13 commonly used benchmark domains, using GPT-5.6-Sol as the LLM. For 12 of the domains we obtain generalized plans together with valid completeness proofs. This is a major advancement of the state of the art in automatic generalized-plan completeness proofs.
• Abstract（参考訳）: 汎用プランニングは、計画ドメインのすべてのインスタンスを解決する計画を計算することを目的としている。 最近の研究では、LLMを使用して、Pythonプログラムの形式でそのような一般化された計画を自動的に生成し、デバッグし、いくつかのドメインで完全なテストデータカバレッジを達成した。 しかし、これらの一般化された計画が実際に完備であるかどうか、すなわち、ドメインのすべてのインスタンスを解くことは、手動による評価によってのみ決定できる。 本稿では、入力として提供されるドメイン制約の仕様に対して、その完全性を証明するとともに、リーンで一般化された計画を自動的に生成するアプローチを提案する。 意味保存型PDDL-to-Lean変換を導入し、LLMを用いて一般化計画とドメイン制約を満たす全てのインスタンスを解く形式的証明を生成する。 完全性証明の正確性は、Leanのカーネルによって決定されます。 GPT-5.6-Sol を LLM として用いた13のベンチマーク領域に対するアプローチを評価する。 12の領域に対して、一般化された計画と有効な完全性証明を得る。 これは、自動一般化計画完全性証明における最先端の進歩である。

関連論文リスト

• On the Generalization Gap in LLM Planning: Tests and Verifier-Reward RL [2.3553294445398567]
  細調整された大規模言語モデル(LLM)は、PDDL計画タスクにおいて、高い有効計画記憶率を達成することができる。 しかし、これが移行可能な計画能力やドメイン固有の一般化を反映しているかどうかは不明だ。
  論文  参考訳（メタデータ） (2026-01-20T20:25:37Z)
• An End-to-end Planning Framework with Agentic LLMs and PDDL [9.718390674899771]
  検証者によって支援される計画のためのエンドツーエンドのフレームワークを提案する。 オーケストレータは、自然言語で書かれた人間の仕様を受け取り、PDDLモデルに変換する。 検証済みのドメインと問題は、計画を生成するために外部の計画エンジンに渡される。
  論文  参考訳（メタデータ） (2025-12-10T13:17:08Z)
• Improved Generalized Planning with LLMs through Strategy Refinement and Reflection [58.79806530685551]
  疑似コードの形で戦略を生成する手法を提案する。 我々は、Pythonデバッグフェーズをリフレクションステップで拡張し、LLMが観測された計画失敗の理由を特定できるようにする。 17のベンチマーク領域で実験を行い、これらの拡張によって一般化された計画の品質が大幅に向上することを示した。
  論文  参考訳（メタデータ） (2025-08-19T14:42:18Z)
• Classical Planning with LLM-Generated Heuristics: Challenging the State of the Art with Python Code [6.88204255655161]
  大規模言語モデル(LLM)は、計画タスクの詳細な定義を伴っても、確実に計画に失敗する。 サイズが大きくなるような配布外タスクであっても、LCMを使って正確な計画を生成する方法を示す。
  論文  参考訳（メタデータ） (2025-03-24T15:50:20Z)
• LLM-Generated Heuristics for AI Planning: Do We Even Need Domain-Independence Anymore? [87.71321254733384]
  大規模言語モデル(LLM)は、特定の計画問題に適した計画手法を生成することができる。 LLMは、いくつかの標準IPCドメインで最先端のパフォーマンスを達成することができる。 これらの結果がパラダイムシフトを意味するのか、既存の計画手法をどのように補完するかについて議論する。
  論文  参考訳（メタデータ） (2025-01-30T22:21:12Z)
• Generalized Planning in PDDL Domains with Pretrained Large Language Models [82.24479434984426]
  PDDLドメインを考慮し、GPT-4を用いてPythonプログラムを合成する。 7つのPDDLドメインでこのアプローチを評価し、4つのアブレーションと4つのベースラインと比較した。
  論文  参考訳（メタデータ） (2023-05-18T14:48:20Z)

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

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