AdvancedMathBench: 고급 수학 증명 생성 및 검증을 위한 벤치마크

고급 수학은 중간 주장과 논리적 연쇄가 맞물려야 하는 작업이라 최종 정답 검사만으로는 모델의 진짜 추론 능력을 측정할 수 없다. AdvancedMathBench는 자연어 증명의 전체 흐름을 검증하고 오류를 국소화할 수 있는 자동화된 검증 파이프라인을 도입함으로써 모델의 과정적 추론 능력을 수치화할 수 있게 했다. 이 벤치마크는 모델이 단지 타당해 보이는 결론을 만들 뿐 아니라 근거와 오류 탐지 능력을 동시에 갖추었는지를 판별하는 기준을 제공한다.

고급 수학 증명은 연속된 중간 명제와 증명의 구조적 정합성이 중요하며, 따라서 단순한 최종 답안 일치 검사는 증명의 타당성을 보장하지 못한다. 기존 벤치마크는 주로 최종 결과 검증에 의존해 모델이 논리적 결함을 포함한 '타당해 보이는' 궤적을 생성해도 통과시키는 한계가 있었다. AdvancedMathBench는 증명의 전체 과정을 대상으로 하는 과정 검증(process verification) 관점을 적용해 이 한계를 보완한다. 검증의 핵심은 모델이 제시한 각 단계의 타당성과 오류 국소화를 일관되게 식별하는 능력이다. 이를 위해 본 논문은 전문가 레이블을 활용해 자동 검증기를 학습시키고, 검증 결과의 질을 메타-검증으로 정량화해 보상 신호로 사용했다. 메타-검증은 단순한 정오 판단이 아니라 검증 논리와 오류 위치의 일치성을 평가하므로, 검증기가 올바른 이유를 갖추도록 유도하는 역할을 한다. 과정 기반 검증은 단순 판단에서 발생하는 과대평가 문제를 완화한다. 논문에서 보인 결과는 동일한 모델이라도 Rough 평가에서는 높은 TPR을 기록할 수 있지만, 메타-검증 기준에서는 낮은 TNR로 인해 실제 균형 성능이 떨어진다는 점을 보여준다. 이로써 신뢰성 있는 수학적 검증을 위해서는 단계별 타당성 판별, 오류 복원 가능성 평가, 그리고 보수적 수용 규칙(pessimistic verification)을 결합해야 한다.

벤치마크 구축은 문제 소싱, 구조화된 파싱, 난이도 전처리, 전문가 검수의 다단계 파이프라인으로 진행되었다. 문제 소스는 대학 학부시험, 박사 자격시험, 공모전 문제, 교과서 연습 문제를 포함해 분야별·난이도별 균형을 맞추었고, 진술형 증명이 요구되지 않는 객관식·기계적 풀이 문제는 제거되었다. 난이도 사전선별은 여러 모델의 생성 궤적에 대한 verifier uncertainty(반복 검증 결과의 엔트로피)를 사용해 너무 쉬운 사례를 필터링하고 정보량이 높은 사례를 선별하는 방식으로 이루어졌다. 검증 파이프라인은 대규모 전문가 주석을 학습 데이터로 활용해 자동 검증기를 학습시키고, 메타-검증기를 RL 보상자로 연결하는 구조로 설계되었다. 구체적으로 약 2k의 주석 예제를 확보하고, 전문가 교정으로 생성한 양성 수리 샘플을 약 1.2k개 추가해 불균형을 완화했다. 학습 단계에서는 Intern-S2-Preview-35B를 시작점으로 GRPO를 사용해 Meta-Ver-RL을 적용했으며, 보상값은 EXACT_MATCH=1.0, BASIC_MATCH=0.5, POOR_MATCH=0.25, WRONG_POLARITY=0으로 정의되었다. 최종 판정 단계에서는 비관적 검증을 적용해 각 증명에 대해 8회의 독립 검증을 병렬로 수행하고 모든 패스가 합격해야만 증명을 수용하도록 했다. 이 규칙은 과다수용을 줄이는 방향으로 TNR을 개선했으며, 보수적 기준 하에서의 최종 수용률과 오류 탐지 성능을 평가 지표로 삼았다. 파이프라인 설계 전반은 ProverBench의 생성 평가와 VerifierBench의 메타-검증 평가를 연결하는 목표로 통합되었다.

