본 논문은 대규모 언어 모델(LLM)을 활용한 자동 정리 증명 분야에서 기존의 전술 기반 생성 방식과 전체 증명 생성 방식을 결합한 새로운 프레임워크인 HybridProver를 제시한다. HybridProver는 LLM을 이용하여 전체 증명 후보를 생성하고, 이로부터 증명 개요를 추출한 후, 전술 기반 생성 모델과 자동화 도구를 활용하여 단계적으로 증명을 완성하는 방식이다. Isabelle 정리 증명기에 HybridProver를 구현하고, 최적화된 Isabelle 데이터셋으로 LLM을 미세 조정하여 miniF2F 데이터셋에서 59.4%의 성공률을 달성, 기존 최고 성능(56.1%)을 능가하는 결과를 보였다. 데이터셋 품질, 훈련 매개변수, 샘플링 다양성이 자동 정리 증명에 미치는 영향도 분석하였다. 모든 코드, 데이터셋, LLM은 오픈소스로 공개되었다.
