Reference. Finite discovery, replay, and audit [ftip-00IV]
✍️source

Finite sampling is treated in § [ftip-0076], deterministic replay in § [ftip-00HA], and audit conditions in § [ftip-00HK].

Related

Audit before commit and failure taxonomy [ftip-00HK]

Definition. An audit-before-commit record [ftip-00HL]

An audit-before-commit record is \(a=(d,scope,checks,reviewer,decision)\). It binds the durable execution record \(d\) to the audited scope, check list, review identity, and a decision in \(\{commit,hold,reject\}\).

Theorem. Audit-before-commit safety gate [ftip-00HM]

A commit decision is admissible only if every required check in an Definition [ftip-00HL] record is pass, the audited digest equals the proposed record digest, and the decision is \(commit\).

Proof.

Admissibility is defined as the conjunction of these three recorded conditions; failure of any conjunct yields hold or reject.

Definition. An independent audit scope [ftip-00HN]

An audit is independent for scope \(S\) when its inputs are frozen before review, its reviewer or checker is distinct from the proposing action, and its decision cannot rewrite \(S\) without a new record. Independence is a protocol condition, not a claim of infallibility.

Example. A latent failure caught before commit [ftip-00HO]

A run may pass unit tests while an independent audit finds that the evaluator version in \(d\) differs from the declared version. The audit holds the commit and records the mismatch; replay alone would not have caught it.

Definition. A reliability failure taxonomy [ftip-00HP]

Classify a failed run by its earliest violated contract: measurement failure (M), grading failure (G), execution/state failure (E), audit failure (A), or transfer failure (T). A single run may receive secondary labels, but the primary label is the earliest failed gate in recorded order.

Lemma. Earliest-failure labels are unique [ftip-00HQ]

For a finite ordered gate chain with at least one failed gate, the earliest failed index is unique and therefore determines one primary taxonomy label.

Proof.

Every nonempty finite subset of ordered indices has a unique least element.

Definition. A remediation record [ftip-00HR]

A remediation record maps a primary label from Definition [ftip-00HP] to an owner, corrective action, re-test scope, and closure condition. Closure requires a new durable record and cannot mutate the failed record in place.

Remark. Scope of audit methodology [ftip-00HS]

Parts III and V of [jarmak2026reliable] motivate durable execution, review, and accountability practices. The audit taxonomy and conjunction gates are proposed operational specifications; they do not establish that an audit is complete or that a committed artifact is correct.

Execution gates and durable state [ftip-00HA]

Definition. An execution gate [ftip-00HB]

An execution gate is a predicate \(g_i(e_i)\) over a recorded stage result \(e_i\). It names its owner, required inputs, pass/fail/unknown outputs, and the artifact versions to which the result applies.

Definition. An ordered gate chain [ftip-00HC]

An ordered gate chain is \((g_1,\ldots ,g_k)\) with stage outputs \(e_1,\ldots ,e_k\); gate \(g_i\) may execute only after its declared prerequisites and records a monotone status in \(\{pass,fail,unknown\}\).

Theorem. A failed gate blocks a release conjunction [ftip-00HD]

For a finite chain, define release status as \(G=\bigwedge _{i=1}^k g_i(e_i)\). If any gate is false, then \(G\) is false.

Proof.

This is the defining conjunction of finitely many Boolean gate predicates. It says nothing about whether a later gate would have passed.

Definition. A durable execution record [ftip-00HE]

A durable execution record is

\[d=(run,revision,environment,inputs,events,artifacts,checks)\]

It is append-only, versioned, and sufficient to locate each gate input and output without relying on worker-local memory.

Definition. A replay contract [ftip-00HF]

A replay contract for \(d\) fixes the executable revision, environment image, input artifact hashes, seed law, and event order. A replay is faithful only when those coordinates are available and the resulting events satisfy the recorded schema.

Theorem. Deterministic replay reproduces a recorded trace [ftip-00HG]

