Blame for code/notes/src/0305-spec-risk.tex

\documentclass[11pt]{article}
\usepackage{common}
\begin{document}
\notehead{0305}{Spec generation risk: the proof of the wrong theorem}{An LLM-written specification can be wrong in ways the kernel cannot see. Spec validation by tests and mutation, the Bayes risk of accepted proofs, and this repository's statement-rewrite finding. Companion notebook: \texttt{notebooks/}\allowbreak\texttt{0305-spec-risk.ipynb}.}

\begin{problem}
\question{When the statement itself is model output, how can ``the proof checks'' and ``the code is correct'' come apart, and how do we detect it?}
Notes 0301--0304 establish what a checked proof guarantees: the statement \emph{as typed} is true. In verifiable code generation the statement itself is model output (a postcondition,
a theorem about the function) or is mediated by a harness (a rewritten or swapped statement). Then ``the proof checks'' and ``the code is correct'' come apart, and the gap is invisible to the kernel and to the reward.
We need (i) a precise notion of \emph{how} a spec can be wrong, (ii) cheap tests that expose it, (iii) a number for the damage, and (iv) gates that keep the statement honest.
\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.5cm}@{}}\toprule
Symbol & Meaning\\\midrule
$P,Q$ & ground-truth pre- and post-condition ($P(x)$, $Q(x,y)$); $\hat P,\hat Q$ generated ones\\
$\phi=\{f\mid\forall x.\,P(x)\Rightarrow Q(x,f\,x)\}$, $\hat\phi$ & programs meeting the true / generated spec\\
sound, complete & $\hat Q$ sound: $\forall x\,y.\ P(x)\wedge\hat Q(x,y)\Rightarrow Q(x,y)$; complete: $\forall x\,y.\ P(x)\wedge Q(x,y)\Rightarrow\hat Q(x,y)$ (VERINA \S4.1)\\
$\mathrm{Pos},\mathrm{Neg}$ & positive tests $\{(x,y):P\wedge Q\}$; negative tests $\{(x,y):P\wedge\neg Q\}$\\
$\kappa(M)$ & fraction of input/output pairs on which mutant $M$ differs from the truth\\
$u$ & probability a generated spec is wrong; $a_c,a_w$ prover success on correct / wrong specs; $r=a_w/a_c$\\\bottomrule\end{tabular}\end{center}

\section{Derivation}
\subsection{Two kinds of ``wrong spec'', and the one that hides}
Work at the level of relations $\hat Q\subseteq X\times Y$. Soundness says $\hat Q\cap P\subseteq Q$ (the spec accepts only correct outputs); completeness says $Q\cap P\subseteq\hat Q$ (it accepts all of them). An unsound spec admits wrong programs (too weak); an incomplete one rejects correct programs (too strong). \emph{Program level:} $\hat\phi\subseteq\phi$ is the claim we care about.
\begin{lemma}[Relation vs program level]\label{lem:rel}
If $\hat Q$ is sound then $\hat\phi\subseteq\phi$. Conversely, if $\hat\phi\subseteq\phi$ and $\hat Q$ is \emph{total on $P$} ($\forall x.\ P(x)\Rightarrow\exists y.\ \hat Q(x,y)$) then $\hat Q$ is sound.
\end{lemma}
\emph{Proof.} First part: for $f\in\hat\phi$ and $P(x)$ we have $\hat Q(x,f\,x)$, hence $Q(x,f\,x)$ by soundness. Second: let $P(x_0)\wedge\hat Q(x_0,y_0)$. Build $f$ with $f(x_0)=y_0$ and, for $x\neq x_0$ with $P(x)$, $f(x)$ any $y$ with $\hat Q(x,y)$ (totality); elsewhere arbitrary. Then $f\in\hat\phi\subseteq\phi$, so $Q(x_0,y_0)$. $\square$

The totality hypothesis is not decoration. If $\hat Q(x_0,\cdot)=\emptyset$ for some $x_0$ with $P(x_0)$, the spec is \emph{unrealisable}: $\hat\phi=\emptyset$, so $\hat\phi\subseteq\phi$ holds vacuously while no implementation can ever be proved correct. The failure then shows up as an unprovable theorem, which (note 0304) is indistinguishable from a weak prover: \textbf{an unrealisable spec is blamed on the model}. Test: $\forall x.\,P(x)\Rightarrow\exists y.\,\hat Q(x,y)$ over a scope.

