PaperlayerView exact revision on arXiv

Source-linked AI summary

Tacet: A Language and Type System for Automatic Statistical Validity Accounting

Chiké Abuah

arXiv:2608.27451v1cs.PLcs.SE

TL;DR

Empirical comparisons often lack checked statistical validity because p-values do not reveal what an analysis examined or how observations are arranged. Tacet makes those properties part of a typed analysis language that prices claims and refuses invalid or unaffordable tests. Its metatheory is machine-checked in Lean 4, with evaluations on published artifacts, while its guarantee remains limited to mFDRη and depends on declared modeling facts.

  • Problem

    Multiple-comparison procedures need selection history and observation structure, but these inputs are properties of the program and cannot be recovered from p-values alone.

  • Method

    Tacet combines footprint-tracking estimation, schema-derived design checking, declared bounds, and wealth-priced claims in a language that refuses improper or unaffordable inferences.

  • Results

    Tacet’s metatheory is machine-checked in Lean 4 with no admitted gaps and is evaluated through a reference implementation and published-artifact case studies.

  • Takeaways & Limitations

    Tacet makes pre-registration a typing rule and prevents outcome-selected samples or structurally mismatched mechanisms from receiving prices that assume otherwise.

  • Takeaways & Limitations

    The guarantee controls mFDRη, a ratio of expectations, and does not imply false discovery rate or family-wise error rate control.

Abstract

from arXiv · show

Empirical comparisons between systems are a standard form of evidence in computer science research, but few are checked for statistical validity: most are never framed as statistical tests at all. Existing multiple-comparison procedures could control the resulting error, but need inputs (what an analysis examined, and how its observations are arranged) that are not recoverable from a list of p-values. We introduce Tacet, a language in which an analysis declares what it generated, states what it expects to find, and is refused any claim it cannot afford or cannot properly test. Its core calculus T pairs a free estimation sublanguage, carrying a reported footprint and a purity bit that records whether any outcome was consulted in building a value, with a priced claim sublanguage, carrying a wealth transformer, connected only by a mechanism that prices a comparison. A sample selected by reading outcomes sets the purity bit and is recorded as having examined everything it read, permanently, so it can never be granted a one-sided or confirmatory price, without the system ever asking whether the analyst intended to cherry-pick. Whether a comparison is paired or clustered is computed statically from the artifact schema, from declared functional dependencies between key fields alone and before any data is read, and a mechanism that assumes that structure away is refused rather than priced. Because the wealth transformer is antitone in the realized p-value, affordability can be checked before the analysis runs too, turning pre-registration into a typing rule. We prove the metatheory machine-checked in Lean 4 with no admitted gaps, and demonstrate the approach on a reference implementation and two case studies on published artifacts, the SWE-bench Verified leaderboard and BIG-Bench Hard.

1. Introduction

Tacet addresses the weak statistical validity of empirical comparisons by recovering analysis properties that p-values alone cannot reveal. It introduces a language that refuses claims when they are unaffordable or improperly tested.

  • Motivation: Empirical comparisons are widely used, but statistical validity is rarely checked in published machine-learning and software-engineering research.Prior annotation studies found limited use and correctness of significance testing.
  • Motivation: Multiple-comparison procedures need to know what sample selection examined and how observations are arranged, properties invisible in results alone.These properties belong to the program that produced the reported numbers.
  • Research questions: Tacet asks whether selection history, experimental design, and affordability can be recovered or checked statically without relying on analyst intent.Its stated questions cover outcome-selected samples, paired or clustered designs, and pre-run affordability.
  • Contributions: Tacet introduces calculus T, combining footprint- and constraint-graded estimation with wealth-transformer-graded claims connected only through a pricing mechanism.The grades record what was read and what wealth remains affordable rather than ordinary numeric quantities.
  • Contributions: Outcome-based selection permanently records the outcomes read, preventing one-sided or confirmatory pricing without modeling whether cherry-picking was intentional.The system distinguishes selection syntactically rather than by inferring analyst motivation.
  • Contributions: The metatheory is machine-checked in Lean 4 with no admitted gaps, and the paper provides an implementation and evaluation on published artifacts.The evaluation includes a published leaderboard and benchmark corpus.

2. Tacet by Example

