論文の概要: VeriPlan: Integrating Formal Verification and LLMs into End-User Planning

• arxiv url: http://arxiv.org/abs/2502.17898v1
• Date: Tue, 25 Feb 2025 06:53:00 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-02-26 15:21:35.194679
• Title: VeriPlan: Integrating Formal Verification and LLMs into End-User Planning
• Title（参考訳）: VeriPlan: 形式検証とLLMをエンドユーザ計画に統合する
• Authors: Christine Lee, David Porfirio, Xinyu Jessica Wang, Kevin Zhao, Bilge Mutlu,
• Abstract要約: 本稿では,エンドユーザープランニングにおけるLCMの信頼性と柔軟性を高めるために,形式的検証手法,特にモデルチェックを適用したVeriPlanを提案する。 本研究は,エンドユーザー計画タスクにおいて,形式検証とユーザ制御機能をLLMに効果的に統合することを示す。
• 参考スコア（独自算出の注目度）: 12.09421887596555
• License:
• Abstract: Automated planning is traditionally the domain of experts, utilized in fields like manufacturing and healthcare with the aid of expert planning tools. Recent advancements in LLMs have made planning more accessible to everyday users due to their potential to assist users with complex planning tasks. However, LLMs face several application challenges within end-user planning, including consistency, accuracy, and user trust issues. This paper introduces VeriPlan, a system that applies formal verification techniques, specifically model checking, to enhance the reliability and flexibility of LLMs for end-user planning. In addition to the LLM planner, VeriPlan includes three additional core features -- a rule translator, flexibility sliders, and a model checker -- that engage users in the verification process. Through a user study (n=12), we evaluate VeriPlan, demonstrating improvements in the perceived quality, usability, and user satisfaction of LLMs. Our work shows the effective integration of formal verification and user-control features with LLMs for end-user planning tasks.
• Abstract（参考訳）: 自動計画は伝統的に専門家の領域であり、製造や医療といった分野で専門家の計画ツールの助けを借りて利用される。 LLMの最近の進歩は、複雑な計画タスクをユーザを支援する可能性から、日々のユーザにとってプランニングがより使いやすくなっている。 しかし、LCMは、一貫性、正確性、ユーザ信頼の問題など、エンドユーザー計画におけるいくつかのアプリケーション課題に直面している。 本稿では,エンドユーザープランニングにおけるLCMの信頼性と柔軟性を高めるために,形式的検証手法,特にモデルチェックを適用したVeriPlanを提案する。 LLMプランナに加えて,VeriPlanには,3つのコア機能 – ルールトランスレータ,柔軟性スライダ,モデルチェッカ – が含まれている。 ユーザスタディ(n=12)を通じてVeriPlanを評価し,LLMの品質,ユーザビリティ,ユーザ満足度の向上を実証した。 本研究は,エンドユーザー計画タスクにおいて,形式検証とユーザ制御機能をLLMに効果的に統合することを示す。

関連論文リスト

• PlanGenLLMs: A Modern Survey of LLM Planning Capabilities [12.322175348741435]
  LLMは計画を生成する大きな可能性を秘めており、初期世界の状態を望ましい目標状態に変換する。 これらのシステムの多くは特定の問題に適応しており、それらを比較したり、新しいタスクに最適なアプローチを決定することは困難である。 我々の調査は、このギャップを埋めるために、現在のLLMプランナの概要を概観することを目的としている。 1990年、カルタムとウィルキンスによる基礎研究に基づいて、完全性、実行可能性、最適性、表現、一般化、効率の6つの重要な性能基準を検証した。
  論文  参考訳（メタデータ） (2025-02-16T17:54:57Z)
• Interactive and Expressive Code-Augmented Planning with Large Language Models [62.799579304821826]
  大きな言語モデル(LLM)は、常識的推論と対話的な意思決定において強力な能力を示す。 近年,制御フローなどのコード・アジャセント技術を用いてLCM出力を構造化し,計画性能を向上させる技術が提案されている。 完全コード表現で動的なLEM計画手法であるREPL-Planを提案する。
  論文  参考訳（メタデータ） (2024-11-21T04:23:17Z)
• Planning Anything with Rigor: General-Purpose Zero-Shot Planning with LLM-based Formalized Programming [13.246017517159043]
  大規模言語モデル(LLM)は近年,計画問題の解決に強い可能性を示している。 LLpreview は LLM を利用して,計画上の問題から重要な情報を抽出し,それらをスクラッチから最適化するフレームワークである。 GPToとClaude 3.5 Sonnetの9つのタスクに対して,LLが平均83.7%,86.8%の最適速度で達成できることを実証した。
  論文  参考訳（メタデータ） (2024-10-15T23:20:54Z)
