用于神经定理证明的HyperTree Proof Search

我们提出了一种基于Transformer架构的自动化定理证明器的在线训练方法。该方法引入了一种受AlphaZero近期成功启发的新搜索算法——超树证明搜索（HyperTree Proof Search, HTPS）。通过在线训练，模型能够从过往的证明搜索过程中持续学习，从而具备在远超训练数据分布的领域中进行泛化的能力。我们通过对三个复杂度逐步提升的环境进行详细消融实验，评估了该流水线主要组件的性能表现。特别地，我们发现仅使用HTPS算法，即使在仅用带注释的证明数据进行训练的情况下，模型也能成功证明65.4%的Metamath定理保留集，显著优于此前由GPT-f达到的56.5%的最先进水平。进一步在未证明定理上进行在线训练后，准确率提升至82.6%。在相近的计算资源预算下，我们在基于Lean的miniF2F课程数据集上的定理证明准确率也从31%提升至42%，实现了该任务上的显著性能突破。