The article introduces Graph2Tac (G2T), a graph neural network that learns hierarchical representations of mathematical concepts in theorem proving. G2T uses a large-scale, graph-based dataset for machine learning in Coq, a proof assistant. It creates a directed graph of dependencies between definitions, allowing it to consider the entire hierarchy of definitions leading to the current goal. G2T is an online model that can adapt in real-time to new Coq projects and their definitions. It works well with other online models that learn from new proof scripts in real-time. The performance of the neural network is boosted by a new definition embedding task, which is trained to compute representations of mathematical concepts not seen during training.
Publication date: 8 Jan 2024
Project Page: https://arxiv.org/abs/2401.02949v1
Paper: https://arxiv.org/pdf/2401.02949
