QEDBench: Quantifying the Alignment Gap in Automated Evaluation of University-Level Mathematical Proofs

Motivation

• Known: 기존에는 LLM이 고등학교 수준 경시대회 문제나 초등 수학 벤치마크(GSM8K, MATH 등)에서 이미 포화 상태에 도달했음이 알려져 있었고, FrontierMath나 IMProofBench 같은 벤치마크가 난이도를 연구자/전문가 수준까지 끌어올렸으나 closed-form answer 검증이나 소규모 데이터셋에 의존하는 한계가 있었다. 또한 Lean 같은 auto-formalization 프레임워크는 정확성을 보장하지만 주석 비용이 커서 확장성이 떨어진다는 트레이드오프가 알려져 있었다.
• Gap: 'LLM-as-a-Judge' 프로토콜은 확장성이 있지만 전문가 판단과의 상관관계가 낮다는 문제가 있었고, 특히 학부 상급~대학원 초년 수준의 증명 기반 수학에서 자동 평가자의 신뢰성을 체계적으로 감사(audit)한 대규모 벤치마크가 부재했다. 기존 연구들은 평가 품질을 모델 성능과 암묵적으로 결부시켰을 뿐, 두 축을 명시적으로 분리하여 judge 자체의 정렬 격차를 측정하지 않았다.
• Why: LLM이 수학 및 과학 연구를 보조하는 자동 채점자·검증자로 활용될 가능성이 커지는 상황에서, judge 모델이 결함 있는 증명에 '엄밀성을 환각(hallucinating rigor)'하며 점수를 부풀린다면 AI 시스템의 자기평가 및 강화학습 기반 훈련 신뢰성 전체가 흔들릴 수 있으므로, 이를 정량적으로 드러내는 것은 매우 중요하다.
• Approach: 이 논문은 course-specific rubric과 expert-domain rubric이라는 이중 루브릭 체계를 설계하고, 5개 solver 모델이 생성한 증명을 7개 judge 모델이 채점한 결과를 PhD급 인간 전문가의 채점 결과와 대조하는 대규모 실증적 벤치마킹 접근을 취한다.

Achievement

Figure 1. Pass Rates by Discipline. The pass rates (score ≥0.9)

1. 정렬 격차의 정량화: Claude Opus 4.5, DeepSeek-V3, Qwen 2.5 Max, Llama 4 Maverick 등 프론티어 judge 모델들이 인간 전문가 대비 최대 +0.18~+0.36의 평균 점수 인플레이션(체계적 긍정 편향)을 보임을 입증했다.
2. 이산-연속 성능 격차 발견: Gemini 3.0 Pro는 전반적으로 0.91의 state-of-the-art 인간 평가 점수를 달성했으나, GPT-5 Pro와 Claude Sonnet 4.5 같은 reasoning 모델은 Discrete Math(0.72, 0.63)와 Graph Theory(0.74, 0.50)에서 급격히 성능이 저하됨을 밝혔다.
3. 대규모 검증된 벤치마크 공개: 1,000시간 이상의 PhD급 전문가 수기 평가에 기반한 최초의 통계적으로 견고한 대학 수준 수학 증명 자동 평가 표준(QEDBench)을 데이터셋, 이중 루브릭 시스템, 평가 로그와 함께 공개하여 향후 AI judge 벤치마킹을 지원한다.

How

• Analysis, Complex Analysis, Abstract Algebra, Discrete Math, Probability Theory, ODEs, Number Theory, Combinatorics, Algorithms, Graph Theory 등 10개 학부 상급/대학원 초년 과목에 대해 문제셋을 구성.
• 1단계(Solution Generation): o3-deep-research, GPT-5 Pro, Claude Sonnet 4.5, Gemini 3.0 Pro, DeepSeek-Prover-V2 등 5개 frontier 모델로 증명 생성(최대 16,384 토큰, 2,000초 타임아웃, 3회 재시도, 실패 시 0점 처리).
• 2단계(Expert Annotation & Rubric Engineering): PhD급 전문가가 [0, 0.25, 0.5, 0.75, 0.9, 1.0] 세분화 척도로 채점하며, GPT-5.2 Pro로 생성(및 Gemini 3.0 Pro로 검증)한 Course-Specific Rubric과 Expert-Domain Rubric 두 종류를 인간 전문가가 반복적으로 개선하여 검증된 정답 기준 확립.
• 3단계(Judge Calibration): GPT-5.2 Pro, Claude Opus 4.5, Gemini 3.0 Pro 등 7개 judge 모델을 배치하여 두 루브릭 모두에 대해 증명을 채점하고, 7×5 평가 매트릭스를 인간 ground truth와 비교하여 judge의 체계적 편향(bias)과 모델별 노이즈를 분리.

Originality

• 평가 품질(judge 신뢰성)과 생성 능력(solver 성능)이라는 두 축을 명시적으로 분리하여 감사한 최초의 대규모 프레임워크라는 점에서 독창적이다.
• Course-Specific Rubric과 Expert-Domain Rubric을 대조하는 이중 루브릭(dual-rubric) 설계를 통해 채점 기준의 엄밀성 수준에 따른 judge 편향 차이를 분리해낸 방법론적 참신성이 있다.
• 단순 최종 정답 정확도가 아닌 대학 수준의 개방형(open-ended) 증명 생성 및 채점에 초점을 맞추어, closed-form 정답에 의존하는 FrontierMath나 소규모의 IMProofBench와 차별화된다.

Limitation & Further Study

• 벤치마크에 사용된 모델들이 실험 시점 기준 최신 프론티어 모델(GPT-5.2 Pro, Claude Sonnet 4.5 등)로 한정되어 있어, 이후 출시된 GPT-5.2 Pro나 Claude Sonnet 4.6 등 신규 모델에는 결과가 적용되지 않을 수 있다.
• 루브릭 자체가 GPT-5.2 Pro로 생성되고 Gemini 3.0 Pro로 검증된 후 인간이 다듬는 방식이라, 초기 루브릭 생성 단계에서 LLM 편향이 완전히 배제되었는지 불확실하다.
• 발췌된 부분만으로는 통계적 유의성 검정, 평가자 간 일치도(inter-rater agreement) 등 세부 방법론적 엄밀성 검증이 충분히 드러나지 않아 추가 확인이 필요하다.
• 후속 연구로는 밝혀진 편향을 교정하는 judge 훈련 기법이나, discrete-continuous 성능 격차의 원인을 규명하는 심층 분석이 필요해 보인다.

Evaluation

총평: LLM judge의 신뢰성이라는 시의적절하고 중요한 문제를 대규모 인간 전문가 평가와 이중 루브릭 설계로 체계적으로 정량화한 견고한 벤치마크 연구로, AI 평가 신뢰성 연구에 실질적으로 기여할 것으로 평가된다.