用于自动定理证明的最小智能体

我们提出了一个最小的代理基线，可以对不同的基于人工智能的定理证明器架构进行系统比较。该设计实现了最先进系统共享的核心功能：迭代证明细化、库搜索和上下文管理。我们使用不同质量的基准来评估我们的基线，并比较各种流行的模型和设计选择，并展示与最先进的方法相比的竞争性能，同时使用明显更简单的架构。我们的结果证明了迭代方法相对于多次单次生成的一致优势，特别是在样本效率和成本效益方面。该实现已开源发布，作为未来研究的候选参考和社区的可访问证明。