Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2401.02949 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916298412261376 |
|---|---|
| author | Blaauwbroek, Lasse Olšák, Miroslav Rute, Jason Massolo, Fidel Ivan Schaposnik Piepenbrock, Jelle Pestun, Vasily |
| author_facet | Blaauwbroek, Lasse Olšák, Miroslav Rute, Jason Massolo, Fidel Ivan Schaposnik Piepenbrock, Jelle Pestun, Vasily |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_02949 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Graph2Tac: Online Representation Learning of Formal Math Concepts Blaauwbroek, Lasse Olšák, Miroslav Rute, Jason Massolo, Fidel Ivan Schaposnik Piepenbrock, Jelle Pestun, Vasily Machine Learning Artificial Intelligence 68T07 (Primary) 68V15 (Secondary) I.2.3; I.2.6 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. |
| title | Graph2Tac: Online Representation Learning of Formal Math Concepts |
| topic | Machine Learning Artificial Intelligence 68T07 (Primary) 68V15 (Secondary) I.2.3; I.2.6 |
| url | https://arxiv.org/abs/2401.02949 |