Fugu-MT 論文翻訳(概要): Bridging LLM Planning Agents and Formal Methods: A Case Study in Plan Verification

論文の概要: Bridging LLM Planning Agents and Formal Methods: A Case Study in Plan Verification

arxiv url: http://arxiv.org/abs/2510.03469v1
Date: Fri, 03 Oct 2025 19:46:55 GMT
ステータス: 翻訳完了
システム内更新日: 2025-10-07 16:52:59.058957
Title: Bridging LLM Planning Agents and Formal Methods: A Case Study in Plan Verification
Title（参考訳）: ブリッジ型LCM計画エージェントと形式的手法:計画検証を事例として
Authors: Keshav Ramani, Vali Tawosi, Salwa Alamir, Daniel Borrajo,
Abstract要約: 我々は、自然言語計画と予測行動の整合性を評価するための新しい枠組みを、クリプキ構造と線形時間論理(LTL)に変換することによって導入する。このフレームワークをPlanBench計画検証データセットの簡易バージョンで体系的に評価し、精度、精度、リコール、F1スコアなどの指標について報告する。
参考スコア（独自算出の注目度）: 5.177308274872149
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: We introduce a novel framework for evaluating the alignment between natural language plans and their expected behavior by converting them into Kripke structures and Linear Temporal Logic (LTL) using Large Language Models (LLMs) and performing model checking. We systematically evaluate this framework on a simplified version of the PlanBench plan verification dataset and report on metrics like Accuracy, Precision, Recall and F1 scores. Our experiments demonstrate that GPT-5 achieves excellent classification performance (F1 score of 96.3%) while almost always producing syntactically perfect formal representations that can act as guarantees. However, the synthesis of semantically perfect formal models remains an area for future exploration.
Abstract（参考訳）: 本稿では,Large Language Models (LLMs) を用いたKripke構造とLTL(Linear Temporal Logic)に変換することで,自然言語計画と期待される動作の整合性を評価する新しいフレームワークを提案する。このフレームワークをPlanBench計画検証データセットの簡易バージョンで体系的に評価し、精度、精度、リコール、F1スコアなどの指標について報告する。実験の結果, GPT-5は優れた分類性能(F1スコア96.3%)を達成でき, ほぼ常に構文的に完璧な形式表現を生成でき, 保証として振る舞うことができた。しかし、意味論的に完全な形式モデルの合成は、将来の探索の領域として残されている。

関連論文リスト

