Proof Verification Is Obligation Coverage: Pessimistic Checking of Open-Ended Mathematical Proofs

Motivation

• Known: 기존 pessimistic verification은 다수의 독립적 리뷰 중 하나라도 fatal error를 발견하면 기각한다는 규칙을 사용하며, 이는 증명 검증의 existential(기각) 측면과 잘 부합한다. 또한 process reward model, generative verifier, coarse-to-fine chunk 검증, 반복 critique 샘플링 등 verifier test-time scaling 기법들이 더 많은 오류를 잡아낼 수 있음이 알려져 있다.
• Gap: 기존 textual-view 검증 기법들은 반복 리뷰나 텍스트 청크 세분화를 통해 오류 발견 확률을 높일 뿐, 증명이 수락되기 위해 반드시 커버되어야 하는 semantic obligation 집합이라는 universal(수락) 측면의 대상 자체를 암묵적으로 남겨둔다. 즉 검증기는 어떤 commitment들이 참이어야 증명 경로가 유효한지를 명시적 state로 기록하지 않아, 수락된 증명이 단지 fatal dependency가 샘플링되지 않은 경우일 수 있다.
• Why: 자연어 증명은 객관적 정답성을 가지지만 단일 최종 답으로 환원되지 않고, 완전한 형식화(formalization)는 여전히 비용이 크고 불완전하기 때문에, LLM 기반 수학 추론 시스템의 신뢰성 있는 보상/검증 신호를 얻기 위해서는 이 중간 지대(informal proof grading)를 다루는 원칙적인 검증 대상 정의가 필요하다.
• Approach: 증명이 유발하는 고위험 semantic obligation(전제, case split, witness bridge, imported dependency, 결론 지지 링크 등)을 추출하고, first-error-wins pessimism 하에서 검사하며, negative certificate가 실제로 candidate proof의 route에 대해 proof-faithful한지 검증하고, 선택적으로 미커버된 fatal obligation의 잔존 여부를 감사하는 OC-PVerify를 제시한다.

Achievement

Figure 5. Cross-model and cross-mode view of obligation cov-

1. 새로운 검증 대상 정의: 프롬프트 스택이 아니라 proof acceptance를 obligation coverage로 재정의하고, pessimistic verification을 non-coverage의 minimal witness에 대한 risk-controlled search로 재해석했다.
2. 구현된 verifier 시스템: obligation extraction, risk scheduling, proof-faithful certificate validation, provenance auditing, coverage convergence, dependency tracing, 별도의 full-credit audit 채널을 포함하는 OC-PVerify를 실제로 구현했다.
3. 정량적 성능 개선: IMO-GradingBench first-50 split에서 provenance-gated OC-PVerify가 정확도 84.0%→92.0%, F1 0.826→0.920으로 개선했으며, full-credit audit은 rubric context 하에서 96.0% 정확도와 zero false accept를 달성했다.
4. 정직한 실패 분석: 전체 300-sample 균형 실행에서는 OC-PVerify가 recall은 개선하지만 specificity를 잃는 현상을 보고하여, dependency tracing과 convergence auditing이 obligation coverage에 필수적임을 보였다.

How

Figure 2. OC-PVerify method overview. The verifier extracts semantic obligations from the candidate proof, prioritizes h

• 후보 증명으로부터 고위험 semantic obligation(정리 전제조건, case 경계, witness 생성 bridge, imported result, domain restriction, parent-child dependency)을 추출
• adversarial falsification, witness construction, route completeness, independent central lemma, provenance dependency에 대한 targeted audit으로 obligation을 선택적으로 증강
• 스케줄된 obligation들을 first-error-wins 결정 규칙으로 검사
• negative decision은 candidate proof가 실제로 사용하는 dependency를 공격하는 proof-faithful certificate가 검증된 경우에만 수락
• convergence mode에서는 미검사된 fatal obligation의 잔존 여부를 감사
• 동일 평가 코드 경로 내에서 standard verification, 반복 whole-proof pessimism, vertical chunk verification, progressive coarse-to-fine verification, pessimistic pruning, prover refinement 등 통제된 baseline들을 보존하여 비교
• IMO-GradingBench의 300-sample 및 first-50 validation split에서 정확도와 F1로 평가

Originality

• 검증 단위를 "샘플링된 텍스트 스팬/청크"에서 "semantic obligation"으로 전환하는 새로운 프레이밍 제시
• pessimistic verification을 non-coverage에 대한 minimal witness를 찾는 risk-controlled search로 재해석하는 이론적 통합
• 기각(existential, 하나의 fatal error)과 수락(universal, 모든 obligation의 커버리지)의 비대칭성을 명시적 state variable로 formalize
• theorem validity 검증과 rubric 기반 full-credit benchmark auditing을 분리하는 채널 설계

Limitation & Further Study

• 전체 300-sample 균형 실행에서는 OC-PVerify가 recall 개선 대비 specificity(false positive rejection)를 잃는 한계가 명확히 드러나며, 이는 dependency tracing/convergence auditing이 아직 완전히 해결되지 않았음을 시사
• first-50 split과 300-sample 전체 결과 간 성능 격차가 존재하여 일반화 가능성에 대한 추가 검증 필요
• 여전히 mature progressive baseline이 300-sample 전체 정확도에서는 최강자로 남아있어, OC-PVerify의 전면적 우위가 아직 입증되지 않음
• 후속 연구로 obligation extraction의 자동화 견고성, provenance-gating의 정밀도 개선, 더 큰 규모/다양한 도메인 벤치마크로의 확장이 필요

Evaluation

총평: 증명 검증을 obligation coverage라는 새로운 대상으로 재정의한 개념적 기여가 뚜렷하며 first-50 split에서의 개선은 고무적이나, 300-sample 전체 결과에서의 specificity 저하는 실용적 완성도 측면에서 추가 검증이 필요함을 보여준다.