論文の概要: 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)とは、ある数学的な記述に対してコンピュータを用いてアルゴリズムの'正しさ'を証明または否定する過程である。
本稿では,凸最適化アルゴリズムである楕円型手法の形式的検証と,それを適用するコード実装について述べる。
コードプロパティとその証明をエンコードするオプションは、詳細である。
これらのコードプロパティと証明の適用性と制限も提示される。
最後に、楕円体アルゴリズムの数値解析において浮動小数点誤差を考慮する。
数値安定性の制御に使用できるアルゴリズムの修正について述べる。
関連論文リスト
- Accelerated zero-order SGD under high-order smoothness and overparameterized regime [79.85163929026146]
凸最適化問題を解くための新しい勾配のないアルゴリズムを提案する。
このような問題は医学、物理学、機械学習で発生する。
両種類の雑音下で提案アルゴリズムの収束保証を行う。
論文 参考訳（メタデータ） (2024-11-21T10:26:17Z) - Homomorphically encrypted gradient descent algorithms for quadratic programming [3.185870720907055]
我々は,2次プログラミングを準同型暗号設定で解くための勾配降下アルゴリズムの適用性について数値解析を行った。
本論文は, 等式的に暗号化された勾配勾配アルゴリズムの有効性を, 直接的に示すものである。
論文 参考訳（メタデータ） (2023-09-04T12:25:14Z) - 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を学習するための最適化問題を定式化する。
論文 参考訳（メタデータ） (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) - Lagrangian Decomposition for Neural Network Verification [148.0448557991349]
ニューラルネットワーク検証の基本的なコンポーネントは、出力が取ることのできる値のバウンダリの計算である。
ラグランジアン分解に基づく新しい手法を提案する。
ランニングタイムのごく一部で、既成の解法に匹敵するバウンダリが得られることを示す。
論文 参考訳（メタデータ） (2020-02-24T17:55:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。