Claim Automation using Large Language Model [0.0]
LLM(Large Language Models)は汎用言語タスクにおいて高いパフォーマンスを達成しているが、規制やデータに敏感なドメインへの展開は依然として限られている。本稿では,非構造化クレームの物語から構造化された修正-アクションレコメンデーションを生成する,ガバナンス対応言語モデリングコンポーネントを提案する。我々は,Low-Rank Adaptation (LoRA) を用いて事前学習LLMを微調整し,クレーム処理パイプライン内の初期決定モジュールにモデルをスコーピングし,クレーム調整者の判断を高速化する。
論文参考訳（メタデータ） (2026-02-18T20:01:12Z)
Autoformalizer with Tool Feedback [52.334957386319864]
自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
論文参考訳（メタデータ） (2025-10-08T10:25:12Z)
Estimating Time Series Foundation Model Transferability via In-Context Learning [74.65355820906355]
時系列基礎モデル(TSFM)は、大規模な事前訓練を通じて強力なゼロショット予測を提供する。微調整は、公開データに制限のあるドメインのパフォーマンス向上に依然として不可欠である。モデル選択をコンテキスト内学習問題として再キャストする転送可能性推定フレームワークであるTimeTicを紹介する。
論文参考訳（メタデータ） (2025-09-28T07:07:13Z)
Can LLM-Reasoning Models Replace Classical Planning? A Benchmark Study [0.0]
大規模言語モデルは、ロボットタスク計画への関心を喚起している。これらのモデルは強力な生成能力を示すが、構造的かつ実行可能な計画の作成における有効性は未だ不明である。本稿では,芸術言語モデルの現状の幅広いスペクトルを体系的に評価する。
論文参考訳（メタデータ） (2025-07-31T14:25:54Z)
Towards Locally Deployable Fine-Tuned Causal Large Language Models for Mode Choice Behaviour [4.378407481656902]
本研究では,移動モード選択予測のためのオープンアクセス型ローカル展開型因果大言語モデル (LLM) の導入について検討した。提案した3つの選好データセットに対して11のLCMをベンチマークし,396の設定をテストし,79,000以上の合成通勤予測を生成した。 LiTransMCはパラメータ効率と損失マスキング戦略で微調整され、重み付きF1スコアは0.6845、ジェンセン=シャノンディバージェンスは0.000245に達した。
論文参考訳（メタデータ） (2025-07-29T02:03:37Z)
Large Language Models for Planning: A Comprehensive and Systematic Survey [29.168219253281453]
大規模言語モデル(LLM)は、特定の計画タスクにおいて顕著なパフォーマンスを示している。本稿では,LLMをベースとした計画の総合的なレビューを行う。
論文参考訳（メタデータ） (2025-05-26T08:44:53Z)
Reliable Decision Support with LLMs: A Framework for Evaluating Consistency in Binary Text Classification Applications [0.7124971549479361]
本研究では,大言語モデル(LLM)のバイナリテキスト分類における一貫性を評価するフレームワークを提案する。我々は,サンプルサイズ要件を定め,不適切な応答の指標を開発し,レータ内およびレータ間信頼性を評価する。
論文参考訳（メタデータ） (2025-05-20T21:12:58Z)
SCORE: Systematic COnsistency and Robustness Evaluation for Large Language Models [4.875712300661656]
本稿では,大規模言語モデルの非敵対的評価のための総合的なフレームワークであるSCORE ($mathbfS$ystematic $mathbfCO$nsistency and $mathbfR$obustness $mathbfE$valuationを提案する。 SCOREフレームワークは、様々な設定で同じベンチマークで繰り返しテストすることでモデルを評価し、精度と一貫性を現実的に見積もる。
論文参考訳（メタデータ） (2025-02-28T19:27:29Z)
Exploring and Benchmarking the Planning Capabilities of Large Language Models [57.23454975238014]
この研究は、大規模言語モデル(LLM)の計画能力を改善するための基礎を築いた。我々は、古典的な計画ベンチマークと自然言語シナリオの両方を含む包括的なベンチマークスイートを構築した。本研究は,LLM計画の強化を目的としたマルチショットインコンテキスト学習について検討し,文脈長の増大と計画性能の向上の関係について検討する。
論文参考訳（メタデータ） (2024-06-18T22:57:06Z)
Latent Semantic Consensus For Deterministic Geometric Model Fitting [109.44565542031384]
我々はLSC(Latent Semantic Consensus)と呼ばれる効果的な方法を提案する。 LSCは、モデルフィッティング問題をデータポイントとモデル仮説に基づく2つの潜在意味空間に定式化する。 LSCは、一般的な多構造モデルフィッティングのために、数ミリ秒以内で一貫した、信頼性の高いソリューションを提供することができる。
論文参考訳（メタデータ） (2024-03-11T05:35:38Z)
Faithful Explanations of Black-box NLP Models Using LLM-generated Counterfactuals [67.64770842323966]
NLPシステムの予測に関する因果的説明は、安全性を確保し、信頼を確立するために不可欠である。既存の手法は、しばしばモデル予測を効果的または効率的に説明できない。本稿では, 対物近似(CF)の2つの手法を提案する。
論文参考訳（メタデータ） (2023-10-01T07:31:04Z)
Evaluating and Explaining Large Language Models for Code Using Syntactic Structures [74.93762031957883]
本稿では,コード用大規模言語モデルに特有の説明可能性手法であるASTxplainerを紹介する。その中核にあるASTxplainerは、トークン予測をASTノードに整合させる自動メソッドを提供する。私たちは、最も人気のあるGitHubプロジェクトのキュレートデータセットを使用して、コード用の12の人気のあるLLMに対して、実証的な評価を行います。
論文参考訳（メタデータ） (2023-08-07T18:50:57Z)
Discover, Explanation, Improvement: An Automatic Slice Detection Framework for Natural Language Processing [72.14557106085284]
スライス検出モデル(SDM)は、データポイントの低パフォーマンスなグループを自動的に識別する。本稿では,NLPタスクの分類のための "Discover, Explain, improve (DEIM)" というベンチマークを提案する。評価の結果,Edisaは情報的セマンティックな特徴を持つ誤り発生データポイントを正確に選択できることがわかった。
論文参考訳（メタデータ） (2022-11-08T19:00:00Z)

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