論文の概要: NeuRes: Learning Proofs of Propositional Satisfiability
- arxiv url: http://arxiv.org/abs/2402.08365v1
- Date: Tue, 13 Feb 2024 10:50:54 GMT
- ステータス: 処理完了
- システム内更新日: 2024-02-14 15:39:40.002112
- Title: NeuRes: Learning Proofs of Propositional Satisfiability
- Title(参考訳): NeuRes: 提案的満足性の学習証明
- Authors: Mohamed Ghanem, Frederik Schmitt, Julian Siber, Bernd Finkbeiner
- Abstract要約: 本稿ではニューロシンボリック証明に基づくSATソルバであるNeuResを紹介する。
設計上、NeuResは不満足さを証明するために命題解決を用いて証明書駆動方式で動作している。
我々は,NeuResが有意な割合で教師の証明を大幅に短縮できることを示した。
- 参考スコア(独自算出の注目度): 8.138288420049127
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We introduce NeuRes, a neuro-symbolic proof-based SAT solver. Unlike other
neural SAT solving methods, NeuRes is capable of proving unsatisfiability as
opposed to merely predicting it. By design, NeuRes operates in a
certificate-driven fashion by employing propositional resolution to prove
unsatisfiability and to accelerate the process of finding satisfying truth
assignments in case of unsat and sat formulas, respectively. To realize this,
we propose a novel architecture that adapts elements from Graph Neural Networks
and Pointer Networks to autoregressively select pairs of nodes from a dynamic
graph structure, which is essential to the generation of resolution proofs. Our
model is trained and evaluated on a dataset of teacher proofs and truth
assignments that we compiled with the same random formula distribution used by
NeuroSAT. In our experiments, we show that NeuRes solves more test formulas
than NeuroSAT by a rather wide margin on different distributions while being
much more data-efficient. Furthermore, we show that NeuRes is capable of
largely shortening teacher proofs by notable proportions. We use this feature
to devise a bootstrapped training procedure that manages to reduce a dataset of
proofs generated by an advanced solver by ~23% after training on it with no
extra guidance.
- Abstract(参考訳): 本稿ではニューロシンボリック証明に基づくSATソルバであるNeuResを紹介する。
他の神経SATの解法とは異なり、NeuResは単に予測するのではなく、満足できないことを証明できる。
設計により、neures は命題解決法を用いて不満足を証明し、unsat と sat の式をそれぞれ満たした真理割当を見つけるプロセスを加速することにより、証明書駆動で動作する。
これを実現するために,グラフニューラルネットワークとポインタネットワークの要素を適応させ,動的グラフ構造からノードのペアを自動回帰的に選択するアーキテクチャを提案する。
我々は,NeuroSATと同じランダムな公式分布を用いて,教師の証明と真理の割り当てのデータセットを用いて,学習と評価を行った。
我々の実験では、NeuResはNuroSATよりも多くのテスト式を、よりデータ効率のよい異なる分布に対してより広いマージンで解決することを示した。
さらに,NeuResは教師の証明を顕著に短縮できることを示した。
この機能を使用してブートストラップされたトレーニング手順を考案し、アドバンストソルバが生成した証明のデータセットを、追加のガイダンスなしでトレーニング後に約23%削減します。
関連論文リスト
- Learning a Neuron by a Shallow ReLU Network: Dynamics and Implicit Bias
for Correlated Inputs [5.7166378791349315]
我々は、単一ニューロンを学習する基本的な回帰タスクとして、1つの隠れた層ReLUネットワークをトレーニングすると、損失がゼロとなることを証明した。
また、最小ランクの補間ネットワークと最小ユークリッドノルムの補間ネットワークのこの設定において、驚くべき区別を示し、特徴付ける。
論文 参考訳(メタデータ) (2023-06-10T16:36:22Z) - ResMem: Learn what you can and memorize the rest [79.19649788662511]
本稿では,既存の予測モデルを拡張するための残差記憶アルゴリズム(ResMem)を提案する。
構築によって、ResMemはトレーニングラベルを明示的に記憶することができる。
ResMemは、元の予測モデルのテストセットの一般化を一貫して改善することを示す。
論文 参考訳(メタデータ) (2023-02-03T07:12:55Z) - Boosting Low-Data Instance Segmentation by Unsupervised Pre-training
with Saliency Prompt [103.58323875748427]
この研究は、低データ体制のための新しい教師なし事前学習ソリューションを提供する。
近年のPrompting技術の成功に触発されて,QEISモデルを強化した新しい事前学習手法を導入する。
実験結果から,本手法は3つのデータセット上でのいくつかのQEISモデルを大幅に向上させることが示された。
論文 参考訳(メタデータ) (2023-02-02T15:49:03Z) - Sample-based Uncertainty Quantification with a Single Deterministic
Neural Network [4.7210697296108926]
より安定かつスムーズなトレーニングを実現するために,disCOネットのニューラルネットワークの改良を提案する。
本稿では,エネルギースコアを用いた予測分布の学習の有効性に関する基礎的証明を提案する。
論文 参考訳(メタデータ) (2022-09-17T22:37:39Z) - Can pruning improve certified robustness of neural networks? [106.03070538582222]
ニューラルネット・プルーニングはディープ・ニューラル・ネットワーク(NN)の実証的ロバスト性を向上させることができることを示す。
実験の結果,NNを適切に刈り取ることで,その精度を8.2%まで向上させることができることがわかった。
さらに,認証された宝くじの存在が,従来の密集モデルの標準および認証された堅牢な精度に一致することを観察する。
論文 参考訳(メタデータ) (2022-06-15T05:48:51Z) - NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks [13.185943308470286]
提案的満足度(SAT)は、計画、検証、セキュリティなど、多くの研究分野に影響を与えるNP完全問題である。
グラフニューラルネットワーク(GNN)を用いたCDCL SATソルバの高速化に向けた最近の研究
本稿では,(1)CDCL SATの解法に必要不可欠である変数の位相(すなわち値)を予測すること,(2)SATの解法開始前に1回だけニューラルネットワークに問い合わせること,の2つの知見に基づくNeuroBackという手法を提案する。
論文 参考訳(メタデータ) (2021-10-26T22:08:22Z) - Training Feedback Spiking Neural Networks by Implicit Differentiation on
the Equilibrium State [66.2457134675891]
スパイキングニューラルネットワーク(英: Spiking Neural Network、SNN)は、ニューロモルフィックハードウェア上でエネルギー効率の高い実装を可能にする脳にインスパイアされたモデルである。
既存のほとんどの手法は、人工ニューラルネットワークのバックプロパゲーションフレームワークとフィードフォワードアーキテクチャを模倣している。
本稿では,フォワード計算の正逆性に依存しない新しいトレーニング手法を提案する。
論文 参考訳(メタデータ) (2021-09-29T07:46:54Z) - Less is More: Data-Efficient Complex Question Answering over Knowledge
Bases [26.026065844896465]
本稿では,複雑な質問応答のためのデータ効率向上学習フレームワークであるNS-CQAモデルを提案する。
我々のフレームワークはニューラルジェネレータとシンボリックエグゼキュータで構成されており、自然言語の質問を原始的なアクションのシーケンスに変換する。
近年の大規模質問応答データセットであるCQAと,マルチホップ質問応答データセットであるWebQuestionsSPの2つのデータセットで評価を行った。
論文 参考訳(メタデータ) (2020-10-29T18:42:44Z) - Enhancing SAT solvers with glue variable predictions [2.635832975589208]
我々は、最先端のSATソルバであるCaDiCaLを改良し、SATCOMP 2018とSATRACE 2019のパフォーマンスを改善し、教師付き学習と強化学習によるSHA-1プレイメージアタックのデータセット上でのパフォーマンスを向上する。
我々はこれらの制限に対処し、より単純なネットワークアーキテクチャを用いて、数百万の節を含む大規模産業問題に対してCPU推論を行い、代わりにエミュレート変数を予測する訓練を行い、ラベル付きデータを簡単に生成し、強化学習タスクとして定式化することができる。
論文 参考訳(メタデータ) (2020-07-06T07:16:49Z) - Modeling from Features: a Mean-field Framework for Over-parameterized
Deep Neural Networks [54.27962244835622]
本稿では、オーバーパラメータ化ディープニューラルネットワーク(DNN)のための新しい平均場フレームワークを提案する。
このフレームワークでは、DNNは連続的な極限におけるその特徴に対する確率測度と関数によって表現される。
本稿では、標準DNNとResidual Network(Res-Net)アーキテクチャを通してフレームワークを説明する。
論文 参考訳(メタデータ) (2020-07-03T01:37:16Z) - Non-linear Neurons with Human-like Apical Dendrite Activations [81.18416067005538]
XOR論理関数を100%精度で学習し, 標準的なニューロンに後続のアピーカルデンドライト活性化(ADA)が認められた。
コンピュータビジョン,信号処理,自然言語処理の6つのベンチマークデータセットについて実験を行った。
論文 参考訳(メタデータ) (2020-02-02T21:09:39Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。