LeanPRM, 형식 증명으로 자연어 수학 추론을 단계별 감독

AI 수학 증명 검증의 병목

대규모 언어 모델은 길고 복잡한 수학 증명을 생성할 수 있지만, 자연스러운 문장이 모든 추론 단계를 보장하지는 않는다. 개방형 증명에서는 최종 답만 확인해 중간 오류를 찾기 어렵고, 사람이 모든 단계를 직접 읽고 정답 여부를 표시하는 방식은 비용이 높다. 따라서 최종 결과가 아니라 추론 과정 자체에 학습 신호를 제공하는 과정 감독이 중요한 과제가 되고 있다.

LeanPRM은 Lean 증명 보조기를 활용해 이러한 단계별 감독 데이터를 자동으로 생성한다. 자연어 설명을 기계적으로 검사할 수 있는 형식 증명과 연결하는 것이 핵심이다.

LeanPRM의 작동 방식

• 증명 쌍 생성: 모델이 자연어 증명과 대응하는 Lean 증명을 함께 만든다. 생성 과정에서 Lean의 피드백을 받지는 않는다.
• 단계별 검사: Lean이 형식 증명의 각 단계를 검사해 정답과 오답에 해당하는 신호를 제공한다.
• 형식화 오류 필터링: 형식 증명이 실패했다고 해서 수학적으로 틀렸다는 뜻은 아니다. 문법이나 자연어와 형식 표현의 불일치가 원인일 수 있으므로, 별도 모델이 이런 사례를 걸러낸다.
• 사람 없는 라벨 생성: 결과 데이터는 10,634개 증명과 약 15만 2천 개의 라벨된 단계로 구성되며, 사람의 주석을 사용하지 않는다.

실험 결과

200개 증명으로 구성된 LeanPRM-Bench에서 LeanPRM으로 학습한 Qwen3-4B 검증기는 단계 라벨의 완전 일치 정확도 74.7%를 기록했다. 같은 기반 모델을 PRM800K로 학습한 검증기는 60.3%였고, 보고된 베이스라인은 48.2%였다. LeanPRM은 IMO 수준 문제에서 best-of-N 방식으로 더 나은 증명을 선택하는 데도 도움을 줬다. 외부 검증 벤치마크 4개 중 3개에서는 PRM800K 기반 검증기보다 높은 성능을 보였다. 연구진은 0.6B부터 8B까지 다양한 모델 크기에서 LeanPRM 학습의 이점도 보고했다.

의미와 남은 과제

이 연구의 핵심은 Lean을 단순한 최종 합격·불합격 판정기가 아니라, 과정 감독 데이터를 생산하는 도구로 활용한 데 있다. 형식 시스템은 실행 가능한 검사를 담당하고, 언어 모델은 자연어 추론과 형식 표현 사이를 연결한다. 이 구조는 긴 추론을 사람이 일일이 검토해야 하는 부담을 줄이고, 검증기 학습에 더 세밀한 신호를 제공할 가능성이 있다.

다만 몇 가지 한계도 있다. 자연어 증명과 Lean 증명이 얼마나 잘 대응하는지에 결과가 좌우되며, 수학적 오류와 형식 표현의 실패를 구분하는 필터도 필요하다. Lean이 증명을 수용했다는 것은 주어진 형식 환경에서 해당 명제가 성립한다는 뜻이지, 자연어 설명이 완전하거나 원래 의도를 충실히 전달한다는 사실까지 자동으로 보장하는 것은 아니다.

따라서 LeanPRM은 수학 추론을 전면적으로 판정하는 만능 해법이라기보다, AI 증명 검증기를 확장 가능하게 훈련하기 위한 데이터 생성 파이프라인으로 보는 편이 적절하다.

출처: Hugging Face Daily Papers