形式証明付きの汎用計画を大規模言語モデルで生成
Provably Complete Generalized Planning with LLMs
この論文をやさしく読む
ひとことで言うと
LLM が作った汎用計画について、与えられた条件を満たすすべての問題を解けることを Lean で検証する方法。
何に役立つ？
計画プログラムのテスト成功だけでは分からない完全性を、形式的に確かめる手段になる。13のベンチマーク領域のうち12で証明が得られた。
この研究の面白いところ
LLM に計画だけでなく証明も生成させ、最終的な正しさは Lean のカーネルがチェックする。
どこまで分かった？
完全性は入力として与えた領域制約の仕様に対するものであり、13領域すべてで証明が得られたわけではない。
v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。
アブストラクトの日本語訳
汎用計画は、ある計画問題の領域に属するすべての事例を解く計画を求める。近年、大規模言語モデル LLM で Python プログラムとして汎用計画を自動生成・修正し、複数の領域でテストデータをすべて解けた例がある。しかし、その計画が実際に領域内のすべての事例を解くという完全性は、手動評価でしか判定できなかった。本研究は、入力された領域制約の仕様に対する完全性の証明とともに、Lean で汎用計画を自動生成する方法を示す。意味を保つ PDDL から Lean への変換を導入し、LLM に、汎用計画と、領域制約を満たすすべての事例をその計画が解くという形式的証明の両方を生成させる。完全性の証明が正しいかどうかは Lean のカーネルが判定する。LLM として GPT-5.6-Sol を使い、よく使われる13のベンチマーク領域で評価したところ、12領域では汎用計画と有効な完全性証明を得た。これは汎用計画の完全性を自動で証明する手法の進展である。
v1の要旨から自動生成。本文の精読・人による確認は未実施。
- 初稿
- 2026-09-22（UTC）
- 最新改訂
- 2026-09-22 · v1
- 査読・掲載
- 査読状況未確認
更新履歴
- v1 2026-09-22 この版を読む
取得できた版を表示。版の更新は査読済みを意味しません。過去版の本文差分は未解析です。
原文の要旨
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.
arXiv ID: 2609.27105 ／ 要約の誤りについて