論文の概要: Machine Learning Meets The Herbrand Universe

• arxiv url: http://arxiv.org/abs/2210.03590v1
• Date: Fri, 7 Oct 2022 14:46:32 GMT
• ステータス: 処理完了
• システム内更新日: 2022-10-10 13:23:32.791736
• Title: Machine Learning Meets The Herbrand Universe
• Title（参考訳）: 機械学習がHerbrand Universeと出会う
• Authors: Jelle Piepenbrock, Josef Urban, Konstantin Korovin, Miroslav Ol\v{s}\'ak, Tom Heskes and Mikola\v{s} Janota
• Abstract要約: ヘルブランドの定理は、一階問題のインスタンス化による命題問題への還元を可能にする。 我々は,このタスクを対象とする最初の機械学習システムを開発した。 トレーニングされたシステムは、正しいインスタンスを予測する際に高い精度を達成できることを示す。
• 参考スコア（独自算出の注目度）: 1.5984927623688914
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The appearance of strong CDCL-based propositional (SAT) solvers has greatly advanced several areas of automated reasoning (AR). One of the directions in AR is thus to apply SAT solvers to expressive formalisms such as first-order logic, for which large corpora of general mathematical problems exist today. This is possible due to Herbrand's theorem, which allows reduction of first-order problems to propositional problems by instantiation. The core challenge is choosing the right instances from the typically infinite Herbrand universe. In this work, we develop the first machine learning system targeting this task, addressing its combinatorial and invariance properties. In particular, we develop a GNN2RNN architecture based on an invariant graph neural network (GNN) that learns from problems and their solutions independently of symbol names (addressing the abundance of skolems), combined with a recurrent neural network (RNN) that proposes for each clause its instantiations. The architecture is then trained on a corpus of mathematical problems and their instantiation-based proofs, and its performance is evaluated in several ways. We show that the trained system achieves high accuracy in predicting the right instances, and that it is capable of solving many problems by educated guessing when combined with a ground solver. To our knowledge, this is the first convincing use of machine learning in synthesizing relevant elements from arbitrary Herbrand universes.
• Abstract（参考訳）: 強力なCDCLベースの命題解法 (SAT) の出現は、自動化推論 (AR) の分野で大きく進歩している。 したがって、arの方向の一つは、今日一般的な数学的問題の大きなコーパスが存在する一階述語論理のような表現的形式論にsatソルバを適用することである。 これは、一階問題から命題問題へのインスタンス化を許容するヘルブランドの定理により可能である。 主な課題は、通常無限のヘルブランド宇宙から正しい例を選択することである。 本研究では,このタスクを対象とする最初の機械学習システムを開発し,その組合せ特性と不変性に対処する。 特に,不変グラフニューラルネットワーク(gnn)に基づくgnn2rnnアーキテクチャを開発し,問題とその解を記号名(スクレムの豊富さに対応する)とは独立に学習し,各節のインスタンス化を提案するrecurrent neural network(rnn)と組み合わせた。 アーキテクチャは、数学的問題とそのインスタンスに基づく証明のコーパスに基づいて訓練され、その性能はいくつかの点で評価される。 学習したシステムは,適切なインスタンスを予測する際に高い精度を達成し,地上の解法と組み合わせることで,多くの問題を解決することができることを示す。 私たちの知る限りでは、任意のHerbrand宇宙から関連する要素を合成するために機械学習を使った最初の説得力がある。

関連論文リスト

• Improving Complex Reasoning over Knowledge Graph with Logic-Aware Curriculum Tuning [89.89857766491475]
  大規模言語モデル(LLM)に基づくKG上の複雑な推論スキーマを提案する。 任意の一階論理クエリを二分木分解により拡張し、LLMの推論能力を刺激する。 広く使われているデータセットに対する実験では、LACTは高度な手法よりも大幅に改善されている(平均+5.5% MRRスコア)。
  論文  参考訳（メタデータ） (2024-05-02T18:12:08Z)
