論文の概要: BarrierBench : Evaluating Large Language Models for Safety Verification in Dynamical Systems

• arxiv url: http://arxiv.org/abs/2511.09363v1
• Date: Thu, 13 Nov 2025 01:49:09 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-11-13 22:34:54.535399
• Title: BarrierBench : Evaluating Large Language Models for Safety Verification in Dynamical Systems
• Title（参考訳）: BarrierBench : 動的システムの安全性検証のための大規模言語モデルの評価
• Authors: Ali Taheri, Alireza Taban, Sadegh Soudjani, Ashutosh Trivedi,
• Abstract要約: バリア証明書合成のための LLM ベースのエージェントフレームワークを提案する。 このフレームワークは自然言語推論を使用して、候補証明書を提案し、洗練し、検証する。 BarrierBenchは、線形、非線形、離散時間、連続時間設定にまたがる100の動的システムのベンチマークである。
• 参考スコア（独自算出の注目度）: 4.530582224312311
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Safety verification of dynamical systems via barrier certificates is essential for ensuring correctness in autonomous applications. Synthesizing these certificates involves discovering mathematical functions with current methods suffering from poor scalability, dependence on carefully designed templates, and exhaustive or incremental function-space searches. They also demand substantial manual expertise--selecting templates, solvers, and hyperparameters, and designing sampling strategies--requiring both theoretical and practical knowledge traditionally shared through linguistic reasoning rather than formalized methods. This motivates a key question: can such expert reasoning be captured and operationalized by language models? We address this by introducing an LLM-based agentic framework for barrier certificate synthesis. The framework uses natural language reasoning to propose, refine, and validate candidate certificates, integrating LLM-driven template discovery with SMT-based verification, and supporting barrier-controller co-synthesis to ensure consistency between safety certificates and controllers. To evaluate this capability, we introduce BarrierBench, a benchmark of 100 dynamical systems spanning linear, nonlinear, discrete-time, and continuous-time settings. Our experiments assess not only the effectiveness of LLM-guided barrier synthesis but also the utility of retrieval-augmented generation and agentic coordination strategies in improving its reliability and performance. Across these tasks, the framework achieves more than 90% success in generating valid certificates. By releasing BarrierBench and the accompanying toolchain, we aim to establish a community testbed for advancing the integration of language-based reasoning with formal verification in dynamical systems. The benchmark is publicly available at https://hycodev.com/dataset/barrierbench
• Abstract（参考訳）: バリア認証による動的システムの安全性検証は、自律的なアプリケーションの正確性を保証するために不可欠である。 これらの証明書の合成には、スケーラビリティの低さ、慎重に設計されたテンプレートへの依存、徹底的あるいは漸進的な関数空間探索による数学的関数の発見が含まれる。 彼らはまた、テンプレート、ソルバ、ハイパーパラメータを選定し、サンプリング戦略を設計すること、そして、形式化された方法ではなく、言語的推論を通じて伝統的に共有される理論的知識と実践的知識の両方を要求した。 このような専門家の推論は、言語モデルによってキャプチャされ、運用できますか? バリア証明書合成のための LLM ベースのエージェント・フレームワークを導入することでこの問題に対処する。 このフレームワークは自然言語推論を使用して、候補証明書を提案し、洗練し、検証し、LSM駆動のテンプレート発見とSMTベースの検証を統合し、安全証明書とコントローラ間の一貫性を確保するためにバリア・コントローラの共合成をサポートする。 この能力を評価するために、線形、非線形、離散時間、連続時間設定にまたがる100の動的システムのベンチマークであるBarrierBenchを導入する。 本実験は, LLM誘導バリア合成の有効性だけでなく, 信頼性と性能向上のための検索補助生成およびエージェント調整戦略の有用性も評価した。 これらのタスク全体で、このフレームワークは有効な証明書を生成する上で90%以上の成功を収めている。 BarrierBenchとそれに付随するツールチェーンをリリースすることによって、動的システムにおける公式な検証を伴う言語ベースの推論の統合を促進するためのコミュニティテストベッドを確立することを目指している。 ベンチマークはhttps://hycodev.com/dataset/barrierbenchで公開されている。

関連論文リスト

• Rethinking Testing for LLM Applications: Characteristics, Challenges, and a Lightweight Interaction Protocol [83.83217247686402]
  大言語モデル(LLM)は、単純なテキストジェネレータから、検索強化、ツール呼び出し、マルチターンインタラクションを統合する複雑なソフトウェアシステムへと進化してきた。 その固有の非決定主義、ダイナミズム、文脈依存は品質保証に根本的な課題をもたらす。 本稿では,LLMアプリケーションを3層アーキテクチャに分解する: textbftextitSystem Shell Layer, textbftextitPrompt Orchestration Layer, textbftextitLLM Inference Core。
  論文  参考訳（メタデータ） (2025-08-28T13:00:28Z)
• Position Paper: Programming Language Techniques for Bridging LLM Code Generation Semantic Gaps [3.61356888205659]
  本稿では,大規模言語モデルにおける意味的ギャップを埋めるのに,プログラミング手法の原則的統合が不可欠であることを論じる。 PL技術は、LLM生成コードを統計的パターンマッチングから真に信頼性と信頼性の高いレベルまで高めることができる。
  論文  参考訳（メタデータ） (2025-07-12T04:32:15Z)
• Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overview [3.135279672650891]
  本稿では,最先端のソフトウェアテストと検証に焦点をあてる。 古典的な形式的手法、LLMに基づく分析、新しいハイブリッド手法の3つの主要なアプローチに焦点を当てている。 LLMによるインサイトとフォーマルリガーを統合することで,ソフトウェア検証の有効性とスケーラビリティが向上するかどうかを解析する。
  論文  参考訳（メタデータ） (2025-03-13T18:22:22Z)
• CELA: Cost-Efficient Language Model Alignment for CTR Prediction [70.65910069412944]
  CTR(Click-Through Rate)予測は、レコメンダシステムにおいて最重要位置を占める。 最近の取り組みは、プレトレーニング言語モデル(PLM)を統合することでこれらの課題を緩和しようとしている。 CTR予測のためのtextbfCost-textbfEfficient textbfLanguage Model textbfAlignment (textbfCELA)を提案する。
  論文  参考訳（メタデータ） (2024-05-17T07:43:25Z)
• Enhancing Security in Federated Learning through Adaptive Consensus-Based Model Update Validation [2.28438857884398]
  本稿では,ラベルフリップ攻撃に対して,FL(Federated Learning)システムを構築するための高度なアプローチを提案する。 本稿では,適応的しきい値設定機構と統合されたコンセンサスに基づく検証プロセスを提案する。 以上の結果から,FLシステムのレジリエンスを高め,ラベルフリップ攻撃の顕著な緩和効果が示唆された。
  論文  参考訳（メタデータ） (2024-03-05T20:54:56Z)
• A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
  システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。 コントローラと証明書を形式的に合成する自動化手法を提案する。 我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
  論文  参考訳（メタデータ） (2023-09-12T09:37:26Z)
• Joint Differentiable Optimization and Verification for Certified Reinforcement Learning [91.93635157885055]
  安全クリティカル制御システムのためのモデルベース強化学習では,システム特性を正式に認定することが重要である。 本稿では,強化学習と形式検証を共同で行う枠組みを提案する。
  論文  参考訳（メタデータ） (2022-01-28T16:53:56Z)

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

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