Solving olympiad geometry without human demonstrations | Nature
올림피아드 수준의 기하학 증명은 인간 수준의 자동 추론에서 중요한 이정표로, 전 세계 최고의 수학 인재들에게도 도전적인 문제로 알려져 있다. 기존의 기계 학습 방법은 대부분의 수학 분야에서 인간 증명을 기계 검증 형식으로 변환하는 높은 비용으로 적용되지 않는다.
연구팀은 인간 시연에 의존하지 않고 수백만 개의 정리와 증명을 합성하여 유클리드 평면 기하학을 위한 정리 증명기 '알파지오메트리(AlphaGeometry)'를 제안한다. 이는 신경언어 모델과 기호 추론 엔진을 사용하여 어려운 문제에서 무한 분기점을 통해 안내한다.
알파지오메트리는 30개의 최신 올림피아드 수준 문제 중 25개를 해결하며, 이전 최고 방법보다 우수하고 국제 수학 올림피아드 금메달리스트의 평균 성능에 근접한다. 모든 기하학 문제를 풀고, 2004년에 번역된 국제 수학 올림피아드 정리의 일반화된 버전을 발견한다.