Tacet separates free description and comparison construction from priced inference, while runtime refusals distinguish unaffordable claims from claims using the wrong instrument. Because wealth depends on claim order, the same evidence can yield different supported findings.

  • Execution model: Tacet runs as a Python library with a runtime monitor enforcing budgets and a checker inspecting bounds and schemas before observation begins.The two components are related by Theorem 7.1 and expose refusals as ordinary Python exceptions.
  • Declarations: The running example declares generated artifacts and observation nesting, while observe folds each observation onto its artifact.This prevents multiple assertions behind one generated patch from becoming separately addressable trials.
  • Analysis stages: Descriptions and comparisons are free, but inference is priced; comparisons receive their statistical instrument from declared design information when claimed.A comparison becomes an inference only when converted into a claim.
  • Refusals: Wrong-instrument refusals are distinct from budget failures because no amount of wealth makes an unpaired test correct for paired data.The system refuses the comparison rather than charging it at an invalid instrument.
  • Order dependence: Order A supports both claims, whereas order B supports one, because alpha-investing refunds supported claims and charges failed ones.The evidence is unchanged; the cheaper claim can fund the more expensive claim only when encountered first.
  • Order dependence: Predictable ordering is fixed independently of p-values or effect sizes, using reading order and submission date in the case studies.The paper contrasts this with random ordering, which can reach several hundred supported claims versus zero under predictable orderings.

3. Background

The background motivates Tacet through multiple-comparison error, sequential wealth accounting, experimental-design validity, and pre-registration. These perspectives explain why p-values alone cannot determine either the correct instrument or the appropriate price.

  • Families of tests: A single valid p-value does not prevent false discoveries across many tests, and dependence changes which multiple-comparison guarantees apply.The leaderboard’s 8,911 comparisons are not independent, so their structure matters.
  • Multiple-comparison procedures: Offline corrections consume a completed batch, whereas sequential procedures spend wealth one test at a time without requiring the total number of tests in advance.Alpha-investing carries wealth between tests and rewards rejections.
  • Sequential procedures: Tacet uses a generalized alpha-investing rule that deducts the stake directly while retaining a guarantee on mFDRη rather than the false-discovery share or family-wise error rate.The rule differs from Foster and Stine’s original deduction but remains in the same sequential family.
  • Experimental design: Paired and clustered observations require instruments that respect their dependence, which Bonferroni and alpha-investing do not detect from p-values.Treating shared units or clusters as independent is a separate design error from multiplicity correction.
  • Pre-registration: Pre-registration fixes relevant comparisons before outcomes are observed, addressing data-dependent paths that can carry the multiplicity of alternatives not taken.Tacet uses declared bounds to make this discipline checkable.
  • Program structure: Two inputs required by these procedures—what the analysis read and how observations are arranged—are properties of the producing program, not recoverable from its numerical results.This is the central background premise for inspecting program structure.

4. Declarations in Tacet

Tacet requires analysts to declare modeling choices about units, schemas, and expected bounds while inferring footprints and design from program structure. These declarations determine the estimand, the statistical design, and whether affordability can be checked before execution.

  • Declared judgments: Tacet’s declared unit, schema, and bound are modeling judgments that the type system enforces but does not verify against the run.The guarantee is conditional on those declarations being honest and consistent with execution.
  • The artifact: An artifact is the output of one generation and is counted once, even when multiple outcomes derive from it.Choosing the artifact rather than an underlying component depends on the relevant failure mode.
  • The artifact: Folding observations onto artifacts changes the estimand rather than merely correcting an overlarge count, and the change need not be conservative.Two groups indistinguishable observation by observation can separate after folding.
  • Measured impact: Across 17 analyses, 11 had a naive-to-artifact count ratio of exactly 1.00, while 6 ranged from 2.53 to 9.00, affecting 35% of analyses.The affected analyses had several checks applied to one generated artifact.
  • The schema: The schema declares identifying keys, functional dependencies, and the independence level, allowing paired or clustered design to be decided statically.For example, declaring that an instance determines its repository supplies the dependency needed for the design check.
  • The bound: Declared bounds allow pre-run affordability checking because the wealth transformer is antitone in p-values and monotone in accumulated wealth.Analyses without bounds can still run under the runtime monitor.
  • Inference: Footprints and design are otherwise inferred from ordinary computation, selections, and the declared schema.The declarations constrain the analysis without requiring every derived property to be written explicitly.

