論文の概要: Constrained Training of Neural Networks via Theorem Proving
- arxiv url: http://arxiv.org/abs/2207.03880v1
- Date: Fri, 8 Jul 2022 13:13:51 GMT
- ステータス: 処理完了
- システム内更新日: 2022-07-11 13:32:41.420114
- Title: Constrained Training of Neural Networks via Theorem Proving
- Title（参考訳）: 定理証明によるニューラルネットワークの制約付きトレーニング
- Authors: Mark Chevallier, Matthew Whyte and Jacques D. Fleuriot
- Abstract要約: 有限トレース上の線形時間論理の深い埋め込み(LTL$_f$)を定式化する。
次に、損失関数 $mathcalL$ を形式化し、その関数 $dmathcalL$ に微分可能であることを正式に証明する。
本研究では,動的運動のための既存のディープラーニングフレームワークのトレーニングに使用する場合,共通の運動仕様パターンに対する予測結果が得られたことを示す。
- 参考スコア（独自算出の注目度）: 0.2578242050187029
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We introduce a theorem proving approach to the specification and generation
of temporal logical constraints for training neural networks. We formalise a
deep embedding of linear temporal logic over finite traces (LTL$_f$) and an
associated evaluation function characterising its semantics within the
higher-order logic of the Isabelle theorem prover. We then proceed to formalise
a loss function $\mathcal{L}$ that we formally prove to be sound, and
differentiable to a function $d\mathcal{L}$. We subsequently use Isabelle's
automatic code generation mechanism to produce OCaml versions of LTL$_f$,
$\mathcal{L}$ and $d\mathcal{L}$ that we integrate with PyTorch via OCaml
bindings for Python. We show that, when used for training in an existing deep
learning framework for dynamic movement, our approach produces expected results
for common movement specification patterns such as obstacle avoidance and
patrolling. The distinctive benefit of our approach is the fully rigorous
method for constrained training, eliminating many of the risks inherent to
ad-hoc implementations of logical aspects directly in an "unsafe" programming
language such as Python.
- Abstract（参考訳）: ニューラルネットワークのトレーニングのための時間的論理的制約の仕様と生成に対する定理証明アプローチを導入する。
有限トレース(LTL$_f$)上の線形時間論理の深い埋め込みと、その意味をイザベル定理証明器の高階論理内で特徴づける関連する評価関数を定式化する。
次に、損失関数 $\mathcal{L}$ を形式化し、その関数 $d\mathcal{L}$ に微分可能であることを正式に証明する。
その後、イザベルの自動コード生成メカニズムを使ってltl$_f$、$\mathcal{l}$、$d\mathcal{l}$のocamlバージョンを作成し、pythonのocamlバインディングを介してpytorchと統合しました。
本研究では,動的運動のための既存のディープラーニングフレームワークのトレーニングに使用すると,障害物回避やパトロールといった共通の運動仕様パターンに対する予測結果が得られることを示す。
このアプローチの独特な利点は、Pythonのような"安全でない"プログラミング言語で論理的側面のアドホックな実装に固有の多くのリスクを排除し、制約付きトレーニングの厳密な方法である。
関連論文リスト
- The Sample Complexity of Online Reinforcement Learning: A Multi-model Perspective [55.15192437680943]
連続状態と行動空間を持つ非線形力学系に対するオンライン強化学習のサンプル複雑性について検討した。
我々のアルゴリズムは、その単純さ、事前知識を組み込む能力、そして良心的な過渡的行動のために、実際に有用である可能性が高い。
論文 参考訳（メタデータ） (2025-01-27T10:01:28Z) - Formally Verified Neurosymbolic Trajectory Learning via Tensor-based Linear Temporal Logic on Finite Traces [0.0]
有限トレース(LTLf)上の線形時間論理に対するテンソル意味論の新しい形式化を提案する。
我々は,この形式化を,制約に対する識別可能な損失関数の定義と検証によって,ニューロシンボリック学習プロセスに統合できることを実証した。
この損失を利用して、プロセスは事前に特定された論理的制約を満たすことを学ぶ。
論文 参考訳（メタデータ） (2025-01-23T14:43:12Z) - Robust Stochastically-Descending Unrolled Networks [85.6993263983062]
Deep Unrolling(ディープ・アンローリング)は、トレーニング可能なニューラルネットワークの層に切り捨てられた反復アルゴリズムをアンロールする、新たな学習最適化手法である。
アンロールネットワークの収束保証と一般化性は、いまだにオープンな理論上の問題であることを示す。
提案した制約の下で訓練されたアンロールアーキテクチャを2つの異なるアプリケーションで数値的に評価する。
論文 参考訳（メタデータ） (2023-12-25T18:51:23Z) - Robust Training and Verification of Implicit Neural Networks: A
Non-Euclidean Contractive Approach [64.23331120621118]
本稿では,暗黙的ニューラルネットワークのトレーニングとロバスト性検証のための理論的および計算的枠組みを提案する。
組込みネットワークを導入し、組込みネットワークを用いて、元のネットワークの到達可能な集合の超近似として$ell_infty$-normボックスを提供することを示す。
MNISTデータセット上で暗黙的なニューラルネットワークをトレーニングするためにアルゴリズムを適用し、我々のモデルの堅牢性と、文献における既存のアプローチを通じてトレーニングされたモデルを比較する。
論文 参考訳（メタデータ） (2022-08-08T03:13:24Z) - Learning Finite Linear Temporal Logic Specifications with a Specialized
Neural Operator [0.0]
本稿では,システム動作のラベル付きトレースから,コンパクトな$mathsfLTL_f$式を学習する問題に対処する。
提案手法は, 時間演算子$mathsfLTL_f$をサブスクライブする特殊リカレントフィルタを含む。
ランダムに生成された$mathsfLTL_f$式の実験は、既存の手法よりも大きな公式サイズにスケールしたNeural$mathsfLTL_f$を示す。
論文 参考訳（メタデータ） (2021-11-07T18:51:02Z) - Skew Orthogonal Convolutions [44.053067014796596]
Lipschitzの制約付き畳み込みニューラルネットワークを$l_2$ノルムでトレーニングすることは、証明可能な対逆ロバスト性、解釈可能な勾配、安定したトレーニングなどに有用である。
Methodabvは、従来の作業よりもはるかに高速な大きな畳み込みニューラルネットワークであるLipschitzのトレーニングを可能にする。
論文 参考訳（メタデータ） (2021-05-24T17:11:44Z) - Reinforcement Learning with External Knowledge by using Logical Neural
Networks [67.46162586940905]
論理ニューラルネットワーク(LNN)と呼ばれる最近のニューラルシンボリックフレームワークは、ニューラルネットワークとシンボリックロジックの両方のキープロパティを同時に提供することができる。
外部知識ソースからのモデルフリー強化学習を可能にする統合手法を提案する。
論文 参考訳（メタデータ） (2021-03-03T12:34:59Z) - Learning Sign-Constrained Support Vector Machines [0.24466725954625884]
符号制約下で経験的リスクを最小化するための2つの最適化アルゴリズムを開発した。
2つのアルゴリズムのうちの1つは、投影勾配法に基づいており、投影勾配法の各イテレーションは計算コストが$o(nd)である。
訓練例と類似性が特徴ベクトルを構成する場合,符号制約が有望な手法であることを実証する。
論文 参考訳（メタデータ） (2021-01-05T12:08:17Z) - On Function Approximation in Reinforcement Learning: Optimism in the
Face of Large State Spaces [208.67848059021915]
強化学習のコアにおける探索・探索トレードオフについて検討する。
特に、関数クラス $mathcalF$ の複雑さが関数の複雑さを特徴づけていることを証明する。
私たちの後悔の限界はエピソードの数とは無関係です。
論文 参考訳（メタデータ） (2020-11-09T18:32:22Z) - Deep neural networks for inverse problems with pseudodifferential
operators: an application to limited-angle tomography [0.4110409960377149]
線形逆問題において擬微分演算子(Psi$DOs)を学習するための新しい畳み込みニューラルネットワーク(CNN)を提案する。
フォワード演算子のより一般的な仮定の下では、ISTAの展開された反復はCNNの逐次的な層として解釈できることを示す。
特に、LA-CTの場合、アップスケーリング、ダウンスケーリング、畳み込みの操作は、制限角X線変換の畳み込み特性とウェーブレット系を定義する基本特性を組み合わせることで正確に決定できることを示す。
論文 参考訳（メタデータ） (2020-06-02T14:03:41Z) - Stochastic Flows and Geometric Optimization on the Orthogonal Group [52.50121190744979]
直交群 $O(d)$ 上の幾何駆動最適化アルゴリズムの新しいクラスを示す。
提案手法は,深層,畳み込み,反復的なニューラルネットワーク,強化学習,フロー,メトリック学習など,機械学習のさまざまな分野に適用可能であることを示す。
論文 参考訳（メタデータ） (2020-03-30T15:37:50Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。