LLM(대규모 언어 모델)이 생성한 피드백을 학습 신호로 삼아 형식 정리 증명 시스템 Lean에서의 추론 성능을 끌어올리는 ‘피드백 증류(Feedback Distillation)’ 기법이 arXiv에 발표됐다. Lean은 수학적 정리를 기계가 검증할 수 있는 형식 언어로 기술하고 증명하는 시스템으로, 수학 연구의 형식화와 소프트웨어 검증에 활용된다. 추론 모델의 사후 학습(post-training)은 보통 지도 미세조정과 검증 가능한 보상 기반 강화학습(특히 GRPO)을 결합하는데, GRPO는 희소한 보상, 제한된 탐색, 모드 붕괴(mode collapse)라는 약점을 갖는다.
연구팀이 제안한 피드백 증류는 자기 증류(self-distillation)의 한 형태다. 모델이 언어 모델로부터 받은 ‘특권적 피드백(privileged feedback)’을 조건으로 삼은 자신의 출력 분포를, 토큰 단위로 스스로 따라 학습하도록 한다. 이 방식은 토큰 수준의 세밀한 지도와 외부 지식 주입을 동시에 가능하게 한다. Lean4 정리 증명에 적용한 실험에서 피드백 증류는 GRPO보다 생성 경로의 다양성을 더 잘 유지했고, 더 높은 정책 엔트로피와 더 나은 pass@k 확장성을 보였다. 두 기법은 상호 보완적이어서, 피드백 증류로 학습한 체크포인트에서 GRPO를 시작하면 어느 한쪽만 쓸 때보다 성능이 더 좋았다.
이 연구는 복잡한 추론을 위한 사후 학습을 개선하는 유망한 경로를 제시한다는 점에서 의미가 있다. AI와 수학의 접점은 빠르게 확장되고 있는데, 2026년 5월 오픈AI(OpenAI)가 80년간 풀리지 않던 에르되시 단위 거리 추측(Erdős unit distance conjecture)을 AI 모델로 반증했다고 발표한 사례가 대표적이다. 다만 이번 결과는 Lean4 증명이라는 특정 과제에서의 보고치이며, 다른 추론 영역으로의 일반화 효과는 후속 연구를 통해 확인될 필요가 있다.
국내 수학 교육 AI 기업이나 소프트웨어 형식 검증 연구팀은 이 논문의 방법론을 자체 시스템에 적용해 볼 수 있다. 대입 수학 문제 풀이, 알고리즘 정확성 검증, 스마트 계약 안전성 분석 등에서 Lean과 같은 형식 증명 시스템의 활용이 기대되는 만큼, 소형 모델에서도 높은 성능을 달성하는 피드백 증류 기법은 실용적 가치가 크다. 특히 자체 수학 AI 파이프라인을 구축하는 연구팀이라면 LLM 피드백을 훈련 데이터로 활용하는 이 접근을 참고할 만하다.
