기술적 요약: 자연어 수학 추론을 위한 위험 제어형 Lean-as-Judge

1. 문제 정의

본 논문은 대규모 언어 모델 (LLM) 이 생성한 자연어 수학 추론을 심판하기 위해 형식 증명 도구 (특히 Lean) 를 사용하는 과제를 다룹니다. 성공적인 Lean 증명은 형식적 명제에 대한 강력한 긍정적 증거를 제공하지만, 증명이 부재하는 것은 모호한 신호입니다. 증명 실패는 수학적으로 잘못된 답을 나타낼 수도 있지만, 잘못 형식화된 경우, 누락된 라이브러리 사실, 또는 증명 탐색 시간 초과로 인해 발생할 수도 있습니다.

현재 접근 방식들은 종종 증명 실패를 부정적 정확도 신호로 간주하여, 수학적 부정확성과 형식적 커버리지 부족을 혼동할 위험이 있습니다. 저자들은 "커버리지 절벽 (coverage cliff)"을 식별했습니다. 즉, 형식적 선택의 신뢰도는 성공적으로 형식화되고 증명된 후보 답안의 비율에 급격히 의존합니다. 커버리지가 높을 때 형식적 선택은 매우 정확하지만, 커버리지가 낮을 때 신호는 신뢰할 수 없게 됩니다.

핵심 문제는 하위 시스템이 언제 형식적 Lean 신호를 신뢰해야 하고, 언제 그 신호를 부정확한 것이 아니라 커버리지 밖 (즉, 미해결) 으로 간주해야 하는지 결정하는 것이며, 동시에 수용된 답안에 대해 유한 표본 위험 보장을 제공하는 것입니다.

2. 방법론: COVCAL

저자들은 커버리지 진단에 기반하여 형식적 답안을 수용할지 아니면 유보할지 결정하는 위험 제어형 선택적 래퍼인 COVCAL(Coverage-Calibrated Lean) 을 제안합니다.

2.1 부분 관측 프레임워크

시스템은 형식 파이프라인을 부분 관측 메커니즘으로 취급합니다. 이는 모든 후보 답안의 진위를 관측하는 것이 아니라 다음 사항만 관측합니다:

1. 잘 형성된 Lean 문장에 도달한 정규화된 답안 클래스는 무엇인가 (Typed Coverage).
2. 그 중 어떤 클래스가 성공적으로 증명되었는가 (Proved Coverage).
3. 가장 높은 가중치를 가진 증명된 클래스의 가중치 대 가장 높은 가중치를 가진 미해결 경쟁자 간의 차이 (Formal Margin).

답안 클래스는 동일한 최종 답을 나타내는 후보 문자열들의 그룹으로 정의됩니다 (예: $1/2$, $0.5$, $2/4$). 형식화되지 않거나 증명되지 않은 클래스는 자동으로 틀린 것이 아니라 미해결로 간주됩니다.

2.2 커버리지 진단

COVCAL 은 주어진 문제 $x$에 대해 네 가지 주요 지표를 계산합니다:

• Typed Coverage ($C_{typ}$): 잘 형성된 Lean 문장에 도달한 (proved, typechecked, 또는 timeout 상태) 후보 클래스들의 총 가중치.
• Proved Coverage ($C_{prf}$): 커널 검사된 증명을 받은 후보 클래스들의 총 가중치.
• Unresolved Rival Mass ($R_{unres}$): 증명되지 않은 가장 높은 가중치를 가진 답안 클래스의 가중치.
• Formal Margin ($M$): 가장 높은 가중치를 가진 증명된 클래스의 가중치와 미해결 경쟁자 질량 간의 차이.

2.3 선택 및 인증

COVCAL 은 임계값 $(\tau_{typ}, \tau_{prf}, \tau_M)$에 기반한 사전 선언된 규칙이 충족될 때만 가장 높은 가중치를 가진 증명된 클래스를 수용합니다. 규칙이 충족되지 않으면 시스템은 유보하거나 (또는 자기 일관성과 같은 비형식적 방법으로 대체합니다).

신뢰성을 보장하기 위해 COVCAL 은 유한 표본 선택적 위험 인증을 사용합니다. 이는 확률 $1-\delta$로 수용된 답안의 선택적 위험 (오류율) 이 최대 $\epsilon$임을 보장합니다. 두 가지 인증 체제가 제안됩니다:

1. Bonferroni Regime: 보정 분할에서 임계값 그리드를 검색하고 다중 비교를 고려하기 위해 유니온-바운드 보정 ($\delta/|T|$) 을 적용합니다. 이는 보수적이며 실현 가능하려면 높은 신호 밀도가 필요합니다.
2. Dev-then-Cal Regime: 독립적인 개발 분할에서 임계값을 선택하고 단일 Clopper-Pearson 바운드 ($\delta$) 를 사용하여 보정 분할에서 한 번 인증합니다. 이는 더 많은 표본 효율성을 가지지만 개발 데이터와 보정 데이터 간의 엄격한 분리가 필요합니다.

2.4 이론적 한계

