공식 수학 문장 커리큘럼 학습

형식적 수학에 적용된 언어 모델링의 맥락에서 전문가 반복(Expert Iteration)의 활용을 탐구한다. 동일한 계산 자원 예산 하에서, 학습과 함께 증명 탐색을 반복적으로 수행하는 전문가 반복 방식이 단순한 증명 탐색에 비해 뚜렷이 우수함을 보여준다. 또한, 다양한 난이도를 가진 형식적 명제 집합에 적용했을 때, 전문가 반복은 해당 문제들의 난이도가 점차 증가하는 교육 과정(curriculum)을 스스로 발견하고 해결할 수 있으며, 이 과정에서 참값(ground-truth) 증명이 필요하지 않다는 점을 관찰하였다. 마지막으로, 수작업으로 정제된 문제 명제 집합에 이 전문가 반복 기법을 적용함으로써, miniF2F 벤치마크에서 최신 기준(SOTA, State-of-the-Art) 성능을 달성하였으며, 고등학교 올림피아드에서 출제된 다수의 도전적인 문제를 자동으로 해결하는 데 성공하였다.