Graph2Tac: Online Representation Learning of Formal Math Concepts

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F24%3A00381582" target="_blank" >RIV/68407700:21730/24:00381582 - isvavai.cz</a>

Result on the web

<a href="https://openreview.net/pdf?id=A7CtiozznN" target="_blank" >https://openreview.net/pdf?id=A7CtiozznN</a>

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Graph2Tac: Online Representation Learning of Formal Math Concepts

Original language description

In proof assistants, the physical proximity be tween two formal mathematical concepts is a strong predictor of their mutual relevance. Fur thermore, lemmas with close proximity regularly exhibit similar proof structures. We show that this locality property can be exploited through on line 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 172 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 15 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 127 over their individual performances. Both solvers outperform all other general-purpose provers for Coq, including CoqHammer, Proverbot9001, and a transformer baseline by at least 148 and are available for practical use by end-users.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

Result was created during the realization of more than one project. More information in the Projects tab.

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year

2024

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

Proceedings of Machine Learning Research

ISBN

—

ISSN

2640-3498

e-ISSN

2640-3498

Number of pages

31

Pages from-to

4046-4076

Publisher name

Proceedings of Machine Learning Research

Place of publication

—

Event location

Vienna

Event date

Jul 21, 2024

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

001347135504008