OpenBMB가 수학 자동 형식화 파이프라인 MathForm을 통째로 오픈소스로 공개했다. 8B 모델 가중치, 검증을 거친 약 36만 7000건 규모의 Lean 4 데이터셋, 평가 코드와 Pass@k 스크립트를 함께 내놓았다. 모델은 Hugging Face에 올라와 있으며 라이선스는 Apache 2.0, 베이스 모델은 Qwen3-8B, 가중치 정밀도는 BF16이다. 프로젝트는 칭화대 자연어처리연구실과 ModelBest(面壁智能)가 공동 지원하는 OpenBMB 팀이 진행했고, 동명의 논문은 이달 중순 arXiv에 제출됐다. 저자는 총 10명이다.
자동 형식화란 자연어로 쓰인 수학 명제를 Lean 4 같은 기계가 검증할 수 있는 형식 언어로 옮기는 작업을 말한다. 어려운 부분은 글자 그대로의 번역이 아니다. Mathlib의 타입 계층과 정의 체계는 방대해서, 명제에 나오는 '연속함수'나 '유한군' 같은 표현을 라이브러리 안의 정확히 대응하는 정의로 매핑해야 하고, 동시에 형식화 이후 명제가 원래 명제와 같은 의미를 유지해야 한다. 둘 중 하나라도 어긋나면 컴파일러는 그대로 통과시켜 버릴 수 있다.
데이터는 어떻게 만들었나
MathForm 파이프라인은 4단계로 이루어진다. 먼저 플래너가 명제 속 수학 개념에 대해 Mathlib을 검색하는데, 검색 도구 LeanExplore가 매번 상위 22개 결과를 반환한다. 모델은 이 검색 결과를 조건으로 Lean 4 명제를 생성한다. 후보는 형식 검사와 컴파일 테스트를 차례로 거치고, 이어 대형 모델 심판이 의미적 일치성을 판정한다. 통과한 경로는 거꾸로 재구성돼 깔끔한 학습 궤적으로 만들어진다.
논문에 실린 한 수치가 반복 작업의 필요성을 보여준다. 이후 라운드들이 보존된 전체 샘플 중 추가로 31.0%를 기여했다. 즉 단 한 번만 생성하고 불합격분을 버렸다면 쓸 수 있는 데이터의 3분의 1 가까이를 잃었을 것이라는 뜻이다.
검색 단계는 이 설계에서 가장 비용 효율적인 부분이다. 모델에게 기억만으로 Mathlib 속 어떤 정의의 정확한 이름과 시그니처를 떠올리게 하는 것은, 사실상 계속 갱신되는 라이브러리를 얼마나 외우고 있는지를 시험하는 셈이다. 대신 라이브러리 조회를 검색 도구에 맡기고 모델은 조립만 담당하게 하면 필요한 파라미터 수는 자연스럽게 줄어든다. 8B가 32B와 맞붙을 수 있는 이유도 여기에 있다. 애초에 둘이 겨루는 과제 자체가 다르다.
결과물로 나온 데이터셋의 이름은 FormalVerse로, 검증된 샘플이 약 36만 7000건이다. 출처는 DeepTheorem, NuminaMath, AceReason-Math, Lean Workbook, Principia-Collection, DeepMath, OpenR1-Math에 걸쳐 있고, 여기에 정통 교과서 내용도 더해졌다. 이 데이터셋은 Hugging Face에서 이미 좋아요 358개를 받았다.
성적표와 그 안의 두 가지 기준
학습은 지도 미세조정 이후 강화학습을 거치는 방식이다. 평가는 여섯 개 벤치마크에 걸쳐 진행됐는데, FormalMATH-Lite와 DeepSeek-ProverBench는 경시수학, CombiBench는 조합수학을 다루고, FATE 시리즈는 대수 난이도에 따라 M·H·X 세 등급으로 나뉜다.
MathForm-8B의 문법 검사 평균 Pass@8은 88.06%, 일치성 검사 평균은 72.37%였다. FATE 세 등급의 일치성 통과율은 순서대로 97.33%, 63.00%, 37.00%였다. 비교 대상에는 Herald Translator-7B, Kimina-Autoformalizer-7B, Mathesis-HPO-7B와 함께 StepFun-Formalizer, Goedel-Formalizer-V2, ReForm 각각의 7B/8B 버전과 32B 버전이 포함됐다. 8B 모델은 여러 테스트셋에서 32B 전용 형식화 모델의 점수를 넘어섰다.
두 지표 사이의 격차는 절대 점수보다 더 많은 것을 말해준다. 문법 검사는 컴파일이 되는지만 묻지만, 일치성 검사는 형식화된 명제가 원래 문제와 같은 의미인지를 묻는다. 88%와 72%, 그 사이 십수 퍼센트포인트가 바로 이 파이프라인이 지금 안고 있는 진짜 병목이다. 컴파일이 된다고 해서 반드시 증명하려던 그 정리는 아니라는 뜻이다.
문턱이 워크스테이션 한 대 수준으로 낮아졌다
본 사이트는 최근 테렌스 타오가 던진 경고, 즉 AI가 만들어내는 증명이 아무도 다 읽을 수 없을 만큼 쏟아질 것이라는 이야기를 다룬 바 있다. 형식화는 그 문제에 대한 또 다른 절반의 답이다. 증명이 Lean 컴파일러를 통과하기만 하면 사람이 읽고 이해할 수 있는지는 더 이상 받아들이는 전제 조건이 아니게 된다. 다만 전제는 명제 자체가 제대로 번역돼야 한다는 것이고, FATE-X에서 나온 37%라는 수치는 아직 그 지점까지 상당한 거리가 남아 있음을 보여준다.
대략 계산해 보면 8B 모델을 BF16으로 불러오는 데는 약 16GB의 VRAM이 필요하고, 같은 정밀도의 32B 모델은 약 64GB 안팎이 필요하다. 전자는 24GB급 소비자용 그래픽카드 한 장으로도 돌릴 수 있지만, 후자는 여러 장이나 전문가용 카드가 있어야 한다. 대학 수학과, 증명 보조 도구 커뮤니티, 소규모 팀 입장에서는 형식화 파이프라인을 돌리는 데 필요한 하드웨어 문턱이 클러스터급에서 단일 머신급으로 낮아진 셈이다. 데이터셋과 평가 스크립트도 함께 공개돼 남들이 재현하고 검증하는 비용도 같이 낮아졌다.
비교표에 늘어선 이름들도 이 분야가 얼마나 붐비는지를 보여준다. Herald, Kimina, Mathesis, StepFun-Formalizer, Goedel-Formalizer-V2, ReForm까지, 모두 최근 1~2년 사이 등장한 전용 형식화 모델이고 하나같이 오픈소스다. 형식화는 일반 대화형 모델처럼 연산 자원을 쏟아붓는다고 차이가 벌어지는 분야가 아니라, 데이터 구축 노하우와 검증 루프의 완성도가 승부를 가르며, 파라미터 규모는 오히려 부차적인 변수가 된다. 논문 속 데모에서 실제 오픈소스 배포까지 이어지는 속도가 대다수의 예상보다 빠르다.
참고 출처: OpenBMB 저장소 및 모델 카드, CocoLoop, arXiv 프리프린트 2608.14221, Hugging Face 데이터셋 페이지; 파라미터 규모, 라이선스, FormalVerse 샘플 수, 벤치마크별 Pass@8 산출 방식을 검증했다.