Magnushammer: A Transformer-Based Approach to Premise Selection
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , , , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2023
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866929280062062592 |
|---|---|
| author | Mikuła, Maciej Tworkowski, Szymon Antoniak, Szymon Piotrowski, Bartosz Jiang, Albert Qiaochu Zhou, Jin Peng Szegedy, Christian Kuciński, Łukasz Miłoś, Piotr Wu, Yuhuai |
| author_facet | Mikuła, Maciej Tworkowski, Szymon Antoniak, Szymon Piotrowski, Bartosz Jiang, Albert Qiaochu Zhou, Jin Peng Szegedy, Christian Kuciński, Łukasz Miłoś, Piotr Wu, Yuhuai |
| contents | This paper presents a novel approach to premise selection, a crucial reasoning task in automated theorem proving. Traditionally, symbolic methods that rely on extensive domain knowledge and engineering effort are applied to this task. In contrast, this work demonstrates that contrastive training with the transformer architecture can achieve higher-quality retrieval of relevant premises, without the engineering overhead. Our method, Magnushammer, outperforms the most advanced and widely used automation tool in interactive theorem proving called Sledgehammer. On the PISA and miniF2F benchmarks Magnushammer achieves $59.5\%$ (against $38.3\%$) and $34.0\%$ (against $20.9\%$) success rates, respectively. By combining \method with a language-model-based automated theorem prover, we further improve the state-of-the-art proof success rate from $57.0\%$ to $71.0\%$ on the PISA benchmark using $4$x fewer parameters. Moreover, we develop and open source a novel dataset for premise selection, containing textual representations of (proof state, relevant premise) pairs. To the best of our knowledge, this is the largest available premise selection dataset, and the first one for the Isabelle proof assistant. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2303_04488 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Magnushammer: A Transformer-Based Approach to Premise Selection Mikuła, Maciej Tworkowski, Szymon Antoniak, Szymon Piotrowski, Bartosz Jiang, Albert Qiaochu Zhou, Jin Peng Szegedy, Christian Kuciński, Łukasz Miłoś, Piotr Wu, Yuhuai Machine Learning Artificial Intelligence Logic in Computer Science This paper presents a novel approach to premise selection, a crucial reasoning task in automated theorem proving. Traditionally, symbolic methods that rely on extensive domain knowledge and engineering effort are applied to this task. In contrast, this work demonstrates that contrastive training with the transformer architecture can achieve higher-quality retrieval of relevant premises, without the engineering overhead. Our method, Magnushammer, outperforms the most advanced and widely used automation tool in interactive theorem proving called Sledgehammer. On the PISA and miniF2F benchmarks Magnushammer achieves $59.5\%$ (against $38.3\%$) and $34.0\%$ (against $20.9\%$) success rates, respectively. By combining \method with a language-model-based automated theorem prover, we further improve the state-of-the-art proof success rate from $57.0\%$ to $71.0\%$ on the PISA benchmark using $4$x fewer parameters. Moreover, we develop and open source a novel dataset for premise selection, containing textual representations of (proof state, relevant premise) pairs. To the best of our knowledge, this is the largest available premise selection dataset, and the first one for the Isabelle proof assistant. |
| title | Magnushammer: A Transformer-Based Approach to Premise Selection |
| topic | Machine Learning Artificial Intelligence Logic in Computer Science |
| url | https://arxiv.org/abs/2303.04488 |