2024 年 8 月 9 日，Yann LeCun 等研究人员在 NeurIPS 2022 上发表的论文《HyperTree Proof Search for Neural Theorem Proving》引起了广泛关注。这篇论文介绍了一种新的搜索算法 ——HyperTree Proof Search（HTPS），旨在通过神经网络改进自动定理证明的效率和准确性。该研究由 Meta 研究团队的 Fabian Gloeckle、Guillaume Lample、Thibaut Lacroix、Mathieu Lachaux、Aurélien Rodriguez、Amaury Hayat、Thibaut Lavril、Gabriel Ebner 和 Javier M. 等人共同完成，并在 GitHub 上公开了相关代码。
HTPS 算法的灵感来源于 AlphaZero 的成功，采用了一种在线训练程序，通过 Transformer 模型实现自动定理证明。HTPS 通过在线训练从之前的证明搜索中学习，使其能够推广到远离训练分布的领域。研究团队在三个复杂度递增的环境中对其主要组件进行了详细的消融研究，结果显示，单凭 HTPS，模型在 Metamath 定理集上的证明成功率达到了 65.4%，超过了之前 GPT-f 的 56.5%。通过对这些未证明的定理进行在线训练，准确率进一步提高到 82.6%。在类似的计算预算下，HTPS 在基于 Lean 的 miniF2F-curriculum 数据集上的证明准确率从 31% 提高到 42%。
HTPS 算法不仅在数学研究中具有重要意义，还可以应用于其他科学领域，如物理学和计算机科学。与传统的自动定理证明系统（ATP）相比，HTPS 通过在线训练和 Transformer 模型的结合，提高了证明的效率和准确性。与交互式定理证明系统（ITP）相比，HTPS 能够自动生成证明步骤，减少了人类干预的需求。