Magnushammer：一种基于Transformer的前提选择方法
Magnushammer: A Transformer-Based Approach to Premise Selection
AI总结：
本文提出Magnushammer，一种基于Transformer对比训练的前提选择方法，在PISA和miniF2F基准上超越Sledgehammer，并结合语言模型将证明成功率提升至71%，同时开源了最大的前提选择数据集。
摘要：
本文提出了一种新颖的前提选择方法，这是自动定理证明中的一个关键推理任务。传统上，该任务依赖于符号方法，这些方法需要大量的领域知识和工程投入。相比之下，本研究证明，采用Transformer架构的对比训练可以在无需工程开销的情况下实现更高质量的相关前提检索。我们的方法Magnushammer在交互式定理证明中超越了最先进且广泛使用的自动化工具Sledgehammer。在PISA和miniF2F基准测试上，Magnushammer的成功率分别达到59.5%（对比38.3%）和34.0%（对比20.9%）。通过将我们的方法与基于语言模型的自动定理证明器相结合，我们在PISA基准上将最先进的证明成功率从57.0%提升至71.0%，同时使用的参数减少了4倍。此外，我们开发并开源了一个新颖的前提选择数据集，其中包含（证明状态，相关前提）对的文本表示。据我们所知，这是最大的可用前提选择数据集，也是首个针对Isabelle证明助手的数据集。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
