LeanPRM이 수학 증명 검증용 단계 라벨을 만든다

LeanPRM은 자연어 수학 증명의 단계마다 정답 라벨을 붙입니다. Lean 증명 보조기(proof assistant)를 이용하는 연구 프레임워크입니다. 연구진은 이 라벨로 학습한 검증기(verifier)가 여러 평가에서 기존 데이터로 학습한 모델을 앞섰다고 보고했습니다. 저는 점수 상승만큼 단계별 판단을 대량으로 만들었다는 점이 눈에 남습니다. 답의 정오를 넘어 풀이의 어느 대목에서 논리가 흔들리는지 살필 자료가 생기기 때문입니다.

Lean을 이용한 검증은 속도를 높이는 데서 학습 자료를 만드는 데까지 넓어지고 있습니다. nano-lean은 Mathlib 검증 시간을 11.85초로 줄였고, LeanPRM은 검증 과정에서 얻은 판단을 단계별 학습 라벨로 바꿉니다. 하나는 검사 속도를, 다른 하나는 검사 결과의 활용 범위를 넓힙니다. [id: ]

사람이 단계 라벨을 하나씩 붙이지 않았습니다. 이번 연구는 Lean 검사를 활용해 사람 주석 없이 10,634개 증명과 15만 2,000개 라벨을 만들었습니다. 연구진은 Lean으로 확인할 수학 명제가 공급되면 데이터셋도 확장할 수 있다고 설명합니다. 증명 검토 도구가 학습 자료 생산에도 쓰인다는 변화가 반갑습니다.

Lean의 피드백 없이 자연어 증명과 형식 증명(formal proof)을 함께 만듭니다. Lean 검사 뒤 두 번째 모델이 문법 때문에 생긴 실패를 걸러 수학 오류에 해당하는 부정 라벨을 남깁니다. 부정 라벨은 문법 오류가 아니라 수학적 오류에 해당하도록 만듭니다. Qwen3-4B의 단계 라벨 정확도는 200개 증명 평가에서 74.7%였고, PRM800K로 학습한 같은 기반 모델은 60.3%였습니다. 이 점수는 해당 평가의 단계 라벨 정확도이며, 15만 2,000개 전체의 정답률은 아닙니다.

논문에서 74.7%가 나온 200개 증명의 평가 기준과 PRM800K 비교 결과를 함께 확인하십시오. 검증기를 쓰고 있다면 답을 아는 풀이의 중간 단계를 일부러 틀리게 바꿔 보십시오. 오류를 표시하는 위치가 달라지는지 살피면 단계 라벨이 실제 검토에 도움이 되는지 시험할 수 있습니다.

수학 풀이를 검토하실 때는 최종 답부터 확인하십니까, 아니면 중간 단계의 오류를 먼저 살피십니까?