5. The Core Language T

T separates free estimation from priced claims, using footprints, purity, schemas, and mechanisms to ensure analyses are properly selected and tested. Its design derives statistical instruments from artifact structure and refuses unsupported or degenerate comparisons.

  • Language structure: T consists of mutually embedded estimation and claim sublanguages, connected only through a mechanism that prices comparisons.Estimation tracks data dependence, while claims track budget effects through wealth transformers.
  • Design premise: Schemas declare artifact-key fields and functional dependencies, allowing paired or clustered design to be computed statically before data is read.The schema’s alignment key and nesting relationships determine the design premise without runtime inspection of values.
  • Language structure: Estimation carries a footprint and purity bit, while claims carry a wealth transformer for sequential budget accounting.The footprint reports what was read; the purity bit records whether outcomes were consulted.
  • Estimation: Outcome-based selection permanently sets purity to read and preserves the full footprint, preventing one-sided or registered pricing.Key selection narrows the footprint without changing purity, whereas outcome selection is conservatively treated as read even if its predicate ignores the outcome.
  • Design premise: T refuses degenerate or unsupported design premises instead of pricing them with an inappropriate instrument.A standard cluster-level alternative could serve clustered unpaired data, but it is not implemented in the described mechanism menu.
  • Design premise: When no mechanism is named, the design lattice derives cluster sign-flip, McNemar exact, or Fisher exact tests for supported designs.The fourth lattice point—clustered without pairing—is refused because the paired correspondence required by the sign-flip test is absent.

6. Wealth Transformers

Tacet represents claims as wealth transformers that compose in an ambient endofunction monoid, with runtime and static pricing governed by p-values, bounds, and wealth. The fixed_fraction rule yields order-dependent composition and a wealth ceiling, while the formal guarantees are scoped to that rule.

  • Transformer definition: Equation 6.1 defines a fixed_fraction transformer that deducts a fraction of wealth and refunds ω when p ≤ i · W.The transformer is Tp(W) = (1 − i) · W + ω · [p ≤ i · W].
  • Scope: The formal development and mechanized argument cover fixed_fraction only, not stake rules whose state depends on verdict history.The paper has not established the required monotonicity for any of the five implemented rules.
  • Transformer algebra: Wealth transformers compose as endofunctions, with associative composition and identity, while the set of individual Tp transformers is not itself a monoid.Tp is monotone in W and antitone in p: smaller p-values can only earn more refund.
  • Transformer algebra: The dynamic transformer is non-commutative, so claim order can materially change final wealth.At W = 0.0005, two claims produce 0.037625 in one order and 0.000125 in the reverse order.
  • Fixed point: At W ∗ = ω/i, an accepted claim returns wealth to the same fixed point, creating a ceiling for runs of accepted claims.With i = 0.5 and ω = α/2 = 0.025, the ceiling is W ∗ = 0.05; the stake there is always ω.
  • Static pricing: Without declared bounds, affordability remains a runtime property because a static checker cannot know whether a refund arrives.The no-refund static transformer is T⊥(W) = (1 − i) · W, which commutes but uses the worst case.
  • Static pricing: Declared p-value bounds restore static affordability because antitonicity makes pricing at the bound conservative.If a claim promises p ≤ p̄, its static price does not overstate the wealth available on an honest run.

7. Metatheory

