論文の概要: Joint Verification and Refinement of Language Models for Safety-Constrained Planning

• arxiv url: http://arxiv.org/abs/2410.14865v1
• Date: Fri, 18 Oct 2024 21:16:30 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-11-28 17:07:37.746146
• Title: Joint Verification and Refinement of Language Models for Safety-Constrained Planning
• Title（参考訳）: 安全制約計画のための言語モデルの連立検証と再定義
• Authors: Yunhao Yang, William Ward, Zichao Hu, Joydeep Biswas, Ufuk Topcu,
• Abstract要約: 本研究では,実行可能計画を生成する手法を開発し,タスク関連安全仕様に対して正式に検証する。 自然言語で高レベルなタスク記述が与えられた場合、提案手法は言語モデルに問い合わせ、実行可能なロボットプログラムの形式で計画を生成する。 その後、生成されたプランをオートマトンベースの表現に変換し、仕様に対するオートマトンの公式な検証を可能にする。
• 参考スコア（独自算出の注目度）: 21.95203475140736
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Although pre-trained language models can generate executable plans (e.g., programmatic policies) for solving robot tasks, the generated plans may violate task-relevant logical specifications due to the models' black-box nature. A significant gap remains between the language models' outputs and verifiable executions of plans. We develop a method to generate executable plans and formally verify them against task-relevant safety specifications. Given a high-level task description in natural language, the proposed method queries a language model to generate plans in the form of executable robot programs. It then converts the generated plan into an automaton-based representation, allowing formal verification of the automaton against the specifications. We prove that given a set of verified plans, the composition of these plans also satisfies the safety specifications. This proof ensures the safety of complex, multi-component plans, obviating the computation complexity of verifying the composed plan. We then propose an automated fine-tuning process that refines the language model to generate specification-compliant plans without the need for human labeling. The empirical results show a 30 percent improvement in the probability of generating plans that meet task specifications after fine-tuning.
• Abstract（参考訳）: 事前訓練された言語モデルは、ロボットタスクを解くための実行可能な計画(例えばプログラムポリシー)を生成することができるが、生成した計画は、ブラックボックスの性質のため、タスク関連論理仕様に違反する可能性がある。 言語モデルの出力と計画の実行検証の間には、大きなギャップが残っている。 本研究では,実行可能計画を生成する手法を開発し,タスク関連安全仕様に対して正式に検証する。 自然言語で高レベルなタスク記述が与えられた場合、提案手法は言語モデルに問い合わせ、実行可能なロボットプログラムの形式で計画を生成する。 その後、生成されたプランをオートマトンベースの表現に変換し、仕様に対するオートマトンの公式な検証を可能にする。 検証済みの一連の計画を考えると、これらの計画の構成も安全性の仕様を満たしていることを証明します。 この証明により、複雑な多成分計画の安全性が保証され、構成された計画を検証する計算の複雑さが回避される。 次に、人間のラベル付けを必要とせずに、言語モデルを洗練して仕様に準拠した計画を生成する自動微調整プロセスを提案する。 実験結果は、微調整後のタスク仕様を満たす計画を生成する確率が30%向上したことを示している。

関連論文リスト

• AgentMath: Empowering Mathematical Reasoning for Large Language Models via Tool-Augmented Agent [80.83250816918861]
  o3やDeepSeek-R1のようなLarge Reasoning Models (LRM)は、長いチェーン・オブ・シークレットを持つ自然言語推論において顕著な進歩を遂げている。 しかし、計算的に非効率であり、複雑な数学的操作を必要とする問題を解く際には精度に苦しむ。 本稿では,言語モデルの推論能力とコードインタプリタの計算精度をシームレスに統合するエージェントフレームワークであるAgentMathを紹介する。
  論文  参考訳（メタデータ） (2025-12-23T19:57:49Z)
