AI가 Lean 증명을 만든다고 할 때, 평가는 “코드가 빌드됐는가?”에서 끝나면 안 됩니다. 더 중요한 질문은 따로 있습니다. 원래 문제와 같은 명제를 증명했는가? 증명 과정에서 몰래 공리를 추가하지 않았는가? 최종 결과를 Lean 커널이 실제로 승인했는가?
FormalQualBench의 Comparator는 바로 이 경계선을 확인하는 장치입니다. FormalQualBench는 박사 자격시험 수준의 수학 정리 23개로 구성된 Lean 4 + Mathlib 벤치마크입니다.1 각 문제는 필요한 정의와 by sorry가 들어간 핵심 정리 문장으로 제공됩니다.2 AI 시스템의 역할은 이 sorry를 실제 증명으로 대체하는 것입니다.
Comparator는 “통과한 코드”가 아니라 “정당한 증명”을 본다
Lean에서 lake build가 성공하면 코드는 일단 컴파일됩니다. 하지만 컴파일 성공이 곧 올바른 증명을 뜻하지는 않습니다. 자동증명 시스템이 원래 문제를 살짝 바꾸거나, 메타프로그래밍 같은 우회 기법을 쓰거나, 추가 공리를 도입한다면 겉보기에는 성공처럼 보일 수 있습니다.
Comparator는 이 위험을 줄이기 위해 해법을 샌드박스에서 확인합니다. 핵심 검사는 세 가지입니다. 해법이 원래 challenge와 같은 정리를 증명하는지, 허용되지 않은 공리를 도입하지 않았는지, 그리고 Lean 커널이 그 증명을 받아들이는지입니다.3
따라서 Comparator의 역할은 단순한 채점기가 아닙니다. “돌아가는 Lean 코드”와 “원래 문제를 안전하게 증명한 Lean 코드”를 구분하는 검증 계층에 가깝습니다.
자동증명이 강해질수록 판정 기준도 중요해진다
최근 Lean 자동증명 시스템의 성능은 빠르게 올라가고 있습니다. MerLean-Prover는 Lean 4 정리 증명기로, sorry 선언을 Lean 커널이 검사할 수 있는 증명으로 대체합니다. 이 시스템은 Planning, Check, Lean 세 종류의 에이전트로 구성됩니다.4
MerLean-Prover의 특징은 단순히 증명 후보를 많이 생성하는 데 있지 않습니다. 재귀적 외부 루프가 개별 증명이 아니라 증명 계획을 수정 단위로 사용한다는 점이 중요합니다.4 즉, 실패한 증명 한 조각만 고치는 방식이 아니라, 어떤 방향으로 증명할지에 대한 계획 자체를 반복적으로 조정합니다.
결과도 주목할 만합니다. MerLean-Prover는 파인튜닝, 맞춤형 강화학습 목적함수, 정리별 스캐폴딩 없이 FormalQualBench에서 23문제 중 10문제를 해결했습니다. 공개 오픈소스 기준선으로 언급된 OpenGauss는 8문제를 해결했습니다.4 Putnam2025에서는 12문제 중 12문제를 모두 닫았고, 전체를 해결한 다음 최상위 시스템보다 더 낮은 총 wall-clock 시간을 기록했습니다.4
이런 흐름은 성능 평가에서 Comparator 같은 검증 장치가 왜 필요한지 보여줍니다. 자동증명 시스템이 더 많은 문제를 풀수록, “정답처럼 보이는 출력”과 “커널이 승인한 정당한 증명”을 엄격히 구분해야 합니다.
Lean 증명 결과를 볼 때 확인할 것
Lean 기반 자동증명 결과를 평가할 때는 빌드 성공 여부만 보면 부족합니다. 최소한 다음 기준을 함께 확인해야 합니다.
Comparator를 통과했는가
Lean 커널이 최종 증명을 승인했는가
해법이 추가 공리를 도입하지 않았는가
원본 정리와 제출된 해법의 정리가 같은가
사용한 Lean/Mathlib 환경이 무엇인가
FormalQualBench Comparator의 실무적 의미는 여기에 있습니다. AI 수학 증명 평가의 기준을 “그럴듯한 출력”에서 “검사 가능한 정당성”으로 옮깁니다. 자동증명 시스템이 강해질수록, 증명을 만들어내는 능력만큼이나 그 증명을 공정하고 안전하게 판정하는 능력이 중요해질 것입니다.
1MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving
4MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving
이 노트는 보도·비평·교육·연구 목적으로 작성되었습니다. 저작권 문의가 있으시면 에서 알려주세요.