Graph2Tac: Online Representation Learning of Formal Math Concepts

TL;DR

This work extensively benchmarks two online solvers implemented in the Tactician platform for the Coq proof assistant, and introduces a graph neural network, Graph2Tac, with a novel approach to build hierarchical representations for new definitions.

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.

Figures (20)

• Figure 1: Our two paradigms of online learning: the online $k$-NN learns from recent proofs and the GNN (Graph2Tac) from recent definitions.
• Figure 2: Our novel definition training task. At the center is a table of learned definition embeddings (orange). During training (above the line), we train both a proof step network to predict tactics (including arguments) and a definition network to calculate definition embeddings (blue) similar to those in the table. During inference (below the line), the definition network is used to calculated hierarchical embeddings (blue) for new definitions that may in turn be used to represent proof states and predict tactic arguments.
• Figure 3: A graph-based representation of the example given in Figure \ref{['fig:overview']}. Each color represents a unique definition or proofstate subgraph. These colored subgraphs are used as inputs to our neural networks. Green corresponds to the function $f$, red to the theorem $T1$, and blue to the proof state from the example. Each node is either a definition node ($T1$, $f$, $\mathbb{N}$, $=$, $+$) or a node representing the part of a term. For example, $@$ is function application, and $\uparrow$ is a variable whose outgoing edge points to its binder. Edges are labeled, but not shown here. Triangles represent portions of the graph which we didn't expand for clarity. Some nodes are shared by multiple colored regions such as the subgraph for $2*$. Definition nodes (but not the rest of the definition) are also shared with all colored regions they touch. The proof terms for $T1$ is excluded from its colored region. See web-paper for full details.
• Figure 4: Detailed Graph2Tac model architecture, composed of a definition task (the top path going from the definition of $f$ to its embedding) and prediction task (the path going from the proof state $2 * x = f x$ to the predicted tactic apply T1). The edge and node embedding tables are excluded from the image.
• Figure 5: Fraction of theorems proved over time and per number of calls to the model. Online solvers are dashed, offline solvers are solid, and symbolic solvers are dotted.