論文の概要: Fossil 2.0: Formal Certificate Synthesis for the Verification and
Control of Dynamical Models
- arxiv url: http://arxiv.org/abs/2311.09793v1
- Date: Thu, 16 Nov 2023 11:18:21 GMT
- ステータス: 処理完了
- システム内更新日: 2023-11-17 14:43:21.421336
- Title: Fossil 2.0: Formal Certificate Synthesis for the Verification and
Control of Dynamical Models
- Title(参考訳): Fossil 2.0: 動的モデルの検証と制御のための形式証明書合成
- Authors: Alec Edwards, Andrea Peruffo, Alessandro Abate
- Abstract要約: 本稿では,証明書を合成するソフトウェアツールの新たなメジャーリリースであるFossil 2.0について述べる。
Fossil 2.0は、新しいインターフェースと大幅に拡張された証明書ポートフォリオを含む、最初のリリースから大幅に改善されている。
- 参考スコア(独自算出の注目度): 60.03938402120854
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: This paper presents Fossil 2.0, a new major release of a software tool for
the synthesis of certificates (e.g., Lyapunov and barrier functions) for
dynamical systems modelled as ordinary differential and difference equations.
Fossil 2.0 is much improved from its original release, including new
interfaces, a significantly expanded certificate portfolio, controller
synthesis and enhanced extensibility. We present these new features as part of
this tool paper. Fossil implements a counterexample-guided inductive synthesis
(CEGIS) loop ensuring the soundness of the method. Our tool uses neural
networks as templates to generate candidate functions, which are then formally
proven by an SMT solver acting as an assertion verifier. Improvements with
respect to the first release include a wider range of certificates, synthesis
of control laws, and support for discrete-time models.
- Abstract(参考訳): 本稿では、通常の微分方程式と差分方程式をモデル化した力学系に対する証明(例えば、リャプノフとバリア関数)を合成するためのソフトウェアツールの新たなメジャーリリースであるFossil 2.0を提案する。
Fossil 2.0は、新しいインターフェース、大幅に拡張された証明書ポートフォリオ、コントローラ合成、拡張性など、最初のリリースから大幅に改善されている。
このツールペーパーの一部として,これらの新機能を紹介する。
Fossilは、その方法の音質を保証する反例誘導誘導合成(CEGIS)ループを実装している。
提案ツールでは,ニューラルネットワークをテンプレートとして,アサーション検証を行うSMTソルバによって正式に証明された候補関数を生成する。
最初のリリースに関する改善には、幅広い証明書、制御法則の合成、離散時間モデルのサポートが含まれる。
関連論文リスト
- CAR: Controllable Autoregressive Modeling for Visual Generation [100.33455832783416]
Controllable AutoRegressive Modeling (CAR)は、条件制御をマルチスケールの潜在変数モデリングに統合する新しいプラグイン・アンド・プレイフレームワークである。
CARは、制御表現を徐々に洗練し、キャプチャし、前訓練されたモデルの各自己回帰ステップに注入して生成プロセスを導く。
提案手法は,様々な条件にまたがって優れた制御性を示し,従来の手法に比べて画質の向上を実現している。
論文 参考訳(メタデータ) (2024-10-07T00:55:42Z) - Random Features Approximation for Control-Affine Systems [6.067043299145924]
制御アフィン構造をキャプチャする非線形特徴表現の2つの新しいクラスを提案する。
提案手法はランダムな特徴(RF)近似を用いて,より少ない計算コストでカーネル手法の表現性を継承する。
論文 参考訳(メタデータ) (2024-06-10T17:54:57Z) - FAENet: Frame Averaging Equivariant GNN for Materials Modeling [123.19473575281357]
データ変換による任意のモデルE(3)-同変や不変化を実現するために,フレームアラグリング(SFA)に依存したフレキシブルなフレームワークを導入する。
本手法の有効性を理論的および実験的に証明し, 材料モデリングにおける精度と計算スケーラビリティを実証する。
論文 参考訳(メタデータ) (2023-04-28T21:48:31Z) - Controllable Text Generation with Neurally-Decomposed Oracle [91.18959622763055]
我々はNeurAlly-Decomposed Oracle (NADO) を用いた自動回帰生成モデルを制御するフレームワークを提案する。
制御可能な生成のためのベースモデルにトークンレベルのガイダンスを組み込むためのクローズドフォーム最適解を提案する。
論文 参考訳(メタデータ) (2022-05-27T20:17:53Z) - Better Feature Integration for Named Entity Recognition [30.676768644145]
両タイプの機能をSynergized-LSTM(Syn-LSTM)に組み込むためのシンプルで堅牢なソリューションを提案する。
その結果、提案モデルが従来のアプローチよりも優れたパフォーマンスを実現し、パラメータを少なくできることが示された。
論文 参考訳(メタデータ) (2021-04-12T09:55:06Z) - AILearn: An Adaptive Incremental Learning Model for Spoof Fingerprint
Detection [12.676356746752893]
増分学習により、学習者は既存のモデルを再訓練することなく、新しい知識を学べる。
安定可塑性ジレンマを克服したインクリメンタル学習の汎用モデル AILearn を提案する。
提案したAILearnモデルがスポフ指紋検出アプリケーションに有効であることを実証する。
論文 参考訳(メタデータ) (2020-12-29T07:26:37Z) - Automated and Formal Synthesis of Neural Barrier Certificates for
Dynamical Models [70.70479436076238]
バリア証明書(BC)の自動的,形式的,反例に基づく合成手法を提案する。
このアプローチは、ニューラルネットワークとして構造化されたBCの候補を操作する誘導的フレームワークと、その候補の有効性を認証するか、反例を生成する音検証器によって支えられている。
その結果,音のBCsを最大2桁の速度で合成できることがわかった。
論文 参考訳(メタデータ) (2020-07-07T07:39:42Z) - Formal Synthesis of Lyapunov Neural Networks [61.79595926825511]
本稿では,リアプノフ関数の自動合成法を提案する。
我々は,数値学習者と記号検証器が相互作用して,確実に正しいリアプノフニューラルネットワークを構築する,反例誘導方式を採用する。
提案手法は,Lyapunov関数を他の手法よりも高速かつ広い空間領域で合成する。
論文 参考訳(メタデータ) (2020-03-19T17:21:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。