\subsection{Spec validation by tests (the VERINA reduction)}
\begin{proposition}[Soundness and completeness are decided by negative and positive tests]\label{prop:tests}
(a) $\hat Q$ is complete iff $\hat Q(x,y)$ holds on every positive pair. (b) $\hat Q$ is sound iff $\hat Q(x,y)$ is false on every negative pair $(P(x),\neg Q(x,y))$. (c) Pre-conditions: $\hat P$ sound ($P\Rightarrow\hat P$) iff $\hat P$ holds on every $x$ with $P(x)$; complete ($\hat P\Rightarrow P$) iff $\hat P$ fails on every $x$ with $\neg P(x)$.
\end{proposition}
\emph{Proof.} (a) completeness is $\forall(x,y).\,(P\wedge Q)\Rightarrow\hat Q$, which is exactly ``$\hat Q$ on all positives''. (b) soundness is $\forall(x,y).\,(P\wedge\hat Q)\Rightarrow Q$, equivalently $\forall(x,y).\,(P\wedge\neg Q)\Rightarrow\neg\hat Q$. (c) identical with $x$ alone. $\square$\\
This is the reduction implemented by VERINA's evaluator: ground-truth specs pass all positive tests and fail all negative ones by construction, so on a \emph{finite} suite \cite{verina} \S4.1 and Appendix~C.5 test ``$\hat Q$ sound'' on negative tests and ``$\hat Q$ complete'' on positive tests. Their worked example is a pre-condition: truth \texttt{k < s.size}; \texttt{k < s.size - 1} is refuted as unsound by the positive test \texttt{(s=[1,2,3,4,5],k=4)}, and \texttt{k < s.size + 1} as incomplete by the negative test \texttt{k=5}. A finite suite is \emph{one-sided}: a violated test certifies the defect; a passed suite yields only ``might hold''.

\paragraph{How good is a random suite?} If a defect is witnessed by a fraction $\kappa$ of the candidate negative (or positive) pairs, $m$ independent random tests miss it with probability $(1-\kappa)^m$ (0304 R2), so $m\ge\ln\delta/\ln(1-\kappa)$ tests are needed. In the notebook's toy domain (40 lists over $\{0,1,2\}$, length $\le3$; 1560 negative pairs; $|\mathrm{Pos}|=40$):
\begin{center}\small\begin{tabular}{@{}lrrrr@{}}\toprule
Candidate postcondition & sound & complete & accepted negatives & rejected positives\\\midrule
Q0 \; sorted $\wedge$ perm (truth) & yes & yes & 0 & 0\\
S1 \; sorted only & \textbf{no} & yes & 760 ($\kappa=.487$) & 0\\
S2 \; sorted $\wedge$ perm $\wedge$ len$\le2$ & yes & \textbf{no} & 0 & 27\\
S3 \; sorted, same length, same sum & \textbf{no} & yes & 22 ($\kappa=.0141$) & 0\\
S4 \; strictly sorted $\wedge$ perm & yes & \textbf{no} & 0 & 24\\
S5 \; sorted $\wedge$ $y=\mathrm{sorted}(x)$ (leaks) & yes & yes & 0 & 0\\
S6 \; perm only & \textbf{no} & yes & 72 & 0\\
S7 \; sorted, same length, $y\subseteq x$ & \textbf{no} & yes & 120 & 0\\\bottomrule\end{tabular}\end{center}
(Here $\kappa$ is the fraction of the 1560 \emph{negative} pairs a defect is witnessed on, because a soundness defect is exposed by drawing from the negatives; the mutation table below draws from all 1600 pairs, so the same predicate S1 $=$ ``drop perm'' has $\kappa=760/1600=.475$ there.) S1 is exposed by about $\ln(0.01)/\ln(1-0.487)\approx7$ random negatives; the subtle S3 needs $\approx325$. The definition-based verdict (all 1600 pairs) and the test-based one agree on all 8 candidates. S5 is \emph{correct} yet useless as a spec: it \emph{is} the implementation (\S3.5).
\emph{Programs passing wrong specs.} Seven candidate programs: the empty list, dedup-sort, clamp-then-sort, ``sort then zero the first element'' all satisfy S1 (4 wrong programs accepted); the identity and the descending sort satisfy S6 (2 accepted); none satisfies Q0. This is the proof of the wrong theorem in miniature: ``verified against S1'' is true of programs that are plainly wrong.