• Can LLM-Reasoning Models Replace Classical Planning? A Benchmark Study [0.0]
  大規模言語モデルは、ロボットタスク計画への関心を喚起している。 これらのモデルは強力な生成能力を示すが、構造的かつ実行可能な計画の作成における有効性は未だ不明である。 本稿では,芸術言語モデルの現状の幅広いスペクトルを体系的に評価する。
  論文  参考訳（メタデータ） (2025-07-31T14:25:54Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。 実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
  論文  参考訳（メタデータ） (2025-05-28T17:57:47Z)
• Towards High-Level Modelling in Automated Planning [0.36373653017571106]
  Unified-Planningは、計画問題を特定し、自動プランナを呼び出すためのハイレベルAPIを提供するPythonライブラリである。 本稿では,高次問題モデリングのための表現性向上を目的としたUPライブラリの拡張について述べる。
  論文  参考訳（メタデータ） (2024-12-09T09:01:13Z)
• Unlocking Reasoning Potential in Large Langauge Models by Scaling Code-form Planning [94.76546523689113]
  CodePlanは、テキストコード形式の計画を生成し、追跡するフレームワークで、高いレベルの構造化された推論プロセスの概要を擬似コードで示します。 CodePlanは、洗練された推論タスク固有のリッチなセマンティクスと制御フローを効果的にキャプチャする。 反応を直接生成するのに比べて25.1%の相対的な改善が達成されている。
  論文  参考訳（メタデータ） (2024-09-19T04:13:58Z)
• Ask-before-Plan: Proactive Language Agents for Real-World Planning [68.08024918064503]
  プロアクティブエージェントプランニングでは、ユーザエージェントの会話とエージェント環境のインタラクションに基づいて、言語エージェントが明確化のニーズを予測する必要がある。 本稿では,明確化,実行,計画の3つのエージェントからなる新しいマルチエージェントフレームワーク,Clarification-Execution-Planning(textttCEP)を提案する。
  論文  参考訳（メタデータ） (2024-06-18T14:07:28Z)
• NExT: Teaching Large Language Models to Reason about Code Execution [50.93581376646064]
  大規模言語モデル(LLM)のコードは通常、プログラムの表面テキスト形式に基づいて訓練される。 NExTは,プログラムの実行トレースを検査し,実行時の動作を判断する手法である。
  論文  参考訳（メタデータ） (2024-04-23T01:46:32Z)
• Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
  AutoSpecは、自動プログラム検証のための仕様を合成するための自動化アプローチである。 仕様の汎用性における既存の作業の欠点を克服し、完全な証明のために十分かつ適切な仕様を合成する。 実世界のX509パーサプロジェクトでプログラムを検証するためにうまく適用することができる。
  論文  参考訳（メタデータ） (2024-03-31T18:15:49Z)
• Probabilistically Correct Language-based Multi-Robot Planning using Conformal Prediction [11.614036749291216]
  本稿では,S-ATLAS for Safe plAnning for Teams of Language-instructed Agentsを提案する。 提案したプランナは,計画実行が成功すると仮定して,ユーザ指定のタスク成功率を達成可能であることを示す。 我々は,本手法が計算効率が高く,ヘルプレートが低いことを示す関連研究との比較実験を行った。
  論文  参考訳（メタデータ） (2024-02-23T15:02:44Z)
• Consolidating Trees of Robotic Plans Generated Using Large Language Models to Improve Reliability [6.4111574364474215]
  LLM(Large Language Models)の固有の確率論的性質は、予測不可能な要素を導入している。 本稿では,多様な現実の要求やシナリオに対して,適切なロボットタスク計画を作成することを目的とした,革新的なアプローチを提案する。
  論文  参考訳（メタデータ） (2024-01-15T18:01:59Z)
• Automated Process Planning Based on a Semantic Capability Model and SMT [50.76251195257306]
  製造システムと自律ロボットの研究において、機械で解釈可能なシステム機能の仕様に「能力」という用語が用いられる。 セマンティック能力モデルから始めて、AI計画問題を自動的に生成するアプローチを提案する。
  論文  参考訳（メタデータ） (2023-12-14T10:37:34Z)
• Planning as In-Painting: A Diffusion-Based Embodied Task Planning Framework for Environments under Uncertainty [56.30846158280031]
  具体的AIのためのタスクプランニングは、最も難しい問題の1つだ。 In-paintingとしての計画」というタスク非依存の手法を提案する。 提案するフレームワークは,様々な具体的AIタスクにおいて,有望なパフォーマンスを実現する。
  論文  参考訳（メタデータ） (2023-12-02T10:07:17Z)
• Fine-Tuning Language Models Using Formal Methods Feedback [53.24085794087253]
  我々は、自律システムにおけるアプリケーションのための、微調整済み言語モデルに対して、完全に自動化されたアプローチを提案する。 本手法は,自然言語タスク記述による事前学習モデルから自動制御器を合成する。 その結果、コントローラが満たした仕様の割合が60%から90%に改善したことが示唆された。
  論文  参考訳（メタデータ） (2023-10-27T16:24:24Z)
• The FormAI Dataset: Generative AI in Software Security Through the Lens of Formal Verification [3.2925005312612323]
  本稿では,脆弱性分類を伴う112,000のAI生成Cプログラムの大規模なコレクションであるFormAIデータセットを提案する。 すべてのプログラムには、型、行番号、脆弱な関数名を示すソースコード内の脆弱性がラベル付けされている。 ソースコードは112,000のプログラムで利用でき、各プログラムで検出された脆弱性を含む別のファイルが付属する。
  論文  参考訳（メタデータ） (2023-07-05T10:39:58Z)
• Embodied Task Planning with Large Language Models [86.63533340293361]
  本研究では,現場制約を考慮した地上計画のための具体的タスクにおけるTAsk Planing Agent (TaPA)を提案する。 推論の際には,オープンボキャブラリオブジェクト検出器を様々な場所で収集された多視点RGB画像に拡張することにより,シーン内の物体を検出する。 実験の結果,我々のTaPAフレームワークから生成されたプランは,LLaVAやGPT-3.5よりも大きなマージンで高い成功率が得られることがわかった。
  論文  参考訳（メタデータ） (2023-07-04T17:58:25Z)
• Multimodal Contextualized Plan Prediction for Embodied Task Completion [9.659463406886301]
  タスクプランニングは従来のロボットシステムにおいて重要なコンポーネントであり、ロボットがより複雑なタスクを実行するためのきめ細かいスキルを組み立てることができる。 シミュレーション実施エージェントにおけるタスク完了のための自然言語を実行可能なアクションに翻訳する最近の作業構築システムは,低レベルのアクションシーケンスを直接予測することに焦点を当てている。 我々は,そのような具体化されたタスク完了データセット - TEACh に対して,より高いレベルの計画表現を予測することに集中する。
  論文  参考訳（メタデータ） (2023-05-10T22:29:12Z)
• Synthesis of Mathematical programs from Natural Language Specifications [0.0]
  様々なビジネス領域で遭遇する決定問題は、数学的なプログラム、すなわち最適化問題としてモデル化することができる。 このようなモデリングを行うプロセスは、しばしばオペレーション研究や高度なアルゴリズムで訓練された専門家の関与を必要とする。 本研究は,データ拡張とビーム後処理によるCodeT5の有効性を評価する。 これらの拡張により、CodeT5baseは実行精度0.73となり、ChatGPTでは0.41、Codexでは0.36より大幅に向上した。
  論文  参考訳（メタデータ） (2023-03-30T06:10:00Z)
• Generating Sequences by Learning to Self-Correct [64.0249217590888]
  自己補正(Self-Correction)は、不完全な世代を反復的に修正する独立した修正器から不完全なベースジェネレータを分離する。 本稿では,3つの多種多様なタスクにおいて,自己補正がベースジェネレータを改善することを示す。
  論文  参考訳（メタデータ） (2022-10-31T18:09:51Z)
• ProgPrompt: Generating Situated Robot Task Plans using Large Language Models [68.57918965060787]
  大規模言語モデル(LLM)は、タスク計画中の潜在的な次のアクションを評価するために使用することができる。 本稿では, プログラム型LCMプロンプト構造を用いて, 配置環境間での計画生成機能を実現する。
  論文  参考訳（メタデータ） (2022-09-22T20:29:49Z)
• Natural Language to Code Translation with Execution [82.52142893010563]
  実行結果-プログラム選択のための最小ベイズリスク復号化。 そこで本研究では,自然言語からコードへのタスクにおいて,事前訓練されたコードモデルの性能を向上することを示す。
  論文  参考訳（メタデータ） (2022-04-25T06:06:08Z)
• Actions You Can Handle: Dependent Types for AI Plans [2.064612766965483]
  本稿では,AIプランナが作成したプランを依存型言語Agdaに組み込む手法を提案する。 ユーザーは、計画のより一般的で抽象的な特性を推論し、検証することができる。
  論文  参考訳（メタデータ） (2021-05-24T13:33:56Z)
• Generating Adversarial Computer Programs using Optimized Obfuscations [43.95037234252815]
  コンピュータプログラムに逆らってそのような学習モデルをだます原則的な方法を検討する。 我々は,従来はリバースエンジニアリングプログラムの試みを避けるために用いられてきたプログラム難読化を用いる。 当社の最良の攻撃提案は、最先端の攻撃生成アプローチよりも52%$改善できることを示します。
  論文  参考訳（メタデータ） (2021-03-18T10:47:15Z)
• From Abstractions to Grounded Languages for Robust Coordination of Task Planning Robots [4.496989927037321]
  コーディネーションに十分な説明性を有しつつ,最大限柔軟である言語の自動構築について検討する。 我々の言語は、任意のタスクの計画を「計画スケッチ」として表現し、それを実現する柔軟性を最大化しつつ、十分な詳細を伝達します。
  論文  参考訳（メタデータ） (2019-05-01T22:05:42Z)

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

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