본 논문은 대규모 언어 모델(LLM)을 이용한 자동 정리 증명 분야에서, Lean과 같은 형식 언어를 사용하여 수학적 정리를 증명하는 과제를 다룹니다. 기존 연구는 LLM이 정확한 형식 증명을 생성할 때까지 수천 번의 시도를 반복하는 방식을 사용했지만, 본 논문에서는 APOLLO라는 모듈형이고 모델에 독립적인 파이프라인을 제시합니다. APOLLO는 Lean 컴파일러의 강점과 LLM의 추론 능력을 결합하여 적은 샘플링 예산으로 더 나은 증명 생성 결과를 얻습니다. LLM이 정리를 증명하고, 여러 에이전트가 증명을 분석하여 구문 오류를 수정하고, Lean을 사용하여 오류를 식별하고, 실패한 하위 보조정리를 분리하며, 자동 솔버를 활용하고, 각 남은 목표에 대해 낮은 top-K 예산으로 LLM을 호출하는 완전 자동화된 프로세스를 진행합니다. 수정된 하위 증명은 재결합되고 재검증되며, 사용자가 제어하는 최대 시도 횟수까지 반복됩니다. miniF2F 벤치마크에서 7B 매개변수 모델 중 75.0%의 새로운 최첨단 정확도를 달성했으며, 샘플링 예산은 1,000회 미만으로 유지했습니다. Goedel-Prover-SFT에 대한 최첨단 정확도를 65.6%로 높였으며, 샘플 복잡도는 25,600회에서 수백 회로 감소시켰습니다. 일반 목적 모델(o3-mini, o4-mini)의 정확도는 3~7%에서 40% 이상으로 향상되었습니다. LLM 출력의 표적화된 컴파일러 기반 수정이 효율성과 정확성 모두에서 극적인 향상을 가져온다는 것을 보여주며, 확장 가능한 자동 정리 증명을 위한 일반적인 패러다임을 제시합니다.