\subsection{Mutation testing of a spec}
Mutate the truth $Q_0=\mathrm{sorted}(y)\wedge\mathrm{perm}(x,y)$: drop an atom; replace $\le$ by $<$ or $\ge$; replace perm by same-length, same-sum, subset; add a redundant conjunct. A mutant is \emph{killed} by a suite iff some test distinguishes it from $Q_0$. For uniform tests, $\Pr[\text{kill}]=1-(1-\kappa(M))^m$; $\kappa=0$ means an \emph{equivalent mutant}, unkillable by any suite.
\begin{center}\small\begin{tabular}{@{}lrrr@{}}\toprule
Mutant & $\kappa$ & $\Pr[\text{kill}],m{=}10$ theory & Monte Carlo (20,000 suites)\\\midrule
drop sorted & .0450 & .3690 & .3715\\
drop perm & .4750 & .9984 & .9986\\
$\le\to<$ & .0150 & .1403 & .1448\\
$\le\to\ge$ & .0375 & .3176 & .3192\\
perm $\to$ same length & .1837 & .8687 & .8689\\
perm $\to$ same sum & .0600 & .4614 & .4608\\
perm $\to$ subset & .2231 & .9199 & .9199\\
add \texttt{len(y)<=2} & .0169 & .1565 & .1540\\
add redundant \texttt{len(x)=len(y)} & 0 & 0 & 0 (equivalent)\\
perm $\to$ $y=\mathrm{sorted}(x)$ & 0 & 0 & 0 (equivalent)\\\bottomrule\end{tabular}\end{center}
The exhaustive suite kills all 8 non-equivalent mutants; the Monte Carlo worst $|z|$ is $1.84$. The practical reading: a spec whose mutants survive a test suite is not pinned down by that suite. Clover \cite{clover} uses the same idea at the level of consistency between code, annotation and docstring and reports acceptance up to 87\% of correct instances with no false positives on adversarial ones, and found 6 incorrect programs in a human-written dataset (abstract).

