論文の概要: Verification and Validation of Convex Optimization Algorithms for Model
Predictive Control
- arxiv url: http://arxiv.org/abs/2005.12588v1
- Date: Tue, 26 May 2020 09:18:14 GMT
- ステータス: 処理完了
- システム内更新日: 2022-11-29 00:31:49.984618
- Title: Verification and Validation of Convex Optimization Algorithms for Model
Predictive Control
- Title(参考訳): モデル予測制御のための凸最適化アルゴリズムの検証と検証
- Authors: Rapha\"el Cohen, Eric F\'eron, Pierre-Lo\"ic Garoche (ENAC)
- Abstract要約: 本稿では,凸最適化アルゴリズムであるEllipsoid法とそのコード実装の形式的検証について述べる。
これらのコードプロパティと証明の適用性と制限も提示される。
数値安定性の制御に使用できるアルゴリズムの修正について述べる。
- 参考スコア(独自算出の注目度): 1.5322124183968633
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Advanced embedded algorithms are growing in complexity and they are an
essential contributor to the growth of autonomy in many areas. However, the
promise held by these algorithms cannot be kept without proper attention to the
considerably stronger design constraints that arise when the applications of
interest, such as aerospace systems, are safety-critical. Formal verification
is the process of proving or disproving the ''correctness'' of an algorithm
with respect to a certain mathematical description of it by means of a
computer. This article discusses the formal verification of the Ellipsoid
method, a convex optimization algorithm, and its code implementation as it
applies to receding horizon control. Options for encoding code properties and
their proofs are detailed. The applicability and limitations of those code
properties and proofs are presented as well. Finally, floating-point errors are
taken into account in a numerical analysis of the Ellipsoid algorithm.
Modifications to the algorithm are presented which can be used to control its
numerical stability.
- Abstract(参考訳): 高度な組込みアルゴリズムは複雑さを増しており、多くの分野における自律性の成長に不可欠である。
しかし、これらのアルゴリズムが持つ約束は、航空宇宙システムのような関心事の応用が安全クリティカルである場合に生じる非常に強い設計制約に適切に注意を払わずに維持することはできない。
形式的検証(英: formal verification)とは、ある数学的な記述に対してコンピュータを用いてアルゴリズムの'正しさ'を証明または否定する過程である。
本稿では,凸最適化アルゴリズムである楕円型手法の形式的検証と,それを適用するコード実装について述べる。
コードプロパティとその証明をエンコードするオプションは、詳細である。
これらのコードプロパティと証明の適用性と制限も提示される。
最後に、楕円体アルゴリズムの数値解析において浮動小数点誤差を考慮する。
数値安定性の制御に使用できるアルゴリズムの修正について述べる。
関連論文リスト
- Accelerating Cutting-Plane Algorithms via Reinforcement Learning
Surrogates [49.84541884653309]
凸離散最適化問題に対する現在の標準的なアプローチは、カットプレーンアルゴリズムを使うことである。
多くの汎用カット生成アルゴリズムが存在するにもかかわらず、大規模な離散最適化問題は、難易度に悩まされ続けている。
そこで本研究では,強化学習による切削平面アルゴリズムの高速化手法を提案する。
論文 参考訳(メタデータ) (2023-07-17T20:11:56Z) - Interpretable Anomaly Detection via Discrete Optimization [1.7150329136228712]
本稿では,シーケンシャルデータから本質的に解釈可能な異常検出を学習するためのフレームワークを提案する。
この問題は計算的に困難であることを示し,制約最適化に基づく2つの学習アルゴリズムを開発した。
プロトタイプ実装を用いて,提案手法は精度とF1スコアの点で有望な結果を示す。
論文 参考訳(メタデータ) (2023-03-24T16:19:15Z) - Accelerated First-Order Optimization under Nonlinear Constraints [73.2273449996098]
我々は、制約付き最適化のための一階アルゴリズムと非滑らかなシステムの間で、新しい一階アルゴリズムのクラスを設計する。
これらのアルゴリズムの重要な性質は、制約がスパース変数の代わりに速度で表されることである。
論文 参考訳(メタデータ) (2023-02-01T08:50:48Z) - Fast and Robust Non-Rigid Registration Using Accelerated
Majorization-Minimization [35.66014845211251]
非剛性登録は、ターゲット形状と整合する非剛性な方法でソース形状を変形させるが、コンピュータビジョンにおける古典的な問題である。
既存のメソッドは通常$ell_p$型ロバストノルムを使用してアライメントエラーを測定し、変形の滑らかさを規則化する。
本稿では、アライメントと正規化のためのグローバルなスムーズなロバストノルムに基づく、ロバストな非剛体登録のための定式化を提案する。
論文 参考訳(メタデータ) (2022-06-07T16:00:33Z) - Regret Bounds for Expected Improvement Algorithms in Gaussian Process
Bandit Optimization [63.8557841188626]
期待されている改善(EI)アルゴリズムは、不確実性の下で最適化するための最も一般的な戦略の1つである。
本稿では,GP予測平均を通した標準既存値を持つEIの変種を提案する。
我々のアルゴリズムは収束し、$mathcal O(gamma_TsqrtT)$の累積後悔境界を達成することを示す。
論文 参考訳(メタデータ) (2022-03-15T13:17:53Z) - Learning Robust Output Control Barrier Functions from Safe Expert
Demonstrations [50.37808220291108]
まず,安全性を保証する手段として,ロバスト出力制御バリア関数(ROCBF)を提案する。
次に、安全なシステム動作を示す専門家による実証からROCBFを学習するための最適化問題を定式化する。
我々は,自律走行シミュレータCARLAのアルゴリズムを実証的に検証し,RGBカメラ画像から安全な制御法を学習する方法を実証する。
論文 参考訳(メタデータ) (2021-11-18T23:21:00Z) - Finite-Bit Quantization For Distributed Algorithms With Linear
Convergence [6.293059137498172]
量子化された通信対象のメッシュネットワーク上での(強い凸)複合最適化問題に対する分散アルゴリズムについて検討する。
通信効率のよい符号化方式と結合した新しい量子化器を提案し, バイアス圧縮(BC-)ルールを効率的に実装した。
数値計算により,提案手法を応用した分散アルゴリズムは,既存の量子化規則を用いたアルゴリズムよりも,通信の複雑さが高いことが示された。
論文 参考訳(メタデータ) (2021-07-23T15:31:31Z) - Dynamic programming by polymorphic semiring algebraic shortcut fusion [1.9405875431318445]
動的プログラミング(動的プログラミング、英: Dynamic Programming、DP)は、難解問題の効率的かつ正確な解法のためのアルゴリズム設計パラダイムである。
本稿では,セミリングに基づくDPアルゴリズムを体系的に導出するための厳密な代数形式について述べる。
論文 参考訳(メタデータ) (2021-07-05T00:51:02Z) - Adaptive Sampling for Best Policy Identification in Markov Decision
Processes [79.4957965474334]
本稿では,学習者が生成モデルにアクセスできる場合の,割引マルコフ決定(MDP)における最良の政治的識別の問題について検討する。
最先端アルゴリズムの利点を論じ、解説する。
論文 参考訳(メタデータ) (2020-09-28T15:22:24Z) - Adaptive Discretization for Model-Based Reinforcement Learning [10.21634042036049]
本稿では,適応離散化手法を導入し,効率的なモデルに基づくエピソード強化学習アルゴリズムを設計する。
我々のアルゴリズムは、空間の適応的な離散化を維持するために拡張された楽観的なワンステップ値反復に基づいている。
論文 参考訳(メタデータ) (2020-07-01T19:36:46Z) - Lagrangian Decomposition for Neural Network Verification [148.0448557991349]
ニューラルネットワーク検証の基本的なコンポーネントは、出力が取ることのできる値のバウンダリの計算である。
ラグランジアン分解に基づく新しい手法を提案する。
ランニングタイムのごく一部で、既成の解法に匹敵するバウンダリが得られることを示す。
論文 参考訳(メタデータ) (2020-02-24T17:55:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。