Thor：使用锤子整合语言模型与自动定理证明器

在定理证明中，从庞大的公理库中筛选出对证明给定猜想具有实际帮助的前提出发，是一个至关重要的任务。这一挑战对所有定理证明系统均构成难题，尤其是基于语言模型的系统，因其在处理大量文本形式的前提出时，推理能力相对有限。本文提出了一种名为Thor的框架，通过融合语言模型与自动化定理证明器，以克服上述困难。在Thor框架中，采用一类称为“锤子方法”（hammers）的技术，利用自动化定理证明器的强大能力进行前提选择，而其余所有任务则交由语言模型完成。实验结果表明，Thor将语言模型在PISA数据集上的成功率从39%提升至57%，并成功解决了8.2%的题目——这些题目单独依靠语言模型或自动化定理证明器均无法解决。此外，在显著更小的计算资源预算下，Thor在MiniF2F数据集上取得的成功率与当前最优方法相当。通过我们提供的简洁协议，Thor可轻松适配大多数主流交互式定理证明系统。