APOLLO는 Lean 컴파일러와 LLM의 추론 능력을 결합하여 수학 정리를 증명하는 자동화된 정리 증명 시스템입니다. 기존의 LLM 기반 정리 증명 방식은 많은 샘플링(수천 번)을 통해 검증 시스템을 통과하는 증명을 생성하는 반면, APOLLO는 LLM이 증명을 생성하고, 에이전트들이 증명의 구문 오류를 수정하고, Lean을 사용하여 실수를 파악하고, 실패한 부분 정리를 분리하고, 자동 솔버를 활용하며, 남은 목표에 대해 저렴한 비용으로 LLM을 호출하는 모듈식 파이프라인을 사용합니다. 수정된 부분 증명을 재결합하고 재검증하는 과정을 사용자 제어 가능한 최대 시도 횟수까지 반복합니다. miniF2F 벤치마크에서 8B 미만 매개변수 모델 중 84.9%의 정확도를 달성했으며, 샘플링 비용은 100 미만으로 유지했습니다. 또한, GoedelProverSFT의 정확도를 65.6%로 높이고, 샘플 복잡도를 25,600에서 수백으로 줄였습니다.
