Graph2Tac: Online Representation Learning of Formal Math Concepts

TL;DR

This paper introduces Graph2Tac, a graph neural network-based online learning method for formal math concepts that significantly improves theorem proving efficiency in proof assistants like Coq.

Contribution

The paper presents a novel hierarchical graph neural network approach, Graph2Tac, for online representation learning of formal math concepts, outperforming offline methods and existing provers.

Findings

Graph2Tac achieves a 1.5x improvement over offline baselines.

Online k-NN solver improves theorem proving by 1.72x.

Combined online methods outperform individual ones by 1.27x.

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.