Large Language Models Can Solve Real-World Planning Rigorously with Formal Verification Tools

要約

大規模な言語モデル（LLMS）は、自己検証や自己批判でさえ、複雑なマルチコンストレント計画の問題の正しい計画を直接生成するのに苦労しています。
たとえば、Xie et al。
（2024）、最高のLLM Openai O1-Previewでは、必要なすべての情報を考慮して10％の成功率で実行可能な旅行計画のみを見つけることができます。
この作業では、複雑なマルチコンストレント計画の問題を制約された満足度の問題として形式化および解決するLLMベースの計画フレームワークを提案することにより、これに取り組みます。
TravelPlannerから主要なユースケースとして始め、私たちのフレームワークの成功率は93.9％を達成し、多様な言い換えプロンプトで効果的であることを示しています。
さらに重要なことは、私たちのフレームワークには強力なゼロショットの一般化可能性があり、新しく作成された目に見えない国際旅行データセットで目に見えない制約をうまく処理し、新しい根本的に異なるドメインによく一般化することです。
さらに、ユーザーの入力クエリが実行不可能である場合、当社のフレームワークは、不満のコアを識別し、障害の理由を提供し、パーソナライズされた修正の提案を提供できます。
私たちのフレームワークは、2つのデータセットからの平均81.6％と91.7％の満足不可能なクエリを修正および解決し、フレームワークのすべての重要なコンポーネントが効果的かつ必要であることを証明できることを示します。
プロジェクトページ：https：//sites.google.com/view/llm-rwplanning。

要約(オリジナル)

Large Language Models (LLMs) struggle to directly generate correct plans for complex multi-constraint planning problems, even with self-verification and self-critique. For example, a U.S. domestic travel planning benchmark TravelPlanner was proposed in Xie et al. (2024), where the best LLM OpenAI o1-preview can only find viable travel plans with a 10% success rate given all needed information. In this work, we tackle this by proposing an LLM-based planning framework that formalizes and solves complex multi-constraint planning problems as constrained satisfiability problems, which are further consumed by sound and complete satisfiability solvers. We start with TravelPlanner as the primary use case and show that our framework achieves a success rate of 93.9% and is effective with diverse paraphrased prompts. More importantly, our framework has strong zero-shot generalizability, successfully handling unseen constraints in our newly created unseen international travel dataset and generalizing well to new fundamentally different domains. Moreover, when user input queries are infeasible, our framework can identify the unsatisfiable core, provide failure reasons, and offers personalized modification suggestions. We show that our framework can modify and solve for an average of 81.6% and 91.7% unsatisfiable queries from two datasets and prove with ablations that all key components of our framework are effective and necessary. Project page: https://sites.google.com/view/llm-rwplanning.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google