論文の概要: Formal Synthesis of Lyapunov Neural Networks

• arxiv url: http://arxiv.org/abs/2003.08910v2
• Date: Wed, 24 Jun 2020 16:33:17 GMT
• ステータス: 処理完了
• システム内更新日: 2022-12-22 05:05:55.579102
• Title: Formal Synthesis of Lyapunov Neural Networks
• Title（参考訳）: リアプノフニューラルネットワークの形式的合成
• Authors: Alessandro Abate, Daniele Ahmed, Mirco Giacobbe, and Andrea Peruffo
• Abstract要約: 本稿では,リアプノフ関数の自動合成法を提案する。 我々は,数値学習者と記号検証器が相互作用して,確実に正しいリアプノフニューラルネットワークを構築する,反例誘導方式を採用する。 提案手法は,Lyapunov関数を他の手法よりも高速かつ広い空間領域で合成する。
• 参考スコア（独自算出の注目度）: 61.79595926825511
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We propose an automatic and formally sound method for synthesising Lyapunov functions for the asymptotic stability of autonomous non-linear systems. Traditional methods are either analytical and require manual effort or are numerical but lack of formal soundness. Symbolic computational methods for Lyapunov functions, which are in between, give formal guarantees but are typically semi-automatic because they rely on the user to provide appropriate function templates. We propose a method that finds Lyapunov functions fully automatically$-$using machine learning$-$while also providing formal guarantees$-$using satisfiability modulo theories (SMT). We employ a counterexample-guided approach where a numerical learner and a symbolic verifier interact to construct provably correct Lyapunov neural networks (LNNs). The learner trains a neural network that satisfies the Lyapunov criteria for asymptotic stability over a samples set; the verifier proves via SMT solving that the criteria are satisfied over the whole domain or augments the samples set with counterexamples. Our method supports neural networks with polynomial activation functions and multiple depth and width, which display wide learning capabilities. We demonstrate our method over several non-trivial benchmarks and compare it favourably against a numerical optimisation-based approach, a symbolic template-based approach, and a cognate LNN-based approach. Our method synthesises Lyapunov functions faster and over wider spatial domains than the alternatives, yet providing stronger or equal guarantees.
• Abstract（参考訳）: 本稿では,自律非線形システムの漸近安定性に対するリアプノフ関数の自動合成法を提案する。 伝統的な手法は分析的であり、手作業を必要とするか、数値的だが形式的な健全性が欠けている。 Lyapunov関数のシンボリック計算法は、その間に形式的な保証を与えるが、一般的には、適切な関数テンプレートを提供するためにユーザに依存するため、半オートマチックである。 本稿では,Lyapunov関数を完全自動で$$using machine learning$-$whileと,形式的な保証として$-$using satisfiability modulo theory (SMT)を提案する。 我々は,数値学習者と記号検証器が相互作用して,確実に正しいリアプノフニューラルネットワーク(LNN)を構築する,反例誘導方式を採用する。 学習者は、サンプルセットに対する漸近安定性に対するリアプノフ基準を満たすニューラルネットワークを訓練し、検証者はSMTにより、基準がドメイン全体にわたって満たされていること、あるいはサンプルセットを反例で拡張していることを証明する。 提案手法は,多項式の活性化機能と深度と幅が広いニューラルネットワークをサポートし,広い学習能力を示す。 提案手法をいくつかの非自明なベンチマークで実証し、数値最適化に基づくアプローチ、シンボリックテンプレートベースのアプローチ、コグネートLNNベースのアプローチと比較した。 提案手法は,Lyapunov関数を他の手法よりも高速かつ広い空間領域で合成する。

関連論文リスト

• The Convex Landscape of Neural Networks: Characterizing Global Optima and Stationary Points via Lasso Models [75.33431791218302]
  ディープニューラルネットワーク(DNN)モデルは、プログラミング目的に使用される。 本稿では,凸型神経回復モデルについて検討する。 定常的非次元目的物はすべて,グローバルサブサンプリング型凸解法プログラムとして特徴付けられることを示す。 また, 静止非次元目的物はすべて, グローバルサブサンプリング型凸解法プログラムとして特徴付けられることを示す。
  論文  参考訳（メタデータ） (2023-12-19T23:04:56Z)
• GloptiNets: Scalable Non-Convex Optimization with Certificates [61.50835040805378]
  本稿では,ハイパーキューブやトーラス上のスムーズな関数を扱う証明書を用いた非キューブ最適化手法を提案する。 スペクトルの減衰に固有の対象関数の正則性を活用することにより、正確な証明を取得し、高度で強力なニューラルネットワークを活用することができる。
  論文  参考訳（メタデータ） (2023-06-26T09:42:59Z)
• Gauss-Newton Temporal Difference Learning with Nonlinear Function Approximation [11.925232472331494]
  非線形関数近似を用いたQラーニング問題を解くため,ガウスニュートン時間差分法(GNTD)学習法を提案する。 各イテレーションにおいて、我々の手法は1つのガウスニュートン(GN)ステップを踏んで平均二乗ベルマン誤差(MSBE)の変種を最適化する。 いくつかのRLベンチマークにおいて、GNTDはTD型よりも高い報酬と高速な収束を示す。
  論文  参考訳（メタデータ） (2023-02-25T14:14:01Z)
• UNIPoint: Universally Approximating Point Processes Intensities [125.08205865536577]
  学習可能な関数のクラスが任意の有効な強度関数を普遍的に近似できることを示す。 ニューラルポイントプロセスモデルであるUNIPointを実装し,各イベントの基底関数の和をパラメータ化するために,リカレントニューラルネットワークを用いた。
  論文  参考訳（メタデータ） (2020-07-28T09:31:56Z)
• Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers [70.70479436076238]
  線形、非線形(ポリノミカル)およびパラメトリックモデルに対するリャプノフ関数を合成する。 パラメトリックテンプレートからLyapunov関数を合成するための帰納的フレームワークを利用する。
  論文  参考訳（メタデータ） (2020-07-21T14:45:23Z)
• Provably Efficient Neural Estimation of Structural Equation Model: An Adversarial Approach [144.21892195917758]
  一般化構造方程式モデル(SEM)のクラスにおける推定について検討する。 線形作用素方程式をmin-maxゲームとして定式化し、ニューラルネットワーク(NN)でパラメータ化し、勾配勾配を用いてニューラルネットワークのパラメータを学習する。 提案手法は,サンプル分割を必要とせず,確固とした収束性を持つNNをベースとしたSEMの抽出可能な推定手順を初めて提供する。
  論文  参考訳（メタデータ） (2020-07-02T17:55:47Z)
• Stable Neural Flows [15.318500611972441]
  ニューラルネットワークによってパラメータ化されたエネルギー汎関数上で軌道が進化するニューラル常微分方程式(ニューラルODE)の確率的に安定な変種を導入する。 学習手順は最適制御問題としてキャストされ、随伴感性分析に基づいて近似解が提案される。
  論文  参考訳（メタデータ） (2020-03-18T06:27:21Z)
• CounterExample Guided Neural Synthesis [12.742347465894586]
  プログラム合成は困難であり、形式的な保証を提供する方法はスケーラビリティの問題に悩まされる。 ニューラルネットワークとフォーマルな推論を組み合わせることで、論理的な仕様をニューラルネットワークを正しい解へと導く一連の例に変換する。 この結果から,形式的推論に基づくガイダンスにより,ニューラルネットワークの性能が大幅に向上することが示唆された。
  論文  参考訳（メタデータ） (2020-01-25T01:11:53Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。