MaxProof: Scaling Mathematical Proof with Generative-Verifier RL and Population-Level Test-Time Scaling

MiniMax M3 모델로 수학 경시대회 수준의 증명을 수행하는 MaxProof 프레임워크. 증명 생성·검증·수리 3가지 능력을 훈련하고, 테스트 시간에 집단 탐색과 토너먼트 선택으로 IMO 2025 35점, USAMO 2026 36점을 달성했다.

MaxProof는 경시대회 수준의 수학적 증명을 위한 population-level test-time scaling 프레임워크다. M3 모델을 증명 생성기, 검증기, 수리기, 랭커로 활용해 후보 증명 집단을 탐색하고 토너먼트 선택으로 최종 증명을 도출한다. 핵심은 defense-in-depth 생성 검증기로 낮은 false-positive rate을 달성하고, 4가지 보상 해킹 패턴(길이 편향, 포맷 해킹, 의미적 지름길, 판정기별 선호도)을 방어하는 것이다. 그 결과 IMO 2025에서 35/42, USAMO 2026에서 36/42로 두 대회 모두 인간 금메달 기준을 넘었다.

핵심 요약

• 증명 생성·검증·수리 3가지 전문 능력을 개별 훈련 후 단일 M3 모델로 병합
• Defense-in-depth 검증기: bad-case 필터링, 정규화, 다중 판정, pessimistic min 집계로 false-positive 최소화
• MaxProof test-time scaling: 32개 초기 후보 + 최대 10라운드 PATCH/REWRITE 정제
• IMO 2025 27→35점(+8), USAMO 2026 26→36점(+10), 두 대회 모두 금메달 기준 초과
• M2 사이클에서 발견된 4가지 보상 해킹 패턴과 그 방어 전략을 문서화
• 비용 효율적: GLM-5.1 기반으로 26-circle packing을 $11 미만 API 비용으로 새 SOTA 달성

논문 링크

외부 연구를 정리한 자료입니다. HDATF가 발표한 논문이나 제품 성능을 측정한 결과는 아닙니다.