LeanPRM이 Lean 검사기로 자연어 증명의 단계별 라벨을 자동 생성한다

무엇인가

AI가 쓰는 수학 증명이 길고 어려워지면서, 그 증명이 한 단계씩 맞는지 확인하는 일이 병목이 됐다. 기존 검증기는 최종 답이 짧게 검사 가능한 문제를 전제로 만들어졌다. 그러나 증명에는 검사할 최종 답이 없고, 정당성은 각 단계가 앞 단계에서 따라 나오는지에 달려 있다. 단계별 정오 라벨을 학습하려면 사람 주석이 필요한데, PRM800K가 약 80만 개의 단계 라벨을 요구했을 만큼 비싸고, 증명은 판정하기 더 어렵다. 샘플링한 이어쓰기가 정답에 도달하는지로 라벨을 만드는 방식도 최종 답이 없으면 적용되지 않는다. Lean 같은 증명 보조기로 형식화하는 길은 전문가 노동이 든다.

어떻게 동작하나

LeanPRM은 이 라벨을 Lean으로부터 얻는다. 1단계에서 모델은 정리를 한 번에 증명하되, 번호가 붙은 자연어 문장마다 그 문장을 수행하는 Lean 전술(tactic)을 짝지어 함께 쓴다. 이때 모델은 자기가 만든 Lean 단계의 실행 결과를 전혀 보지 못한다. 피드백을 주면 모델이 실수를 고치거나 포기해버려 라벨링하려는 진짜 오류가 사라지기 때문이다. 출발점은 공개 형식 코퍼스의 서로 다른 정리 진술 약 17,800개로, 대부분 NuminaMath-LEAN과 Lean-Workbook에서 왔고 NuminaMath 쪽은 Gemini Flash-Lite가 매긴 'hard' 등급에서 골랐다. 생성에는 주로 Claude Sonnet 5, 일부 초기 부분집합에는 Claude Opus 4.8을 썼다.

무엇과 다른가

2단계에서 고정된 형식 증명을 Lean 4와 Mathlib(v4.25.0-rc2)로 컴파일한다. 컴파일 오류는 문장과 전술이 1대1로 짝지어져 있으므로 정확히 한 단계를 가리킨다. 수학은 맞아도 형식 문법 때문에 실패할 수 있으므로, 두 번째 모델 호출이 진술·단계·컴파일러 출력을 읽고 판정한다. 판정은 정답, 수학적 오류, 구문 오류 셋이고 구문 오류는 수학을 바꾸지 않는 선에서 한 번만 패치해 다시 컴파일한다. 첫 실패 이전 단계는 정답, 첫 실패 단계와 그 이후 모든 단계는 오답으로 라벨링한다. 이렇게 13,940개 진술에서 라벨이 붙었고, 중복·빈 증명 제거와 품질 관리를 거쳐 최종적으로 자연어 증명 10,634개(정답 6,370, 오답 4,264), 라벨된 단계 152,005개가 사람 주석 없이 만들어졌다. 오류는 10개 클래스로 분류되는데, 6개는 수학적 결함(근거 없는 가정, 잘못된 부등식 한계, 틀린 예시나 구성, 빠진 경우·부수 조건, 잘못된 대수적 항등식, 모듈러·가약성 추론 오류)이고 4개는 형식화 실패다. 저자들은 Claude Opus 5를 심사자로 쓴 두 번의 블라인드 감사로 자동 라벨을 검증했는데, 형식화 계열 클래스(오답 시도의 35.8%)의 단계가 77~93%에서 건전하다고 판정된 반면 수학 계열은 절반 미만이 건전 판정을 받았다. 그래서 첫 실패가 형식화 계열인 시도는 전부 제거해, 모든 음성 라벨이 수학적 오류 클래스를 갖도록 했다.

어떻게 쓰나