Tacet’s metatheory connects static affordability and design checks with runtime statistical accounting, proving both mechanized soundness and the limits of its guarantees.

  • Static and runtime agreement: Theorem 7.1 proves that every statically certified claim is accepted by the runtime monitor when declared bounds are honest at run time.The result is per claim, so later claims can still be assessed after an earlier refusal.
  • mFDR control: The runtime guarantee controls mFDRη at α under the stated probabilistic hypotheses, with the wealth process defined and proved adapted in Lean.For every horizon t, mFDRη(t) = E[V(t)] / (E[R(t)] + η) ≤ α.
  • Assumptions and limits: The design premise remains an assumption: static checking is sound only when declared dependencies and identifying keys are genuine facts about the data.The weaker dependence condition accommodates paired and clustered designs, but the schema declarations are not discharged automatically.
  • Composing the two theorems: The composed theorem separates guarantees: honesty of declared bounds establishes feasibility, while error control holds without conditioning on the honesty event.A dishonest bound may invalidate affordability for a claim but cannot invalidate the mFDRη bound.
  • Mechanization and scope: The mechanized development reports no admitted gaps, while the theorem’s practical scope depends on its explicit hypotheses and recorded filtration.The proof uses an arbitrary probability space and Mathlib’s Bochner integral and conditional expectation.
  • Folding: Folding changes the estimand rather than merely weakening evidence, and can be anti-conservative in concrete configurations.Across 4,000 configurations, folded p-values were smaller 6.3% of the time; one moved from 0.044 to 0.0016.

8. Implementation

Tacet is embedded in Python as a runtime monitor plus a pre-execution checker that tracks what analyses read, enforces declared plans, and audits affordability and design.

  • Runtime tracking: The reference implementation separates a runtime monitor from a static front end, with tracked values propagating footprints through ordinary arithmetic and selections.The core implementation contains 1,994 non-blank, non-comment-only Python lines.
  • Footprints and purity: Outcome-based selection retains the full read footprint, while key-based selection records only the artifacts selected before outcomes are consulted.In the worked example, key selection narrows to six artifacts, whereas outcome selection keeps eight but retains a footprint of fifteen.
  • Threats and limits: The implementation remains vulnerable to untracked escapes and broader account-boundary threats, including a fresh Study that re-observes rows after earlier results were read.The shipped-code correspondence with the Lean development was tested on 599 random programs rather than proved.
  • Pre-registration: The observe boundary seals a plan before data access, making pre-registration a syntactic scoping rule rather than a claim about analyst intention.Declared claims must also occur in declared order and at most once.
  • Static audit: The static audit reads source without executing it, reconstructs literal straight-line plans, and reports affordability before observe runs.In the transcript, two of three claims are certified and the third is refused before data access.
  • Case study: The SWE-bench schema lets the static and runtime design checks agree on the declared paired or clustered comparison structure.The static half decides from declarations alone, while the runtime half checks the realized keys.

9. Evaluation

Tacet is evaluated on two published case studies, where its typed designs recover appropriate tests and its budget accounts for claims under predictable orderings. The results show that clustering and ordering materially affect support, while retrospective reconstructions limit what the case studies establish.

  • Evaluation: The case studies reconstruct claim families retrospectively from published outcomes, so they demonstrate recoverable inputs and informative prices rather than advance-declared validity.Both corpora were selected after outcomes were available, and H3 remains unverified.
  • Evaluation: SWE-bench Verified contains 134 submissions and 8,911 pairwise claims, with comparisons paired at the instance level and clustered when repository structure is respected.Tacet derives the design from declared keys and refuses an opaque cluster key rather than assuming independence.
  • Evaluation: BIG-Bench Hard is analyzed as 26 paired, task-level claims using McNemar’s exact test, with examples nested within tasks and a two-sided α = 0.05 price.The released outputs reproduce all 22 checkable table points to one decimal place and cover 26 of 27 released tasks.
  • Evaluation: Across BIG-Bench Hard, 19 of 26 claims are supported in alphabetical order, while chain-of-thought scores higher on 21 tasks and 21 tasks clear p < 0.05.Two tasks show the raw-score direction opposing the labeled claim, illustrating why two-sided rejection does not itself establish the claimed sign.
  • Evaluation: Clustering changes the pooled BIG-Bench Hard result from p = 1.76×10−192 at the example level to p = 8.37×10−6 at the task level, though both remain significant.The task-level result reflects 26 evidence units rather than 6,261 independent examples.
  • Evaluation: Order matters most for marginal effects: the leaderboard yields 0 supported claims in reading order versus a random median of 28, while strong effects make ordering nearly irrelevant.The budget can keep 19 of 26 BIG-Bench Hard claims in alphabetical order, but leaderboard order can exhaust wealth before later claims.
  • Evaluation: Against fixed corrections, Benjamini–Yekutieli keeps 2,038 of 8,911 leaderboard claims while Tacet keeps 0 under both predictable orderings; on BIG-Bench Hard, Tacet keeps 19 of 26, matching Benjamini–Hochberg.The comparison separates design correction from multiplicity correction: Bonferroni can endorse 6,467 comparisons when instances are incorrectly treated as independent.