\subsection{Six mechanisms of ``proof of the wrong theorem'' (with Lean evidence)}
\paragraph{(a) Weak spec.}
\begin{lstlisting}
def badSort (xs : List ℕ) : List ℕ := []
theorem badSort_weak_spec (xs : List ℕ) : List.Sorted (· ≤ ·) (badSort xs) := List.sorted_nil
theorem badSort_not_perm : ¬ (∀ xs : List ℕ, List.Perm xs (badSort xs))    -- proved via length_eq
\end{lstlisting}
The weak-spec theorem holds with no axioms; the refutation of the full spec uses $\{\texttt{propext}\}$. VERINA reports concrete LLM failures of this kind: an \emph{unsound} postcondition that does not exclude leading zeros, and one that mishandles $n=0$ in the ``smallest single-digit prime factor'' task, so that it rejects a valid positive test and accepts a negative test \cite{verina} Appendix~E, Figs.~22--23.
\paragraph{(b) Leaking spec.} A computable spec that restates the recursion is proved by \texttt{rfl}-level reasoning (notebook B2: \texttt{leak\_proof}); a relational spec (\texttt{IsFib}) forces a real induction (\texttt{myfib\_isfib}). CLEVER \cite{clever} Fig.~2--3 uses non-computable specs for exactly this reason, and strengthens the protocol: the model must also \emph{prove its generated spec equivalent to a held-out ground-truth spec} (QED~1) before the implementation proof (QED~2) counts.
\paragraph{(c) Vacuous hypotheses.}
\begin{lstlisting}
theorem vac_stmt (n : ℕ) (h₀ : n < 5) (h₁ : n > 7) : n = 12345 := by omega
\end{lstlisting}
compiles. A satisfiability probe \texttt{decide (∃ n < 100, n < 5 ∧ n > 7)} is \texttt{false}; for the consistent pair (\texttt{n < 10}) it is \texttt{true}. Audits of miniF2F and its relatives report ``vacuous theorems'' among their 398 mechanically certified issues \cite{faults26}; ProofGate's audit adds a negation-counterexample probe \cite{proofgate}.
\paragraph{(d) Statement rewrite (our finding).} In this repository's P2 pipeline (\texttt{docs/P2.md}, \S8c item 18) verification ported Goedel's \texttt{problem\_check}, which \emph{swaps the original statement in} and re-runs the candidate's tactics; ``a completion whose displayed theorem is false or different is ACCEPTED whenever its tactics prove the original''. The notebook reproduces it against four gates on \texttt{mathd\_algebra\_478} (reference conclusion \texttt{v = 65}):
\begin{center}\footnotesize\begin{tabular}{@{}P{3.7cm}P{1.5cm}P{2.1cm}P{3.3cm}P{3.3cm}@{}}\toprule
Candidate (displayed statement) & compile-only & swap & strict & defeq\\\midrule
C0 honest & accept & accept & accept & accept\\
C1 displays \texttt{v = 66}, tactics prove 65 & reject & \textbf{accept} & reject (\texttt{statement\_\allowbreak mismatch}) & reject (\texttt{compile\_\allowbreak error})\\
C2 weakened to \texttt{v ≤ 65} & \textbf{accept} & \textbf{accept} & reject (\texttt{statement\_\allowbreak mismatch}) & reject (\texttt{bridge\_\allowbreak failed})\\
C3 extra false hypothesis \texttt{v < 0} & \textbf{accept} & reject (tactics name \texttt{h₄}) & reject & reject (\texttt{bridge\_\allowbreak failed})\\
C4 binders renamed $b\to b_1$ & accept & accept & reject (\texttt{statement\_\allowbreak mismatch}) & accept\\\bottomrule\end{tabular}\end{center}
Compile-only credits the \emph{easier theorems} C2 and C3 (C3 is vacuous). The swap harness credits C1 and C2 (the displayed statement is not what was proved). The strict tier (token-equal signature \emph{and} the kernel bridge: the kernel must accept the candidate as a term of the \emph{type of the reference}; \texttt{docs/LEAN\_VERIFIER.md} \S2) rejects all four rewrites; the defeq mode accepts only the genuine $\alpha$-renaming. In training the finding is mitigated: \texttt{build\_sft\_data.py} now drops statement-unfaithful samples; the evaluation keeps Goedel's rule so numbers stay comparable (an explicit, documented trade-off).
\paragraph{(e) Silent elaboration.} \texttt{theorem t (x : ℕ) : x + 1 > xx} elaborates to \texttt{∀ \{xx : ℕ\} (x : ℕ), x + 1 > xx} under \texttt{autoImplicit}, and is an error with it off (0302). Numeral types and truncated subtraction (0302) are the same class.
\paragraph{(f) Unrealisable specs.} \S3.1: no program can meet it; every attempt fails and the blame lands on the prover.

