아리스토텔레스: 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
초록
우리는 형식적 검증(formal verification)과 비형식적 추론(informal reasoning)을 결합한 AI 시스템인 Aristotle을 소개한다. 이 시스템은 2025년 국제 수학 올림피아드 문제에서 금메달 수준의 성능을 달성했다. Aristotle은 세 가지 주요 구성 요소를 통합한다: Lean 증명 탐색 시스템, 보조정리를 생성하고 형식화하는 비형식적 추론 시스템, 그리고 전용 기하학 문제 해결기이다. 우리의 시스템은 자동 정리 증명(automated theorem proving) 분야에서 최첨단 성능과 우수한 확장성을 보여준다.
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.