10. Limitations and Threats to Validity

The paper’s guarantees and case studies have explicit scope boundaries: several assumptions remain external, the accounting is conditional, and some data-processing and inference settings are unsupported. The evaluation also does not measure predictive validity, false refusals, annotation burden, or non-author usability.

  • Guarantee scope: mFDRη is a ratio of expectations and implies neither false discovery rate nor family-wise error rate.On the running example, the budget supports no claims under both predictable orderings, while random ordering typically supports a median of 28 of 8,911 claims.
  • Guarantee scope: The guarantee is conditional on reporting every test and maintaining honest declared bounds, p-values, designs, and study boundaries.Undisclosed failed claims, fresh Studies, or dishonest declarations can invalidate the accounting assumptions.
  • Evaluation boundaries: Both case studies reconstruct claim families retrospectively, leave H3 unverified, and therefore do not certify that the guarantee held.Different family reconstructions produce different reported results, including the full 8,911-claim and adjacent-rank 133-claim leaderboard families.
  • Evaluation boundaries: The evaluation reports no predictive-validity test, false-refusal rate, annotation-burden measurement, or non-author analyst study.Consequently, it does not distinguish the leaderboard’s zero supported claims from possible checker over-strictness.
  • Implementation boundaries: The footprint cannot detect outcome-dependent filtering performed before observe, and one investment rule, fixed_fraction, is mechanized.Other shipped QUDE rules and arbitrary refund parameters remain outside the proved scope.
  • Data and inference boundaries: Folding outcomes onto artifacts can change the estimand, flatter concentrated failures, and treat partial pairing as full pairing conservatively but wastefully.Unmatched continuous comparisons have no mechanism, and outcome-selected samples retain only unconditional two-sided pricing rather than valid post-selection inference.

11. Related Work

Tacet relates to prior systems by combining design-derived mechanism selection, statistical-program verification, and sequential accounting. Its distinguishing interface recovers selection and observation structure from programs, then prices claims through a persistent balance.

  • Statistical procedures: Online FDR methods provide sequential investment rules, but still require correctly typed p-values as input.Tacet adds program-level recovery of observation arrangement and outcome consultation before pricing those p-values.
  • Interactive exploration: QUDE supports exploratory investment rules and order-gaming control, whereas Tacet tracks programs and declarations rather than user-interface interactions.Tacet does not attempt to improve QUDE’s five investment rules.
  • Design-driven selection: Tea and Tisane compile declared designs into valid instruments or models, while Tacet prices the resulting comparisons and carries wealth across claims.The systems can compose through the mechanism interface without requiring duplicate declarations.
  • Type systems: Tacet’s graded types track footprints and purity, borrowing machinery from graded and linear type systems without requiring linear-type reconstruction.Its footprint inference costs one annotation because propagation unions operand footprints.
  • Program verification: Belief Hoare Logic and StatWhy verify whether stated test assumptions hold, whereas Tacet computes paired and clustered structure from artifact keys.Tacet derives the design premise from declared dependencies instead of taking pairing as an analyst-written axiom.
  • Composition: Across these comparisons, Tacet answers how many instrument uses an analysis can afford, complementing systems that select or verify instruments.Its running balance also exposes exhaustion, a capability absent from systems that do not carry state between calls.

12. Conclusion

Tacet makes statistical validity inputs properties of typed programs rather than results alone. It tracks what outcomes were consulted, computes comparison structure before execution, and prices claims through declared plans and mechanisms.

  • Conclusion: Tacet requires analyses to declare generated artifacts, expected findings, and claims that they can afford and properly test.Its grammar includes observations, samples, estimations, mechanisms, claims, and plans.
  • Conclusion: A footprint records the observations supporting a value, while the purity bit distinguishes key-determined selections from outcome-consulting selections.Outcome-selected samples are permanently marked read and cannot receive one-sided or confirmatory pricing.
  • Conclusion: Paired and clustered comparisons are computed before execution from declared dependencies between artifact-key fields.The computation is sound given genuine declared dependencies and identifying keys, with runtime alignment checking providing an independent safeguard.
  • Conclusion: The claim sublanguage carries plans and mechanisms that connect declared bounds and sidedness to priced comparisons.Programs consist of a plan followed by claims, with mechanisms selected at claim time from declarations.

