범용 대규모 언어모델(LLM)이 형식 수학 정리 증명에서 최고 수준 성능을 달성하도록 지원하는 에이전트 프레임워크 LEAP가 arXiv에 공개됐다. LLM은 비형식적 수학 추론에는 강하지만 린(Lean) 같은 형식 언어로 기계적으로 검증 가능한 증명을 생성하는 데는 어려움을 겪어 왔다. LEAP는 비형식적 추론, 지시 따르기, 반복적 자기 개선 같은 파운데이션 모델의 역량을 활용해 이 간극을 메우는 것을 목표로 한다.
LEAP는 복잡한 문제를 더 작은 단위로 분해하고, 린 컴파일러와의 지속적 상호작용을 통해 비형식적 증명 청사진과 형식 코드 구성을 연결하는 방식으로 작동한다. 벤치마크 평가에서 두 가지 주목할 만한 결과가 나왔다. 2025년 퍼트남 수학 경시대회(Putnam Competition) 12문제를 모두 해결해 최근 특화 형식 수학 모델과 동등한 성과를 냈다. 또한 연구팀이 새로 만든 Lean-IMO-Bench에서 범용 LLM의 단회(one-shot) 형식 해결률을 10% 미만에서 70%로 끌어올렸으며, 이는 금메달급 전문 IMO 시스템이 세운 48% 기준을 넘어선 수치다.
LEAP는 응용 연구 수준의 활용 가능성도 입증했다. 짝수 차수 케일리 그래프(Cayley graph)의 해밀턴 분해를 다루는 크누스(Knuth)의 짝수 차수 케일리 그래프 해밀턴 분해 문제의 핵심 하위 문제에 대해 검증된 형식 증명을 자율적으로 생성했다. 논문은 2026년 6월 2일 arXiv에 제출됐으며 하루 뒤 수정 버전(v2)으로 갱신됐다.
형식 수학 정리 증명 자동화는 소프트웨어 검증, 수학 교육 보조, 미해결 문제 탐색 등 광범위한 응용 가능성을 가진 분야다. 기존에는 특화 모델이나 전통적 정리 증명기가 주를 이뤘지만, LEAP는 범용 LLM에 에이전트 프레임워크를 결합하는 방식으로 전문 시스템과 경쟁하는 성능을 달성했다는 점에서 주목받는다.
