VeriBench: An End-to-End Formal Verification Benchmark for AI Coding Agents in Lean 4

Motivation

• Known: HumanEval, SWE-Bench 계열의 테스트 기반 코딩 벤치마크는 유한한 테스트가 behaviorally important bug를 놓치는 구조적 한계가 있으며, VERINA, FVAPPS, CLEVER, DafnyBench 같은 formal-verification 벤치마크는 proof completion이나 scaffolded verified generation 등 파이프라인의 일부 단계만을 평가해왔다.
• Gap: 기존 formal-verification 벤치마크들은 명세가 미리 주어진 상태에서 증명 완성 여부만 평가하거나 component-level subtask를 compensatory aggregation 방식으로 결합해 왔으며, developer-written source code로부터 적절한 formal specification을 추론하고 이를 curator의 의도된 obligation과 일치시키는 end-to-end 능력은 평가되지 않았다.
• Why: 보안이 중요한 high-assurance 도메인에서 AI coding agent를 신뢰성 있게 평가하려면 테스트 통과보다 강력한 기계 검증 가능한 신호가 필요하며, 어느 한 단계라도 실패하면 전체 인증서가 무효화되는 conjunctive한 검증의 본질을 반영한 평가 체계가 필수적이기 때문이다.
• Approach: 저자들은 Python 소스만 주어진 상태에서 agent가 verifier feedback을 받으며 반복적으로 구현, 테스트, theorem, proof를 포함한 완전한 Lean 4 아티팩트를 생성하도록 요구하는 end-to-end agentic 벤치마크 VeriBench와, 5개 per-task factor의 로그 도메인 기하평균으로 conjunctive하면서도 smooth한 평가를 제공하는 SCSC 지표를 제안한다.

Achievement

Figure 3. Human score distributions (0–5): lenient set (n = 297, left) and expert/harsh set (n = 193, right).

1. VeriBench 벤치마크 구축: HumanEval-style program, classical algorithm, Python standard-library function, 보안 예제로 구성된 614-task canonical core와 cryptography, aerospace, medical device, compiler 등 14개 도메인에 걸친 282-task VeriBench-IndustrySet을 포함한 총 896개 과제의 end-to-end Python-to-Lean4 autoformalization 벤치마크를 공개했다.
2. SCSC 지표 제안: typecheck 여부, sorry 없는 증명, LLM-judge 기반 semantic coverage, 두 개의 reference-side validity gate(D1, D2)를 결합한 5요소 로그 도메인 기하평균 SCSC를 설계하여 conjunctive하면서도 smooth한 부분점수 평가를 실현했다.
3. specification gap 발견: Codex, Claude Code, Leanstral-v2가 각각 SCSC 0.42, 0.36, 0.23에 그쳤고, iterative self-correction이 single-shot 대비 14.3% 향상을 가져왔음에도 theorem-to-reference coverage는 세 agent 모두 0.11 이하로 정체되어, proof search보다 specification synthesis가 더 심각한 병목일 수 있음을 시사하는 candidate 증거를 제시했다.
4. judge 신뢰성 검증: LLM judge의 coverage 판정을 5명의 독립적인 human rater와 대조하여 Pearson r=0.70 (p<10^-11)의 상관관계를 확보함으로써 judge 기반 지표의 타당성을 뒷받침했다.

How

Figure 2. VERIBENCH evaluation topology. Each solid arrow is

• 896개 과제(614-task canonical core + 282-task VeriBench-IndustrySet)를 HumanEval, classical algorithm, Python stdlib, MIT 6.858 기반 보안 예제, 14개 산업 도메인에서 수집·구성
• 각 task마다 curator가 작성한 reference Lean 4 theorem/proof를 기준으로 두 가지 reference-side validity gate D1(compile), D2(prove) 설정
• agent에게 Python 소스만 제공하고 verifier feedback을 활용한 agentic loop에서 구현, 테스트, theorem, proof를 포함하는 완전한 Lean 4 파일을 자동 생성하도록 요구
• SCSC = exp((1/5) Σ log f_i) 형태의 로그 도메인 기하평균으로 5개 factor(typecheck, no-sorry proof, LLM-judge coverage, D1, D2)를 conjunctive하게 결합
• Codex(GPT-5.4), Claude Code(Sonnet 4.6), Leanstral v2 세 frontier coding agent를 single-shot 및 iterative self-correction 조건에서 평가
• LLM judge의 coverage 추정치를 5명의 독립 human rater와 비교하여 Pearson 상관계수로 calibration 검증(Appendix E)

Originality

• 기존 벤치마크(VERINA, FVAPPS, CLEVER, DafnyBench, Clover, Vericoding)가 Lean theorem, Dafny triplet, NL description, pre-existing formal spec 등 이미 정제된 입력에서 시작하는 것과 달리, VeriBench는 executable Python file을 유일한 source artifact로 삼아 agent가 formal specification과 Lean proof obligation을 동시에 추론하도록 요구하는 최초의 end-to-end 벤치마크이다.
• compensatory aggregation의 한계를 지적하고 conjunctive하면서도 smooth한 partial-credit 평가를 실현하는 SCSC라는 새로운 로그 도메인 기하평균 지표를 제안했다.
• specification synthesis를 proof search와 대등하거나 그 이상의 병목으로 규명한 실증적 발견(specification gap)을 제시했다.

Limitation & Further Study

• coverage factor가 kernel-checked entailment가 아닌 LLM-judge 추정치에 기반하므로, 저자들 스스로도 이를 candidate evidence로 명시하며 reference-side narrowness, judge harshness, representation mismatch 등 대안적 설명 가능성을 완전히 배제하지 못한다.
• human calibration이 Pearson r=0.70 수준으로 상당히 높지만 완벽하지 않아 judge의 체계적 편향 가능성이 남아있다.
• 평가 대상이 Codex, Claude Code, Leanstral-v2 세 가지 frontier agent에 한정되어 있어 더 다양한 모델 및 아키텍처에 대한 일반화 가능성은 후속 연구가 필요하다.
• VeriBench-IndustrySet이 synthetic 또는 license-cleared adaptation으로 구성되어 있어 실제 산업 현장의 복잡성을 온전히 반영하는지에 대한 추가 검증이 필요하다.

Evaluation

총평: 테스트 기반 평가의 구조적 한계를 넘어 end-to-end formal verification을 agentic 방식으로 평가하는 새로운 벤치마크와 지표를 제시하며, specification synthesis가 proof search 못지않은 병목임을 보인 의미 있는 실증 연구이나 coverage 판정이 LLM judge에 의존한다는 점은 향후 보완이 필요하다.