Appendix B. Soundness of the Footprint and the Purity Bit

Appendix B formalizes why footprints faithfully report the observations a value depends on and why clean selections depend only on artifact keys. The purity bit is conservative: outcome-based selection is always read, preventing laundering into confirmatory status.

  • Definitions: An estimation term denotes the observations selected from a run and combined into its value.observe produces folded observations; key filters use artifact keys; outcome predicates use folded outcomes; arithmetic unions footprints.
  • Footprint soundness: Footprint soundness proves that a typed value’s observations lie within its footprint and satisfy declared constraints.Membership depends only on artifact keys and an observation’s own outcome, so outside-footprint outcomes cannot change the value’s selected observations.
  • Purity soundness: Purity soundness proves that clean selections are functions of artifact keys alone, independent of outcomes.The proof follows the observe, key-selection, outcome-selection, and arithmetic typing rules.
  • Purity enforcement: Outcome selection always concludes read, so a value cannot launder an outcome-dependent selection into a clean type.Both one-sided and confirmatory claim rules require clean estimation premises.
  • Proof boundary: The appendix notes that footprint-reporting clause (c) remains on paper, while other soundness clauses are mechanized.The remaining clause is a two-run substitution property rather than a single-term structural recursion fact.
  • Purity enforcement: Shared constraints do not make outcome-selected samples confirmatory: the purity bit, rather than pins alone, separates the cases.A key-filtered sample followed by an outcome predicate retains its key constraint but becomes read.

Appendix E. Operational Semantics of the Runtime Monitor and the Checker

The runtime monitor prices claims using observed p-values, while the static checker prices declared bounds and tracks affordability separately from verdicts. Their shared wealth semantics support fixed_fraction without solvency premises, but several implementation identifications and the claim-level design checker have explicit scope limitations.

  • Operational configurations: Both systems operate over one shared wealth pool and differ only in whether the transformer receives a runtime p-value or a declared bound.The runtime price is supplied by an external oracle; the static checker uses declared bounds when available.
  • Verdicts and affordability: Runtime acceptance is the verdict b = [p ≤αj], whereas affordability failures occur when p > αj rather than when solvency fails.Support counts therefore measure claims accepted by the budget and p-value, not the static judgment Ok.
  • Wealth transitions: fixed_fraction deducts αj = iW directly and refunds ω on rejection, so reachable wealth remains nonnegative without a separate solvency premise.This contrasts with QUDE rules, whose superlinear loss deduction requires and enforces cost(αj) ≤W.
  • Static checking: A declared bound is checked using T̄p, and antitonicity in p makes an honest bound conservative because the real run can refund at least as often.Undeclared claims use the no-refund transformer, while declared bounds drive the static shadow trace.
  • Implementation boundary: The implementation identifies literal bound p̄ = 1 with an unbounded claim arithmetically, but bookkeeping still marks the literal-bound claim REFUSED.This identification is sound only under the stated invariant that wealth remains below 1/i; without it, the unbounded-ω gap remains open.
  • Mechanization scope: The mechanized checker does not mechanize the claim-level design premise; design, mechanism assumptions, and plan membership remain a routine finite-decision argument.The mechanized checker consumes claim-sequence normal form with price already treated as an oracle.

Appendix F. Proof of Theorem 7.1

