@inproceedings{
miku{\l}a2023magnushammer,
title={Magnushammer: A Transformer-Based Approach to Premise Selection},
author={Maciej Miku{\l}a and Szymon Antoniak and Szymon Tworkowski and Bartosz Piotrowski and Albert Jiang and Jin Peng Zhou and Christian Szegedy and {\L}ukasz Kuci{\'n}ski and Piotr Mi{\l}o{\'s} and Yuhuai Wu},
booktitle={The 3rd Workshop on Mathematical Reasoning and AI at NeurIPS'23},
year={2023},
url={https://openreview.net/forum?id=WgaVCqZeIU}
}
We present Magnushammer: a novel approach to premise selection -- a crucial task in automated theorem proving. Traditionally, symbolic methods that rely on 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 domain knowledge or feature engineering overhead.  Magnushammer outperforms the most advanced and widely used automation tool in interactive theorem proving: 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 Magnushammer with a language-model-based theorem prover, we further improve the state-of-the-art proof success rate from $57.0\%$ to $71.0\%$ on the PISA benchmark. Moreover, we develop and open source a novel, large dataset for premise selection.
Magnushammer: A Transformer-Based Approach to Premise Selection
Maciej Mikuła Szymon Antoniak Szymon Tworkowski Bartosz Piotrowski Albert Jiang Jin Peng Zhou Christian Szegedy Łukasz Kuciński Piotr Miłoś Yuhuai Wu