論文の概要: Graph2Tac: Online Representation Learning of Formal Math Concepts
- arxiv url: http://arxiv.org/abs/2401.02949v3
- Date: Sun, 23 Jun 2024 13:54:33 GMT
- ステータス: 処理完了
- システム内更新日: 2024-06-26 02:32:50.649638
- Title: Graph2Tac: Online Representation Learning of Formal Math Concepts
- Title（参考訳）: Graph2Tac: 形式数学概念のオンライン表現学習
- Authors: Lasse Blaauwbroek, Miroslav Olšák, Jason Rute, Fidel Ivan Schaposnik Massolo, Jelle Piepenbrock, Vasily Pestun,
- Abstract要約: 証明において、2つの形式的な数学的概念の間の物理的近接は、それらの相互関係の強い予測因子である。
この局所性特性はオンライン学習技術によって利用でき、オフライン学習者を超えている問題解決エージェントが得られることを示す。
我々は、Coq証明アシスタントのためにTacticianプラットフォームで実装された2つのオンライン解決器をベンチマークした。
- 参考スコア（独自算出の注目度）: 0.6597195879147557
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: In proof assistants, the physical proximity between two formal mathematical concepts is a strong predictor of their mutual relevance. Furthermore, lemmas with close proximity regularly exhibit similar proof structures. We show that this locality property can be exploited through online learning techniques to obtain solving agents that far surpass offline learners when asked to prove theorems in an unseen mathematical setting. We extensively benchmark two such online solvers implemented in the Tactician platform for the Coq proof assistant: First, Tactician's online $k$-nearest neighbor solver, which can learn from recent proofs, shows a $1.72\times$ improvement in theorems proved over an offline equivalent. Second, we introduce a graph neural network, Graph2Tac, with a novel approach to build hierarchical representations for new definitions. Graph2Tac's online definition task realizes a $1.5\times$ improvement in theorems solved over an offline baseline. The $k$-NN and Graph2Tac solvers rely on orthogonal online data, making them highly complementary. Their combination improves $1.27\times$ over their individual performances. Both solvers outperform all other general-purpose provers for Coq, including CoqHammer, Proverbot9001, and a transformer baseline by at least $1.48\times$ and are available for practical use by end-users.
- Abstract（参考訳）: 証明アシスタントでは、2つの形式的な数学的概念間の物理的な近接は、それらの相互関連性の強い予測因子である。
さらに、近接した補題は、よく似た証明構造を示す。
本研究では,この局所性特性をオンライン学習手法により活用し,未知の数学的条件下での定理の証明を依頼したとき,オフライン学習者よりはるかに上回る解法エージェントを得ることを示す。
第一に、Tacticianのオンラインの$k$-nearestの隣の解法は、最近の証明から学ぶことができ、オフラインの等価性よりも証明された定理の1.72\times$の改善を示す。
第2に、新しい定義のための階層的表現を構築するための新しいアプローチを備えたグラフニューラルネットワーク、Graph2Tacを導入する。
Graph2Tacのオンライン定義タスクは、オフラインベースラインで解決された定理の1.5\times$の改善を実現する。
k$-NNとGraph2Tacのソルバは直交のオンラインデータに依存しており、非常に補完的だ。
彼らの組み合わせは個々のパフォーマンスよりも$1.27\times$を改善する。
CoqHammer、Proverbot9001、およびトランスフォーマーベースラインを少なくとも$1.48\times$で上回り、エンドユーザーによる実用的な使用が可能である。
関連論文リスト
- 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。