論文の概要: 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次元モデルにスケールするだけでなく, 生成したリアプノフ関数とその有効領域に対する新しい音響性証明を提供することを示す。
関連論文リスト
- 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) - FAENet: Frame Averaging Equivariant GNN for Materials Modeling [123.19473575281357]
データ変換による任意のモデルE(3)-同変や不変化を実現するために,フレームアラグリング(SFA)に依存したフレキシブルなフレームワークを導入する。
本手法の有効性を理論的および実験的に証明し, 材料モデリングにおける精度と計算スケーラビリティを実証する。
論文 参考訳(メタデータ) (2023-04-28T21:48:31Z) - Third quantization of open quantum systems: new dissipative symmetries
and connections to phase-space and Keldysh field theory formulations [77.34726150561087]
3つの方法全てを明示的に接続する方法で第3量子化の手法を再構成する。
まず、我々の定式化は、すべての二次ボゾンあるいはフェルミオンリンドブラディアンに存在する基本散逸対称性を明らかにする。
ボソンに対して、ウィグナー関数と特徴関数は密度行列の「波動関数」と考えることができる。
論文 参考訳(メタデータ) (2023-02-27T18:56:40Z) - Learning and Inference in Sparse Coding Models with Langevin Dynamics [3.0600309122672726]
本稿では確率的潜在変数モデルで推論と学習が可能なシステムについて述べる。
ランゲヴィン力学を用いて潜伏変数を推論する連続時間方程式を導出することにより、スパース符号化モデルのこのアイデアを実証する。
ランゲヴィン力学は、L1ノルムが小さいのに対して、潜伏変数をゼロにすることを推奨する'L0スパース'系において、後続分布からサンプリングする効率的な手順をもたらすことを示す。
論文 参考訳(メタデータ) (2022-04-23T23:16:47Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。