기술 요약: Mask-Proof

문제 정의

대규모 언어 모델(LLM)은 수학적 문제 해결 및 연구 수준의 증명 능력이 점점 향상되고 있으나, 다양한 출처에 걸친 긴 증명 과정에서 **단계별 추론(step-level reasoning)**을 측정할 수 있는 확장 가능하고 재현 가능한 도구가 결정적으로 부족하다. 기존의 평가 방법들은 다음과 같은 세 가지 주요 한계점을 가진다:

1. 정답 중심 편향(Answer-Centric Bias): GSM8K 및 MATH와 같은 벤치마크는 최종 정답에 집중하며, 중간 추론 과정의 엄밀성을 평가하는 데 실패한다.
2. 비용이 많이 드는 전문가 채점: 증명의 품질을 평가하는 것은 종종 인간 전문가를 필요로 하며, 이는 규모를 키우기 어렵고 도메인 전반에 걸쳐 재현하기 어렵다.
3. 문맥 및 의존성 격차(Context and Dependency Gaps): 실제 연구 증명은 외부 보조 정리(lemma), 매크로 및 명시되지 않은 배경 사실에 의존한다. 이러한 의존성을 복구하지 않고 단계를 마스킹(masking)하면, 결정 불가능한 과제가 되어 추론 능력의 결여를 정보의 부재와 혼동하게 만든다.
4. 검증의 어려움: 표기법의 다양성과 등가적인 재구성(equivalent reformulations)으로 인해 자동 검증이 저해되며, 문자열 매칭은 불충분하고 기호 기반 도구는 일반적인 보장을 제공하기에 역부족이다.

방법론: Mask-Proof 파이프라인

저자들은 이질적인 연구 증명을 검증 가능하고 자기 완결적인 단계별 평가 문제로 변환하도록 설계된 LLM 기반 자동 데이터 큐레이션 파이프라인인 Mask-Proof를 소개한다. 이 파이프라인은 세 가지 핵심 단계로 작동한다:

1. 논문 수집 및 증명 추출

• 출처: 사전 학습 오염(pretraining contamination)을 최소화하기 위해 파이프라인은 최근 arXiv 제출물(2025년 8월~10월)을 큐레이션한다.
• 필터링: 단순한 정의적 증명이나 패턴 완성형 증명을 제외하여 비사소한(non-trivial) 추론이 요구되도록 LaTeX 소스를 추출하고 필터링한다.
• 인간 감사: 모든 최종 인스턴스는 수학적 정확성, 문맥 충분성, 지름길 단서(shortcut cues)의 부재를 검증하기 위해 도메인 전문가의 수동 감사를 거친다.

2. 자동 데이터 큐레이션

파이프라인은 Codex CLI를 사용하여 두 가지 핵심 작업을 수행한다:

• 자기 완결적 복구(Self-Contained Recovery): 시스템은 내부 교차 참조(예: \ref, \eqref)를 탐색하고 사용자 정의 매크로를 확장함으로써 의존성을 해결한다. 암묵적 의존성(다른 곳에서 정의된 기호)의 경우, 소스 LaTeX에서 정의 문장을 검색하여 이를 "추가 정보(Additional Information)"로 첨부한다. 이를 통해 마스킹된 단계가 제공된 문맥만을 사용하여 해결될 수 있도록 보장한다.
• 에이전트 기반 마스킹(Agentic Masking): 무작위 마스킹 대신, 파이프라인은 **핵심 추론 결정 공식 단계(key inference-critical formula steps)**를 선택하는 에이전트를 사용한다. 선택된 단계는 [MASK] 토큰으로 대체된다. 선택 기준은 마스킹된 단계가 국소적인 표면 단서나 얕은 패턴 매칭으로 해결될 수 없도록 하여, 모델이 전역적 정의와 지역적 변수를 합성하도록 강제한다.
• 충실성(Faithfulness): 파이프라인은 단계 선택과 마스크 적용을 분리하여 의도하지 않은 증명 재작성을 방지하고, 남은 텍스트가 원본과 동일하게 유지되도록 한다.

3. 자동 평가 (Mask-ProofJudge)

