본 논문은 대규모 언어 모델(LLM)을 이용한 자동 정리 증명 분야에서, 기존의 반복적인 증명 생성 방식의 한계를 극복하기 위해 APOLLO라는 새로운 파이프라인을 제시합니다. APOLLO는 Lean 컴파일러와 LLM의 추론 능력을 결합하여 증명 생성의 정확성을 높이고 샘플링 비용을 낮춥니다. LLM이 생성한 증명을 여러 에이전트가 분석하고, 구문 오류를 수정하며, Lean을 이용해 오류를 식별하고, 실패한 하위 보조정리를 분리하고, 자동 솔버를 활용하며, 남은 목표에 대해 LLM을 저렴한 top-K 예산으로 호출하는 모듈화되고 모델에 독립적인 과정을 자동화합니다. 수정된 하위 증명을 재결합하고 재검증하는 과정을 사용자가 제어하는 최대 시도 횟수까지 반복합니다. miniF2F 및 Goedel-Prover-SFT 벤치마크에서 기존 최고 성능을 능가하는 결과를 달성하며, 샘플링 비용을 크게 줄였습니다.
