ATG: Benchmarking Automated Theorem Generation for Generative Language Models

人类可以发展新的定理，探索更广泛和复杂的数学结果。虽然当前的生成式语言模型（LM）在自动证明定理方面取得了显著的进展，但它们生成新的或可重复使用的定理的能力仍未得到充分探索。如果没有新的定理，当前的LM将难以证明远离给定假设的更难的定理，因为搜索空间呈指数级增长。因此，本文提出了一个自动定理生成（ATG）基准，评估代理是否能够自动生成有价值（可能是全新的）定理，作为可重用的知识，适用于下游定理证明。具体而言，我们通过根据它们的证明深度将Metamath库分为三个集合：公理、库和问题，构建了ATG基准。我们进行了广泛的实验，以调查当前的LM是否能够在库中生成定理，并使问题定理证明受益。结果表明，高质量的ATG数据有助于模型在下游ATP上的表现。然而，当前的LM仍有改进ATG并生成更先进和类似于人类的定理的空间。我们希望新的ATG挑战可以为高级复杂定理证明带来一些启示。

论文旨在解决自动证明定理中缺乏新定理的问题，提出了自动定理生成（ATG）基准测试，以评估模型是否能够生成有价值的、可重用的定理，并应用于下游定理证明。

通过将Metamath库分为公理、库和问题三个部分，构建了ATG基准测试，研究当前语言模型是否能够生成库中的定理，并对下游ATP的性能产生影响。实验结果表明，高质量的ATG数据可以提高模型在下游ATP中的性能。

论文提出了ATG基准测试，探索了自动定理生成的可能性，为下游ATP提供了可重用的知识。实验使用Metamath库进行，证明了ATG数据可以提高模型的性能。然而，当前语言模型仍有提高ATG能力的空间。

最近的相关研究包括《Neural Theorem Provers》、《DeepMath - Deep Sequence Models for Premise Selection》等。