• 태스크: 모델은 마스킹된 공식 단계를 재구성하는 과제를 수행한다.
• 판사(Judge): LLM 기반 평가 모델(GPT-OSS-120B High)이 모델의 출력값과 정답 사이의 의미적 등가성을 평가한다.
• 분산 감소: 생성의 확률적 변동성을 처리하기 위해, 시스템은 문제당 4개의 솔루션을 샘플링하고 다수결 투표를 통해 판단을 집계한다.
• 지표: 주요 지표는 4번의 독립적인 시도에 대한 평균 정확도를 나타내는 Avg@4이다.

주요 기여

1. Mask-Proof 파이프라인: 단계별 평가에서의 "무엇을 측정할 것인가"와 "어떻게 점수를 매길 것인가"라는 과제를 해결하며, 실제 연구 증명을 검증 가능한 마스킹 단계 과제로 변환하는 재현 가능하고 자동화된 프레임워크를 제공한다.
2. Mask-ProofJudge: 변산성이 감소된 투표를 통해 인간 주석가와 96.8%의 일치도를 달성하며 캘리브레이션된 자동 평가 프레임워크이다.
3. Mask-ProofBench: 다양한 연구 분야(예: 대수 기하학, 위상 수학, 편미분 방정식)를 아우르는 292개의 큐레이션된 문제로 구성된 벤치마크이다. 모든 인스턴스는 수동으로 감사되었으며 자기 완결적으로 설계되었다.

실험 결과

저자들은 17개의 최첨단 LLM(표준 모델 및 추론 강화 모델 모두 포함)을 Mask-ProofBench와 IMO-ProofBench에서 파생된 교차 데이터셋 서브셋으로 평가하였다.

• 추론 능력 경계: 약 32%의 정확도에서 명확한 성능 경계가 나타났다. 모든 추론 강화 모델(예: GPT-5.2, DeepSeek-R1)은 이 임계값을 초과한 반면, 표준 모델은 그 미만이었다. 추론 강화 모델은 표준 모델보다 12%에서 27% 더 높은 성능을 보였다.
• 자기 완결성에 대한 절제 연구(Ablation): 의존성 복구 모듈을 제거했을 때 성능 저하가 11%에서 23% 발생하였으며, 이는 문맥의 완전성이 유효한 평가에 필수적임을 확인시켜 준다.
• 마스킹 전략에 대한 절제 연구: 무작위 마스킹은 성능을 크게 부풀려(예: 표준 모델이 ~8%에서 ~50%로 급증), 추론 모델과 표준 모델 간의 성능 격차를 사실상 제거했다. 에이전트 기반 마스킹은 지름길 활용을 방지하고 변별력을 유지하는 데 필수적임이 입증되었다.
• 전문가와의 상관관계: IMO-ProofBench에 적용했을 때, Mask-Proof 파이프라인은 인간 개입형 채점이나 별도의 루브릭 없이도 전문가의 인간 채점과 0.79의 Spearman 순위 상관계수를 달성했다.
• 재현성: 파이프라인의 독립적인 실행은 의존성 복구(재현율 97.2%)와 마스크 선택(의미적으로 근접한 마스크를 셀 때 89.3%의 일관성)에서 높은 일관성을 보였다.

의의 및 주장

본 논문은 Mask-Proof가 단계별 수학적 추론을 평가하기 위한 충실하고, 재현 가능하며, 비교 가능한 방법을 제공함으로써 AI for Science의 "측정 격차"를 해결한다고 주장한다.

• 확장성: 전문가 채점의 저비용 대안을 제공하여, 실제 현장의 연구 수준 증명을 평가할 수 있게 한다.
• 타당성: 자기 완결적 문맥과 에이전트 기반 마스킹을 강제함으로써, 단순한 지름길 활용이나 문맥 복사가 아닌 진정한 추론을 측정한다.
• 일반화: 파이프라인은 도메인 특화 루브릭 설계 없이도 전문가의 합의와 일치하는 모델 순위를 생성하며 외부 데이터셋(IMO-ProofBench)으로 성공적으로 일반화된다.

저자들은 비록 LaTeX 이외의 소스 및 잠재적인 잔류 누출(residual leakage)에 관한 한계가 존재하지만, Mask-Proof가 단계별 추론을 재현 가능한 과학적 현상으로서 연구하기 위한 기초를 마련하며, 최종 정답 정확도를 넘어 증명 과정 자체의 엄밀성을 평가하는 단계로 나아간다고 결론짓는다.