\subsection{How much damage: the Bayes risk of an accepted proof}
Suppose a generated spec is wrong with probability $u$; the prover succeeds with probability $a_c$ on a correct spec and $a_w$ on a wrong one. Then
\[
\Pr[\text{wrong}\mid\text{accepted}]=\frac{u\,a_w}{u\,a_w+(1-u)\,a_c}=\frac{u\,r}{u\,r+1-u},\qquad r=\frac{a_w}{a_c}.
\]
\emph{Proof.} Bayes' rule with $\Pr[\text{accepted}\mid\text{wrong}]=a_w$, $\Pr[\text{accepted}\mid\text{correct}]=a_c$. $\square$\\
$r$ is an empirical ratio, not a theorem. For \emph{too-weak} wrong specs $r\ge1$ is plausible (if a program meets $s$ and $s\Rightarrow s'$ it meets $s'$, so $s'$ is semantically easier), but that is a statement about programs: a real prover need not find a proof of the weaker statement more often. And \emph{too-strong} (incomplete) wrong specs are harder, with $r<1$; $a_w$ is an average over both kinds, so $r\ge1$ holds only if weak specs dominate the wrong ones. Anchor: VERINA's best model produces a spec that is both sound and complete in $52.3\%$ of tasks \cite{verina} (abstract), i.e.\ $u\approx0.477$ if every non-passing spec is wrong (an upper estimate: some are ``unknown''). With $r=5$: $\Pr=0.82$; with $r=20$: $0.948$. Monte Carlo (200,000 draws per row): $0.8198$ vs $0.8202$; $0.9480$ vs $0.9480$; worst $|z|=1.72$ over 7 settings.
\begin{proposition}[Degenerate optimum]\label{prop:degen}
Let the reward be $\mathbf 1[\text{accepted proof}]$, the policy choose the specification $s$ as well as the program and proof, and let the prover's acceptance probability for the specification \texttt{True} be $a_{\mathtt{True}}$ (a proof is \texttt{trivial}). Then \texttt{True} maximises the expected reward over specifications whenever $a_{\mathtt{True}}\ge a(s)$ for all $s$; in particular when $a_{\mathtt{True}}=1$.
\end{proposition}
\emph{Proof.} Expected reward for spec $s$ is $a(s)\le1$; for $s=\mathtt{True}$ it is $a_{\mathtt{True}}$. $\square$\\
(The point is that the semantic ordering $s\Rightarrow s'$ gives \emph{program}-level monotonicity ($f\models s\Rightarrow f\models s'$) but not monotonicity of a learned prover's success; the proposition therefore rests on \texttt{True} being trivially provable, which is an assumption we state, not a consequence of the lattice.)\\
This is the formal reason that reward for ``verified'' must be tied to a \emph{fixed} statement (the strict bridge), or to a spec the model must prove equivalent to a held-out one (CLEVER), or to tests that bound $\hat Q$ from both sides (VERINA).

\section{Boxed result}
\begin{result}
\textbf{R1.} $\hat Q$ complete $\iff$ true on all positives; sound $\iff$ false on all negatives; relation-level soundness $\Rightarrow$ program-level, converse if $\hat Q$ is total on $P$ (unrealisable specs break it).\\
\textbf{R2.} A defect with witness fraction $\kappa$ survives $m$ uniform tests with probability $(1-\kappa)^m$; $\kappa=0$ is an equivalent mutant.\\
\textbf{R3.} $\Pr[\text{wrong}\mid\text{accepted}]=u r/(u r+1-u)$, $r=a_w/a_c\ge1$.\\
\textbf{R4.} With a policy-chosen spec the reward optimum is the weakest spec. Statement-integrity gates form a \emph{partial} order, not a chain: compile-only and swap are incomparable (C1 passes only swap, C3 only compile-only); defeq (bridge) is stricter than both on these candidates; strict (tokens $+$ bridge $+$ axioms) is stricter than defeq.
\end{result}

\paragraph{Numerical verification (notebook 0305, all cells executed).}
\begin{center}\small\begin{tabular}{@{}P{8.2cm}P{4.1cm}P{3.2cm}@{}}\toprule
Identity & result & error\\\midrule
R1: definition vs test-based verdict, 8 candidates $\times$ 1600 pairs & 8/8 identical & 0\\
R2: kill probability $1-(1-\kappa)^{10}$, 10 mutants $\times$ 20,000 suites & worst $|z|=1.84$ & $\le1.8$ s.e.\\
R2: equivalent mutants detected as $\kappa=0$ & 2 of 10 & 0\\
R3: Bayes formula, 7 settings $\times$ 200,000 draws & worst $|z|=1.72$ & $\le1.7$ s.e.\\
(a) Lean: \texttt{badSort} passes weak spec; fails perm & axioms $\emptyset$ / $\{\texttt{propext}\}$ & ---\\
(c) vacuity probe: Lean \texttt{decide} vs Python & \texttt{false}/\texttt{true} both agree & 0\\
(d) four gates $\times$ five candidates (real \texttt{StrictVerifier}) & table above, as predicted 20/20; accepted sets compile $\{$C0,C2,C3,C4$\}$, swap $\{$C0,C1,C2,C4$\}$, defeq $\{$C0,C4$\}$, strict $\{$C0$\}$ & incomparable pair asserted\\\bottomrule\end{tabular}\end{center}

\section{What breaks}
\begin{center}\small\begin{tabular}{@{}P{3.5cm}P{6.4cm}P{5.5cm}@{}}\toprule
Failure & Mechanism & Assumption violated\\\midrule
Tests as proof & a passing suite gives only ``might hold''; defects with small $\kappa$ need many tests & the suite covers the defect region (VERINA's suites reach 100\% code coverage of the ground truth, not of $\hat Q$)\\
Equivalent mutants & unkillable, inflate the denominator of a mutation score & mutants are non-equivalent (check $\kappa>0$ exhaustively where possible)\\
Tests derived from the same model & an LLM that writes spec \emph{and} tests shares the misconception & independence of spec and tests\\
Bounded scope & exhaustive checks only cover the scope & small-scope hypothesis (0304)\\
Judge LLM audits & recall-oriented semantic audits are noisy: the paper's LLM-assisted semantic audit has precision $0.30$ and recall $0.82$ for Claude Sonnet~4.5 with thinking (\cite{faults26}, Table~6; GPT-5.2 with thinking: $0.24$/$0.91$) & the auditor is calibrated\\
Spec leakage & S5-like specs are correct but make the proof trivial and prove nothing about reasoning & the spec is not the implementation\\
Harness trust & swap harness and compile-only gate credit different theorems (table (d)) & the proved statement equals the reference\\
Formal $\ne$ informal & even with a perfect bridge, the \emph{reference} may mis-state the problem: over half of the 488 miniF2F statements have a formal/informal mismatch, 16 are unprovable \cite{minif2frev} & the reference statement is faithful\\\bottomrule\end{tabular}\end{center}

\nextnote{0306 surveys the benchmarks that operationalise all of this (VERINA, CLEVER, FVAPPS, DafnyBench, miniCodeProps): what each measures, how it validates its specs, and how their numbers should (and should not) be compared.}

\begin{small}
\begin{thebibliography}{99}
\bibitem{verina} Z.~Ye et al., \emph{VERINA}, arXiv:2505.23135: abstract (72.6\% code, 52.3\% spec soundness+completeness, 4.9\% proof); \S3.2 (``Preventing trivial code generation''); \S4.1 (definitions, Fig.~3 evaluator); \S4.2 (proof of the \emph{ground-truth} spec prevents definitionally equivalent code/spec); Appendix~C.5 (Table~5); Appendix~E (Figs.~22--23, unsound/incomplete LLM postconditions).
\bibitem{clever} A.~Thakur et al., \emph{CLEVER}, arXiv:2505.13938: abstract; Fig.~1 (two QEDs: spec isomorphism then implementation); Fig.~2--3 and Appendix~A.1 (spec leakage, non-computable specs).
\bibitem{clover} C.~Sun et al., \emph{Clover: Closed-Loop Verifiable Code Generation}, arXiv:2310.17807, abstract (consistency checks among code, docstrings, annotations; 87\% acceptance, no false positives on adversarial instances).
\bibitem{minif2frev} M.~Ospanov, F.~Farnia, R.~Yousefzadeh, \emph{miniF2F-Lean Revisited}, arXiv:2511.03108 (formal/informal mismatches in over half of the 488 problems; 16 unprovable statements).
\bibitem{faults26} P.~S.~Ammanamanchi, S.~Bhat, S.~Biderman, \emph{Faults in Our Formal Benchmarking}, arXiv:2606.29493 (ICML 2026), abstract (4,833 findings; 398 mechanically certified: counterexamples, vacuous theorems, unsound axioms); Table~6 (semantic-audit precision/recall).
\bibitem{proofgate} ProofGate: a reproducible audit of faithfulness, alignment and vacuity in state-of-the-art Lean theorem provers (ICML 2026 AI-for-Math workshop poster, \texttt{icml.cc/virtual/2026/82433}); four-check audit incl.\ a negation-counterexample probe. Workshop poster, not arXiv; read via the vault note.
\bibitem{house} This repository: \texttt{align/docs/P2.md} \S8c item 18 (statement rewrite), \texttt{align/docs/LEAN\_VERIFIER.md} \S2 (strict tier, statement bridge) and \S6 item 3 (statement fidelity).
\end{thebibliography}
\end{small}
\end{document}