Counterexample-Carrying FormalRx: Lean-Checkable Witnesses for Autoformalization Misalignment

Motivation

• Known: FormalRx와 같은 기존 진단 벤치마크는 자연어-Lean 쌍의 정합성 여부를 판정(verdict), 오류 카테고리화, 위치 지정, 수정문 생성(correction) 작업을 요구하며, type checking이 통과해도 의미적으로 틀릴 수 있다는 점은 이미 알려진 문제이다. BEq+ 같은 방법은 formal equivalence를 증명하려 시도해 사람 판단과 상관관계가 높은 자동 정렬 평가를 제공한다.
• Gap: 기존 correction-only 진단은 candidate와 intended formalization이 의미적으로 다르다는 것을 증명하지 못한다. Lean은 자신이 본 명제만 검사할 뿐, 원래 자연어 의미가 제대로 포착되었는지는 검사하지 않으므로, 수정안 제시만으로는 오정렬 진단이 인식론적으로 약한 상태로 남는다.
• Why: 단일 수치 스코어링은 raw Lean acceptance 상승이 실제 의미 이해 개선인지, 아니면 단순히 proof engineering(예: sorry나 escape hatch 회피) 능력 향상인지 구분하지 못하게 가리는데, 이 구분이 autoformalization 신뢰성 평가에서 중요한 맹점임을 이 논문이 드러낸다.
• Approach: 매 오정렬 진단마다 candidate와 intended formalization을 기계적으로 분리하는 작은 Lean-checkable artifact(witness)를 요구하는 task를 정의하고, 7개 witness family 분류체계와 sorry/admit/escape hatch를 거부하는 adversarial 검증 프로토콜을 제시한다.

Achievement

1. Task 정의 및 taxonomy: counterexample-carrying semantic alignment task를 정의하고, candidate_weaker, candidate_stronger, candidate_incomparable, candidate_vacuous, local_delta 등 semantic relation 라벨과 7개 witness family 분류체계를 제시했다.
2. 검증 프로토콜: sorry, admit, blocked proof escape, statement mutation을 거부하고 선택적으로 axiom inspection을 수행하는 adversarial Lean 검증 프로토콜을 설계했다.
3. 실행 가능한 204-example artifact: 25개 synthetic seed, 26개 FormalRx-derived, 153개 확장 커버리지 예제로 구성된 실행 가능한 stress artifact를 구축했다.
4. 모델 평가 결과: GPT-4.1-mini, GPT-4.1, Claude Haiku에 대해 204-example 실행을 완료하고, Lean-feedback repair가 raw Lean acceptance를 23-61% 향상시키지만 semantic direction까지 맞는 joint metric은 GPT-4.1-mini strict funnel에서 13/204에 불과함을 보였다.
5. mode 비교 분석: GPT-4.1-mini에서 full mode(33/204 raw, 48/204 repair 후)가 gold-target mode(21/204)보다 Lean을 더 자주 통과함을 보여, raw Lean 성공이 witness construction과 self-target selection을 혼동할 수 있음을 시사했다.

How

• 각 example은 자연어 statement N, candidate Lean statement C, intended Lean statement I로 구성되며, gold-correction mode와 end-to-end mode 두 가지로 평가
• 모델 출력은 FormalRx-style schema를 확장하여 aligned, error_type, error_location, corrected_statement, semantic_relation, witness_type, witness_lean, witness_explanation 필드를 포함
• semantic_relation은 candidate_weaker, candidate_stronger, candidate_incomparable, candidate_vacuous, local_delta로 분류
• Lean 검증 시 sorry, admit, escape hatch, statement mutation을 거부하는 adversarial 프로토콜 적용
• Lean-feedback을 이용한 one-pass repair ablation을 수행하여 raw acceptance와 repair 후 acceptance를 비교
• joint semantic-proof metric으로 raw Lean acceptance 뿐 아니라 정확한 semantic direction까지 요구하는 엄격한 평가 도입

Originality

• 기존 벤치마크(FormalRx)가 correction만 요구하는 것과 달리, 의미적 차이를 기계적으로 증명하는 executable Lean witness를 diagnosis에 필수적으로 결합한 최초의 task 설계
• BEq+가 equivalence 증명 실패를 inconclusive negative로 남기는 것과 달리, 실패의 원인(constant, quantifier swap, domain change, boundary case 등)을 localized witness family로 세분화하여 설명 가능하게 만듦
• Nitpick, Nunchaku 등 기존 model finder가 고립된 수학적 명제의 반증에 초점을 맞춘 것과 달리, candidate와 intended formalization 간의 semantic delta 자체를 목표로 하는 점에서 차별화

Limitation & Further Study

• FormalRx-CC는 formal-separation 단계만 감사(audit)할 뿐, 자연어-Lean 간의 faithfulness를 직접 인증하지는 못함
• 204-example artifact는 leaderboard가 아니라 benchmark-construction validation과 smoke run 성격의 스트레스 테스트에 불과하여 규모가 작고 대표성이 제한적
• frozen hidden test split, 독립적인 inter-annotator reliability, BEq+와의 matched head-to-head 비교, DeepSeek-Prover/Goedel-Prover/Kimina-Prover 같은 specialized prover baseline과의 비교는 향후 과제로 남겨짐
• 평가 모델이 GPT-4.1-mini, GPT-4.1, Claude Haiku 세 종류로 제한되어 있어 다른 최신 모델이나 특화된 prover에 대한 일반화 가능성이 검증되지 않음

Evaluation

총평: Autoformalization 진단 벤치마크에 형식적으로 검증 가능한 counterexample witness라는 개념을 도입해 raw Lean acceptance와 실제 의미 이해를 구분하는 중요한 통찰을 제공하지만, 아직 초기 단계의 소규모 stress artifact이며 hidden test split, inter-annotator reliability, specialized prover 비교 등 후속 검증이 필요한 워크숍 페이퍼 수준의 기여이다.