ProofFusion：通过自适应检索增强推理提升神经定理证明性能

《Proceedings of the ACM on Software Engineering》：ProofFusion: Improving Neural Theorem Proving via Adaptive Retrieval-Augmented Reasoning

　　

摘要AI总结

要查看此由AI生成的总结，您需要拥有高级访问权限。

了解更多登录

摘要

摘要

交互式定理证明是一种确保复杂软件系统正确性的强大方法。然而，它通常需要大量的人工工作，因此在实际应用中成本较高。最近，基于神经网络的方法在自动生成证明策略方面显示出潜力。不过，现有方法存在训练数据中策略使用分布不均的问题。少数常用策略占据了概率分布的主导地位，而许多罕见但至关重要的策略则在模型的候选排序中被持续忽视。这种分布偏差可能导致在证明搜索过程中过早放弃原本可以证明的目标。此外，神经网络在生成策略时的决策过程缺乏明确的推理轨迹，使得人类难以解释或验证其背后的逻辑。为了解决这些限制，我们提出了ProofFusion，这是一种自适应的检索增强推理框架，无需重新训练即可提升神经定理证明器的证明能力。我们的核心灵感来自于人类证明者通过参考类似已证明的定理来指导自己推理的方式。具体而言，我们开发了一种具备证明语义感知能力的检索器，它能从知识库中查找语义上相似的历史证明目标及其策略，从而生成一组可追溯的参考决策。接着，我们采用双轨重排融合机制，将神经模型的原始预测与检索到的参考策略相结合。此外，为减少检索可能引入的噪声，我们设计了一种能力自适应检索机制，能够动态判断何时应用检索。我们在真实的交互式定理证明环境中，对26个Coq项目中的10,782个定理进行了系统性评估。实验结果表明，ProofFusion使四种最先进的神经定理证明器证明的定理数量平均增加了6.89%，同时还证明了17.50%之前无法证明的定理。此外，它还显著提高了证明步骤的可解释性，四种证明器的平均可解释证明目标比例达到了82.1%。总体而言，这些结果表明ProofFusion是现有神经定理证明系统的实用且有效的补充，提升了系统的性能和可解释性。

AI总结

AI生成的总结（实验性）

此总结是由自动化工具生成的，未经文章作者撰写或审核。它旨在帮助读者发现相关内容、评估文章相关性，以及帮助来自相关研究领域的读者理解本文内容。它是对作者提供的摘要的补充，而作者提供的摘要仍是文章的主要总结。完整文章仍是权威版本。点击此处了解更多。

点击此处，可以对该总结的准确性、清晰度和实用性发表意见。您的反馈将有助于改进未来的总结版本。

要查看此由AI生成的通俗语言总结，您需要拥有高级访问权限。