Magnushammer: A Transformer-Based Approach to Premise Selection
arxiv(2023)
摘要
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 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 4x 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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要