AI Coding Benchmarks Need Proofs, Not Just Tests

Motivation

• Known: SWE-Bench Verified, LiveCodeBench, Terminal-Bench, Aider Polyglot 등 test-based coding benchmark들이 frontier LLM 평가의 주류이며, HumanEval처럼 기존 벤치마크가 saturation되면 HumanEval+, MBPP+, SWE-Bench+, UTBoost 등 더 강한 test suite로 보강하는 cascade 패턴이 반복되어 왔다.
• Gap: 유한한 test suite는 입력 공간 전체를 커버할 수 없어 정답 코드와 그럴듯하지만 틀린 코드를 구분하지 못하며, 아무리 정교한 curation을 거쳐도 test passing이 일반적인 semantic correctness 보장으로 전환될 수 없다는 구조적 한계가 존재한다. Verina, VeriBench 같은 formal verification 전용 benchmark는 존재하지만, 이 proof oracle이 SWE-Bench 같은 real-world, multi-file, test-blessed production code에도 확장되는지는 검증되지 않은 open question이었다.
• Why: 벤치마크 목표가 모델 학습을 형성한다는 점에서, test-only leaderboard가 지속되면 모델이 proof-generation 능력 없이 code generation만 강화하는 방향으로 훈련될 위험이 있으며, frontier model들이 이미 test-based benchmark에서 saturation에 도달해 순위 변별력을 상실하고 있어 proof-based evaluation으로 전환할 시급성이 높다.
• Approach: 저자들은 (1) test 기반 오라클의 구조적·통계적·수학적 한계를 논증하는 이론적 축, (2) 두 개의 Lean 4 benchmark(Verina, VeriBench)에서 frontier model들의 test-pass와 proof-pass 격차를 측정하는 실증적 축, (3) SWE-Bench에서 손수 formalize한 case-study grid라는 세 축으로 position을 뒷받침한다.

Achievement

Figure 1. Test-pass (blue) and proof-pass (red) across two frontier

1. 구조적 불충분성 논증: test 기반 오라클이 finite input-output check에 불과하다는 점, Goodhart's law에 의한 overfitting 위험, 그리고 iid sampling 하에서 P(all k tests pass | bug rate ε) = (1-ε)^k 같은 통계적 논증으로 rare bug를 놓칠 확률이 구조적으로 크다는 것을 보였다.
2. 실증적 test-pass/proof-pass gap 측정: 여러 frontier reasoning model(o1, o3-mini, o4-mini, o3, Opus/Sonnet 시리즈 등) 스냅샷에 걸쳐 Verina(n=189), VeriBench(n=153) 벤치마크에서 test-pass는 100%에 근접하지만 proof-pass는 한 자릿수%에 머무는 큰 격차(75-95%)를 실증적으로 확인했다.
3. prover-limited zone 개념화: test는 통과하지만 정해진 budget 내에서 correctness proof도 counterexample도 얻지 못하는 영역을 정의하여, 기존 test 기반 평가가 놓치는 부분을 정량화했다.
4. SWE-Bench case study: merged-and-fixed 버그들에 대해 formal specification이 실제로 buggy code와 upstream fix를 구분해내지만 해당 repository의 test suite는 이를 구분하지 못함을 hand-formalized grid로 보였다.

How

Figure 1. Test-pass (blue) and proof-pass (red) across two frontier

• Plank 1(§3): 벤치마크 cascade 사례(HumanEval→HumanEval+, MBPP→MBPP+, SWE-Bench→SWE-Bench+/UTBoost 등) 분석과 Goodhart's law, iid sampling 하의 수학적 bound (1-ε)^k를 통해 test 기반 평가가 근본적으로 불충분함을 논증
• Plank 2(§4): Verina와 VeriBench라는 두 Lean 4 benchmark에서 두 frontier model lineage(Claude, OpenAI o-series)의 여러 스냅샷에 대해 동일 prompt로 implementation task(test로 채점)와 proof task(reference implementation에 대한 specification 증명)를 각각 수행시켜 test-pass와 proof-pass율을 비교 측정 (Lean compiler error를 피드백하며 최대 3회 typecheck retry, 10회 proof retry)
• Plank 3(§5): SWE-Bench에서 merged-and-fixed 버그를 손수 formal specification으로 만들어, test suite로는 구분 안 되지만 proof oracle로는 buggy code와 fix를 구분할 수 있는 case를 grid 형태로 구축

Originality

• Test 기반 코딩 벤치마크의 한계를 empirical(cascade)-statistical(Goodhart, sampling)-mathematical(구조적 불충분성)의 세 층위로 체계화하여 논증한 점이 새로움
• 기존 formal verification 벤치마크(Verina, VeriBench 등)가 다루던 순수 학술적 세팅을 넘어, SWE-Bench라는 real-world production 코드에 proof oracle을 처음으로 확장 적용한 시도
• test-pass와 proof-pass를 같은 task, 같은 모델 스냅샷에 대해 나란히 측정하여 "prover-limited zone"이라는 개념으로 gap을 정량화한 실증적 기여

Limitation & Further Study

• Verina, VeriBench는 여전히 single-function, 상대적으로 curated된 task 위주이며 SWE-Bench case study는 hand-formalized된 소규모 grid에 불과해 대규모 real-world 코드베이스로의 일반화는 제한적
• proof-based evaluation 자체가 formal specification 작성 비용이 크고 Lean 4 같은 특정 프로버 생태계에 의존하므로, 벤치마크 확장성과 다양한 언어/도메인 적용 가능성에 대한 논의가 부족
• proof 생성 능력을 학습 목표로 삼았을 때 발생할 수 있는 새로운 형태의 Goodharting(specification-passing이지만 실제 유용성과 괴리된 proof)에 대한 논의가 미흡
• 후속 연구로는 자동 specification 생성/검증 파이프라인의 scaling, 다양한 production 코드베이스에 대한 대규모 proof-based benchmark 구축이 필요

Evaluation

총평: Test 기반 코딩 벤치마크의 saturation 문제를 구조적·통계적·실증적으로 설득력 있게 짚어내고 proof-based evaluation이라는 대안을 구체적 실험과 사례로 뒷받침한 시의적절하고 중요한 position paper이나, 실제 대규모 도입을 위한 scalability 문제는 향후 과제로 남아있다.