본 논문은 대규모 언어 모델(LLM)과 Lean 컴파일러를 결합한 모듈형 에이전트 프레임워크인 APOLLO를 제안합니다. APOLLO는 LLM의 추론 능력과 Lean 컴파일러의 강점을 활용하여 낮은 토큰 및 샘플링 예산으로 더 나은 증명 생성 결과를 달성합니다. APOLLO는 LLM이 정리에 대한 증명을 생성하고, 에이전트들이 증명을 분석, 수정, 오류 식별, 자동 해결사 활용, LLM 호출 등을 수행하는 자동화된 프로세스를 통해 작동합니다. miniF2F 벤치마크에서 APOLLO는 8B 미만 매개변수 모델에서 새로운 최고 정확도인 84.9%를 달성했으며, Goedel-Prover-SFT의 정확도를 65.6%로 향상시켰습니다.
