論文の概要: 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%削減します。

関連論文リスト

• Rethinking Classifier Re-Training in Long-Tailed Recognition: A Simple Logits Retargeting Approach [102.0769560460338]
  我々は,クラスごとのサンプル数に関する事前知識を必要とせず,シンプルなロジットアプローチ(LORT)を開発した。 提案手法は,CIFAR100-LT, ImageNet-LT, iNaturalist 2018など,様々な不均衡データセットの最先端性能を実現する。
  論文  参考訳（メタデータ） (2024-03-01T03:27:08Z)
• Boosting Low-Data Instance Segmentation by Unsupervised Pre-training with Saliency Prompt [103.58323875748427]
  この研究は、低データ体制のための新しい教師なし事前学習ソリューションを提供する。 近年のPrompting技術の成功に触発されて,QEISモデルを強化した新しい事前学習手法を導入する。 実験結果から,本手法は3つのデータセット上でのいくつかのQEISモデルを大幅に向上させることが示された。
  論文  参考訳（メタデータ） (2023-02-02T15:49:03Z)
• HyperImpute: Generalized Iterative Imputation with Automatic Model Selection [77.86861638371926]
  カラムワイズモデルを適応的かつ自動的に構成するための一般化反復計算フレームワークを提案する。 既製の学習者,シミュレータ,インターフェースを備えた具体的な実装を提供する。
  論文  参考訳（メタデータ） (2022-06-15T19:10:35Z)
• CAFA: Class-Aware Feature Alignment for Test-Time Adaptation [50.26963784271912]
  テスト時間適応(TTA)は、テスト時にラベルのないデータにモデルを適応させることによって、この問題に対処することを目的としている。 本稿では,クラス認識特徴アライメント(CAFA, Class-Aware Feature Alignment)と呼ばれる単純な機能アライメント損失を提案する。
  論文  参考訳（メタデータ） (2022-06-01T03:02:07Z)
• Training Data Subset Selection for Regression with Controlled Generalization Error [19.21682938684508]
  そこで我々は,データサブセット選択のための効率的な大規模化最小化アルゴリズムを開発した。 SELCONは、現在の最先端技術よりも精度と効率を効果的に交換する。
  論文  参考訳（メタデータ） (2021-06-23T16:03:55Z)
• BiFair: Training Fair Models with Bilevel Optimization [8.2509884277533]
  我々は,ユーティリティの最小化と公正な関心の喪失を両立させる,BiFairという新しいトレーニングアルゴリズムを開発した。 我々のアルゴリズムは、常により良い性能、すなわち、与えられた公正度メトリックのより優れた値、あるいはより高い精度で到達する。
  論文  参考訳（メタデータ） (2021-06-03T22:36:17Z)
• Less is More: Data-Efficient Complex Question Answering over Knowledge Bases [26.026065844896465]
  本稿では,複雑な質問応答のためのデータ効率向上学習フレームワークであるNS-CQAモデルを提案する。 我々のフレームワークはニューラルジェネレータとシンボリックエグゼキュータで構成されており、自然言語の質問を原始的なアクションのシーケンスに変換する。 近年の大規模質問応答データセットであるCQAと,マルチホップ質問応答データセットであるWebQuestionsSPの2つのデータセットで評価を行った。
  論文  参考訳（メタデータ） (2020-10-29T18:42:44Z)
• Modeling Token-level Uncertainty to Learn Unknown Concepts in SLU via Calibrated Dirichlet Prior RNN [98.4713940310056]
  現代パーソナルアシスタントにおける音声言語理解(SLU)の主な課題は、発話から意味概念を抽出することである。 最近の研究では、疑問と回答を収集し、未知のデータを学習し、質問すべきである。 疑わしい監督なしにシーケンスの不確かさをモデル化するために、ソフトマックスベースのスロット充填ニューラルネットワークアーキテクチャを組み込んだ。
  論文  参考訳（メタデータ） (2020-10-16T02:12:30Z)
• A Neural Network Approach for Online Nonlinear Neyman-Pearson Classification [3.6144103736375857]
  論文の中では,オンラインと非線形の両方で初となる新しいNeyman-Pearson(NP)分類器を提案する。 提案する分類器は、オンライン方式でバイナリラベル付きデータストリーム上で動作し、ユーザが指定し、制御可能な偽陽性率の検出能力を最大化する。 提案アルゴリズムは大規模データアプリケーションに適しており,実時間処理による偽陽性率制御性を実現している。
  論文  参考訳（メタデータ） (2020-06-14T20:00:25Z)
• The Right Tool for the Job: Matching Model and Instance Complexities [62.95183777679024]
  NLPモデルが大きくなればなるほど、訓練されたモデルを実行するには、金銭的・環境的なコストを発生させる重要な計算資源が必要である。 我々は、推論中、早期(かつ高速)の"exit"を可能にする文脈表現微調整の修正を提案する。 3つのテキスト分類データセットと2つの自然言語推論ベンチマークの2つのタスクで、5つの異なるデータセットに対して提案した修正を検証した。
  論文  参考訳（メタデータ） (2020-04-16T04:28:08Z)
• PrIU: A Provenance-Based Approach for Incrementally Updating Regression Models [9.496524884855559]
  本稿では,予測精度を犠牲にすることなく,モデルパラメータを漸進的に更新する手法PrIUを提案する。 漸進的に更新されたモデルパラメータの正しさと収束性を証明し、実験的に検証する。 実験結果から, PrIU-optはスクラッチからモデルを再トレーニングするのに対して, 非常に類似したモデルを得るよりも, 最大2桁のスピードアップを達成できることがわかった。
  論文  参考訳（メタデータ） (2020-02-26T21:04:06Z)

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

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