Graph2Tac: Learning Hierarchical Representations of Math Concepts in Theorem proving

要約

数学とその応用には概念が豊富にあります。
それらは主題分野によって大きく異なり、各数学論文またはアプリケーションで新しいものが導入されます。
形式理論は、相互に参照する定義、定理、証明の階層を構築します。
AI エージェントが新しい定理を証明するとき、その定理に関連する数学的概念や補題のほとんどは、トレーニング中に一度も見たことがない可能性があります。
これは、Coq 証明アシスタントに特に当てはまります。Coq 証明アシスタントには、Coq プロジェクトの多様なライブラリがあり、それぞれに独自の定義、補題、さらにはそれらの補題を証明するために使用されるカスタム戦術手順が含まれています。
エージェントにとって、そのような新しい情報をその場で知識ベースに組み込むことが不可欠です。
私たちは、Coq の機械学習用に新しい大規模なグラフベースのデータセットを利用することで、この目標に向かって取り組んでいます。
私たちは、定義間の依存関係の有向グラフを誘導する Coq 用語の忠実なグラフ表現を利用して、現在の目標だけでなく、定義の階層全体も考慮する新しいグラフ ニューラル ネットワーク Graph2Tac (G2T) を作成します。
それが現在の目標につながりました。
G2T は、ユーザーのワークフローに深く統合され、新しい Coq プロジェクトとその定義にリアルタイムで適応できるオンライン モデルです。
新しい証明スクリプトからリアルタイムで学習する他のオンライン モデルとよく補完します。
私たちの新しい定義埋め込みタスクは、トレーニング中には見ら​​れなかった数学的概念の表現を計算するようにトレーニングされ、ニューラル ネットワークのパフォーマンスを最先端の k 最近傍予測子に匹敵するまで向上させます。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google