Graph2Tac: Learning Hierarchical Representations of Math Concepts in Theorem proving

Concepts abound in mathematics and its applications. They vary greatlybetween subject areas, and new ones are introduced in each mathematical paperor application. A formal theory builds a hierarchy of definitions, theorems andproofs 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 havenever been seen during training. This is especially true in the Coq proofassistant, which has a diverse library of Coq projects, each with its owndefinitions, lemmas, and even custom tactic procedures used to prove thoselemmas. It is essential for agents to incorporate such new information intotheir 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 afaithful graph-representation of Coq terms that induces a directed graph ofdependencies between definitions to create a novel graph neural network,Graph2Tac (G2T), that takes into account not only the current goal, but alsothe entire hierarchy of definitions that led to the current goal. G2T is anonline model that is deeply integrated into the users' workflow and can adaptin real time to new Coq projects and their definitions. It complements wellwith other online models that learn in real time from new proof scripts. Ournovel definition embedding task, which is trained to compute representations ofmathematical concepts not seen during training, boosts the performance of theneural network to rival state-of-the-art k-nearest neighbor predictors.