論文の概要: Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks (Extended Version)

• arxiv url: http://arxiv.org/abs/2003.07959v4
• Date: Thu, 25 Jun 2020 16:43:51 GMT
• ステータス: 処理完了
• システム内更新日: 2022-12-22 22:05:45.763410
• Title: Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks (Extended Version)
• Title（参考訳）: 拡張型連続論理ネットワークを用いた非線形ループ不変量の学習
• Authors: Jianan Yao, Gabriel Ryan, Justin Wong, Suman Jana, Ronghui Gu
• Abstract要約: 我々は、一般SMT学習のための新しいニューラルネットワーク、Gated Continuous Logic Network (G-CLN)を導入する。 G-CLNは継続論理ネットワーク(CLN)アーキテクチャを拡張し、ゲーティングユニットとドロップアウトを提供する。 G-CLNの収束率は2次問題に対して9.7.5%、CLNモデルに対して39.2%である。
• 参考スコア（独自算出の注目度）: 19.87276407545565
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Verifying real-world programs often requires inferring loop invariants with nonlinear constraints. This is especially true in programs that perform many numerical operations, such as control systems for avionics or industrial plants. Recently, data-driven methods for loop invariant inference have shown promise, especially on linear invariants. However, applying data-driven inference to nonlinear loop invariants is challenging due to the large numbers of and magnitudes of high-order terms, the potential for overfitting on a small number of samples, and the large space of possible inequality bounds. In this paper, we introduce a new neural architecture for general SMT learning, the Gated Continuous Logic Network (G-CLN), and apply it to nonlinear loop invariant learning. G-CLNs extend the Continuous Logic Network (CLN) architecture with gating units and dropout, which allow the model to robustly learn general invariants over large numbers of terms. To address overfitting that arises from finite program sampling, we introduce fractional sampling---a sound relaxation of loop semantics to continuous functions that facilitates unbounded sampling on real domain. We additionally design a new CLN activation function, the Piecewise Biased Quadratic Unit (PBQU), for naturally learning tight inequality bounds. We incorporate these methods into a nonlinear loop invariant inference system that can learn general nonlinear loop invariants. We evaluate our system on a benchmark of nonlinear loop invariants and show it solves 26 out of 27 problems, 3 more than prior work, with an average runtime of 53.3 seconds. We further demonstrate the generic learning ability of G-CLNs by solving all 124 problems in the linear Code2Inv benchmark. We also perform a quantitative stability evaluation and show G-CLNs have a convergence rate of $97.5\%$ on quadratic problems, a $39.2\%$ improvement over CLN models.
• Abstract（参考訳）: 実世界のプログラムを検証するには、非線形制約付きループ不変量の推定がしばしば必要となる。 これは、アビオニクスや工業プラントの制御システムなど、多くの数値演算を実行するプログラムにおいて特に当てはまる。 近年、ループ不変推論のためのデータ駆動手法は、特に線形不変量において有望であることが示されている。 しかし、非線形ループ不変量へのデータ駆動推論の適用は、高次項の多量および等級、少数のサンプルに過度に適合する可能性、および可能な不等式境界の広い空間のために困難である。 本稿では,一般smt学習のための新しいニューラルネットワークであるゲート型連続論理ネットワーク(g-cln)を導入し,非線形ループ不変学習に適用する。 G-CLNは継続論理ネットワーク(CLN)アーキテクチャを拡張し、ゲーティングユニットとドロップアウトにより、モデルが多数の用語で一般的な不変性をしっかりと学習できるようにする。 有限プログラムサンプリングから生じるオーバーフィッティングに対処するため,実領域での非有界サンプリングを容易にするループセマンティクスを連続関数に緩和する分数サンプリングを導入する。 さらに、我々は、厳密な不等式境界を自然に学習する新しいCLN活性化関数PBQU(Piecewise Biased Quadratic Unit)を設計する。 一般非線形ループ不変量の学習が可能な非線形ループ不変推論系にこれらの手法を組み込む。 非線形ループ不変量のベンチマークを用いてシステム評価を行い, 平均実行時間53.3秒で, 先行処理よりも3倍の27の問題を26個解決したことを示す。 線形Code2Invベンチマークの124問題を全て解き、G-CLNの汎用学習能力を更に示す。 また, 定量的安定度評価を行い, g-cln が二次問題に対して 97.5\%$, cln モデルより39.2\%$向上することを示す。

関連論文リスト

• Efficient Interpretable Nonlinear Modeling for Multiple Time Series [5.448070998907116]
  本稿では,複数時系列に対する効率的な非線形モデリング手法を提案する。 異なる時系列変数間の非線形相互作用を含む。 実験結果から,提案アルゴリズムは相似的にVAR係数の支持値の同定を改善することが示された。
  論文  参考訳（メタデータ） (2023-09-29T11:42:59Z)
