AI系统在数学奥赛中达到金牌水平，融合形式与非形式推理。
Aristotle: IMO-level Automated Theorem Proving
- 结合形式验证与非形式推理，自动生成并形式化定理。
- 在2025年国际数学奥林匹克问题上表现相当于金牌水平。
- 专设几何求解器，具备良好可扩展性，适合自动化证明研究者。
我们提出Aristotle，一个将形式验证与非形式推理相结合的AI系统，在2025年国际数学奥林匹克（IMO）问题上实现了相当于金牌的性能。该系统由三部分组成：一个用于Lean证明搜索的系统、一个生成并形式化引理的非形式推理模块，以及一个专用几何求解器。实验表明，该系统在自动化定理证明任务中达到当前最优表现，且具备良好的可扩展性，为复杂数学命题的自动验证提供了新范式。
原文摘要 · Abstract (English)
We introduce Aristotle, an AI system that combines formal verification with informal reasoning, achieving gold-medal-equivalent performance on the 2025 International Mathematical Olympiad problems. Aristotle integrates three main components: a Lean proof search system, an informal reasoning system that generates and formalizes lemmas, and a dedicated geometry solver. Our system demonstrates state-of-the-art performance with favorable scaling properties for automated theorem proving.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。