一个极简智能体实现高效自动定理证明，成本更低。
A Minimal Agent for Automated Theorem Proving
- 采用迭代优化+知识库检索的极简智能体架构
- 在多个测试集上表现接近顶尖模型，成本仅为几分之一
- 适合想快速验证想法或资源有限的研究者使用
我们提出一种极简智能体基线，可系统性比较不同基于AI的定理证明架构。该设计实现了当前先进系统的共性功能：迭代式证明优化、知识库搜索与上下文管理。通过在多种不同基准上评估，对比了前沿语言模型和设计选择。结果表明，该方法在性能上媲美最先进方案，但架构更简单，成本显著降低。同时，我们证实迭代策略相比单次生成在样本效率和成本效益上具有一致优势。代码已开源，可作为未来研究参考，也向社区提供了一个可访问的定理证明工具。
原文摘要 · Abstract (English)
We propose a minimal agentic baseline that enables systematic comparison across different AI-based theorem prover architectures. This design implements the core features shared among state-of-the-art systems: iterative proof refinement, library search and context management. We evaluate this agentic approach using qualitatively different benchmarks and compare various frontier language models and design choices. Our results show competitive performance compared to state-of-the-art approaches, while using a significantly simpler architecture and a fraction of their cost. Additionally, we demonstrate consistent advantages of an iterative approach over multiple single-shot generations, especially in terms of sample efficiency and cost effectiveness. The implementation is released open-source as a candidate reference for future research and as an accessible prover for the community.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。