論文の概要: 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アレスト近傍予測器に向上させる。
関連論文リスト
- Efficient Solution of Point-Line Absolute Pose [52.775981113238046]
点や線である可能性のある特徴間の3D--2D対応に基づくポーズ推定の特定の問題を再検討する。
得られた解法は数値的に安定かつ高速であることを示す。
論文 参考訳（メタデータ） (2024-04-25T12:09:16Z) - Efficient Methods for Non-stationary Online Learning [67.3300478545554]
本稿では, 動的後悔と適応的後悔を最適化する効率的な手法を提案し, ラウンド当たりの投影回数を$mathcalO(log T)$から$ $1$まで削減した。
本手法は,パラメータフリーオンライン学習において開発された還元機構を基礎として,非定常オンライン手法に非自明なツイストを必要とする。
論文 参考訳（メタデータ） (2023-09-16T07:30:12Z) - Reduction Algorithms for Persistence Diagrams of Networks: CoralTDA and
PrunIT [27.411830935369498]
計算コストが高いことが、トポロジカルデータ分析の成功を妨げる主要な障害となっている。
我々は,大規模グラフの完全永続化図を計算するために,2つの新しい,驚くほど単純で効果的なアルゴリズムを開発した。
大規模ネットワークにおける実験により,新しい手法で最大95%の計算ゲインが得られることが示された。
論文 参考訳（メタデータ） (2022-11-24T16:52:48Z) - PDE-Based Optimal Strategy for Unconstrained Online Learning [40.61498562988079]
部分微分方程式(PDE)を解くことによって時間変化ポテンシャル関数を生成するフレームワークを提案する。
我々のフレームワークは、いくつかの古典的なポテンシャルを回復し、より重要なことは、新しいものを設計するための体系的なアプローチを提供する。
これは最適なリード定数を持つ最初のパラメータフリーアルゴリズムである。
論文 参考訳（メタデータ） (2022-01-19T22:21:21Z) - Training Free Graph Neural Networks for Graph Matching [103.45755859119035]
TFGMは、グラフニューラルネットワーク(GNN)ベースのグラフマッチングのパフォーマンスをトレーニングなしで向上するフレームワークである。
TFGMをさまざまなGNNに適用することは、ベースラインよりも有望な改善を示している。
論文 参考訳（メタデータ） (2022-01-14T09:04:46Z) - Provably Efficient Generative Adversarial Imitation Learning for Online
and Offline Setting with Linear Function Approximation [81.0955457177017]
GAIL(Generative Adversarial mimicion Learning)では、特定の報酬セットにおいて、専門家の政策からそのパフォーマンスを区別できないように、専門家のデモンストレーションからポリシーを学習することを目的としている。
GAILをオンラインとオフラインの両方で線形関数近似を用いて検討し、その変換関数と報酬関数は特徴写像において線形である。
論文 参考訳（メタデータ） (2021-08-19T16:16:00Z) - Online Machine Learning Techniques for Coq: A Comparison [2.9412498294532856]
我々は,Coq証明アシスタントにおける戦術学習と証明のためのオンライン機械学習技術の比較を行った。
この仕事は、ユーザーによって書かれた証明から新しい証明を合成するCoq用のプラグインであるTacticianをベースにしています。
論文 参考訳（メタデータ） (2021-04-12T05:12:35Z) - Online Apprenticeship Learning [58.45089581278177]
見習い学習(AL)では、コスト関数にアクセスせずにマルコフ決定プロセス(MDP)が与えられます。
目標は、事前に定義されたコスト関数のセットで専門家のパフォーマンスに一致するポリシーを見つけることです。
ミラー下降型ノンレグレットアルゴリズムを2つ組み合わせることで,OAL問題を効果的に解くことができることを示す。
論文 参考訳（メタデータ） (2021-02-13T12:57:51Z) - Learning Bayesian Networks Under Sparsity Constraints: A Parameterized
Complexity Analysis [7.99536002595393]
本稿では,ネットワーク上あるいはそのモラル化されたグラフ上に制約を加える際に,最適なベイズネットワークの構造を学習する問題について検討する。
モラル化されたグラフに少なくとも$k$のエッジを持つ最適ネットワークを学習すると、おそらく$f(k)cdot |I|O(1)$-timeアルゴリズムが存在しない。
論文 参考訳（メタデータ） (2020-04-30T12:31:13Z) - Geometrically Principled Connections in Graph Neural Networks [66.51286736506658]
我々は、幾何学的深層学習の新興分野におけるイノベーションの原動力は、幾何が依然として主要な推進力であるべきだと論じている。
グラフニューラルネットワークとコンピュータグラフィックスとデータ近似モデルとの関係:放射基底関数(RBF)
完全連結層とグラフ畳み込み演算子を組み合わせた新しいビルディングブロックであるアフィンスキップ接続を導入する。
論文 参考訳（メタデータ） (2020-04-06T13:25:46Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。