• Constrained Optimization via Exact Augmented Lagrangian and Randomized Iterative Sketching [55.28394191394675]
  等式制約付き非線形非IBS最適化問題に対する適応的不正確なニュートン法を開発した。 ベンチマーク非線形問題,LVMのデータによる制約付きロジスティック回帰,PDE制約問題において,本手法の優れた性能を示す。
  論文  参考訳（メタデータ） (2023-05-28T06:33:37Z)
• A Fast Scale-Invariant Algorithm for Non-negative Least Squares with Non-negative Data [18.81091632124107]
  我々は、データ自体が非負であることを示し、この場合の非負性は問題を容易にすることを示した。 特に、制約のない最小二乗問題のオラクルの複雑さは、データ行列定数の1つで必ずスケールするが、非負のデータを含む非負の最小二乗問題は乗法誤差に解けることを示す。
  論文  参考訳（メタデータ） (2022-03-08T02:02:32Z)
• Towards Data-driven LQR with KoopmanizingFlows [8.133902705930327]
  本稿では,線形時間不変モデル(LTI)を連続時間非自律非線形力学のクラスで学習するための新しいフレームワークを提案する。 我々は、有意な持ち上げ座標を同時に学習しながら、制御において線形なクープマン作用素の有限表現を学習する。
  論文  参考訳（メタデータ） (2022-01-27T17:02:03Z)
• Training Recurrent Neural Networks by Sequential Least Squares and the Alternating Direction Method of Multipliers [0.20305676256390928]
  本稿では、最適隠れネットワークパラメータを決定するために凸と2倍の差分損失と正規化項を用いることを提案する。 逐次最小二乗と交互方向乗算器を組み合わせる。 このアルゴリズムの性能は非線形システム同定ベンチマークで検証される。
  論文  参考訳（メタデータ） (2021-12-31T08:43:04Z)
• The SKIM-FA Kernel: High-Dimensional Variable Selection and Nonlinear Interaction Discovery in Linear Time [26.11563787525079]
  変数選択と推定の両方において、カーネルのトリックが適切なベイズモデルによる計算をO(#共変量)時間に還元する方法を示す。 提案手法は,大規模で高次元なデータセットの既存の手法よりも優れている。
  論文  参考訳（メタデータ） (2021-06-23T13:53:36Z)
• Hybrid Trilinear and Bilinear Programming for Aligning Partially Overlapping Point Sets [85.71360365315128]
  多くの応用において、部分重なり合う点集合が対応するRPMアルゴリズムに不変であるようなアルゴリズムが必要である。 まず、目的が立方体有界関数であることを示し、次に、三線型および双線型単相変換の凸エンベロープを用いて、その下界を導出する。 次に、変換変数上の分岐のみを効率よく実行するブランチ・アンド・バウンド(BnB)アルゴリズムを開発する。
  論文  参考訳（メタデータ） (2021-01-19T04:24:23Z)
• Learning the Linear Quadratic Regulator from Nonlinear Observations [135.66883119468707]
  我々は、LQR with Rich Observations(RichLQR)と呼ばれる連続制御のための新しい問題設定を導入する。 本設定では, 線形力学と二次的コストを有する低次元連続潜伏状態によって環境を要約する。 本結果は,システムモデルと一般関数近似における未知の非線形性を持つ連続制御のための,最初の証明可能なサンプル複雑性保証である。
  論文  参考訳（メタデータ） (2020-10-08T07:02:47Z)
• Hardness of Random Optimization Problems for Boolean Circuits, Low-Degree Polynomials, and Langevin Dynamics [78.46689176407936]
  アルゴリズムの族は高い確率でほぼ最適な解を生成できないことを示す。 ブール回路の場合、回路複雑性理論で知られている最先端境界を改善する。
  論文  参考訳（メタデータ） (2020-04-25T05:45:59Z)
• Neural Networks are Convex Regularizers: Exact Polynomial-time Convex Optimization Formulations for Two-layer Networks [70.15611146583068]
  我々は、線形整列ユニット(ReLU)を用いた2層ニューラルネットワークのトレーニングの正確な表現を開発する。 我々の理論は半無限双対性と最小ノルム正規化を利用する。
  論文  参考訳（メタデータ） (2020-02-24T21:32:41Z)
• Multiscale Non-stationary Stochastic Bandits [83.48992319018147]
  本稿では,非定常線形帯域問題に対して,Multiscale-LinUCBと呼ばれる新しいマルチスケール変更点検出法を提案する。 実験結果から,提案手法は非定常環境下での他の最先端アルゴリズムよりも優れていた。
  論文  参考訳（メタデータ） (2020-02-13T00:24:17Z)

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

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