If the execution map is deterministic in the coordinates fixed by Definition [ftip-00HF], replaying the same inputs, revision, environment, and seed produces the same event trace.

Proof.

Induct over the finite event sequence. Equal initial coordinates give equal first events; determinism and equal prefixes give the next event.

Example. Replayability is not correctness [ftip-00HH]

A reproducible run can deterministically reproduce a wrong patch or a misconfigured evaluator. Replay establishes trace identity under its contract; it does not establish that the trace met the intended utility or safety goal.

Definition. A state-integrity digest [ftip-00HI]

For durable record \(d\), let \(H(d)\) be a cryptographic digest of its canonical serialized fields. A replay request fails closed when the supplied record digest or any referenced input hash differs from the declared value.

To bind a replay result to an audit decision, the replay trace must be included in the audited record and covered by its digest. A matching digest for other fields does not bind that trace to the decision.

Remark. Scope of execution methodology [ftip-00HJ]

Part III of [jarmak2026reliable] motivates containment, durable execution, and recovery records. Deterministic replay and matching digests establish execution consistency; they do not ensure correctness.

Finite discovery and support [ftip-0076]

A successful continuation can have positive probability and still be difficult to observe within a finite rollout budget. This subsection separates the probability of observing a success from support, coverage, and capability acquisition.

Convention. Repeated attempts and the discovery event [ftip-0077]

Fix a task instance, evaluator, success threshold, and a joint law for \(B\geq 1\) attempts. Let \(E_i\) be the event that attempt \(i\) succeeds. The discovery event by attempt \(B\) is

\[ D_B=\bigcup _{i=1}^{B}E_i. \]

Write \(p_i=\Pr (E_i)\). Independence is an additional property of the declared joint law; it is not implied by repeated decoding, a shared model, or a common environment. In the independent and identically distributed case, write \(p_i=p\). When the attempt law is the one fixed in Definition [ftip-005U], this \(p\) is the corresponding successful-support probability.

Theorem. Discovery under independent attempts [ftip-0078]

Assume the events \(E_1,\ldots ,E_B\) of Convention [ftip-0077] are independent. Then

\[ \Pr (D_B)=1-\prod _{i=1}^{B}(1-p_i). \]

In particular, independent attempts with a common success probability \(p\) satisfy

\[ \Pr (D_B)=1-(1-p)^B. \]

Proof.

The complement of discovery is \(D_B^{\mathsf c}=\bigcap _{i=1}^{B}E_i^{\mathsf c}\). Independence gives \(\Pr (D_B^{\mathsf c})=\prod _i\Pr (E_i^{\mathsf c}) =\prod _i(1-p_i)\). Taking complements proves the first identity; substituting \(p_i=p\) proves the specialization.

This finite statement follows from the displayed hypotheses. The calculation in Example [ftip-0067] is its ten-attempt numerical preview.

Corollary. A rollout budget for target discovery probability [ftip-0079]

This is a finite corollary of Theorem [ftip-0078], obtained from its displayed hypotheses.

Let \(0<\delta <1\). Under the independent and identically distributed setup of Theorem [ftip-0078], suppose first that \(0<p<1\). The least positive integer budget whose discovery failure probability is at most \(\delta \) is

\[ B_{\min } =\left \lceil \frac {\log \delta }{\log (1-p)}\right \rceil . \]

If \(p=0\), no finite positive budget reaches failure probability below one. If \(p=1\), one attempt suffices.

Proof.

For \(0<p<1\), Theorem [ftip-0078] gives failure probability \((1-p)^B\). The inequality \((1-p)^B\leq \delta \) is equivalent to \(B\geq \frac {\log \delta }{\log (1-p)}\) because both logarithms are negative. The least integer solution is the displayed ceiling. The two boundary cases follow directly from \((1-p)^B\).

Lemma. Discovery bounds from conditional success rates [ftip-007A]

Put \(D_0=\varnothing \). Whenever \(\Pr (D_{i-1}^{\mathsf c})>0\), define the surviving conditional success rate

