최근 인공지능(AI) 기반의 수학 정리 증명기(theorem prover)는 놀라운 발전을 보이고 있지만, 이를 위해서는 방대한 양의 학습 데이터와 엄청난 연산 자원이 필요하다는 한계가 있었습니다. 이러한 문제를 해결하기 위해 새로운 오픈소스 린(Lean) 정리 증명기 '피타고라스-프루버(Pythagoras-Prover)'가 등장했습니다. 이 증명기는 실용적인 연산 예산 내에서 효율적으로 작동하면서도, 기존의 훨씬 큰 규모의 모델들을 뛰어넘는 성능을 보여주며 AI 수학 증명 분야에 새로운 가능성을 제시하고 있습니다.
피타고라스-프루버는 두 가지 핵심 패러다임을 결합합니다. 첫째, 40억(4B) 및 320억(32B) 매개변수 규모의 자동회귀(autoregressive) 모델을 통해 순차적인 추론 능력을 강화했습니다. 둘째, 개념 증명(proof-of-concept) 단계의 40억 매개변수 확산(diffusion) 기반 증명기를 도입하여 추론 시 린(Lean) 증명을 반복적으로 개선하는 방식을 사용합니다. 학습 효율성을 높이기 위해, 연구팀은 린(Lean)으로 검증된 코퍼스를 쉬움, 중간, 어려움 난이도로 계층화하여 커리큘럼 기반의 지도 미세조정(SFT)을 수행했습니다. 이를 통해 모델은 짧고 간단한 증명부터 길고 복잡한 증명까지 점진적으로 증명 기술을 습득하게 됩니다. 또한, 동적 증명 추론 필터링(dynamic proof-reasoning filtering) 기법을 도입하여 정보 가치가 높은 증명 추적(proof traces)을 보존하면서도 각 인스턴스를 8k 토큰 컨텍스트 예산 내로 유지했습니다.
특히 주목할 만한 기술은 '증강된 린 정형화(Augmented Lean Formalisation, ALF)'입니다. 이는 부족한 검증된 코퍼스를 다양한 형식적 진술 변형으로 확장하는 기법으로, 모든 변형 인스턴스를 일일이 정형적으로 검증하지 않고도 자가 증류(self-distillation)를 통해 추가적인 학습 신호를 제공합니다. 알려진 문제를 교란하면서도 형식적 특성을 유지함으로써, ALF는 특정 진술의 표면적 형태에 대한 의존도를 줄여줍니다. 이러한 혁신적인 접근 방식 덕분에 피타고라스-프루버-4B는 167배 적은 매개변수에도 불구하고 MiniF2F-Test 벤치마크에서 기존 최고 성능 모델인 딥시크-프루버-V2-671B(DeepSeek-Prover-V2-671B)를 능가하는 86.1%의 정확도(pass@32)를 달성했습니다. 피타고라스-프루버-32B는 오픈소스 모델 중 최고 수준인 93.0%의 정확도를 기록했으며, PutnamBench 문제 672개 중 93개를 해결하는 인상적인 성과를 보였습니다. 이러한 결과는 AI 기반 수학 증명기가 더 적은 자원으로도 복잡한 수학 문제를 해결할 수 있음을 입증하며, AI를 활용한 과학 및 공학 연구에 중요한 도구로 자리매김할 잠재력을 보여줍니다.