• Tunable Complexity Benchmarks for Evaluating Physics-Informed Neural Networks on Coupled Ordinary Differential Equations [64.78260098263489]
  本研究では,より複雑に結合した常微分方程式(ODE)を解く物理インフォームドニューラルネットワーク(PINN)の能力を評価する。 PINNの複雑性が増大するにつれて,これらのベンチマークに対する正しい解が得られないことが示される。 PINN損失のラプラシアンは,ネットワーク容量の不足,ODEの条件の低下,局所曲率の高さなど,いくつかの理由を明らかにした。
  論文  参考訳（メタデータ） (2022-10-14T15:01:32Z)
• Graph Neural Networks for Propositional Model Counting [1.0152838128195467]
  グラフネットワーク(GNN)は最近、論理的推論タスクの解決に活用されている。 本稿では, 自覚的GNNによって拡張され, #SAT 問題を大まかに解くために訓練された, Kuch 等の信念伝播のための GNN フレームワークに基づくアーキテクチャを提案する。
  論文  参考訳（メタデータ） (2022-05-09T17:03:13Z)
• Graph Neural Networks are Dynamic Programmers [0.0]
  グラフニューラルネットワーク(GNN)は動的プログラミング(DP)と一致すると主張される ここでは、理論と抽象代数学の手法を用いて、GNNとDPの間に複雑な関係が存在することを示す。
  論文  参考訳（メタデータ） (2022-03-29T13:27:28Z)
• Can Graph Neural Networks Learn to Solve MaxSAT Problem? [22.528432249712637]
  我々は,理論的および実践的両面から,マックスサット問題の解法学習におけるGNNの能力について検討した。 我々はベンチマークからMaxSATインスタンスの解法を学ぶために2種類のGNNモデルを構築し、実験によりGNNがMaxSAT問題を解く魅力的な可能性を示す。 また,アルゴリズムアライメント理論に基づいて,GNN が MaxSAT 問題のある程度の解法を学習できるという理論的な説明も提示する。
  論文  参考訳（メタデータ） (2021-11-15T07:33:33Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
  論文  参考訳（メタデータ） (2021-07-15T04:47:35Z)
• Neural-Symbolic Solver for Math Word Problems with Auxiliary Tasks [130.70449023574537]
  我々のNS-rは、問題を読み取り、問題をエンコードする問題リーダーと、記号方程式を生成するプログラマと、答えを得るシンボリックエグゼキュータから構成される。 また, 目的表現の監督とともに, 4つの新たな補助的目的によって, 異なる記号的推論を強制的に行うように最適化した。
  論文  参考訳（メタデータ） (2021-07-03T13:14:58Z)
• Conditional physics informed neural networks [85.48030573849712]
  固有値問題のクラス解を推定するための条件付きPINN(物理情報ニューラルネットワーク)を紹介します。 一つのディープニューラルネットワークが、問題全体に対する偏微分方程式の解を学習できることが示される。
  論文  参考訳（メタデータ） (2021-04-06T18:29:14Z)
• Machine Number Sense: A Dataset of Visual Arithmetic Problems for Abstract and Relational Reasoning [95.18337034090648]
  文法モデルを用いて自動生成される視覚的算術問題からなるデータセット、MNS(Machine Number Sense)を提案する。 これらの視覚的算術問題は幾何学的フィギュアの形をしている。 我々は、この視覚的推論タスクのベースラインとして、4つの主要なニューラルネットワークモデルを用いて、MNSデータセットをベンチマークする。
  論文  参考訳（メタデータ） (2020-04-25T17:14:58Z)
• SpatialSim: Recognizing Spatial Configurations of Objects with Graph Neural Networks [31.695447265278126]
  本稿では,外部オブザーバの視点に不変な幾何学的空間構成のクラスを学習し,比較する方法を示す。 本稿では,新しい幾何学的推論ベンチマークであるSpatialSim(Spatial similarity)を提案する。 次に,完全接続型メッセージパスグラフニューラルネットワーク(MPGNN)が示す帰納的リレーショナルバイアスが,これらの課題の解決にどのように役立つかを検討する。
  論文  参考訳（メタデータ） (2020-04-09T14:13:20Z)

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

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