ProverBench에서 GPT-5.5-xhigh는 UG 분할에서 64.5%를, QE 분할에서 48.9%를 기록해 난이도 상승에 따른 성능 감소가 명확히 드러났다. 여러 프론티어 모델이 QE 분할에서 큰 성능 하락을 겪었으며, 이는 박사 자격 수준의 증명 구성 능력이 여전히 모델들에게 어려운 과제임을 시사한다. 기존의 HMMT나 USAMO 같은 답안 중심 벤치마크에 비해 ProverBench는 생성된 증명의 과정적 타당성을 더 엄격히 평가해 모델 성능을 낮게 측정했다. VerifierBench에서는 Rough 평가와 Meta-Verification 평가 간의 격차가 두드러졌다. 모델들이 Rough(단순 polarity)에서는 높은 TPR을 보일 수 있으나 Meta-Verification에서는 평균 TNR이 12.3포인트 감소했고 평균 Balanced F1은 9.0포인트 하락했다. 최고 오픈소스 검증기인 DeepSeek-V4-Pro는 Meta-Verification Balanced F1 65.1%로 가장 우수한 균형을 보였지만 여전히 전문가 수준에는 미치지 못했다. 자동 검증기 자체의 평가에서 파이프라인은 보편 LLM-as-judge보다 우수함을 보였다. 보수적 검증과 메타-검증 기반 RL, 추가 주석, 양성 샘플 보강의 조합으로 최종적으로 held-out 94샘플에서 Rough Balanced F1 82.1%와 Meta-Verification Balanced F1 73.9%를 달성했다. Ablation 결과는 메타-검증 보상이 오류 탐지(TNR)를 향상시키고, 양성 보강이 TPR을 회복시키며 비관적 검증이 거짓 수용을 추가로 줄였음을 보여준다.

전체 아키텍처는 문제 수집·파싱·선별 모듈과 ProverBench/VerifierBench 데이터셋, 그리고 자동 검증 파이프라인으로 구성된다. 문제 수집 단계에서는 PDF 파싱을 통해 문제 진술을 통일 포맷으로 변환하고, 객관식·정답 일치형 문제는 배제해 자연어 증명 생성이 요구되는 문제만 남겼다. 난이도 선별은 다수의 최첨단 LLM을 이용한 생성과 Intern-S2-Preview-35B 기반 반복 검증으로 얻은 검증 불확실성(entropy)을 기준으로 수행되었다. 자동 검증기의 학습 데이터는 원 벤치마크 레이블에 추가 생성·수정 과정으로 확대되어 약 2k의 주석 예제를 확보했고, 전문가의 수리 수정 가이드를 바탕으로 약 1.2k의 양성 보강 샘플을 추가했다. 검증기 학습은 Intern-S2-Preview-35B를 출발점으로 GRPO를 통해 수행되었고, 메타-검증기는 검증 출력의 정합도에 따라 보상을 부여하도록 설계되었다. 보상 매핑은 문헌과 동일하게 EXACT_MATCH=1.0, BASIC_MATCH=0.5, POOR_MATCH=0.25, WRONG_POLARITY=0을 사용해 정량적 신호를 제공했다. 파이프라인의 핵심 알고리즘적 장치는 메타-검증 보상, 긍정 샘플 보강, 그리고 비관적 검증 규칙의 결합이다. 메타-검증 보상은 검증 논리의 질을 강화해 단순 polarity 보상으로는 얻기 어려운 오류 탐지 능력을 향상시켰다. 긍정 보강은 전문 수정 가이드를 이용해 오류 증명을 수리하고 강한 모델로 재검증해 양성 샘플을 얻는 방식으로 데이터 편향을 완화했으며, 비관적 검증은 8회의 병렬 검증 중 하나라도 실패하면 수용하지 않는 보수적 수용 규칙을 적용해 거짓 수용을 추가로 억제했다. 평가 설정은 ProverBench의 생성 평가에 대해 비관적 검증 기준을 적용한 수치와 VerifierBench의 meta-verification 프로토콜을 따르는 정밀도 지표로 나뉜다. VerifierBench의 평가에서는 단순 TPR/TNR뿐 아니라 검증 논리와 오류 국소화의 일치 정도를 메타-검증으로 측정해 더 엄격한 균형 성능을 산출했다. Ablation 실험은 각 구성요소가 TPR, TNR, Balanced F1에 미치는 영향을 수치적으로 분리해 보였다.

논문이 명시한 주요 한계 중 하나는 모델들이 '타당해 보이는' 증명을 과다 수용하는 편향으로 인해 검증 성능이 제한된다는 점이다. 데이터 선별과 전문가 주석 과정에서 불확실성 중심 샘플링은 유용한 네거티브 사례를 확보했지만 이로 인해 학습 데이터가 부정 예제로 편향될 수 있으며, 추가 주석은 TNR을 높였으나 TPR을 낮추는 영향을 보였다. 자동 검증기의 성능은 메타-검증기와 전문가 레이블 품질에 크게 의존하므로, 주석의 범위와 일관성이 부족하면 일반화 성능이 저하될 위험이 남아 있다.