Formal-AVS: a Lean benchmark for anytime-valid confidence-sequence theorem proving

Motivation

• Known: MiniF2F, ProofNet, Verina, FormalMATH, LeanDojo 등 기존 Lean proof benchmark들은 고정된(statement library) 정리 집합에 대한 closure율을 측정해왔으며, anytime-valid confidence sequence는 A/B testing과 순차적 임상시험에서 optional stopping 문제를 해결하는 이론으로 이미 잘 알려져 있다.
• Gap: 기존 Lean 벤치마크들은 drafter가 custom definitions, multi-module import chain, domain-specific lemma vocabulary를 가진 고유한 conceptual structure의 라이브러리를 탐색할 수 있는지를 테스트하지 않으며, Mathlib에는 HR-family, betting family, Whitehouse vector, asymptotic CLT family의 formalization이 전혀 존재하지 않는다.
• Why: Anytime-valid confidence sequence는 실제 A/B testing과 임상시험에 배포되는 통계 방법인데, 구현 코드의 사소한 버그(missing absolute value, off-by-one 등)가 coverage guarantee를 조용히 무효화할 수 있어 Lean으로 이론-구현 일치를 형식 검증하는 것이 실질적 안전성 문제와 직결된다.
• Approach: formal-avs-lean이라는 companion Lean 4 라이브러리를 새로 구축해 4개 family의 rate function을 instantiate하고, 이를 기반으로 60개 target theorem(6개 tier로 구성)에 대해 4개 closed-source generalist, 2개 open-weights prover(DSPv2-7B, Goedel-Prover-V2-8B), Harmonic Aristotle을 single-shot/agentic/unbounded 세 capability level에서 평가한다.

Achievement

1. Single-shot generalist 한계 규명: Single-shot generalist closure는 최대 22/60(Gemini, hint-list prompt)에 그치고 cross-function target에서는 0으로 떨어짐을 보였다.
2. Agentic loop의 효과 입증: 4-round agentic refinement loop(cycle prove r=4)가 non-Aristotle solver 최초로 cross-function target을 closure하고, Gemini의 hint-list 우위(19=19)가 사라져 prompt-sensitivity gap을 좁힘을 확인했다.
3. Harmonic Aristotle의 압도적 성능과 false-as-stated target 발견: unbounded compute 하에서 Aristotle이 53/60을 axiom-clean 상태로 closure했고, 다른 모든 solver가 accept한 3개의 false-as-stated target을 surfacing했다.
4. 재현 가능한 artefact 공개: 벤치마크, companion Lean library(formal-avs-lean), 그리고 closed proof·refutation witness·axiom audit을 포함한 14-session Aristotle history archive를 공개했다.

How

• companion library 구축: formal-avs-lean(Apache-2.0, ~3k lines)을 8개 모듈(Basic, HowardRamdas, WaudbySmithBetting, WhitehouseVector, AsymptoticCLT, Quantization, PhiTransform, MatchingConstants)로 구성하고 4개 family의 rate function ηF와 dependency lemma를 증명
• 6-tier target 설계: T0-T3는 proof shape 기준 사전 정의, T4-T5는 평가 후 부여되는 empirical failure category로 구성, ~50개 axiom-clean dependency lemma로 target을 bound하여 수작업 axiom audit 가능하게 설계
• hint-ablation 실험: log-domain substitution hint(lateral re-encoding)와 Mathlib-lemma-chain hint(tactic vocabulary)를 직교적으로 분리한 3-column ablation을 수행해 두 요소가 동시에 필요함을 확인
• capability level 구분 평가: completion-style(single-shot) baseline과 agentic-mode(4-round refinement loop), unbounded(Aristotle) 세 층위로 나누어 solver별 closure rate 비교
• axiom audit 및 반증 수집: Lean #print axioms 출력을 이용한 per-session axiom-audit과 counterexample witness를 통해 drafter의 hallucination과 진짜 closure를 구분

Originality

• Mathlib에 전혀 표현되지 않은 research subfield(anytime-valid confidence sequence)를 대상으로 한 최초의 Lean formalization 벤치마크라는 도메인 독창성
• 기존 벤치마크(MiniF2F, ProofNet, Verina, FormalMATH 등)와 달리 고정된 statement library가 아닌 custom conceptual structure(자체 정의, multi-module import chain, domain-specific lemma vocabulary)를 탐색하는 능력을 테스트
• hint를 log-domain substitution과 Mathlib-lemma-chain 두 축으로 분리한 orthogonal ablation 설계는 기존 hint-ablation 연구의 단일 "context" 축 접근과 차별화
• target statement뿐 아니라 axiom-audited dependency proof, refutation witness, 14-session Aristotle history archive까지 함께 공개하는 이중 artefact 공개 방식

Limitation & Further Study

• 벤치마크 규모가 60개 target으로 제한적이며, 이는 저자가 수작업으로 axiom-clean dependency lemma를 증명할 수 있는 한계(~50개)에 의해 bound된 설계 상 제약이다.
• Harmonic Aristotle은 closed-source proprietary 시스템으로 재현성이 API key 접근에 의존하며, 완전한 open reproducibility를 보장하지 못한다.
• 단일 저자(1인 저술)에 의한 연구로 target curation과 axiom audit의 objectivity 검증이 제한적일 수 있다.
• false-as-stated target 발견이 3개에 그쳐 이 현상의 일반성(다른 도메인에도 통용되는지)에 대한 추가 검증이 필요하다.
• 후속 연구로는 벤치마크 확장(더 많은 family, 더 큰 cross-function target), 다른 open-weights 최신 prover와의 비교, agentic loop round 수 증가에 따른 saturation 분석 등이 필요하다.

Evaluation

총평: 통계적으로 중요하지만 Lean formalization이 전무했던 anytime-valid confidence sequence 도메인에 최초의 벤치마크와 companion library를 제공하고, single-shot/agentic/unbounded 세 capability level에서 solver 간 뚜렷한 성능 차이와 false-as-stated target 발견이라는 흥미로운 결과를 보여주는 알찬 workshop 논문이다.