Model Collapse Despite Ground-Truth Verification

Motivation

• Known: 기존에는 recursive generation에서 발생하는 model collapse를 막기 위해 ground-truth verifier(예: Lean proof checker)로 생성된 artifact를 필터링하면 품질이 보장된다고 여겨져 왔으며, 검증기가 accept한 artifact만 남기면 안전하다는 암묵적 전제가 널리 쓰인다.
• Gap: 검증기(verifier)는 개별 산출물(artifact)이 declared manifest 하에서 체크되는지에 대한 local한 판정만 내릴 뿐, source 분포 Q가 target 분포 P의 모든 mode를 커버하는지(population support)는 전혀 보장하지 않는다는 점이 간과되어 왔다. 즉 pass rate라는 numerator는 정확해도 denominator(어떤 population을 대표하는가)가 불명확하면 target-risk 주장으로 이어질 수 없다.
• Why: proof-supervised LLM, unit-test 기반 코드 생성, wet-lab 프로토콜 등 exact verifier를 사용하는 다양한 벤치마크에서, 높은 pass rate가 실제로는 target population에 대한 일반화 보장이 아니라 좁은 covered subpopulation에 대한 진술일 수 있음을 드러내어, 검증 기반 안전성 주장의 오용을 막는 측정 규약(reporting protocol)을 제공하기 때문에 중요하다.
• Approach: target space X와 verifier-artifact space Z를 분리하는 typed setup을 구성하고, adapter τ: Z→X를 통한 anchored source law S=τ#Q와 target law P 사이의 support, discrepancy, formalization gap을 정량화하는 risk ledger 및 hypothesis-testing 프로토콜을 제안한다.

Achievement

네 가지 기여를 통해 verifier 통과율이 target-risk 주장으로 이어지기 위한 명시적 조건과 계산 가능한 감사(audit) 절차를 제시한다.

How

• target space X(law P, head hX)와 verifier-artifact space Z(law Q, head hZ)를 분리하는 typed framework를 구성하고, Lean verifier V_Lean을 통한 source loss L^h_Z와 target loss L^h_X를 정의.
• 측정 가능한 adapter τ:Z→X로 anchored source law S=τ#Q를 정의하고, full target partition C={C0,...,Cm}을 사전 선언(predeclare)하여 population support(qj>0)와 operational support(유한 표본에서의 신뢰구간 및 충분한 표본수)를 구분.
• unsupported-mode 정리: qj=0<pj인 target mode Cj에 대해, source-side verifier 통계량만으로는 해당 cell에서의 target 행동을 식별할 수 없음을 증명 (두 시스템이 동일한 verifier 통계량을 가지면서도 target risk가 해당 mode의 mass만큼 차이 날 수 있음).
• loss-class discrepancy dH(Pj,Sj) (integral probability metric, 식 (1))와 one-sided formalization gap ε_form,j(h) (식 (2))를 정의하여, Lean soundness가 formalization gap에 대한 상한을 전혀 보장하지 않음을 명시.
• 고정 모델에 대한 target-risk audit bound를 residual mass, unsupported target mass, verified source loss, loss-class discrepancy, formalization error, holdout uncertainty의 합으로 구성하고, independent holdout 위에서 concentration 논증으로 증명.
• 이를 hypothesis test로 전환: H0: RP(h)>ε, H1: RP(h)≤ε, test level η, upper-bound statistic T_audit을 declare한 뒤 T_audit≤ε 형태의 명시적 rejection rule을 요구하는 computable reporting protocol(cellwise ledger table 포함)을 제안.

Originality

• model collapse를 recursive generation 관점이 아니라 "verifier가 정확해도 support-loss가 발생할 수 있다"는 hypothesis-testing/domain-adaptation 관점에서 formalize한 점이 독창적이다.
• verifier acceptance(local, artifact-level 판정)와 target-risk claim(population-level 진술)을 명확히 분리하는 typed setup 및 raw mass pj, qj를 명시적으로 노출시키는 ledger 개념을 도입.
• 단순 two-sample discrepancy(MMD 등)를 labeled-loss certificate로 오용하지 않도록 loss-class에 의해 통제되는 integral probability metric으로 discrepancy를 재정의.
• formalization gap을 discrepancy와 별도의 항으로 분리하여, "Lean이 sound하다고 해서 formalization gap이 통제되는 것은 아니다"라는 미묘하지만 실질적인 논점을 명시.

Limitation & Further Study

• 이 논문은 이론적 measurement rule과 reporting protocol을 제시할 뿐, 실제 Lean 데이터셋이나 현존 벤치마크에 대한 경험적(empirical) 검증이나 실험 결과가 없다(저자 스스로도 "not an empirical claim that current Lean datasets fail"이라고 명시).
• partition C의 선택(coarsening/refinement)에 따라 결과의 민감도가 달라질 수 있음을 인정하지만, 이에 대한 구체적 방법론이나 자동화된 partition 선택 절차는 제시되지 않음.
• adapter τ 및 discrepancy dH, formalization gap ε_form을 실제로 추정하기 위해서는 target sampling, cell annotation, semantic adjudication 등 상당한 추가 비용이 필요하나, 이를 실무에서 어떻게 확보할지에 대한 구체적 가이드가 부족.
• 후속 연구로는 제안된 ledger를 실제 Lean 기반 정리 증명 벤치마크(예: MiniF2F, Lean 관련 데이터셋)에 적용해 실증적으로 검증하는 작업이 필요할 것으로 보인다.

Evaluation

총평: 검증기(verifier)의 exactness와 target population에 대한 generalization을 개념적으로 명확히 분리하고, 이를 formal hypothesis-testing 언어로 정식화한 시의적절하고 정교한 이론적 기여이나, 실증적 검증이 부재한 워크숍 논문 수준의 포지션 페이퍼(position paper)적 성격이 강하다.