neurips-2026-avs-bench/formal-anytime-valid-stats
Formal-AVS: A Lean Benchmark for Anytime-Valid Confidence-Sequence Theorem Proving 60 Lean 4 theorem targets on anytime-valid confidence sequences across four families (Howard-Ramdas, betting, Whitehouse vector, asymptotic CLT). Benchmark Structure 60 targets grouped into tiers T0-T3 (pre-evaluation) and categories T4-T5 (empirical) 7 drafters evaluated across single-shot, agentic, and unbounded modes 14 Aristotle sessions (unbounded refinement)… See the full description on the dataset page: https://huggingface.co/datasets/neurips-2026-avs-bench/formal-anytime-valid-stats.
Formal-AVS: A Lean Benchmark for Anytime-Valid Confidence-Sequence Theorem Proving
60 Lean 4 theorem targets on anytime-valid confidence sequences across four families (Howard-Ramdas, betting, Whitehouse vector, asymptotic CLT).
Benchmark Structure
- 60 targets grouped into tiers T0-T3 (pre-evaluation) and categories T4-T5 (empirical)
- 7 drafters evaluated across single-shot, agentic, and unbounded modes
- 14 Aristotle sessions (unbounded refinement)
Headline Results (pass@5 on 60-target benchmark)
Usage
from datasets import load_dataset
ds = load_dataset("neurips-2026-avs-bench/formal-anytime-valid-stats")Source Datasets
Hand-authored from scratch. Theorem statements formalize results from:
- Howard et al. (2021) — doi:10.1214/20-AOS1991
- Waudby-Smith and Ramdas (2024) — doi:10.1214/23-AOS2276
- Whitehouse et al. (2025) — arXiv:2503.09714
No pre-existing machine learning datasets were used as source data.
Data Collection and Provenance
Collection. Theorem statements were manually written in Lean 4 by the paper authors, formalizing properties of four anytime-valid confidence sequence families from the three source papers listed above. No crowdsourcing, no web scraping, no automated generation.
Annotation. Tier labels (T0-T5) were assigned by the paper authors based on proof shape before any solver evaluation. Per-drafter closure rates were computed by automated sweep: pass@5 with one greedy sample at T=0 and four stochastic samples at T=0.7. Axiom audits were performed via the Lean #print axioms command. Seven language model drafters (Claude Sonnet 4.6, Kimi K2.5, Gemini 3 Pro, Mistral Large 3, Claude Opus 4.6, DSPv2-7B, Goedel-V2-8B) and Harmonic Aristotle were used for proof closure evaluation. The Lean 4 kernel served as the ground-truth verifier.
Personal and Sensitive Information
None. The dataset contains only mathematical theorem statements and solver evaluation metadata.
Social Impact and Limitations
Anytime-valid confidence sequences are deployed in production A/B testing and clinical trial monitoring systems. Formally verified implementations reduce the risk of silent coverage-guarantee violations. This benchmark measures how close current provers are to automating that verification.
Limitations. The benchmark covers one subfield (anytime-valid statistics) with 60 targets. Closure rates may not transfer to other Lean libraries with different import structures. Aristotle is a closed-source system.
Biases. The targets are curated from a single domain and a single proof assistant (Lean 4). Performance on this benchmark does not predict performance on other mathematical domains or proof systems.
License
CC-BY-4.0