Graph2Tac: Online Representation Learning of Formal Math Concepts

Kód výsledku v 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>

Výsledek na webu

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

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Graph2Tac: Online Representation Learning of Formal Math Concepts

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Graph2Tac: Online Representation Learning of Formal Math Concepts

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

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

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

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

Rok uplatnění

2024

Kód důvěrnosti údajů

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

Název statě ve sborníku

Proceedings of Machine Learning Research

ISBN

—

ISSN

2640-3498

e-ISSN

2640-3498

Počet stran výsledku

31

Strana od-do

4046-4076

Název nakladatele

Proceedings of Machine Learning Research

Místo vydání

—

Místo konání akce

Vienna

Datum konání akce

21. 7. 2024

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

001347135504008