論文の概要: Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial
- arxiv url: http://arxiv.org/abs/2605.26577v1
- Date: Tue, 26 May 2026 05:49:19 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-27 17:51:41.690215
- Title: Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial
- Title(参考訳): ニューラルネットワーク検証器α-β-CROWNによるブリッジ制御:チュートリアル
- Authors: Haoyu Li, Xiangru Zhong, Hao Cheng, Bin Hu, Huan Zhang,
- Abstract要約: $,!$-CROWN はグラフとして表される非線形関数の汎用的バウンディングエンジンである。
本チュートリアルでは,$,!$-CROWNの基礎について論じ,様々な制御関連計算タスクへの応用について紹介する。
- 参考スコア(独自算出の注目度): 23.69448525306035
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Learning-based methods for synthesizing controllers have gained popularity due to their high expressiveness and strong empirical performance. However, in safety-critical scenarios such as autonomous driving, robotics, and power systems, empirical performance alone is insufficient, and formal verification of controller properties such as stability and safety is highly desirable. Unfortunately, many prior verification approaches are either tied to specific structural assumptions on the system or the certificate, making them difficult to transfer across settings, or suffer from poor scalability on higher-dimensional neural network systems. In this tutorial, we present a unified framework that aims to mitigate this gap via bridging control with the state-of-the-art neural network verifier $α,\!β$-CROWN (alpha-beta-CROWN). At its core, $α,\!β$-CROWN is a general-purpose bounding engine for nonlinear functions represented as computation graphs: given an input domain, it can produce certified bounds and explicit linear relaxation of the nonlinear function. These certified bounds are useful on their own for tasks such as reachability analysis, and they also provide the foundation for more complex routines that perform satisfiability checking and optimization. More specifically, many control problems reduce to verifying real-valued inequalities over a state domain (e.g., Lyapunov theory). Consequently, $α,\!β$-CROWN enables scalable verification of such conditions by computing tight bounds and recursively partitioning and pruning subdomains based on the bounds. Thanks to GPU parallelization, this pipeline demonstrates superior scalability on verification and optimization problems that are challenging for traditional approaches. In this tutorial, we discuss the basics of $α,\!β$-CROWN and introduce its application to various control-related tasks.
- Abstract(参考訳): 制御器を合成する学習的手法は,高い表現力と強い経験的性能によって人気を博している。
しかし、自律運転、ロボット工学、電力システムといった安全クリティカルなシナリオでは、経験的性能だけでは不十分であり、安定性や安全性などの制御特性の形式的検証が極めて望ましい。
残念ながら、多くの事前検証アプローチは、システムや証明書の特定の構造的前提に結びついているので、設定間での転送が困難になるか、高次元のニューラルネットワークシステムでのスケーラビリティの低下に悩まされる。
本チュートリアルでは,最先端のニューラルネットワーク検証器$α,\!でブリッジ制御することで,このギャップを軽減することを目的とした統一フレームワークを提案する。
β$-CROWN (alpha-beta-CROWN)。
その中核は、$α,\!
β$-CROWN は、計算グラフとして表される非線形関数の汎用的バウンディングエンジンである。
これらの認定された境界は、到達可能性分析のようなタスクに単独で有用であり、また、満足度チェックと最適化を行うより複雑なルーチンの基盤を提供する。
より具体的には、多くの制御問題は状態領域上の実値の不等式(例えば、リャプノフ理論)を検証することに還元される。
その結果、$α,\!
β$-CROWNは、厳密な境界を計算し、境界に基づいて再帰的に分割し、サブドメインを刈り取ることにより、そのような条件のスケーラブルな検証を可能にする。
GPU並列化のおかげで、このパイプラインは従来のアプローチでは難しい検証と最適化の問題に優れたスケーラビリティを示している。
このチュートリアルでは、$α,\!
β$-CROWNを導入し、様々な制御関連タスクに適用する。
関連論文リスト
- Hierarchical End-to-End Taylor Bounds for Complete Neural Network Verification [10.685380941330687]
ニューラルネットワークの到達可能性解析は、与えられた入力領域上で達成可能な出力の集合を計算または束縛しようとする。
既存のアプローチは、ほとんどの2階情報を利用しており、高階情報を体系的に活用していない。
textscHiTaB は Hessian, $nabla2 f$ と Lipschitz 定数 $L_nabla2 f$ の2階スムーズ性を利用する新しい検証フレームワークである。
論文 参考訳(メタデータ) (2026-05-11T14:16:13Z) - Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification [9.733843486234878]
最先端ニューラルネットワーク(NN)検証は、分岐とバウンド(BaB)の手順を高速なバウンディング技術で適用することが、多くの挑戦的な検証特性に対処する上で重要な役割を果たしていることを示す。
本稿では,NN検証の有効性を高めるために,スケーラブルで効率的な手法のクラスである線形制約駆動型クリッピングフレームワークを紹介する。
論文 参考訳(メタデータ) (2025-12-11T19:59:37Z) - Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagation [50.53301323864253]
制御バリア関数 (CBF) は非線形動的制御システムの安全性を保証するための一般的なツールである。
本稿では,ニューラルネットワークがCBFとなるために必要な条件に対して,一方向に線形な上界と下界に基づいて,ニューラルCBFを検証するための新しい枠組みを提案する。
我々のアプローチは、CBFの最先端の検証手順よりも大きなニューラルネットワークにスケールする。
論文 参考訳(メタデータ) (2025-11-09T11:51:15Z) - A General Framework for Property-Driven Machine Learning [1.0485739694839669]
逆行訓練は,小摂動に対するロバスト性を向上させるために,$epsilon$-cubesで行うことができることを示す。
コンピュータビジョン以外の領域は、一般化された超矩形を通してより柔軟な入力領域の仕様を必要とすることがある。
本稿では,これら2つの補完的アプローチを,プロパティ駆動機械学習の単一フレームワークに組み込む方法について検討する。
論文 参考訳(メタデータ) (2025-05-01T11:33:38Z) - Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation [67.63756749551924]
学習ベースのニューラルネットワーク(NN)制御ポリシは、ロボット工学と制御の幅広いタスクにおいて、印象的な経験的パフォーマンスを示している。
非線形力学系を持つNNコントローラのトラクション領域(ROA)に対するリアプノフ安定性の保証は困難である。
我々は、高速な経験的ファルシフィケーションと戦略的正則化を用いて、Lyapunov証明書とともにNNコントローラを学習するための新しいフレームワークを実証する。
論文 参考訳(メタデータ) (2024-04-11T17:49:15Z) - Towards Practical Control of Singular Values of Convolutional Layers [65.25070864775793]
畳み込みニューラルネットワーク(CNN)の訓練は容易であるが、一般化誤差や対向ロバスト性といった基本的な特性は制御が難しい。
最近の研究では、畳み込み層の特異値がそのような解像特性に顕著に影響を及ぼすことが示された。
我々は,レイヤ表現力の著しく低下を犠牲にして,先行技術の制約を緩和するための原則的アプローチを提供する。
論文 参考訳(メタデータ) (2022-11-24T19:09:44Z) - Learning Robust Output Control Barrier Functions from Safe Expert Demonstrations [50.37808220291108]
本稿では,専門家によるデモンストレーションの部分的な観察から,安全な出力フィードバック制御法を考察する。
まず,安全性を保証する手段として,ロバスト出力制御バリア関数(ROCBF)を提案する。
次に、安全なシステム動作を示す専門家による実証からROCBFを学習するための最適化問題を定式化する。
論文 参考訳(メタデータ) (2021-11-18T23:21:00Z) - Global Optimization of Objective Functions Represented by ReLU Networks [77.55969359556032]
ニューラルネットワークは複雑で非敵対的な関数を学ぶことができ、安全クリティカルな文脈でそれらの正しい振る舞いを保証することは困難である。
ネットワーク内の障害を見つけるための多くのアプローチ(例えば、敵の例)があるが、これらは障害の欠如を保証できない。
本稿では,最適化プロセスを検証手順に統合し,本手法よりも優れた性能を実現する手法を提案する。
論文 参考訳(メタデータ) (2020-10-07T08:19:48Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。