본 논문은 커버리지 진단 없이 (즉, 증명의 존재에만 의존하여) 미해결이고 동등하지 않은 경쟁 클래스가 존재하는 경우, 비자명한 점별 정확도 인증서를 유도할 수 없음을 증명합니다. 누락된 형식적 증거는 수학적 거짓의 증거가 아니라 미해결 상태의 증거입니다.

3. 주요 기여

1. 커버리지 절벽 특성화: MATH-500 데이터셋에서 저자들은 높은 증명 커버리지에서 "증명 승리" 답안이 96% 정확하지만 낮은 커버리지에서는 20% 만 정확함을 보여줍니다. 이는 커버리지와 마진이 높을 때만 Lean 증명이 신뢰할 수 있음을 확립합니다.
2. 신호 희소성과 충실도: 형식 신호는 희소하고 불완전합니다. 7B 자동 형식화기는 문제의 28% 에 대해서만 클래스를 증명합니다. furthermore, 수동 감사는 이러한 증명 중 약 43% 만이 원래 문제에 충실함을 (나머지는 자명한 항등식이나 참이지만 관련 없는 명제) 드러냈습니다.
3. COVCAL 방법론: 부분 관측 하에서 위험을 인증하는 선택적 예측 프레임워크입니다. 이는 증명 실패의 비대칭성을 명시적으로 처리하고 수용된 예측에 대한 유한 표본 보장을 제공합니다.
4. 형식화기 의존성 실현 가능성: 본 논문은 인증서 실현 가능성이 자동 형식화 커버리지에 의해 지배됨을 보여줍니다. 7B 형식화기는 보수적인 Bonferroni 체제에 너무 희소한 신호를 생성하여 (20 개의 부트스트랩 분할 모두를 거부), Goedel-Prover-V2-8B(79% 커버리지 달성) 와 같은 증문제어 특화 형식화기는 20 개 분할 중 17 개에서 방법을 실현 가능하게 만듭니다.

4. 실험 결과

실험은 Qwen2.5-Math-7B 를 생성에 사용하고 다양한 형식화기를 자동 형식화에 사용하여 MATH-500 의 필터링된 부분집합 (378 개 예시) 에서 수행되었습니다.

• 기선 성능: 유보 없이 자기 일관성만으로도 91% 정확도를 달성합니다.
• COVCAL 성능:
  • 7B 형식화기를 사용한 Bonferroni regime 하에서, 신호가 엄격한 유니온 바운드를 충족하기에 너무 희소하여 모든 입력을 거부합니다 (20 개 분할 중 0 개).
  • 7B 형식화기를 사용한 dev-then-cal regime 하에서, 20 개 분할 중 12 개가 인증됩니다. 수용 비율은 약 21% 이며, 수용된 정확도는 0.93 입니다.
  • Goedel-Prover-V2-8B(전문화된 형식화기) 를 사용하면 증명 커버리지가 79% 로 상승합니다. Bonferroni 는 20 개 분할 중 17 개에서 실현 가능해지며, 문제의 약 48% 를 수용하여 0.98 의 수용 정확도를 달성합니다.
• 충실도 감사: 45 개의 층화 예시에 대한 수동 감사 결과, 증명된 명제의 73.6% 가 비자명하고 정확했으나, 문제 진술에 충실한 것은 43% 에 불과했습니다. 많은 "증명된" 명제는 문제의 제약을 포착하지 못한 참인 부수적 사실이나 자명한 항등식이었습니다.

5. 중요성과 주장

본 논문의 주요 기여는 단순히 원시 정확도를 향상시키는 것이 아니라, 위험 제어 하에 부분 형식 신호를 언제 그리고 어떤 형식화기로 신뢰할 수 있는지에 대한 정확한 설명이라고 주장합니다.

• 원시 정확도 대비 위험 제어: 자기 일관성이 이미 91% 정확도를 가지므로, COVCAL 의 가치는 수용하는 답안 하위 집합에 대한 인증서를 제공하여 "정확"과 "부정확"이 아닌 "검증됨"과 "미해결"을 구분하는 데 있습니다.
• 부분 관측 처리: 이 작업은 형식 검증을 선택적 예측 문제로 재정의하여, 증명 부재를 미해결 후보로 취급함으로써 형식화 실패로 인한 올바른 추론의 오표식을 방지합니다.
• 전문화에 대한 의존성: 결과는 원시 모델 규모가 전문화를 대체할 수 없음을 강조합니다. 증제 특화 형식화기는 증명 커버리지 측면에서 더 큰 일반 모델보다 훨씬 뛰어난 성과를 내며, 이는 인증 가능한 위험 제어의 구속 조건입니다.

저자들은 COVCAL 이 Lean 을 심판자로 사용하는 보수적인 인터페이스 역할을 한다고 결론지었습니다. 이는 위험 인증서를 지원할 만큼 충분한 답안 질량을 자동 형식화기가 커버할 때만 실현 가능하고 유익하지만, 모든 답안이 검증됨을 보장하지는 않습니다.