Theorem 7.1 establishes that the static checker’s wealth trace never exceeds the runtime trace and that every statically certified claim is runtime-accepted under honest declared bounds. The result extends to programs mixing declared and undeclared claims, with certification applying only to affordable honest declarations.

  • Proof ingredients: The proof relies on monotonicity in wealth, antitonicity in p, and the no-refund transformer being a lower bound for every priced transformer.These three lemmas compare the static and runtime wealth steps.
  • Wealth invariant: Induction proves ˆWj ≤Wj for every step, regardless of preceding certified, refused, or undeclared claims.Notes leave wealth unchanged, while claims are handled by comparing the appropriate transformers.
  • Partial pre-registration: Undeclared claims require no honesty assumption for the wealth invariant because they use the no-refund transformer, but they receive no static verdict.Only declared claims are eligible for static certification.
  • Certification soundness: When a declared bound is certified, honesty gives pj ≤p̄j, and the wealth invariant then implies pj ≤iWj, exactly the runtime acceptance condition.The checker’s certification therefore entails acceptance by the runtime monitor for that claim.
  • Validation setup: The empirical theorem check uses 599 programs across two corpora, with 4,880 claims, comparing the static checker against the runtime monitor.The supplied corpus description identifies the fixed code-model comparison and the tuned wealth-trajectory corpus.

Appendix G. Empirical Validation of Theorem 7.1

Empirical validation tests whether static certification agrees with runtime monitoring across fixed and tuned corpora. Honest bounds produce zero violations, while the tuned corpus exercises certification across varied wealth trajectories and the experiment measures the cost of imprecise bounds.

  • Theorem validation: Zero honest-bound violations occur on both corpora, matching Theorem 7.1’s prediction.The tuned corpus makes this informative by certifying claims across multiple positions and wealth trajectories.
  • Corpus contrast: The fixed corpus certifies 18 claims, all at position 1, while higher-slack rows certify none and therefore hold vacuously.This corpus contains 1,911 claims over fixed paired code-model comparisons.
  • Cost of imprecision: Bound imprecision has corpus-dependent cost: the fixed corpus shows a cliff because threefold overstatement exceeds the smallest realized pairwise p-value threshold.Declaring within 1.5× costs nothing there, whereas threefold overstatement costs everything.

Appendix H. The Deletion Attack

The deletion attack studies an analyst who omits failed tests before reporting them under a complete null. Such deletion prevents wealth from decaying, keeps stakes from shrinking, and can drive mFDRη toward one; the crossing depends on the null p-value source.

  • Attack mechanism: Deleting non-rejections keeps wealth at least at w0, so every later test retains a stake of at least iw0.The honest analyst’s wealth instead decays geometrically while expected rejections saturate.
  • Attack outcome: Under a complete null, the deleting analyst’s mFDRη grows linearly with expected rejections and approaches 1.For perfectly uniform null p-values, the α = 0.05 crossing occurs at five tests.
  • Crossing analysis: Table 9 compares the crossing point against average rejection probability at the opening stake for four null p-value sources.Five tests is the closed-form floor, reached only under perfect uniformity.
  • Case-study comparison: BIG-Bench Hard lies near the uniform-p-value floor, whereas SWE-bench Verified crosses over a range because its shuffled outcomes retain instance-specific difficulty.The synthetic sweep is conservative because 20 tasks yield few discordant pairs for McNemar’s exact test.

Appendix J. Checker Runtime

The appendix characterizes checker and related mechanism costs, emphasizing that synthetic timings are orientation rather than a benchmark. It reports sub-second checking at 10,000 claims, while distinguishing checker costs from runtime-monitor and exact-p-value costs.

  • Measurement cautions: The synthetic sweep is orientation, not a benchmark, because between-invocation variance exceeds the in-process ranges.The 10,000-claim point had medians of 169, 173, and 176 ms across back-to-back runs.
  • Measurement cautions: The checker’s fold grows faster than linearly across claim counts, while parsing contributes roughly one-third to one-half of total time.The fold costs reported per decade are 0.62, 6.9, and 113 ms; the source leaves the super-linear term open.
  • Checker runtime: 10,000 claims complete in a fifth of a second on every measured invocation.The reported scale is comparable to the leaderboard’s 8,911-claim family and nearly four hundred times BIG-Bench Hard’s claim count.
  • Checker runtime: Literal-loop unrolling of 5,000 claims costs about 180 ms and grows somewhat faster than linearly.The stated loop-unrolling cap bounds this cost.
  • Mechanism cost: At BIG-Bench Hard’s pooled claim with k = 26 clusters, dynamic-programming convolution computes the cluster sign-flip exact p-value in under two milliseconds instead of nearly a minute by enumeration.This mechanism cost is separate from the checker’s own cost and dominates at scale.
Loading 2608.27451v1…