실험은 Qwen3 0.6B·4B·8B를 thinking 모드로 GRPO 학습해 진행했다. 증명마다 temperature 1에서 8개 응답을 샘플링해 그룹 내 보상을 정규화하고, 중요도 비율은 [0.8, 1.26]으로 클리핑, KL 페널티 계수 10⁻³, 업데이트당 64개 증명, 학습률 10⁻⁶, 총 500 업데이트다. 보상은 r = 0.7·R_step + 0.3·1[예측 판정 = 실제 판정]이고, 오류가 있는 증명에서 R_step은 정답 단계 재현율 R_c와 오답 단계 재현율 R_i의 곱이다. 곱을 쓰는 이유는 전부 정답 또는 전부 오답으로 찍는 지름길을 막기 위해서다. 예컨대 5·6단계가 틀린 증명에서 6단계만 지적하면 R_c=1, R_i=1/2이므로 R_step=0.5, r=0.65가 된다. 같은 레시피·예산에서 LeanPRM-Verifier-4B는 PRM800K-Verifier-4B를 5개 벤치마크 중 4개에서 앞섰다. LeanPRM-Bench에서 74.7 대 60.3으로 14.4점, Hard2Verify 9.7점, PRMBench 4.1점, IMO-GradingBench 9.4점 차이다. 학습 전 Qwen3-4B의 LeanPRM-Bench 정확도는 48.2였다. PRM800K 쪽은 학습 데이터와 분포가 같은 짧은 풀이를 쓰는 ProcessBench에서만 8.1점 앞선다. 최종 답 보상으로 19,200개 NuminaMath 문제를 푼 NuminaMath-Solver-4B는 자체 검증 문제 정답률을 30.0%에서 47.5%로 올렸지만, LeanPRM-Bench에서는 학습 전 모델과 1점 이내에 머물고 모든 외부 벤치마크에서 오히려 떨어졌다. 즉 수학 문제 풀이 강화학습만으로는 검증 능력이 생기지 않는다.

전제와 한계

테스트 시점 활용도 확인했다. IMO-GradingBench의 30개 문제마다 사람이 채점한 약 33개의 증명이 있는데, 문제당 N개를 뽑아 검증기가 수용한 것 중 하나를 고르게 했다. N=16에서 LeanPRM-Verifier-4B는 35.9% 확률로 정답 증명을 골라 무작위 선택의 32.4%를 웃돌았고, 이득은 N=8까지 커졌다. 같은 레시피의 PRM800K-Verifier-4B는 33.2%에 그쳤는데, 실제로는 30%만 정답인데도 전체 증명의 약 79%를 수용해 선택이 사실상 무작위와 다르지 않았다. 모델 크기별로는 LeanPRM-Bench에서 학습 후 향상 폭이 0.6B 31점, 4B 27점, 8B 29점이었다. 학습 전 8B는 4B보다 2.5점 낮은 45.7에서 출발해 결국 4B와 비슷해졌고(74.7 대 75.0), 0.6B는 크게 뒤처진다. 8B는 Hard2Verify 증명의 9%에서 파싱 불가 응답을 내 4B의 2%보다 형식 실패가 많았고, 파싱된 답만 보면 74.7 대 75.1로 비슷했다.

개발자 관점에서 이 논문의 핵심은 정확한 검사기가 존재하는 영역을 라벨 생성기로만 쓰고, 실제 모델은 자연어만 읽게 만든 구조다. Lean은 학습 데이터를 만들 때 오프라인으로 한 번만 쓰이고, 학습된 검증기는 형식 증명을 입력으로 받지 않는다. 그래서 형식화(autoformalization) 파이프라인을 따로 구축하지 않고도 단계별 피드백을 얻는다. 같은 패턴은 최종 정답이 없지만 부분적으로 기계 검증이 가능한 과제, 예컨대 코드의 테스트 스위트나 과학 시뮬레이터로 옮길 수 있다고 저자들은 본다. 실무에서 재사용하려면 라벨 규약을 먼저 확인해야 한다. LeanPRM은 첫 실패 이후 모든 단계를 오답으로 표시하는데, ProcessBench는 해법의 타당성에 영향을 줄 때만 근거 누락을 오류로 세므로 이 규약 차이가 벤치마크 점수를 갈라놓는다. PRMBench도 기본 PRMScore 대신 first-error accuracy로 평가한 이유가 같다.

저자들이 밝힌 한계는 분명하다. 수학적 오류와 형식화 실패를 가르는 판단 자체가 모델 분류에 의존하고, 그 검증은 표본에 대한 단일 심사 모델로만 이뤄졌으므로 경계선 단계는 여전히 잘못된 라벨을 가질 수 있다. Lean 라벨을 PRM800K의 사람 라벨과 비교했지만, 같은 증명에 LLM 심사자가 라벨한 데이터로 학습시킨 대조군이 없어서 성능 향상이 라벨 때문인지 증명 스타일 데이터로 학습한 덕인지 분리하지 못한다. LeanPRM-Bench는 학습 데이터와 같은 파이프라인, 같은 Claude 생성기를 쓰므로 일반화의 근거는 대부분 4개의 외부 벤치마크에 실려 있다. 또한 음성 예시가 Claude 자신의 실수에서 나오므로, 실제 검증기가 탐지해야 할 오류 범위보다 좁을 수 있다.