論文の概要: Learning Reliable Logical Rules with SATNet
- arxiv url: http://arxiv.org/abs/2310.02133v1
- Date: Tue, 3 Oct 2023 15:14:28 GMT
- ステータス: 処理完了
- システム内更新日: 2023-10-04 13:37:35.130575
- Title: Learning Reliable Logical Rules with SATNet
- Title(参考訳): satnetによる信頼できる論理ルールの学習
- Authors: Zhaoyu Li, Jinpei Guo, Yuhe Jiang, Xujie Si
- Abstract要約: 我々は、入力出力の例から基礎となるルールを学習する差別化可能なMaxSATソルバSATNetの上に構築する。
基礎的真理規則に対して有効な検証手法をいくつか導入する。
ストリームトランスフォーメーションとスドク問題に関する実験は、デコードされたルールが信頼性が高いことを示している。
- 参考スコア(独自算出の注目度): 7.951021955925275
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Bridging logical reasoning and deep learning is crucial for advanced AI
systems. In this work, we present a new framework that addresses this goal by
generating interpretable and verifiable logical rules through differentiable
learning, without relying on pre-specified logical structures. Our approach
builds upon SATNet, a differentiable MaxSAT solver that learns the underlying
rules from input-output examples. Despite its efficacy, the learned weights in
SATNet are not straightforwardly interpretable, failing to produce
human-readable rules. To address this, we propose a novel specification method
called "maximum equality", which enables the interchangeability between the
learned weights of SATNet and a set of propositional logical rules in weighted
MaxSAT form. With the decoded weighted MaxSAT formula, we further introduce
several effective verification techniques to validate it against the ground
truth rules. Experiments on stream transformations and Sudoku problems show
that our decoded rules are highly reliable: using exact solvers on them could
achieve 100% accuracy, whereas the original SATNet fails to give correct
solutions in many cases. Furthermore, we formally verify that our decoded
logical rules are functionally equivalent to the ground truth ones.
- Abstract(参考訳): 高度なAIシステムには、論理的推論とディープラーニングの橋渡しが不可欠だ。
本研究は, 既定論理構造に頼ることなく, 微分可能学習を通じて解釈可能かつ検証可能な論理規則を生成することによって, この目標に対処する新しい枠組みを提案する。
我々のアプローチは、入力出力例から基礎となるルールを学習する差別化可能なMaxSATソルバSATNetの上に構築されている。
その効果にもかかわらず、SATNetの学習重量は直接解釈可能ではなく、人間が読めるルールを作成できない。
そこで本研究では,satnet の学習重みと重み付き maxsat 形式の命題的論理規則のセットとの交換性を実現する "maximum equal" という新しい仕様法を提案する。
さらに,復号化重み付きMaxSAT公式を用いて,基礎的真理規則に対して有効な検証手法をいくつか導入する。
ストリーム変換とスドク問題の実験では、デコードされたルールは信頼性が高く、正確な解法を用いることで100%の精度が得られるが、元のSATNetでは多くの場合、正しい解が得られない。
さらに, 復号化論理則が基本真理則と機能的に等価であることを正式に検証する。
関連論文リスト
- Self-Satisfied: An end-to-end framework for SAT generation and prediction [0.7340017786387768]
高速SAT問題生成のためのハードウェアアクセラレーションアルゴリズムと幾何SAT符号化を導入する。
これらの進歩により、何千もの変数と数万の節でSAT問題へのアプローチをスケールできます。
私たちの研究の基本的な側面は、SATデータの本質と、機械学習モデルのトレーニングに適合する可能性に関するものです。
論文 参考訳(メタデータ) (2024-10-18T22:25:54Z) - Assessing SATNet's Ability to Solve the Symbol Grounding Problem [19.52506478494672]
SATNetは、論理ルールの推論に使用でき、ディープニューラルネットワークの微分可能な層として統合される、賞を受賞したMAXSATソルバである。
本研究では,個々のSudoku桁の画像を論理的表現で識別する中間ラベルがない場合,SATNetは視覚的Sudokuでは完全にフェールすることを示す。
そこで本研究では, MNIST に基づく検定をシンボル基底問題の簡単な例として提案し, 一般の微分可能な記号解法に対する正当性チェックとして機能する。
論文 参考訳(メタデータ) (2023-12-13T04:29:32Z) - SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
本研究では,大規模言語モデル (LLM) の推論能力を向上させるために,新しい満足度支援言語モデリング (SatLM) 手法を提案する。
我々はLLMを用いて命令型プログラムではなく宣言型タスク仕様を生成し、既製の自動定理証明器を利用して最終解を導出する。
我々はSATLMを8つの異なるデータセット上で評価し、命令パラダイムにおいてプログラム支援されたLMよりも一貫して優れていることを示す。
論文 参考訳(メタデータ) (2023-05-16T17:55:51Z) - Estimating the hardness of SAT encodings for Logical Equivalence
Checking of Boolean circuits [58.83758257568434]
LEC インスタンスの SAT 符号化の硬さは SAT パーティショニングでは textitw.r. と推定できることを示す。
そこで本研究では, SAT符号化の難易度を精度良く推定できるパーティショニング法を提案する。
論文 参考訳(メタデータ) (2022-10-04T09:19:13Z) - SATformer: Transformer-Based UNSAT Core Learning [0.0]
本稿では,SAT 問題に対する Transformer ベースのアプローチである SATformer を紹介する。
SATformerは、問題を直接解決するのではなく、満足できないことに焦点をあてて、その問題を反対方向からアプローチする。
SATformerは、シングルビットの満足度結果と最小限の不満コアを使用して、マルチタスク学習アプローチでトレーニングされる。
実験の結果,SATformerは既存のソルバのランタイムを平均21.33%削減できることがわかった。
論文 参考訳(メタデータ) (2022-09-02T11:17:39Z) - Learning Symmetric Rules with SATNet [9.238700679836855]
SATNet のパラメータの条件に対象ルールの所定の対称性を変換する SATNet の変種である SymSATNet を提案する。
また,実例から対象ルールの対称性を自動的に検出する手法についても述べる。
スドクとルービックキューブを用いた実験により,SymSATNetがベースラインSATNetよりも大幅に向上したことを示す。
論文 参考訳(メタデータ) (2022-06-28T13:36:34Z) - DeepSAT: An EDA-Driven Learning Framework for SAT [9.111341161918375]
We present DeepSAT, a novel-to-end learning framework for the Boolean satisfiability (SAT) problem。
DeepSATは最先端の学習ベースSATソリューションに対して,大幅な精度向上を実現している。
論文 参考訳(メタデータ) (2022-05-27T03:20:42Z) - Neuro-Symbolic Inductive Logic Programming with Logical Neural Networks [65.23508422635862]
我々は最近提案された論理ニューラルネットワーク(LNN)を用いた学習規則を提案する。
他のものと比較して、LNNは古典的なブール論理と強く結びついている。
標準ベンチマークタスクの実験では、LNNルールが極めて解釈可能であることを確認した。
論文 参考訳(メタデータ) (2021-12-06T19:38:30Z) - Learning Symbolic Rules for Reasoning in Quasi-Natural Language [74.96601852906328]
我々は,ルールを手作業で構築することなく,自然言語入力で推論できるルールベースシステムを構築した。
本稿では,形式論理文と自然言語文の両方を表現可能な"Quasi-Natural"言語であるMetaQNLを提案する。
提案手法は,複数の推論ベンチマークにおける最先端の精度を実現する。
論文 参考訳(メタデータ) (2021-11-23T17:49:00Z) - Transformer-based Machine Learning for Fast SAT Solvers and Logic
Synthesis [63.53283025435107]
CNFベースのSATとMaxSATは論理合成と検証システムの中心である。
そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
論文 参考訳(メタデータ) (2021-07-15T04:47:35Z) - RNNLogic: Learning Logic Rules for Reasoning on Knowledge Graphs [91.71504177786792]
本稿では知識グラフに基づく推論のための論理規則の学習について研究する。
論理規則は、予測に使用されるときに解釈可能な説明を提供するとともに、他のタスクに一般化することができる。
既存の手法は、検索スペースの検索の問題や、スパース報酬による非効率な最適化に悩まされている。
論文 参考訳(メタデータ) (2020-10-08T14:47:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。