• SELP: Generating Safe and Efficient Task Plans for Robot Agents with Large Language Models [24.22168861692322]
  等価投票、制約付き復号化、ドメイン固有の微調整という3つの重要な洞察を提示する。 等価投票は、複数の線形時間論理(LTL)式の生成とサンプリングによって一貫性を保証する。 制約付き復号法は生成された公式を使って計画の自動回帰推論を実行する。 ドメイン固有の微調整は、特定のタスクドメイン内で安全で効率的なプランを生成するために、LSMをカスタマイズする。
  論文  参考訳（メタデータ） (2024-09-28T22:33:44Z)
• Learning to Plan for Retrieval-Augmented Large Language Models from Knowledge Graphs [59.76268575344119]
  知識グラフ(KG)から得られた計画データを用いて,大規模言語モデル(LLM)計画能力を向上するための新しいフレームワークを提案する。 KGデータで微調整されたLLMは、計画能力を向上し、検索を含む複雑なQAタスクを処理するのがより適している。
  論文  参考訳（メタデータ） (2024-06-20T13:07:38Z)
• Exploring and Benchmarking the Planning Capabilities of Large Language Models [57.23454975238014]
  この研究は、大規模言語モデル(LLM)の計画能力を改善するための基礎を築いた。 我々は、古典的な計画ベンチマークと自然言語シナリオの両方を含む包括的なベンチマークスイートを構築した。 本研究は,LLM計画の強化を目的としたマルチショットインコンテキスト学習について検討し,文脈長の増大と計画性能の向上の関係について検討する。
  論文  参考訳（メタデータ） (2024-06-18T22:57:06Z)
• Ask-before-Plan: Proactive Language Agents for Real-World Planning [68.08024918064503]
  プロアクティブエージェントプランニングでは、ユーザエージェントの会話とエージェント環境のインタラクションに基づいて、言語エージェントが明確化のニーズを予測する必要がある。 本稿では,明確化,実行,計画の3つのエージェントからなる新しいマルチエージェントフレームワーク,Clarification-Execution-Planning(textttCEP)を提案する。
  論文  参考訳（メタデータ） (2024-06-18T14:07:28Z)
• Formal-LLM: Integrating Formal Language and Natural Language for Controllable LLM-based Agents [39.53593677934238]
  大規模言語モデル(LLM)により、AIエージェントは複雑なタスクを解決するためのマルチステッププランを自動的に生成し実行することができる。 しかし、現在のLLMベースのエージェントは、しばしば無効または実行不可能な計画を生成する。 本稿では、自然言語の表現性と形式言語の精度を統合することで、LLMをベースとしたエージェントのための新しい「フォーマルLLM」フレームワークを提案する。
  論文  参考訳（メタデータ） (2024-02-01T17:30:50Z)
• Small LLMs Are Weak Tool Learners: A Multi-LLM Agent [73.54562551341454]
  大規模言語モデル(LLM)エージェントはスタンドアロンのLLMの機能を大幅に拡張する。 本稿では、上記の機能をプランナー、呼び出し元、要約器に分解する新しい手法を提案する。 このモジュール化されたフレームワークは、個々の更新と、それぞれの機能を構築するための小さなLLMの潜在的な使用を容易にする。
  論文  参考訳（メタデータ） (2024-01-14T16:17:07Z)
• Learning to Plan with Natural Language [111.76828049344839]
  大規模言語モデル(LLM)は、様々な基本自然言語タスクにおいて顕著な性能を示している。 複雑なタスクを完了するためには、ステップごとに特定のソリューションを生成するためにLCMをガイドするタスクの計画が必要です。 本研究では,(1)第1学習課題計画フェーズにおいて,LCMが学習エラーフィードバックから導出するように促した新たなステップバイステップのソリューションと行動指示を用いてタスク計画を反復的に更新する,という2つの段階を含む学習計画手法を提案する。
  論文  参考訳（メタデータ） (2023-04-20T17:09:12Z)
• PlanBench: An Extensible Benchmark for Evaluating Large Language Models on Planning and Reasoning about Change [34.93870615625937]
  PlanBenchは、自動計画コミュニティで使用されるドメインの種類に基づいたベンチマークスイートである。 PlanBenchはタスクドメインと特定の計画機能の両方に十分な多様性を提供します。
  論文  参考訳（メタデータ） (2022-06-21T16:15:27Z)

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

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