\[ q_i=\Pr (E_i\mid D_{i-1}^{\mathsf c}). \]

If these rates are defined through step \(B\), then

\[ \Pr (D_B^{\mathsf c})=\prod _{i=1}^{B}(1-q_i). \]

Consequently, if \(0\leq \underline q\leq q_i\leq \overline q\leq 1\) for every surviving step, then

\[ 1-(1-\underline q)^B \leq \Pr (D_B) \leq 1-(1-\overline q)^B. \]

Proof.

The chain rule gives \(\Pr (D_i^{\mathsf c})=\Pr (D_{i-1}^{\mathsf c})(1-q_i)\). Iteration proves the product identity, and the coordinatewise bounds on \(1-q_i\) give the two discovery bounds.

No independence assumption is used. The conditional rates may change with the earlier failures, an adaptive decoder, or a changing environment state.

This finite statement follows from the displayed hypotheses.

Remark. Discovery is neither acquisition nor coverage [ftip-007B]

The discovery event concerns whether a declared sampling procedure observes at least one success. Increasing its probability can be an elicitation effect in the sense of Definition [ftip-0005]: more attempts expose behaviour that already had positive probability. It is not by itself the independent before--after comparison required by Definition [ftip-0007].

Successful-support coverage in Definition [ftip-005V] integrates an instance-level threshold over a task law. A large discovery probability on one instance therefore does not establish broad coverage or the uniform task-family witness of Definition [ftip-005X].

Theorem. Finite exponential tilting preserves support [ftip-007C]

Fix a prompt \(x\), a finite response set \(\mathcal Y\), a reference policy \(\pi _{\mathrm {ref}}\), a finite real reward \(r(x,y)\), and \(\beta >0\). Let \(\pi _r\) be the normalized exponential tilt of Definition [ftip-003O]. Then, for every \(y\in \mathcal Y\),

\[ \pi _r(y\mid x)>0 \quad \Longleftrightarrow \quad \pi _{\mathrm {ref}}(y\mid x)>0. \]

Proof.

The multiplier \(\exp (r(x,y)/\beta )\) is finite and strictly positive. The finite normalizer \(Z_r(x)\) is also strictly positive. Multiplication by the first quantity and division by the second therefore preserve whether the reference mass is zero or positive.

The source policy form appears as equation (4) in [rafailov2023direct, Section 4]; the displayed result is the finite corollary derived here. Infinite rewards, non-normalizable response spaces, approximate optimization, and changes to the generation mechanism lie outside the statement.

Remark. Formal support and operational discoverability [ftip-007D]

Support preservation is a statement about exact positive probability. A response can remain in mathematical support while its mass becomes too small to observe within the available rollout budget. The identities in Theorem [ftip-0078] and Corollary [ftip-0079] quantify this distinction for declared independent attempts.

Top-\(k\) truncation, nucleus sampling, finite numerical precision, context limits, and parser constraints can also remove an operational route even when the underlying softmax law assigns it positive mass. Claims about elicitation must therefore name both the policy law and the executable inference procedure.

Example. Counterexample: Equal one-shot success, unequal successful coverage [ftip-007E]

Let the evaluation law be uniform on two instances \(x_1,x_2\). Consider protocols \(P\) and \(P'\) with successful-support probabilities

\[ \bigl (p_P(x_1),p_P(x_2)\bigr ) =\left (\frac 12,\frac 12\right ), \qquad \bigl (p_{P'}(x_1),p_{P'}(x_2)\bigr ) =(1,0). \]

Both protocols have mean one-shot success \(1/2\). At threshold \(\alpha =1/2\), however, Definition [ftip-005V] gives

\[ \operatorname {Cov}_{1/2}(P)=1, \qquad \operatorname {Cov}_{1/2}(P')=\frac 12. \]

Thus average success does not determine successful-support coverage. The example is finite and uses the same task law and threshold for both protocols; it does not compare their training costs or establish acquisition.