論文の概要: Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers
- arxiv url: http://arxiv.org/abs/2007.10865v1
- Date: Tue, 21 Jul 2020 14:45:23 GMT
- ステータス: 処理完了
- システム内更新日: 2022-11-08 05:49:30.657656
- Title: Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers
- Title（参考訳）: smtソルバを用いたリアプノフ関数の自動合成と音合成
- Authors: Daniele Ahmed, Andrea Peruffo, Alessandro Abate
- Abstract要約: 線形、非線形(ポリノミカル)およびパラメトリックモデルに対するリャプノフ関数を合成する。
パラメトリックテンプレートからLyapunov関数を合成するための帰納的フレームワークを利用する。
- 参考スコア（独自算出の注目度）: 70.70479436076238
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: In this paper we employ SMT solvers to soundly synthesise Lyapunov functions
that assert the stability of a given dynamical model. The search for a Lyapunov
function is framed as the satisfiability of a second-order logical formula,
asking whether there exists a function satisfying a desired specification
(stability) for all possible initial conditions of the model. We synthesise
Lyapunov functions for linear, non-linear (polynomial), and for parametric
models. For non-linear models, the algorithm also determines a region of
validity for the Lyapunov function. We exploit an inductive framework to
synthesise Lyapunov functions, starting from parametric templates. The
inductive framework comprises two elements: a learner proposes a Lyapunov
function, and a verifier checks its validity - its lack is expressed via a
counterexample (a point over the state space), for further use by the learner.
Whilst the verifier uses the SMT solver Z3, thus ensuring the overall soundness
of the procedure, we examine two alternatives for the learner: a numerical
approach based on the optimisation tool Gurobi, and a sound approach based
again on Z3. The overall technique is evaluated over a broad set of benchmarks,
which shows that this methodology not only scales to 10-dimensional models
within reasonable computational time, but also offers a novel soundness proof
for the generated Lyapunov functions and their domains of validity.
- Abstract（参考訳）: 本稿では、与えられた力学モデルの安定性を主張するリアプノフ関数を音声合成するためにSMTソルバを用いる。
リアプノフ関数の探索は、2階論理公式の充足可能性として構成され、モデルのすべての可能な初期条件に対して所望の仕様(安定性)を満たす関数が存在するかどうかを問う。
我々は線形、非線形(多項)、パラメトリックモデルに対してリアプノフ関数を合成する。
非線形モデルに対しては、このアルゴリズムはリャプノフ関数の妥当性の領域も決定する。
パラメトリックテンプレートからLyapunov関数を合成するための帰納的フレームワークを利用する。
学習者はリアプノフ関数を提案し、検証者はその妥当性を確認し、その欠如は反例(状態空間上の点)を介して表現され、学習者がさらに利用する。
検証者はSMTソルバZ3を用いて,手順の全体的健全性を確保する一方で,最適化ツールGurobiに基づく数値的アプローチと,Z3に基づく音響的アプローチの2つの選択肢を検討した。
この手法は, 妥当な計算時間内に10次元モデルにスケールするだけでなく, 生成したリアプノフ関数とその有効領域に対する新しい音響性証明を提供することを示す。
関連論文リスト
- Analytical Lyapunov Function Discovery: An RL-based Generative Approach [6.752429418580116]
解析的リアプノフ関数(ローカル)を構築するために変換器を用いたエンドツーエンドフレームワークを提案する。
本フレームワークは,候補リアプノフ関数を生成するトランスフォーマーベーストレーナーと,候補表現を検証するファルシファイアから構成される。
本稿では,制御文献に未同定なリアプノフ関数が発見可能であることを示す。
論文 参考訳（メタデータ） (2025-02-04T05:04:15Z) - Accelerated zero-order SGD under high-order smoothness and overparameterized regime [79.85163929026146]
凸最適化問題を解くための新しい勾配のないアルゴリズムを提案する。
このような問題は医学、物理学、機械学習で発生する。
両種類の雑音下で提案アルゴリズムの収束保証を行う。
論文 参考訳（メタデータ） (2024-11-21T10:26:17Z) - RUMBoost: Gradient Boosted Random Utility Models [0.0]
RUMBoostモデルは、ランダムユーティリティモデル(RUM)の解釈可能性と行動的堅牢性と、ディープラーニング手法の一般化と予測能力を組み合わせる。
本稿では,RUMBoostモデルとMLおよびRandom Utilityベンチマークモデルとの比較を行い,ロンドンの選好モード選択データについて検討した。
論文 参考訳（メタデータ） (2024-01-22T13:54:26Z) - Efficient Model-Free Exploration in Low-Rank MDPs [76.87340323826945]
低ランクマルコフ決定プロセスは、関数近似を持つRLに対して単純だが表現力のあるフレームワークを提供する。
既存のアルゴリズムは、(1)計算的に抽出可能であるか、または(2)制限的な統計的仮定に依存している。
提案手法は,低ランクMPPの探索のための最初の実証可能なサンプル効率アルゴリズムである。
論文 参考訳（メタデータ） (2023-07-08T15:41:48Z) - Reinforcement Learning from Partial Observation: Linear Function Approximation with Provable Sample Efficiency [111.83670279016599]
部分観察決定過程(POMDP)の無限観測および状態空間を用いた強化学習について検討した。
線形構造をもつPOMDPのクラスに対する部分可観測性と関数近似の最初の試みを行う。
論文 参考訳（メタデータ） (2022-04-20T21:15:38Z) - High-dimensional Functional Graphical Model Structure Learning via
Neighborhood Selection Approach [15.334392442475115]
機能的グラフィカルモデルの構造を推定するための近傍選択手法を提案する。
したがって、関数が無限次元であるときに存在しないような、明確に定義された精度作用素の必要性を回避することができる。
論文 参考訳（メタデータ） (2021-05-06T07:38:50Z) - Sinkhorn Natural Gradient for Generative Models [125.89871274202439]
本研究では,シンクホーンの発散による確率空間上の最も急降下法として機能するシンクホーン自然勾配(SiNG)アルゴリズムを提案する。
本稿では,SiNG の主要成分であるシンクホーン情報行列 (SIM) が明示的な表現を持ち,対数的スケールの複雑さを正確に評価できることを示す。
本実験では,SiNGと最先端のSGD型解法を定量的に比較し,その有効性と有効性を示す。
論文 参考訳（メタデータ） (2020-11-09T02:51:17Z) - The connections between Lyapunov functions for some optimization
algorithms and differential equations [0.0]
我々は、ネステロフ最適化手法の族に対する(離散的な)リャプノフ関数を解析的に導出する。
重球法のようなODEの族における典型的な離散化の大多数は、ここで構築されたリャプノフ関数に類似した性質を持つリャプノフ函数を持たないことを示す。
論文 参考訳（メタデータ） (2020-09-01T19:49:11Z) - Formal Synthesis of Lyapunov Neural Networks [61.79595926825511]
本稿では,リアプノフ関数の自動合成法を提案する。
我々は,数値学習者と記号検証器が相互作用して,確実に正しいリアプノフニューラルネットワークを構築する,反例誘導方式を採用する。
提案手法は,Lyapunov関数を他の手法よりも高速かつ広い空間領域で合成する。
論文 参考訳（メタデータ） (2020-03-19T17:21:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。