アリストテレス：IMOレベルの自動定理証明
Aristotle: IMO-level Automated Theorem Proving
October 1, 2025
著者: Tudor Achim, Alex Best, Kevin Der, Mathïs Fédérico, Sergei Gukov, Daniel Halpern-Leister, Kirsten Henningsgard, Yury Kudryashov, Alexander Meiburg, Martin Michelsen, Riley Patterson, Eric Rodriguez, Laura Scharff, Vikram Shanker, Vladmir Sicca, Hari Sowrirajan, Aidan Swope, Matyas Tamas, Vlad Tenev, Jonathan Thomm, Harold Williams, Lawrence Wu
cs.AI
要旨
我々は、形式的検証と非形式的推論を組み合わせたAIシステム「アリストテレス」を紹介する。このシステムは、2025年の国際数学オリンピックの問題において金メダル相当の性能を達成した。アリストテレスは、Lean証明探索システム、補題を生成し形式化する非形式的推論システム、および専用の幾何学ソルバーの3つの主要コンポーネントを統合している。本システムは、自動定理証明において最先端の性能を示し、良好なスケーリング特性を有している。
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.