SubgoalXL: 정리 증명을 위한 하위목표 기반 전문가 학습

수학과 컴퓨터 과학의 교차점에 위치한 형식적 정리 증명 분야는 대형 언어 모델(LLMs)의 발전으로 인해 재조명되고 있습니다. 본 논문에서는 이사벨 환경에서 LLMs의 형식적 정리 증명 능력을 향상시키기 위해 하위목표 기반 증명과 전문가 학습을 결합한 새로운 접근 방식인 SubgoalXL을 소개합니다. SubgoalXL은 두 가지 중요한 문제를 해결합니다: 특화된 수학 및 정리 증명 데이터의 부족, 그리고 LLMs의 개선된 다단계 추론 능력 필요성입니다. 데이터 효율성을 최적화하고 하위목표 수준의 감독을 사용하여, SubgoalXL은 제한된 인간 생성 증명에서 더 풍부한 정보를 추출합니다. 이 프레임워크는 하위목표 지향적인 증명 전략과 전문가 학습 시스템을 통합하여, 형식적 문장, 증명, 그리고 하위목표 생성기를 반복적으로 개선합니다. Isabelle 환경이 하위목표 기반 증명에서 제공하는 장점을 활용하여, SubgoalXL은 표준 miniF2F 데이터셋에서 56.1%의 새로운 최고 성능을 달성하였습니다. 이는 절대적으로 4.9%의 향상을 의미하며, 특히 SubgoalXL은 miniF2F에서 41개의 AMC12 문제, 9개의 AIME 문제, 그리고 3개의 IMO 문제를 성공적으로 해결하였습니다. 이러한 결과들은 제한된 데이터 활용도를 극대화하고 복잡한 추론에 대한 목표 지향적 가이드를 적용함으로써 형식적 정리 증명에서 효과를 입증하며, AI 추론 능력의 지속적인 발전에 기여하고 있습니다. 구현은 \url{https://github.com/zhaoxlpku/SubgoalXL}에서 확인할 수 있습니다.