論文の概要: Graph2Tac: Learning Hierarchical Representations of Math Concepts in
Theorem proving
- arxiv url: http://arxiv.org/abs/2401.02949v2
- Date: Tue, 9 Jan 2024 18:53:19 GMT
- ステータス: 処理完了
- システム内更新日: 2024-01-10 12:58:14.554123
- Title: Graph2Tac: Learning Hierarchical Representations of Math Concepts in
Theorem proving
- Title(参考訳): Graph2Tac: 定理証明における数学概念の階層的表現学習
- Authors: Jason Rute, Miroslav Ol\v{s}\'ak, Lasse Blaauwbroek, Fidel Ivan
Schaposnik Massolo, Jelle Piepenbrock, Vasily Pestun
- Abstract要約: AIエージェントが新しい定理を証明しているとき、その定理に関連する数学的概念や補題のほとんどは、トレーニング中に一度も見られなかったかもしれない。
これは、Coqプロジェクトの多種多様なライブラリを持ち、それぞれ独自の定義、補題、さらにはそれらの補題を証明するために使用されるカスタム戦術の手順を持つCoq証明アシスタントに特に当てはまる。
私たちは、Coqにおける機械学習のために、新しい大規模でグラフベースのデータセットを活用することで、この目標に向かっています。
- 参考スコア(独自算出の注目度): 0.6990493129893112
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Concepts abound in mathematics and its applications. They vary greatly
between subject areas, and new ones are introduced in each mathematical paper
or application. A formal theory builds a hierarchy of definitions, theorems and
proofs that reference each other. When an AI agent is proving a new theorem,
most of the mathematical concepts and lemmas relevant to that theorem may have
never been seen during training. This is especially true in the Coq proof
assistant, which has a diverse library of Coq projects, each with its own
definitions, lemmas, and even custom tactic procedures used to prove those
lemmas. It is essential for agents to incorporate such new information into
their knowledge base on the fly. We work towards this goal by utilizing a new,
large-scale, graph-based dataset for machine learning in Coq. We leverage a
faithful graph-representation of Coq terms that induces a directed graph of
dependencies between definitions to create a novel graph neural network,
Graph2Tac (G2T), that takes into account not only the current goal, but also
the entire hierarchy of definitions that led to the current goal. G2T is an
online model that is deeply integrated into the users' workflow and can adapt
in real time to new Coq projects and their definitions. It complements well
with other online models that learn in real time from new proof scripts. Our
novel definition embedding task, which is trained to compute representations of
mathematical concepts not seen during training, boosts the performance of the
neural network to rival state-of-the-art k-nearest neighbor predictors.
- Abstract(参考訳): 数学における概念とその応用。
対象分野によって大きく異なり、各数学論文や応用に新しいものが導入される。
形式理論は、互いに参照する定義、定理、証明の階層を構築する。
AIエージェントが新しい定理を証明しているとき、その定理に関連する数学的概念や補題のほとんどは、トレーニング中に見たことがないかもしれない。
これは、Coqプロジェクトの多種多様なライブラリを持ち、それぞれ独自の定義、補題、さらにはそれらの補題を証明するために使用されるカスタム戦術の手順を持つCoq証明アシスタントに特に当てはまる。
エージェントは、そのような新しい情報をオンザフライで知識ベースに組み込むことが不可欠である。
私たちは、coqの機械学習のために、新しい大規模グラフベースのデータセットを利用することで、この目標に向かって取り組んでいる。
我々は、定義間の依存関係の有向グラフを誘導するCoq用語の忠実なグラフ表現を活用して、現在の目標だけでなく、現在の目標に繋がった定義の階層全体も考慮に入れた、新しいグラフニューラルネットワークGraph2Tac(G2T)を作成します。
G2Tは、ユーザのワークフローに深く統合され、新しいCoqプロジェクトとその定義にリアルタイムで適応できるオンラインモデルである。
新しい証明スクリプトからリアルタイムで学習する他のオンラインモデルとも相性がいい。
我々の新しい定義埋め込みタスクは、トレーニング中に見えない数学的概念の表現を計算するために訓練され、ニューラルネットワークの性能を、最先端のkアレスト近傍予測器に向上させる。
関連論文リスト
- Machine learning and information theory concepts towards an AI
Mathematician [77.63761356203105]
人工知能の現在の最先端技術は、特に言語習得の点で印象的だが、数学的推論の点ではあまり重要ではない。
このエッセイは、現在のディープラーニングが主にシステム1の能力で成功するという考えに基づいている。
興味深い数学的ステートメントを構成するものについて質問するために、情報理論的な姿勢を取る。
論文 参考訳(メタデータ) (2024-03-07T15:12:06Z) - The Tactician's Web of Large-Scale Formal Knowledge [0.0]
Tactician's Webは、強く相互接続され、マシンチェックされ、正式な数学的知識を提供するプラットフォームである。
Coq証明アシスタント上に構築されたこのプラットフォームは、さまざまな形式理論を含むデータセットをエクスポートする。
証明エージェントは、同じリッチなデータ表現を通じてCoqと相互作用し、定理のセットで自動的にベンチマークすることができる。
論文 参考訳(メタデータ) (2024-01-05T18:52:35Z) - Knowledge Graph Embedding: An Overview [42.16033541753744]
本稿では,知識グラフの完成に関する現在の研究状況について概観する。
我々は,KG埋め込み(KGE)設計の2つの主要分野に焦点を当てた:1)距離ベース手法と2)意味マッチング方式である。
次に,2次元および3次元アフィン操作からインスピレーションを得る複合Eと複合E3Dを探索する。
論文 参考訳(メタデータ) (2023-09-21T21:52:42Z) - A Survey of Knowledge Graph Reasoning on Graph Types: Static, Dynamic,
and Multimodal [57.8455911689554]
知識グラフ推論(KGR)は、知識グラフに基づくマイニング論理則に基づいて、既存の事実から新しい事実を推論することを目的としている。
質問応答やレコメンデーションシステムなど、多くのAIアプリケーションでKGを使うことに大きなメリットがあることが証明されている。
論文 参考訳(メタデータ) (2022-12-12T08:40:04Z) - Learning Representations of Entities and Relations [0.0]
この論文は,リンク予測タスクに取り組むことを目的とした知識グラフ表現の改善に焦点を当てている。
最初のコントリビューションはHypERであり、リンク予測性能を単純化し改善する畳み込みモデルである。
第2のコントリビューションは比較的単純な線形モデルであるTuckERで、このモデルが導入された時点では、最先端のリンク予測性能が得られた。
第3の貢献は、双曲空間に埋め込まれた最初のマルチリレーショナルグラフ表現モデルである MuRP である。
論文 参考訳(メタデータ) (2022-01-31T09:24:43Z) - What is Learned in Knowledge Graph Embeddings? [3.224929252256631]
知識グラフ(英: knowledge graph, KG)とは、有向グラフの頂点と辺として実体と関係を表すデータ構造である。
本稿では,関係性間の規則の学習が,組込み方式の性能向上の要因であるかどうかを考察する。
合成KGの実験により、KGモデルがモチーフを学習し、その能力が非モチーフエッジによってどのように劣化するかを示す。
論文 参考訳(メタデータ) (2021-10-19T13:52:11Z) - Dynamic Semantic Graph Construction and Reasoning for Explainable
Multi-hop Science Question Answering [50.546622625151926]
マルチホップQAのための説明可能性を得ながら,より有効な事実を活用できる新しいフレームワークを提案する。
a) tt AMR-SG,(a) tt AMR-SG,(a) tt AMR-SG,(a) tt AMR-SG,(c) グラフ畳み込みネットワーク(GCN)を利用した事実レベルの関係モデリング,(c) 推論過程の導出を行う。
論文 参考訳(メタデータ) (2021-05-25T09:14:55Z) - ExplaGraphs: An Explanation Graph Generation Task for Structured
Commonsense Reasoning [65.15423587105472]
スタンス予測のための説明グラフ生成の新しい生成および構造化コモンセンスリゾニングタスク(および関連するデータセット)を紹介します。
具体的には、信念と議論が与えられた場合、モデルは、議論が信念を支持しているかどうかを予測し、予測されたスタンスに対する非自明で完全で曖昧な説明として機能する常識強化グラフを生成する必要がある。
グラフの83%は、様々な構造と推論深度を持つ外部のコモンセンスノードを含んでいる。
論文 参考訳(メタデータ) (2021-04-15T17:51:36Z) - Geometrically Principled Connections in Graph Neural Networks [66.51286736506658]
我々は、幾何学的深層学習の新興分野におけるイノベーションの原動力は、幾何が依然として主要な推進力であるべきだと論じている。
グラフニューラルネットワークとコンピュータグラフィックスとデータ近似モデルとの関係:放射基底関数(RBF)
完全連結層とグラフ畳み込み演算子を組み合わせた新しいビルディングブロックであるアフィンスキップ接続を導入する。
論文 参考訳(メタデータ) (2020-04-06T13:25:46Z) - Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。
実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文 参考訳(メタデータ) (2020-02-17T16:06:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。