# 自动化定理证明的最小化智能体 ## 摘要我们提出了一个最小化智能体架构。.

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