Blame for code/notes/src/0306-benchmarks-landscape.tex

\documentclass[11pt]{article}
\usepackage{common}
\begin{document}
\notehead{0306}{Verified-code benchmarks: what each measures and how to read the numbers}{VERINA, CLEVER, FVAPPS, DafnyBench, miniCodeProps, from their papers: which obligations each discharges by machine and which it assumes, and the arithmetic (pass@$k$, intervals, composite bounds) a headline number needs. Companion notebook: \texttt{notebooks/}\allowbreak\texttt{0306-benchmarks-landscape.ipynb}.}

\begin{problem}
\question{What does each verified-code benchmark's headline number actually certify, and how do we turn it into a claim with an error bar?}
Five benchmarks report ``verified code generation'' numbers from $0.6\%$ to $68\%$. They are not comparable on their face: they ask for different things (write a proof; write a spec; write the code), take the specification from different places (given, hidden, generated and tested), use different checkers (Lean kernel, Dafny/Z3, tests plus property tests), and report different statistics. We need (i) a common frame that says what a ``success'' certifies, and (ii) the arithmetic that turns a published number into a claim with an error bar. Notes 0301--0305 supply the ingredients; this note applies them.
\end{problem}
\stepcounter{section}% the problem box counts as section 1: keeps every \S and notebook cross-reference stable

\section{Notation}
\begin{center}\small\begin{tabular}{@{}lP{10.6cm}@{}}\toprule
Symbol & Meaning\\\midrule
$\nu,\ \pi,\ (P,Q),\ \rho$ & natural-language description; implementation; specification (pre, post); proof\\
CodeGen, SpecGen, ProofGen & produce $\pi$; produce $(P,Q)$; produce $\rho$ (VERINA's three foundational tasks \cite{verina} \S4.1)\\
$O_1,\dots,O_4$ & obligations: $O_1$ code behaves as intended; $O_2$ $(\hat P,\hat Q)$ is sound and complete for the intent; $O_3$ $\pi\models(P,Q)$; $O_4$ the formal statement is faithful to $\nu$\\
$n,c,k$ & samples per task, correct among them, budget in $\mathrm{pass@}k$\\
$\hat p=s/N$ & observed success rate on $N$ tasks; $z=1.96$\\
$P_A,P_B,P_C$ & stage success probabilities of a composite task\\\bottomrule\end{tabular}\end{center}

\section{Derivation}
\subsection{A common frame: which obligations does a success certify?}
A fully verified program carries four obligations. A benchmark can \emph{discharge} an $O_i$ by proof (kernel/verifier), by tests (evidence only), or merely \emph{assume} it from a human author.
\begin{center}\footnotesize\begin{longtable}{@{}P{2.1cm}P{1.8cm}P{2.1cm}P{3.0cm}P{3.2cm}P{2.5cm}@{}}\toprule
Benchmark & Size, language & Task (output) & Spec comes from & Spec validation ($O_2,O_4$) & Checker and trust\\\midrule\endhead
\textbf{VERINA} \cite{verina} & 189 tasks, Lean~4 (MBPP, LiveCodeBench, LeetCode); 46 with reference proofs & CodeGen, SpecGen, ProofGen, and compositions & hand-written ground truth $(P,Q)$; model-generated in SpecGen & $\hat P,\hat Q$ vs truth: prove, else \texttt{decide}/\texttt{plausible} on positive/negative tests (median 5 / 12 per task, 100\% coverage of reference code); verdict \emph{holds / does not hold / might hold / unknown}; error bars for unknown & Lean kernel for proofs; \texttt{\#guard} unit tests for code; testing for specs (\emph{evidence})\\
\textbf{CLEVER} \cite{clever} & 161 of HumanEval's 164, Lean~4 & (1) spec + proof of \emph{isomorphism} to a hidden spec; (2) implementation + proof & hidden, hand-written, non-computable ground truth & $O_2$ \emph{proved}: generated spec $\Leftrightarrow\ \psi^*$ (QED~1); no tests, no LLM annotations & Lean kernel for both QEDs; success needs both\\
\textbf{FVAPPS} \cite{fvapps} & 4715 samples, Lean~4.12 (APPS: Codeforces, LeetCode); 2089 ``guarded'', 1083 ``guarded and plausible'' & implement the \texttt{def} and prove each \texttt{theorem} stated with \texttt{sorry} & \emph{properties} extracted from tests by an LLM (property-based tests turned into theorems), not a full spec & unit tests as \texttt{\#guard\_\allowbreak msgs} on a Python-translated solution (tier \emph{guarded}); Lean property-based testing (Plausible, tier \emph{plausible}) & Lean kernel for proofs; spec quality is \emph{tested}, partial\\
\textbf{DafnyBench} \cite{dafnybench} & 782 ground-truth Dafny programs ($\sim$53k LOC) & \texttt{fill\_\allowbreak hints}: reinsert \texttt{assert}/\texttt{invariant} removed from a verified program & given \texttt{requires}/\texttt{ensures} (human, from GitHub, Clover, dafny-synthesis) & none beyond: success requires the same \texttt{requires}/\texttt{ensures} be kept and no \texttt{assume false}/\texttt{\{:verify false\}} & Dafny verifier (SMT-backed): trust base includes the solver\\
\textbf{miniCodeProps} \cite{minicp} & 201 properties, Lean~4 (95 TIP functions, Haskell$\to$Lean) & ProofGen only (code and property given) & TIP: human-written properties of lists, trees, heaps, sorting & none needed: statements fixed; split easy (medley 86) / medium+hard (termination+sorting 115) & Lean kernel\\\bottomrule\end{longtable}\end{center}

\textbf{Reading the frame.} Obligation by obligation:
\begin{center}\footnotesize\begin{tabular}{@{}lcccc@{}}\toprule
 & $O_1$ code intent & $O_2$ spec quality & $O_3$ code $\models$ spec & $O_4$ statement faithful\\\midrule
VERINA ProofGen & tests (given) & assumed (given) & \textbf{proved} & assumed\\
VERINA SpecGen & --- & \textbf{tested} / proved if lucky & --- & tested\\
VERINA CodeGen & \textbf{tested} & assumed & --- & ---\\
CLEVER & --- & \textbf{proved} (iso) & \textbf{proved} & assumed (hand-written)\\
FVAPPS & tested (tier) & \textbf{tested} (partial) & \textbf{proved} (properties only) & assumed (LLM-written)\\
DafnyBench & --- & assumed & \textbf{proved} (solver) & assumed\\
miniCodeProps & --- & assumed & \textbf{proved} & assumed\\\bottomrule\end{tabular}\end{center}
Only CLEVER makes the model prove its spec against a held-out truth; everything else either assumes the statement or tests it. This is the 0305 lattice (R4 there): a number from a benchmark that assumes $O_2$ and $O_4$ says nothing about spec generation risk.

\paragraph{Three concrete caveats visible in the papers themselves.} (i) FVAPPS's displayed sample (Fig.~2) includes the theorem \texttt{solve\_\allowbreak elections\_\allowbreak nonnegative : solve\_elections n voters >= 0}, whose conclusion holds for every \texttt{Nat}: it carries no information (derived from the figure; the paper does not comment). Proof success on property-theorems is therefore an \emph{upper-biased} proxy for correctness. (ii) CLEVER documents that computable specs ``leak'' the implementation so that a copy plus a trivial proof suffices \cite{clever} Fig.~2--3. (iii) DafnyBench notes that Clover's own specifications sometimes repeat the implementation (their Appendix F) \cite{dafnybench} \S1.

\subsection{Reading a number, part 1: pass@$k$}
Given $n$ samples with $c$ correct, a uniformly random $k$-subset has no correct member with probability $\binom{n-c}{k}/\binom nk$, so the per-task estimator is $1-\binom{n-c}{k}/\binom nk$, and the benchmark score is its mean over tasks (Chen et al.\ \cite{codex} \S2.1, Eq.~(1)).
\begin{proposition}[Unbiased]\label{prop:unb} Let $k\le n$ and let the $n$ samples for a task be i.i.d.\ with success probability $p$ (so $c\sim\mathrm{Bin}(n,p)$). Then $\mathbb E\bigl[1-\binom{n-c}{k}/\binom nk\bigr]=1-(1-p)^k$, with the convention that the ratio is $0$ when $n-c<k$.\end{proposition}
\emph{Proof.} Condition on the outcome vector: a uniformly chosen $k$-subset avoids all $c$ correct samples with probability $\binom{n-c}{k}/\binom nk$. Averaging over the i.i.d.\ outcomes, the chosen subset (selected independently of the outcome values) is itself $k$ i.i.d.\ draws, so the probability that none is correct is $(1-p)^k$. Hence $\mathbb E\bigl[\binom{n-c}{k}/\binom nk\bigr]=(1-p)^k$. $\square$\\
The conditions matter: the statement is per task and needs i.i.d.\ samples (a sampler with a shared seed, or dependence on a verifier-guided search, breaks it) and $n\ge k$; the benchmark score, the mean over tasks, is then unbiased for $\frac1T\sum_t\bigl[1-(1-p_t)^k\bigr]$, not for $1-(1-\bar p)^k$ (Jensen again).\\
\emph{The plug-in is biased:} $1-(1-c/n)^k$ has expectation $\ne1-(1-p)^k$ (Jensen on the convex map $x\mapsto(1-x)^k$ gives $\mathbb E(1-\hat p)^k\ge(1-p)^k$, so the plug-in \emph{under}-estimates, Chen et al.\ Appendix~A; measured in the notebook: bias $-0.019$ to $-0.072$ at $n\le100$).
\paragraph{Stable form.} $\dfrac{\binom{n-c}{k}}{\binom nk}=\dfrac{(n-c)!\,(n-k)!}{(n-c-k)!\,n!}=\prod_{i=n-c+1}^{n}\dfrac{i-k}{i}=\prod_{i=n-c+1}^{n}\Bigl(1-\dfrac ki\Bigr)$ (cancel $(n-c)!$ against the first $n-c$ factors of $n!$ and $(n-k)!$ against $(n-c-k)!$), valid for $n-c\ge k$ (else the ratio is $0$ and $\mathrm{pass@}k=1$). The factorial form overflows float64 beyond $170!$; the product does not. This is the script of Chen et al.\ Fig.~3.

\paragraph{Protocols are not interchangeable.} VERINA reports pass@1 from 5 samples per task (App.\ C.3); miniCodeProps uses GPT-4o pass@32 and, in a second row, 2 rounds of refinement with $k=16$ per round; DafnyBench allows up to 10 attempts with the verifier's error message fed back (first attempt $\approx54\%$, plateau $\approx65\%$ by $n\approx5$, best $67.8\%$ in Table~3) \cite{dafnybench} \S4.1, \S4.3. Published gaps due to protocol alone: DafnyBench $+14$ points; miniCodeProps $+2.5$ points ($34.8\to37.3\%$). Compare numbers only at equal $k$, equal attempt budget, equal timeout.

\subsection{Reading a number, part 2: intervals for small benchmarks}
Treat tasks as exchangeable Bernoulli trials (\emph{named approximation}: FVAPPS's $406$ theorems come from $100$ problems and are positively correlated; independence makes its interval too narrow). The Wald interval $\hat p\pm z\sqrt{\hat p(1-\hat p)/N}$ fails for small $N\hat p$. The Wilson interval is the set of $p$ not rejected by the score test: $(\hat p-p)^2\le z^2p(1-p)/N$. Expanding, $(1+z^2/N)\,p^2-(2\hat p+z^2/N)\,p+\hat p^2\le0$, whose roots are
\[
p_\pm=\frac{\hat p+\frac{z^2}{2N}\pm z\sqrt{\frac{\hat p(1-\hat p)}{N}+\frac{z^2}{4N^2}}}{1+z^2/N}.
\]
Coverage by Monte Carlo (40,000 replications each): at $N=161,\,p=0.005$ Wald covers only $55.2\%$, Wilson $95.4\%$; at $N=189,\,p=0.049$: $94.5\%$ vs $96.0\%$; at $N=782,\,p=0.68$ both $\approx95\%$.
\begin{center}\small\begin{tabular}{@{}llrr@{}}\toprule
Benchmark & Setting (as reported) & rate & Wilson 95\% interval\\\midrule
CLEVER & best few-shot LLM, end-to-end ($1/161$) & 0.6\% & [0.1\%, 3.4\%]\\
VERINA & best model, proof, pass@1 ($4.9\%$; $k\approx9$) & 4.8\% & [2.5\%, 8.8\%]\\
VERINA & best model, spec sound+complete ($52.3\%$; $k\approx99$) & 52.4\% & [45.3\%, 59.4\%]\\
miniCodeProps & GPT-4o pass@32+refinement, overall ($75/201$) & 37.3\% & [30.9\%, 44.2\%]\\
miniCodeProps & same, medium+hard ($8/115$) & 7.0\% & [3.6\%, 13.1\%]\\
FVAPPS & Claude 3.5 Sonnet ($121/406$; clustered, too narrow) & 29.8\% & [25.6\%, 34.4\%]\\
FVAPPS & Gemini 1.5 Pro ($74/406$) & 18.2\% & [14.8\%, 22.3\%]\\
DafnyBench & best model, Table~3 ($67.8\%$ of 782 $=530$) & 67.8\% & [64.4\%, 71.0\%]\\
DafnyBench & ``No LLM'' baseline, Table~3 ($26.9\%\approx210/782$) & 26.9\% & [23.9\%, 30.1\%]\\\bottomrule\end{tabular}\end{center}
The project rule recorded in the roadmap memory (``do not claim RL gains below one binomial SE on miniF2F'') is this arithmetic: at $N=244$ and $\hat p\approx0.8$ one SE is $2.6$ points.

\subsection{Reading a number, part 3: composite tasks}
End-to-end success is a conjunction of stages (code $\wedge$ spec $\wedge$ proof; CLEVER's QED~1 $\wedge$ QED~2).
\begin{proposition}[Fr\'echet bounds]\label{prop:frechet}
For events $A_1,\dots,A_m$: $\ \max\bigl(0,\sum_jP(A_j)-(m-1)\bigr)\le P(\bigcap_jA_j)\le\min_jP(A_j)$, and both bounds are attained by some dependence structure.
\end{proposition}
\emph{Proof.} Upper: $\bigcap A_j\subseteq A_i$. Lower: $P(\bigcap A_j)=1-P(\bigcup A_j^c)\ge1-\sum_j(1-P(A_j))$ by the union bound. Attainment of the upper bound: the comonotone coupling $A_j=\{U<P(A_j)\}$ with one uniform $U$ gives $\bigcap_jA_j=\{U<\min_jP(A_j)\}$ (notebook: $0.0491$ vs $0.049$). Attainment of the lower bound: lay the complements $A_j^c$ on consecutive arcs of the circle $[0,1)$, of lengths $1-P(A_j)$, with $U$ uniform on the circle. If $\sum_j(1-P(A_j))\le1$ the arcs are disjoint, $P(\bigcup A_j^c)=\sum_j(1-P(A_j))$ and equality holds in the union bound; otherwise they cover the circle and $P(\bigcap A_j)=0=\max(0,\cdot)$ (notebook: six marginal vectors, exact rational arithmetic). $\square$\\
VERINA's best stage rates ($72.6\%$ code, $52.3\%$ spec, $4.9\%$ proof) give $P(\text{all})\in[0,0.049]$ for any dependence; independence would give $1.9\%$. (Caveat: VERINA's ProofGen stage is posed against the \emph{ground-truth} spec, not the generated one, so this is an illustration of the bound, not a reading of their end-to-end figure.)

\subsection{Reading a number, part 4: a trivial baseline}
Every benchmark should be read against what a null system scores. DafnyBench reports its own: Table~3 lists a ``No LLM'' row at $26.9\%$ (``Dafny succeeds in auto-verifying some programs even without hints''), i.e.\ about $210$ of the 782 programs \cite{dafnybench} \S4.3. The per-source counts of \S3.1 give an independent derivation: 113 (GitHub) $+$ 23 (Clover) $+$ 72 (dafny-synthesis) $=208$ programs verify with no hints, $208/782=26.6\%$, two programs short of the reported figure (we do not know the cause: harness rerun, timeout, or counting). The null score is therefore $\approx27\%$, and the best reported $67.8\%$ is about $41$ points above it. Analogous null baselines for the other benchmarks are the \texttt{sorry}-free trivial proof tactics (\texttt{simp}, \texttt{omega}, \texttt{decide}) on properties like FVAPPS's \texttt{>= 0}; we have not measured them (open question).

\section{Boxed result}
\begin{result}
\textbf{R1.} Each benchmark certifies a different subset of $\{O_1,\dots,O_4\}$ (matrix above); only CLEVER proves $O_2$ against a hidden truth.\\
\textbf{R2.} $\mathrm{pass@}k=1-\binom{n-c}{k}\big/\binom nk=1-\prod_{i=n-c+1}^{n}(1-k/i)$; unbiased: $\mathbb E=1-(1-p)^k$.\\
\textbf{R3.} Wilson: $p_\pm=\Bigl(\hat p+\tfrac{z^2}{2N}\pm z\sqrt{\tfrac{\hat p(1-\hat p)}N+\tfrac{z^2}{4N^2}}\Bigr)\Big/(1+\tfrac{z^2}N)$.\\
\textbf{R4.} $\max(0,\sum P_j-(m-1))\le P(\text{all})\le\min P_j$.\\
\textbf{R5.} No-op baseline of DafnyBench: $26.9\%$ as reported (Table~3, $\approx210/782$); the \S3.1 counts give $208/782=26.6\%$.
\end{result}

\paragraph{Numerical verification (notebook 0306, all cells executed).}
\begin{center}\small\begin{tabular}{@{}P{8.3cm}P{4.3cm}P{3cm}@{}}\toprule
Identity / claim & size & max abs error / result\\\midrule
R2: stable product vs exact rational (\texttt{Fraction}) & 303 $(n,c,k)$ triples & $6.1\times10^{-16}$\\
R2: naive float64 factorial ratio at $n=200$ & --- & \texttt{nan} (exact $0.6602$)\\
R2: $\mathbb E[\mathrm{pass@}k]=1-(1-p)^k$, exact binomial sum & 6 settings & $6.7\times10^{-16}$\\
R2: plug-in bias $\mathbb E[1-(1-c/n)^k]-(1-(1-p)^k)$ & 6 settings & $-0.019$ to $-0.072$\\
R3: Wilson endpoints solve $(\hat p-p)^2=z^2p(1-p)/N$ & 5 cases & residual $<10^{-12}$\\
R3: Wilson coverage vs Wald, 6 $(N,p)$ cells $\times$ 40,000 & Wilson $\ge0.946$; Wald $0.552$ at $(161,.005)$ & ---\\
R4: Fr\'echet bounds on random joint laws ($m=2,3$) & 20,000 laws & 0 violations; upper bound attained ($0.0491$ vs $0.049$)\\
R4: lower Fr\'echet bound attained by an explicit coupling & 6 marginal vectors & exact\\
R5 and paper arithmetic (22 checks: sums, ratios of Tables, DafnyBench Table~3 $\pm$ equal one binomial s.e., $208$ vs $26.9\%$) & 22 & 21 consistent; 1 flagged\\\bottomrule\end{tabular}\end{center}
The flagged item: FVAPPS reports Gemini ``74 (18.5\%)'' of 406 theorems; $74/406=18.2\%$ (its abstract says $18\%$). The DafnyBench source counts sum correctly ($556+62+164=782$), the $\pm$ in its Table~3 equal one binomial standard error at $N=782$ (e.g.\ $1.7$ for $67.8\%$), and all nine miniCodeProps rates match their counts (e.g.\ $65/86=75.6\%$, $70/201=34.8\%$).

\section{What breaks}
\begin{center}\small\begin{tabular}{@{}P{3.6cm}P{6.5cm}P{5.4cm}@{}}\toprule
Failure & Mechanism & Assumption violated\\\midrule
Cross-benchmark comparison & different tasks, specs, $k$, attempts, timeouts, Lean versions & ``same unit''; compare only within a protocol\\
Assumed statements & DafnyBench, miniCodeProps, FVAPPS take $O_2,O_4$ from humans/LLMs; formal statements of related benchmarks contain defects (miniF2F: mismatch in over half of 488 \cite{minif2frev}) & the statement is faithful (0305)\\
Test-based spec grading & VERINA: testing certifies $>40\%$ of generated specs while proofs certify $<4\%$ (App.~C.5); a \emph{might hold} is not a proof & the suite separates good from bad specs\\
Partial properties & FVAPPS theorems can be trivial or partial (e.g.\ $\ge0$ on \texttt{Nat}) & proved properties $\Rightarrow$ correctness\\
Leakage & computable specs copy the implementation (CLEVER Fig.~2--3); Clover specs sometimes repeat the code (DafnyBench \S1) & spec is implementation-agnostic\\
Contamination & DafnyBench scrapes public GitHub (before the end of 2023) and lists repos to exclude; HumanEval is widely seen in training & test items unseen\\
Small $N$, clustering & intervals of $\pm3$--$7$ points; FVAPPS clustering unmodelled & i.i.d.\ tasks\\
Prompt/tuning & DafnyBench: fixed temperature, 4096-token limit, prompts ``not very systematically tuned'' \cite{dafnybench} \S5.3 & headline = capability\\
Version skew & our pin is Lean~4.9.0-rc1; FVAPPS (4.12), VERINA (uses \texttt{plausible}, newer tactics) may not compile unchanged & statements elaborate on our pin (\textbf{not tested here})\\
Null baseline & DafnyBench ``No LLM'' $=26.9\%$ (Table~3) & the metric starts at 0\\\bottomrule\end{tabular}\end{center}

\paragraph{What to carry forward.} For an RL or SFT loop whose reward is a kernel-checked proof: use a benchmark whose statement is fixed (miniCodeProps, VERINA ProofGen, DafnyBench analogue) so that the strict bridge of 0305 applies; use CLEVER-style spec proofs when the model must produce the spec; report Wilson intervals and a null baseline; never mix $k$.

\nextnote{End of the formal-methods primer (0301--0306). The loop back to the training notes (0101--0205): a verifier is a reward only to the extent that 0301's gate, 0305's statement bridge and 0306's statistics hold.}

\begin{small}
\begin{thebibliography}{99}
\bibitem{verina} Z.~Ye et al., \emph{VERINA: Benchmarking Verifiable Code Generation}, arXiv:2505.23135 (ICLR 2026): abstract (189 tasks; 72.6\%, 52.3\%, 4.9\%); \S3.1 (data format; 46 reference proofs; test medians), \S4.1 (tasks, metrics, Fig.~3 evaluator), Appendix~C.5 and Table~5, Appendix~C.3 (2-shot prompts; 5 samples per task for pass@1).
\bibitem{clever} A.~Thakur et al., \emph{CLEVER: A Curated Benchmark for Formally Verified Code Generation}, arXiv:2505.13938 (NeurIPS 2025 D\&B): abstract (161 problems); \S1 (few-shot LLMs solve ``up to 1/161'' end-to-end), Fig.~1 (two QEDs), Fig.~2--3 (spec leakage; non-computable specs). The 54.0\% for a specialised prover is reported by a different paper (Goedel-Code-Prover, via the vault summary) and is not used above.
\bibitem{fvapps} Q.~Dougherty, R.~Mehta, \emph{Proving the Coding Interview}, arXiv:2502.05714: abstract (4715; 1083; Sonnet 30\%, Gemini 18\%); \S II-B (pipeline; Lean 4.12.0), II-C (tiers 4715/2089/1083); \S III-A/D/E (baselines, 406 theorems of 100 samples, \texttt{Id.run do}); Fig.~2 (sample 23, theorem \texttt{solve\_\allowbreak elections\_\allowbreak nonnegative}).
\bibitem{dafnybench} C.~Loughridge et al., \emph{DafnyBench}, arXiv:2406.08467: abstract (over 750 programs, 53,000 lines, 68\%); \S1 (Clover specs sometimes repeat the implementation, App.~F); \S3.1 (782 programs; 113/23/72 verify with no hints); \S3.2 (task and success criteria); \S4.1 (10 attempts, temperature 0.3, 4096 tokens); \S4.2--4.3 and Table~3 (Claude~3 Opus $67.8\pm1.7\%$; ``No LLM'' $26.9\%$; first try $\sim54\%$; plateau $\sim65\%$); \S5.3 (fixed temperature, 4096 tokens, prompts not systematically tuned).
\bibitem{minicp} E.~Lohn, S.~Welleck, \emph{miniCodeProps}, arXiv:2406.11915: abstract (201 properties); Table~1 (composition); Table~3 (GPT-4o pass@32 34.8\%/37.3\% with refinement ($k{=}16,T{=}2$); ntp-ctx-1.3B 35.8\%).
\bibitem{codex} M.~Chen et al., \emph{Evaluating Large Language Models Trained on Code}, arXiv:2107.03374: \S2.1, Eq.~(1) (unbiased pass@$k$), Fig.~3 (stable implementation), Appendix~A (bias of $1-(1-\hat p)^k$).
\bibitem{minif2frev} M.~Ospanov et al., \emph{miniF2F-Lean Revisited}, arXiv:2511.03108.
\bibitem{wilson27} E.~B.~Wilson, ``Probable inference, the law of succession, and statistical inference'', JASA 1927; M.~Fr\'echet (1935) for the bounds; derived above. \emph{Not on arXiv; not fetched; both results are re-derived in this note and checked numerically.}
\end{thebibliography}
\end{small}
\end{document}