Magnushammer: A Transformer-Based Approach to Premise Selection
Magnushammer利用对比学习和Transformer提升命题选择，成功率达59.5%，参数少4倍。
核心发现
方法论
Magnushammer采用两阶段检索策略：首先利用Transformer编码的proof state与premise的余弦相似度进行快速筛选（SELECT），选出前1024个候选premises；然后通过proof state与premise的交互式编码，进行重排序（RERANK），以获得更精确的相关性评分。训练过程中，SELECT使用InfoNCE损失，RERANK采用二元交叉熵。模型基于预训练的Transformer骨架，输入为proof state和premise的文本描述，利用对比学习优化嵌入空间的相似性。数据集由超过4.4百万个（proof state, premise）对组成，涵盖了Isabelle的庞大证明库。
关键结果
- 在PISA基准测试中，Magnushammer实现了59.5%的成功率，显著优于Sledgehammer的38.3%。在miniF2F测试中，成功率达34.0%，优于20.9%的基线。与基于语言模型的自动定理证明器结合后，PISA的成功率从57.0%提升至71.0%，参数减少4倍。模型在不同计算预算下表现出良好的扩展性，特别是在中等资源条件下优势明显。
- 通过引入大规模的文本描述数据，Magnushammer实现了对传统符号方法的超越，展现了深度学习在形式化推理中的潜力。数据集的规模和多样性保证了模型的泛化能力，训练样本中包含人类和Sledgehammer生成的证明路径，增强了模型的鲁棒性。模型参数从38M到86M不等，性能随规模提升而稳步增长。
- 在多步推理场景中，结合Thor框架，Magnushammer实现了71.0%的最高成功率，超越了以往的多步推理方法。实验证明，模型在参数和数据规模有限的情况下，仍能保持优异性能，显示出极佳的效率和实用性。
研究意义
该研究突破了自动定理证明中命题选择的瓶颈，利用深度Transformer模型实现高效、低成本的相关性检索，显著提升了符号推理的自动化水平。其在大规模文本描述数据上的成功，表明深度学习模型具备理解复杂数学语境的潜力，为未来形式化数学和AI推理系统的发展提供了新思路。该方法不仅减少了对领域专家的依赖，还能广泛应用于不同的证明助手和逻辑体系中，推动自动推理技术的普及与创新。
技术贡献
本研究提出了基于对比学习的Transformer命名实体嵌入方法，用于命题选择，突破了传统符号方法对工程和领域知识的依赖。引入两阶段检索机制，有效结合快速筛选与上下文重排序，提升了检索质量。数据集的规模和多样性为深度模型提供了丰富的训练资源，模型参数较少但表现优异，验证了深度学习在形式推理中的潜力。模型架构和训练策略为未来大规模知识库的高效利用提供了技术基础。
新颖性
这是首个将对比学习与Transformer结合应用于命题选择的研究，提出了层次化检索框架，显著优于传统符号和深度模型方法。首次公开了规模最大、内容丰富的Isabelle专用数据集，为学界提供了宝贵资源。该方法在参数效率和性能方面均实现突破，展示了深度模型在符号推理中的新可能。
局限性
- 模型对极端复杂或模糊的证明状态仍存在理解困难，尤其在推理路径多样或信息不足时表现有限。训练数据虽大但偏向特定逻辑体系，迁移到其他证明助手或逻辑体系时可能需要调整。计算成本虽低于传统方法，但大规模预训练和推理仍需一定硬件资源，限制了广泛部署。此外，模型在极少样本或新颖证明场景中的泛化能力仍需验证。
未来方向
未来将探索多模态信息融合，结合结构化知识和自然语言描述，提升模型理解能力。还计划扩展到其他证明体系和逻辑，增强模型的通用性。优化模型结构以降低计算成本，提升推理速度。同时，将引入主动学习和持续学习机制，动态更新知识库，适应不断增长的数学知识体系。
AI 总览摘要
自动定理证明的核心难题之一是高效准确地选择相关命题（premises），以支持复杂数学证明。传统方法依赖符号工程和领域知识，成本高、适应性差。本文提出Magnushammer，一种基于Transformer的深度学习模型，通过对比学习实现两阶段检索：快速筛选（SELECT）和上下文重排序（RERANK），显著提升了命题选择的质量。
在大规模文本描述数据和预训练模型基础上，Magnushammer在PISA和miniF2F基准测试中分别达到59.5%和34.0%的成功率，优于最先进的Sledgehammer工具。与基于语言模型的自动定理证明器结合后，成功率在PISA上从57.0%提升到71.0%，参数减少四倍，显示出极佳的效率和效果。
该方法的核心在于利用Transformer编码proof state和premise的文本描述，通过对比学习优化嵌入空间，实现高效检索。两阶段机制结合了快速筛选和精确重排序，兼顾效率与准确性。大规模数据集的支持使模型具备良好的泛化能力，验证了深度学习在形式化推理中的潜力。
这项研究不仅推动了自动定理证明技术的边界，也为未来在不同证明助手和逻辑体系中的应用提供了可能。其低参数成本和高性能表现，为构建智能化数学推理系统奠定了基础。未来工作将关注模型的迁移能力、多模态融合及持续学习，推动自动推理技术的广泛普及。
深度分析
研究背景
数学推理的自动化已成为人工智能的重要方向之一。早期符号方法如Resolution和自然演绎在形式化证明中取得一定成效，但对知识工程和逻辑结构依赖较大。近年来，深度学习特别是Transformer模型在自然语言处理中的成功激发了其在数学推理中的应用潜力。代表性工作包括DeepMath、HOList、GPT-3在数学推理中的尝试，以及符号与神经结合的混合方法。尽管如此，命题选择仍面临效率与准确性难题，传统符号工具如Sledgehammer依赖手工特征和启发式，难以充分利用大规模数据。本文在此基础上，提出基于对比学习的Transformer模型，结合大规模文本描述，突破了现有瓶颈。
核心问题
自动定理证明中，命题选择是关键环节。现有符号方法依赖工程化特征提取，难以适应不同逻辑体系，且在大规模知识库中效率不足。深度学习模型虽具潜力，但缺乏大规模、标注丰富的训练数据，导致性能有限。如何在保证效率的同时，提升命题相关性检索的准确性，成为亟待解决的问题。此外，现有方法在多步推理和大规模知识库中表现不佳，限制了自动推理的实用性和普及。
核心创新
本研究的核心创新包括：1）提出基于对比学习的Transformer嵌入机制，有效捕捉proof state与premise的语义关系；2）设计两阶段检索框架，结合快速筛选（SELECT）和上下文重排序（RERANK），兼顾效率与精度；3）构建并公开了规模最大、内容丰富的Isabelle专用命题选择数据集，支持深度模型训练。相比传统符号方法，模型参数更少，训练数据利用率更高，能在有限资源下实现优异性能。这些创新共同推动了深度推理模型的实用化。
方法详解
- �� 采用预训练Transformer作为基础架构，输入为proof state和premise的文本描述。
- �� 通过对比学习（InfoNCE）训练SELECT模块，使其在嵌入空间中最大化相关命题的相似性。
- �� SELECT模块快速计算proof state与所有premise的余弦相似度，筛选出前1024个候选。
- �� RERANK模块利用proof state与premise的交互式编码，输出更精确的相关性评分，重新排序候选premises。
- �� 训练过程中，使用正负样本对优化模型，正样本为实际使用的premise，负样本为随机或最可能的误判premise。
- �� 构建大规模（4.4百万个实例）数据集，结合人类和Sledgehammer生成的证明路径，增强模型泛化能力。
- �� 在推理阶段，先用SELECT快速筛选，再用RERANK进行细致排序，最后选择前KR个premise用于证明。
实验设计
- �� 采用PISA和miniF2F两个公开基准，评估模型的成功率。
- �� 比较Sledgehammer、BM25、TF-IDF、OpenAI嵌入等多种检索方法。
- �� 使用不同模型参数（38M、86M）进行训练，调优超参数如批次大小、负样本比例。
- �� 进行消融实验，验证两阶段检索的贡献。
- �� 在多步推理场景中，结合Thor框架，测试模型在复杂证明中的表现。
- �� 评估模型在不同计算预算下的扩展性和效率。
结果分析
- �� Magnushammer在PISA基准上达59.5%的成功率，优于Sledgehammer的38.3%，提升显著。
- �� 在miniF2F中，成功率达34.0%，优于20.9%的基线。
- �� 与语言模型结合后，PISA成功率从57.0%提升至71.0%，参数减少4倍。
- �� 在不同计算预算下，模型表现稳定，特别在中等资源条件中优势明显。
- �� 大规模数据集和对比学习策略显著提升了模型的泛化能力和检索质量。
应用场景
- �� 适用于各种证明助手（如Isabelle、Coq、Lean）中的自动命题选择，降低人工成本。
- �� 支持自动化数学推理、定理验证和复杂证明的自动生成，推动AI在数学和逻辑领域的应用。
- �� 长远来看，可用于构建通用推理系统，辅助科学研究、工程设计和教育培训，提升自动化水平。
局限与展望
- �� 模型在极端复杂或模糊状态下仍表现有限，特别是在信息不足或推理路径多样时。
- �� 训练数据偏向特定逻辑体系，迁移到其他体系可能需重新调优。
- �� 大规模预训练和推理仍需较高硬件资源，限制普及。
- �� 泛化能力在新颖或少样本场景中尚待验证，未来需优化模型的适应性。
通俗解读 非专业人士也能看懂
想象你在厨房做饭，准备一道复杂的菜肴。每次你需要找到合适的调料（premises）来完成一道菜（证明）。传统方法就像靠记忆和经验，手工挑选每个调料，费时费力。现在，Magnushammer像一个聪明的助手，它能快速扫描所有调料的标签（文本描述），判断哪些可能适合当前菜肴。它先用快速筛选（SELECT）把一大堆调料缩小到最可能的几样，然后再用更细致的检查（RERANK）确认它们的适用性。这样一来，厨师（证明者）就能更快找到合适的调料，做出美味的菜肴。这种方法让厨房变得更高效，也让厨师不用记太多复杂的配方，依靠智能助手就能完成复杂的任务。
简单解释 像给14岁少年讲一样
想象你在学校里准备科学项目，你需要找到一些资料（premises）来支持你的实验（证明）。以前，你可能要翻很多书，靠记忆和经验挑选资料，这很花时间，也容易忘记重要的内容。现在，有个聪明的机器人助手（Magnushammer），它可以帮你快速找到和你的项目最相关的资料。它先用一个快速搜索，把所有资料中最可能有用的几百个筛出来，然后再用更聪明的办法，逐个检查这些资料，挑出最合适的几条。这样，你就可以用更少的时间，找到最有用的资料，完成你的科学项目。这个助手用的是最新的AI技术，能理解资料的内容，就像你用智能搜索一样，帮你省时省力，还能做得更好！
原文摘要
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.