核心发现
方法论
INT基准测试通过生成不等式定理和证明来评估自动定理证明的泛化能力。使用变压器和图神经网络作为基线，并在测试时加入蒙特卡罗树搜索（MCTS）以提高新定理的证明能力。
关键结果
- 变压器在大多数泛化任务中表现优于图神经网络，尽管其分布外泛化差距较大。使用MCTS后，测试成功率显著提高。
- 在不同的初始条件和未见过的公理组合上，图神经网络表现出更好的泛化能力。
- 变压器在训练和测试数据来自同一分布时表现更好，但在分布外任务中表现较差。
研究意义
该研究通过引入INT基准测试，显著推动了学习辅助定理证明领域的发展。它解决了数据稀缺和分布外泛化能力不足的问题，为进一步研究提供了一个轻量且用户友好的环境。
技术贡献
INT提供了一个理论上无限的数据生成过程，允许在六个不同维度上评估泛化能力。它的轻量级设计使得快速模拟成为可能，支持复杂的规划方法如MCTS。
新颖性
INT是第一个专门设计用于评估定理证明泛化能力的基准测试。与之前的基准测试不同，它提供了一个轻量且快速的证明环境。
局限性
- 变压器在分布外任务中的泛化能力较差，尤其是在公理顺序变化时。
- INT生成的定理可能不够现实，影响实际应用。
- MCTS的计算成本较高，可能限制其在大规模问题上的应用。
未来方向
未来研究可以探索如何增强变压器的分布外泛化能力，以及如何降低MCTS的计算成本。同时可以扩展INT以生成更复杂和更现实的定理。
AI 总览摘要
在学习辅助定理证明领域，泛化能力是一个关键挑战。现有解决方案通常在分布外任务中表现不佳，限制了其应用范围。为解决这一问题，研究人员提出了INT，一个专门设计用于评估定理证明泛化能力的不等式基准测试。INT通过生成理论上无限数量的定理和证明，为研究人员提供了一个轻量且快速的证明环境。
INT基准测试的核心在于其灵活的定理生成过程，允许在六个不同维度上评估泛化能力。研究人员使用变压器和图神经网络作为基线，并在测试时加入蒙特卡罗树搜索（MCTS）以提高新定理的证明能力。实验结果表明，变压器在大多数泛化任务中表现优于图神经网络，尽管其分布外泛化差距较大。
尽管INT在评估泛化能力方面取得了显著进展，但仍存在一些局限性。变压器在分布外任务中的表现较差，尤其是在公理顺序变化时。此外，INT生成的定理可能不够现实，影响实际应用。未来研究可以探索如何增强变压器的分布外泛化能力，以及如何降低MCTS的计算成本。
深度解读
原文摘要
In learning-assisted theorem proving, one of the most critical challenges is to generalize to theorems unlike those seen at training time. In this paper, we introduce INT, an INequality Theorem proving benchmark, specifically designed to test agents' generalization ability. INT is based on a procedure for generating theorems and proofs; this procedure's knobs allow us to measure 6 different types of generalization, each reflecting a distinct challenge characteristic to automated theorem proving. In addition, unlike prior benchmarks for learning-assisted theorem proving, INT provides a lightweight and user-friendly theorem proving environment with fast simulations, conducive to performing learning-based and search-based research. We introduce learning-based baselines and evaluate them across 6 dimensions of generalization with the benchmark. We then evaluate the same agents augmented with Monte Carlo Tree Search (MCTS) at test time, and show that MCTS can help to prove new theorems.