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

Statistical validity in empirical system comparisons is rarely checked, while multiple-comparison procedures require design information unavailable from p-values alone. Tacet makes analyses declare their evidence and expectations, statically tracks outcome use and comparison structure, and rejects unaffordable or improperly tested claims. Its metatheory is machine-checked in Lean 4, with a reference implementation and case studies on published artifacts.

  • Problem

    Empirical comparisons are rarely checked for statistical validity, and results alone do not reveal the observation structure required by appropriate multiple-comparison procedures.

    Source: §1 · pp. 1–2

  • Method

    Tacet combines footprint and purity tracking with statically inferred comparison design and wealth-based claim pricing, rejecting claims that are unaffordable or improperly tested.

    Source: §1 · p. 3, §5.2 · p. 11, §12 · p. 47

  • Results

    Tacet proves its design computation sound and demonstrates the approach with a reference implementation and evaluations on published artifacts.

    Source: §1 · p. 3, §12 · p. 47

  • Takeaways & Limitations

    A type system can supply analysis and design information that multiple-comparison procedures need before results are observed, while refusing mechanisms that could silently misalign observations.

    Source: §5.4 · p. 16, §12 · p. 47

    Tacet controls mFDRη at α, which is a ratio of expectations and implies neither the false discovery rate nor the family-wise error rate.

    Source: §10 · p. 38

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 widespread lack of statistically valid empirical comparisons by recovering multiple-comparison inputs from programs and enforcing valid, affordable claims. Its language tracks outcome-dependent selection, infers experimental structure from schemas, checks affordability before execution, and provides machine-checked guarantees.

Motivation

  • Only 36 of 180 ACL/TACL papers used a correct significance test, while statistical testing in machine-translation papers never exceeded 65% and declined after 2016.These findings motivate treating statistical validity as a systems property rather than relying on published results or author intentions.Source: §1 · p. 1

Language and type system

  • The core calculus T separates free estimation, graded by footprints and constraints, from priced claims, graded by wealth transformers connected only through comparison-pricing mechanisms.The system answers whether program-derived inputs can support multiple-comparison control rather than trying to reconstruct them from p-values.Source: §1 · p. 2

Selection tracking

  • Tacet permanently records outcome-selected samples as examining their read observations, preventing pre-registration or one-sided and confirmatory prices without modeling analyst intent.Key-based selection remains eligible because its footprint depends only on artifact keys; outcome-based selection does not.Source: §1 · pp. 2–3

Experimental design

  • Tacet computes paired or clustered comparison structure statically from declared artifact-key dependencies, refusing mechanisms that assume away the inferred structure.Leaderboard comparisons are paired because systems attempt the same instances, and the schema exposes this fact before results are read.Source: §1 · pp. 2–3

Static affordability

  • Because wealth transformers are antitone in realized p-values, declared bounds make affordability checkable before execution, turning pre-registration into a typing rule.This directly addresses whether an analysis can be shown affordable before it runs.Source: §1 · pp. 2–3

Guarantees and evaluation

  • Lean 4 machine-checks Tacet’s metatheory without admitted gaps, including checker soundness, mFDRη control under stated conditions, and acceptance-implies-control without trusting declared-bound honesty.The paper also presents a reference implementation requiring artifact-key and cluster-level declarations and evaluates it on published artifacts.Source: §1 · p. 3

2. Tacet by Example

Tacet demonstrates how Python analyses declare generated artifacts and observation structure, while runtime monitoring prices claims and rejects unaffordable or structurally invalid inferences. The example shows that claim order affects discoveries even when evidence is unchanged, and that folding observations prevents unexpressible trial splitting at an estimand cost.

Running example

  • Tacet’s running example treats the SWE-bench Verified leaderboard [JYW+24] as 134 submissions whose resolved-instance sets induce 8,911 pairwise system-comparison claims.Analyses declare what was generated and how observations nest; passed only specifies how outcomes are read from rows.Source: §2 · p. 3

Observation structure

  • observe folds each observation onto its artifact, making assertions behind one generated patch unaddressable as separate trials, though folding changes the estimand and is not always conservative.The protection against post hoc trial splitting therefore has a substantive inferential cost.Source: §2 · p. 4

Pricing and refusals

  • Tacet separates free descriptions and comparisons from priced inference, with runtime refusals reporting the claim’s stake, remaining balance, and prior charged and retained claims.A Note cannot be used as a Stat, preserving an analyst-declared boundary between description and inference.Source: §2 · pp. 4–5

Instrument selection

  • Tacet computes the comparison instrument from declarations at observe, and refuses an explicitly requested unpaired Fisher exact test when the samples are paired.This is distinguished from budget failure: acceptable price cannot make an unpaired instrument correct for paired data.Source: §2 · pp. 4–5

Order dependence

  • Order A supports both claims, whereas order B supports only one because alpha-investing refunds supported claims but charges failures, making order affect available wealth despite unchanged evidence.A cheaper supported claim can fund a later expensive claim; encountering the expensive claim first halves the stake and forfeits that opportunity.Source: Figure 1 · p. 5, §2 · p. 5
  • At leaderboard scale, predictable ordering produces 0 supported claims, while a random ordering can reach up to several hundred.The case studies use ordering fixed independently of p-values or effect sizes, such as reading order or submission date.Source: §2 · pp. 5–6

3. Background

The background establishes why statistical validity depends on both multiplicity control and analysis-design facts unavailable from p-values alone. It contrasts offline corrections with online wealth-based procedures and motivates pre-registration and program-level recovery of selection and dependence.

Families of tests

  • Exact tests are super-uniform under their nulls, but testing k hypotheses can make at least one false rejection likely as k grows.For independent tests the bound is 1 − (1 − α)^k; at α = 0.05 and k = 8,911 it exceeds 0.999999, while arbitrary dependence gives bounds between α and min(1, kα).Source: §3 · p. 6

Classical procedures

  • Bonferroni and Benjamini–Hochberg are offline procedures requiring all k p-values, while ordinary Benjamini–Hochberg lacks its guarantee under arbitrary dependence.Benjamini–Yekutieli extends false-discovery-rate control to arbitrary dependence, but neither offline approach handles analysts who add tests after seeing results.Source: §3 · p. 6

Sequential procedures

  • Sequential alpha-investing carries stochastic wealth across tests, allowing the number of comparisons to remain unknown while controlling mFDRη through a wealth process.Tacet deducts the stake i · W directly and relies on generalized alpha-investing rather than Foster and Stine’s original deduction rule.Source: §3 · pp. 6–7

Experimental design

  • The data’s pairing and clustering determine which exact test is licensed, because incorrect independence assumptions can invalidate results even when the resulting p-value is numerically precise.The served tests are Fisher’s hypergeometric test [Fis35], McNemar’s marginal-homogeneity test, and the cluster sign-flip test [WRW+14], each with a distinct null and dependence assumption.Source: §3 · p. 7

Pre-registration

  • Pre-registration converts a declared bound into a checkable constraint before analysis, addressing data-dependent paths that carry multiplicity beyond the reported comparison.The motivation follows the garden of forking paths and adaptive data analysis [DFH+15].Source: §3 · p. 7

Selective inference

  • Selective inference treats outcome-based reporting as selection regardless of intent, so Tacet recovers the event from the selecting program and withholds one-sided and confirmatory prices.The p-value is not recomputed; the recovered selection event instead prevents prices that assume no selection occurred.Source: §3 · pp. 7–8

4. Declarations in Tacet

Tacet requires analysts to declare the artifact, schema, and optional bound because these modeling judgments cannot be recovered from data. The checker enforces consistency with those declarations while inferring remaining analysis structure.

Declarations and inference

  • All declarations are modeling judgments that analysis cannot recover, so Tacet guarantees only that execution remains consistent with honestly supplied units, schemas, and bounds.Footprints and design structure are otherwise inferred from ordinary arithmetic, schemas, and selections.Source: §4 · pp. 8–9

The artifact

  • The artifact declaration chooses the estimand by identifying one generation as the unit of analysis, rather than correcting an overcounted measurement.The appropriate unit depends on the claimed failure mode, which the data alone cannot determine; folding can separate observation-indistinguishable groups.Source: §4 · p. 8
  • 35% of analyses were affected by artifact folding, with naive-to-artifact count ratios of exactly 1.00 for 11 analyses and 2.53–9.00 for 6.Across 17 analyses in two corpora, no ratio fell between these modes; pass@k [CTJ+21] [AON+21] already encodes benchmark-specific units in its harness.Source: §4 · p. 8

The schema

  • The schema declares identifying and functional-dependency fields, allowing Tacet to determine statically whether comparisons are paired or clustered.Omitting the relevant schema declaration costs a factor of 48 on the leaderboard.Source: §4 · p. 8

The bound

  • A declared bound enables pre-run affordability checking because the wealth transformer is antitone in p-values and monotone in accumulated wealth.Without a bound, the analysis still runs under a runtime monitor; with one, the declaration under-approximates wealth from an honest execution.Source: §4 · p. 9

5. The Core Language T

T separates free estimation from priced claims, connecting them only through mechanisms that convert outcome-independent estimates into affordable statistical claims. Its schema-indexed design premise statically determines valid comparison structure and refuses claims when the instrument or key structure cannot be justified.

5. The Core Language T

  • T embeds a free estimation language tracking data provenance and a priced claim language tracking wealth, with mechanisms as their only interface.Estimation carries the data a value rests on, while claims carry budget effects; no claim term crosses back into estimation.Source: §5 · p. 9

5.1. Schemas.

  • Schemas declare key fields, identifying fields, functional dependencies, and cluster level so comparison design can be computed statically before data is read.Schema indices prevent cross-schema combinations and bind the design premise to the schema declared at observe.Source: §5.1 · p. 10

5.2. Estimation.

  • Outcome-dependent selection permanently sets purity to read and preserves the full footprint, preventing later one-sided or confirmatory pricing from treating the value as preregistered.Key selection narrows footprints without changing purity, whereas outcome selection is conservatively classified as read even if its predicate ignores the outcome.Source: §5.1 · p. 10, §5.2 · p. 11

5.3. Claims.

  • Claims compose sequentially through wealth transformers, whose non-commutative function composition models data-dependent refunds rather than scalar additive costs.T-Claim accepts two-sided mechanisms, while clean purity is required by the rules that cash in preregistration or one-sided pricing.Source: §5.1 · p. 10, §5.3 · pp. 12–13

5.4. The Design Premise.

  • The design premise matches mechanisms to paired, clustered, or independent structure from schema constraints, refuses opaque or unsupported designs, and rejects pairing assumptions without correspondence.Fisher’s exact test serves independent data, McNemar’s exact test paired data, and the cluster sign-flip test paired clustered data; the clustered-without-pairing point is refused because its required correspondence is absent.Source: §5.4 · pp. 15–16

6. Wealth Transformers

Wealth transformers price claims by updating a current pool according to investment, refund, and realized p-values. The fixed-fraction rule supports static affordability through conservative declared bounds, but its formal guarantees do not extend to history-dependent staking rules.

Claim transformers

  • Tp(W) = (1 − i) · W + ω · [p ≤ i · W] updates wealth by staking fraction i and refunding ω when p ≤ iW.Transformers compose as endofunctions; Tp is monotone in W and antitone in p.Source: §6 · pp. 16–17

Scope and limitation

  • Equation 6.1 applies only to fixed_fraction, while history-dependent staking rules lack the established monotone-in-state invariant and are not covered by the formal guarantees.The implementation includes five rules, but the equations, appendices, and mechanization address fixed_fraction only.Source: §6 · p. 17

Ceiling behavior

  • At W* = ω/i, accepted claims preserve wealth, creating a ceiling whose stake is always ω and explaining strongest-first invariance under the tested i-sweep.With i = 0.5 and ω = 0.025, the ceiling is W* = 0.05.Source: §6 · pp. 16–17

Parameter choices

  • The defaults ω = w0 = α/2 are more conservative than permitted maxima, and a single claim opens at α/4 under the shipped settings.Raising ω toward α would let two BIG-Bench Hard tasks clear the larger stake, showing the reported accounting tax depends on the default.Source: §6 · pp. 17–18

Static pricing

  • Declared p-value bounds enable conservative static pricing, moving affordability checks from runtime execution to type-checking.Because T is antitone in p, pricing a promise p ≤ p̄ cannot overstate the real wealth.Source: §6 · p. 18

7. Metatheory

The metatheory establishes static checker soundness, mFDR control, and their unconditional composition under explicit assumptions, with mechanization in Lean 4. It also characterizes trust boundaries and shows that folding can change Fisher p-values by changing the estimand, while remaining sound only relative to the declared dependence structure and unit of analysis.

7. Metatheory

  • Theorem 7.1 establishes per-claim static under-approximation: with honest bounds and 0 < i ≤1, ω ≥0, every checker-certified claim is monitor-accepted.The invariant holds through certified, refused, and undeclared claims, enabling validation after earlier refusals have drained the shadow pool.Source: §7 · pp. 18–19
  • Empirical validation covered 599 programs and 4,880 claims: honest bounds never produced checker acceptance when the monitor refused, whereas dishonest bounds broke the implication.The experiments also found cliff-like costs for overstated bounds at low data resolution and slope-like costs when resolution was ample.Source: §7 · p. 19
  • Design-premise soundness shows schema-and-constraint design cannot license a silently misaligned paired or clustered mechanism when the run conforms to its declared dependencies and key.The theorem is one-directional: cross-side meaning of identifying fields, omitted dependencies, and genuine schema declarations remain trusted, while runtime alignment refuses non-injective keys.Source: §7 · pp. 20–21

7.1. mFDR Control.

  • Theorem 7.4 proves mFDRη(t) = E[V(t)] / (E[R(t)] + η) ≤ α for every horizon under complete accounting, within-claim validity, conditional super-uniformity, and bounded refunds.The guarantee relies on the recorded filtration and remains an assumption for heavily dependent case-study p-value sequences; schema declarations relocate, but do not discharge, dependence assumptions.Source: §7.1 · pp. 22–23

7.2. Composing the Two Theorems.

  • Checker acceptance implies unconditional mFDRη control, while honest declared bounds additionally ensure every claim is accepted by the runtime monitor.Honesty affects feasibility, not error control: the monitor prices every claim, including those with dishonest bounds, and refuses unaffordable claims.Source: §7.2 · p. 23

7.3. The Mechanization.

  • The Lean 4 development machine-checks the accounting theorems, design premise, estimation lemmas, and measure-theoretic supermartingale without admitted gaps or `sorry` statements.The mechanization uses arbitrary probability spaces, filtrations, conditional expectations, and a pathwise identification with the runtime monitor’s fold; one two-run substitution lemma remains unmechanized.Source: §7.3 · pp. 24–25

7.4. Non-Conservativity of Folding.

  • The folding conservativity claim is false: the paper introduces two groups of 25 artifacts with four observations each, equal failure totals, and different failure distributions.The supplied passage identifies the counterexample setup and Table 1, but does not provide the resulting test statistics here.Source: §7.4 · p. 25, Table 1 · p. 25
  • Folding was conservative in 86.9% of 4,000 configurations but anti-conservative in 6.3%, moving one p-value from 0.044 to 0.0016 and crossing the threshold in 11 configurations.The sharpest threshold crossing moved 0.31 to 0.038.Source: §7.4 · p. 25
  • Folding changes the estimand from the fraction of observations passing to the fraction of artifacts passing completely, so it can treat groups with dispersed failures differently.The all-or-nothing reduction makes the folded quantity the one named by the declaration, not the raw observation-level quantity.Source: §7.4 · p. 25
  • Theorem 7.6 proves folding is sound relative to its declaration: under the declared paired, clustered, or independent dependence pattern, valid mechanisms produce valid p-values for the folded estimand.Deterministic folding cannot create dependence between disjoint independent raw observations and may weaken declared dependence without harming validity.Source: §7.4 · pp. 25–26
  • The guarantee certifies only that the declared question was answered at the stated budget; it cannot correct a p-value computed at the wrong unit of analysis.Choosing the unit chooses the question, so the analyst must supply the antecedent needed for the guarantee.Source: §7.4 · p. 26

8. Implementation

Tacet’s reference implementation realizes footprint and purity tracking, pre-registration, and static affordability/design audits in dependency-free Python, while exposing limits of its honest-but-fallible threat model. The implementation’s static checker can refuse unaffordable claims before data access, but excludes dynamic plans and cannot replace external account-boundary records.

Implementation

  • Tacet’s core comprises 1,994 dependency-free Python lines, with runtime monitoring and static analysis implementing observation, footprint propagation, selection, mechanisms, and p-value spending.The optional investment rules add 186 lines outside the certified perimeter.Source: §8 · p. 26

Threat model

  • The implementation’s trusted base includes Tacet, Python, and an unproved correspondence to Lean tested on 599 random programs, under an honest-but-fallible analyst threat model.Analysts can directly mutate wealth or escape tracking, so the shipped monitor does not defend against deliberate defeat of accounting.Source: §8 · pp. 26–27

Value-level footprint tracking

  • Footprints union artifacts through arithmetic, count repeated artifacts once, and distinguish key-based narrowing from outcome-based selection that reads every candidate artifact.Sensitivity bounds multiply separately, and squaring a tracked value can send the numeric grade to infinity [ASDN21].Source: §8 · p. 27

Pre-registration as a scoping rule

  • Pre-registration seals plans at observe, fixes claim order and uniqueness, and permits one-sided prices and data-free affordability checks from declared bounds.The registration stores labels, optional bounds, sidedness, and key literals without references to observed data; skipped declarations remain recorded.Source: §8 · pp. 27–28

The static audit

  • Two of three claims are certified and the third refused before observe runs, while six leaderboard comparisons are all refused without reading data.The static checker reads source without execution, exits nonzero on refusals, and reproduces the runtime refusal for the six leaderboard comparisons.Source: §8 · p. 29

Limits

  • Static auditing excludes nonliteral, branch-dependent, or runtime-generated plans, while later Studies can re-observe data and unplanned claims can invalidate runtime certification despite honest declared bounds.A violated bound still charges the real p-value; the certificate applies only when priced claims follow the plan’s order, with permitted skips and no premature exploratory claims.Source: §8 · p. 30

9. Evaluation

Evaluation shows that Tacet refuses each targeted misuse, recovers statistically necessary structure from real artifacts, and preserves many strong claims while exposing failures caused by dependence, ordering, and retrospective reconstruction. A synthetic pre-registered run satisfies every theorem hypothesis and demonstrates that accepted analyses inherit the promised guarantee.

9. Evaluation

  • The real case studies recover typed designs and informative prices but are retrospective reconstructions with unverified (H3), so they do not certify the theorem’s guarantee.The certified guarantee is demonstrated only on synthetic data constructed to satisfy the hypotheses.Source: §9 · p. 30, §9.5 · p. 37

9.1. Refusal Case Studies.

  • The refusal suite triggered five minimal defects, including missing cluster structure, an unplanned one-sided test, late registration, reordered claims, and outcome-selected sampling.Each refusal had an accepting twin, but the suite tested intended refusals rather than false-refusal frequency; the library and calculus enforce equivalent judgments at different points.Source: §9.1 · pp. 31–33

9.2. Case Study: the SWE-bench Verified Leaderboard.

  • On SWE-bench Verified, cluster-level analysis supported no claims and bankrupted by the sixth claim, whereas instance-level analysis supported 5,518 claims and changed adjacent-rank p-values by up to 48×.The cluster-level family had 8,911 claims across 12 repositories and a sharpest possible p-value of 0.000488; Tables 2 and 3 report both resolutions.Source: §9.2 · p. 33

9.3. Case Study: BIG-Bench Hard.

  • On BIG-Bench Hard, the budget supported 19 of 26 claims, while chain-of-thought scored higher on 21 tasks and 21 tasks cleared p < 0.05.The result is based on 26 tasks and 6,261 examples; two significant outcomes favored direct prompting, illustrating that two-sided rejection does not encode direction.Source: §9.3 · p. 34

9.4. Comparing the Two Case Studies.

  • Across the two corpora, ordering dominated marginal effects but was nearly irrelevant for strong effects: leaderboard reading order kept 0 claims, versus a random-draw median of 28.The random maximum was 302, still below the strongest-first ceiling of 6,545, and shuffling can improve covered orderings when fixed independently of evidence.Source: §9.4 · p. 35, Table 2 · p. 35
  • On dependent leaderboard comparisons, Benjamini–Yekutieli kept 2,038 of 8,911 claims while Tacet matched Holm and Bonferroni at 0; on BIG-Bench Hard, Tacet matched Benjamini–Hochberg at 19 of 26.Fixed corrections did not detect the design error: Bonferroni still endorsed 6,467 of 8,911 comparisons when instances were treated as independent.Source: §9.4 · p. 35, Table 3 · p. 36
  • Synthetic validation showed that design correctness, rather than the correction layered on top, determined whether error-rate measurements were meaningful: cluster-level Benjamini–Hochberg, Bonferroni, and Tacet held under the complete null.At instance level, every procedure exceeded its own α because the declared independence hypothesis was violated; at skill gap 2, Benjamini–Hochberg had mFDRη 0.0130 and FWER 0.1110.Source: §9.4 · p. 36, Table 4 · p. 37

9.5. A Certified Run.

  • Both declared synthetic claims were affordable before data existed and were kept, while the genuine null was correctly refused, establishing a checker-accepted run under all Theorem 7.4 hypotheses.The claims had p = 0.00012 and p = 0.00244 against bounds of 0.01, while “A beats B” had p = 0.9048; the audit reported stakes 0.0125 and 0.0188 before observe.Source: §9.5 · pp. 37–38

10. Limitations and Threats to Validity

The guarantee is conditional and narrower than false-discovery or family-wise control, with major unverified assumptions about complete reporting, study boundaries, dependence, and declared inputs. The implementation also leaves important validity, usability, scope, and budget-allocation questions open.

Guarantee scope

  • mFDRη controls a ratio of expected false discoveries, not the false-discovery rate, family-wise error rate, or the raw share of false discoveries.In a 4,000-trial equal-skill simulation, every discovery was false while the raw false share was 1.00 and mFDRη was 0.0031; the static guarantee currently covers fixed_fraction only.Source: §10 · p. 38

Completeness and account boundaries

  • The guarantee assumes every test and Study is reported, but omitted failed claims or repeatedly opened Studies can reset accounting and evade detection.For analysts who never pay for failures, mFDRη approaches 1, crossing α after 5 uniform-null tests and after 4–15 corpus-based nulls; external timestamped records are required.Source: §10 · pp. 39–40

Modeling and declaration threats

  • Validity depends on modeling choices and honest declarations: claim-family reconstruction, bounds, p-values, dependence ordering, clusters, and directional labels are not fully checked.Pre-observe filtering is invisible; post-selection samples cannot receive one-sided or confirmatory prices; retries can expose realized p-values; opaque keys, undeclared nesting, and partial pairing remain conservative or unverified.Source: §10 · pp. 40–41

Evaluation gaps

  • The evaluation demonstrates implementation behavior but does not measure false refusals, annotation burden, independent analysts, non-author codebases, or predictive validity.The five refusals establish specification matching only, while the paper does not test whether supported comparisons replicate more often than refused ones.Source: §10 · p. 40

Mechanism and data limitations

  • Scope remains limited to fixed_fraction, bounded refund settings, binary or paired continuous comparisons, and folded outcomes that can favor concentrated failures.Unmatched continuous comparisons are unsupported, arbitrary ω is unproved, and partial pairing is treated as full pairing on the intersection, conservatively but wastefully.Source: §10 · pp. 40–41

Budget allocation

  • Per-footprint budgets are unsound at scale: under a complete null, mFDRη reached 0.056 at 10 pools and 0.40 at 100, whereas one pooled budget held.The failure arises because each pool receives its own mFDRη cushion; accounting is incremental and reports exhaustion, but these properties do not strengthen the guarantee.Source: §10 · pp. 39, 41

11. Related Work

Tacet extends statistical validity accounting by recovering program-level inputs that existing procedures require, while complementing meta-science, exploration, design-declaration, verification, and graded-type-system research. Compared with Tea, Tisane, and Belief Hoare Logic, Tacet adds persistent session accounting, provenance-sensitive pricing, and pre-data static checks, while remaining composable with systems that select or verify individual mechanisms.

11. Related Work

  • Existing statistical procedures control multiplicity but assume correctly typed p-values; Tacet instead recovers observation structure and read provenance before pricing comparisons.Online FDR methods [RZWJ18], dependent procedures [ZRJ21, WR22], and classical references address control rules, while Tacet supplies inputs those rules cannot recover from p-values alone.Source: §11 · p. 42
  • Meta-science shows widespread ignored or misapplied significance testing, while Tacet prices the specific analytic path taken rather than enumerating unexecuted alternatives.Annotation studies [MFR21], statcheck, and replicability analysis [DBBR17] establish the problem; multiverse and specification-curve analyses address a different question.Source: §11 · pp. 42–43
  • QUDE prices exploratory sessions but assumes independence, whereas Tacet derives dependence structure from artifact keys and records outcome-driven narrowing through program-visible provenance.QUDE’s five exploration investment rules are not improved upon; Tacet addresses its stated inability to recover structural facts such as shared repositories.Source: §11 · p. 43, §11.1 · p. 45

11.1. Comparison with Tea and Tisane.

  • Tea and Tisane derive valid instruments from declared designs, but neither carries state across calls, records upstream provenance, or accounts for a persistent family of claims.Tea corrects only comparisons within one call, while Tisane scopes one model to one design; Tacet adds footprint tracking, composition, and a running balance.Source: §11.1 · pp. 44–45
  • Tacet complements Tea and Tisane: their design front ends can select mechanisms, while Tacet prices results and carries the balance across claims.The shared interface is spend(label, p-value, footprint), but neither half alone prevents the full family-wise error of Section 9.2’s leaderboard.Source: §11.1 · p. 46

11.2. Comparison with Belief Hoare Logic and StatWhy.

  • Belief Hoare Logic and StatWhy verify assumptions and corrections for explicitly specified tests, but cannot express a sequential family whose future members are not yet specified.Their verified Bonferroni reasoning fixes k in the specification; Tacet instead accounts for sequential claims, with the weaker mFDRη guarantee described in Section 10.Source: §11.2 · p. 46
  • BHL takes pairedness and prior direction as asserted beliefs, whereas Tacet computes structure from artifact keys and makes preregistration syntactic before observe.StatWhy uses a solver and one specification per test; Tacet uses two declarations and a fold, trading expressiveness for automation and lower analyst burden.Source: §11.2 · pp. 46–47

12. Conclusion · Appendix A. Syntax of T

Tacet supplies program-level information that multiple-comparison procedures cannot recover from p-values, refusing claims that are unaffordable or improperly tested. Appendix A specifies T’s syntax for samples, estimations, claims, plans, and programs.

12. Conclusion

  • Tacet makes analyses declare generated artifacts and expected findings, while refusing claims they cannot afford or properly test.Its wealth accounting descends from alpha-investing, while the type system supplies program properties needed by multiple-comparison procedures.Source: §12 · p. 47
  • Whether a narrowing predicate consulted outcomes is syntactic, so outcome-dependent selection cannot receive an unjustified confirmatory treatment.This property is determined from the program rather than reconstructed from reported p-values.Source: §12 · p. 47
  • Whether comparisons are paired or clustered is computed before execution from declared dependencies between key fields, with soundness proved under genuine dependency and key assumptions.The type system cannot verify those assumptions, so runtime alignment checks catch violations independently.Source: §12 · p. 47

Appendix A. Syntax of T

  • Appendix A defines T’s metavariables for runs, artifact keys, outcome predicates, claim labels, mechanisms, bounds, plans, sidedness, constraints, and operators.The sample sort restricts selection to per-observation structures, preventing selection over arithmetic combinations without remaining observation-level structure.Source: Appendix A · p. 52
  • The grammar defines samples as observations followed by key or predicate selection, estimations as samples or arithmetic combinations, and claims as notes, mechanisms, or sequences.This separates the sample, estimation, and claim constructs used by T.Source: Appendix A · p. 52
  • Plans associate claim labels with declared bounds, sidedness, and constraints, while programs combine a plan with a claim command.The syntax includes an empty plan and sequential plan extension.Source: Appendix A · p. 52
  • Appendix E associates programs with the normal form c1 ; . . . ; cn, and Appendix D supplies the typing rules that extend plans.These appendices connect the grammar to sequential execution and plan typing.Source: Appendix A · p. 52

Appendix B. Soundness of the Footprint and the Purity Bit · Appendix C. Design-Premise Details · Appendix D. Typing Rules for Pre-registration

The appendices establish that Tacet’s footprint and purity tracking are semantically sound, clarify design-premise computation, and formalize pre-registration constraints that prevent invalid confirmatory claims. They also expose implementation boundaries, including order, omission, repetition, and incomplete-account conditions that typing alone cannot enforce.

Appendix B. Soundness of the Footprint and the Purity Bit

  • Tacet proves that typed estimation terms report only the artifact keys they depend on, preserve declared constraints, and remain unaffected by outcomes outside their footprint.Footprint soundness is established by induction over the typing derivation; its key and constraint clauses are mechanized in Lean 4, while the substitution clause remains on paper.Source: Appendix B · pp. 53–54
  • Clean selections depend only on artifact keys, so outcome-dependent selection cannot be laundered into a clean type and cannot support one-sided or confirmatory pricing.T-SelectOutcome always produces read, whereas clean terms are noninterfering with respect to outcomes; clean values may still compute statistics over outcomes after selection.Source: Appendix B · pp. 53–54

Appendix C. Design-Premise Details

  • Design computation closes dependencies from parent to child, and its single-field restriction is a simplification because the downstream system consumes only the resulting distinguishing-field set.Reversing the closure direction incorrectly makes cross-mode comparisons appear paired; the case studies use dependencies such as instance determining repository and task determining mode.Source: Appendix C · p. 54
  • p = 0.0078 instead of p = 1.0 on the same no-signal dataset shows that serving the refused clustered-without-pairing case makes results depend solely on row arrival order.The degenerate alignment key retains all but one observation per cluster per side, with the survivor determined by dictionary insertion order; Fisher’s exact test on the balanced 8-of-16 sides should return p = 1.0.Source: Appendix C · p. 54

Appendix D. Typing Rules for Pre-registration

  • Pre-registration is enforced through matching labels, sidedness, constraints, and clean estimation premises, while the plan grammar itself guarantees that the plan is written before observation is introduced.T-OneSided is the only rule granting a one-sided mechanism a type, and T-Registered reuses the same design premise and constraint metavariables for confirmatory certification.Source: Appendix D · p. 55
  • A claim using outcome filtering can never be confirmatory because T-SelectOutcome sets the purity bit to read, even when its key constraints match a registration.Leaving the constraint unchanged would create a hole in which outcome-filtered comparisons appear to have the same design as their unfiltered counterparts; the implementation’s pin-dropping remains sound under design non-degeneracy.Source: Appendix D · p. 56
  • The typing rules do not enforce plan order, omission, repetition, or complete-account provenance, so the implementation rejects duplicate labels while affordability and external timestamped records handle the remaining audit obligations.Declared labels are charged once even if omitted, while incomplete accounts cannot be identified from the claim term alone and must be documented externally.Source: Appendix D · pp. 56–57

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

The appendix formalizes runtime and static checking as transition systems over one wealth pool, distinguishing data-dependent support from statically checked affordability. It establishes fixed-fraction progress and relative decidability while exposing conditions and bookkeeping gaps in the implementation’s unbounded-claim treatment.

Operational semantics

  • Runtime and static monitors share claim-sequence transitions, with runtime pricing from concrete p-values and static pricing from declared bounds over a single wealth pool.The runtime price is treated as an external oracle; the static checker threads declared-bound transformers through a shadow wealth trace.Source: Appendix E · pp. 57, 59
  • Under fixed_fraction, every claim deducts αj = iW and refunds ω on rejection, so wealth remains nonnegative without a solvency premise and runtime execution cannot get stuck.This guarantee is specific to fixed_fraction; QUDE rules use superlinear deductions, require cost(αj) ≤ W, and enforce caps.Source: Appendix E · pp. 57–58

Support and affordability

  • Support is the runtime verdict b = [p ≤ αj], whereas affordability is the data-independent static judgment Ok; reported support counts therefore differ from static acceptance.The appendix identifies support counts such as 6,545 of 8,911 as budget-afforded runtime rejections, not static Ok judgments.Source: Appendix E · p. 58

Implementation discrepancies

  • The Plan.audit identification of unbounded claims with bound p̄ = 1 is sound only under an unproved wealth invariant and mishandles formal refusal versus genuinely unbound unknown status.The invariant requires max(w0, ω/i) < 1/i; without it, repeated refunds can push runtime wealth above 1/i, while the formal grammar refuses literal bound 1.Source: Appendix E · pp. 59–60

Decidability

  • Checking is decidable relative to an oracle for observe footprints and decidable field/value equality, but the claim-level argument is not mechanized and practical Python checking conservatively refuses unresolved syntax.Estimation checking follows total structural recursions; claim checking uses finite fixed-point and lookup computations, while the implementation stops when literal resolution fails.Source: Appendix E · pp. 60–61

Appendix F. Proof of Theorem 7.1

The proof establishes the monotonicity, antitonicity, and no-refund properties of T, then uses them to show that the static wealth trace never exceeds the runtime trace. Consequently, every certified claim is accepted at runtime, and partial pre-registration preserves the invariant when declared bounds are honest.

Auxiliary lemmas

  • The Lean proof establishes that T is monotone in wealth, antitone in p, and bounded below by the no-refund transformer.These three lemmas are proved directly and support the theorem’s induction.Source: Appendix F · p. 61

Theorem 7.1 proof

  • Induction over program steps proves the static wealth trace satisfies ˆWj ≤ Wj and that every checker-certified claim is accepted by the runtime monitor.The proof handles notes, undeclared claims, certified claims, and refused claims while preserving the invariant.Source: Appendix F · pp. 61–62
  • Antitonicity is essential because charging a declared bound remains sound when the realized p-value is smaller, whereas charging T⊥ would not support the typed checker.Honesty gives pj ≤ ¯pj, allowing the proof to compare the declared price with the runtime price and transfer affordability to runtime acceptance.Source: Appendix F · p. 62

Corollary F.4

  • Partial pre-registration preserves ˆWj ≤ Wj when every declared bound is honest, while undeclared claims require no honesty and leave the invariant intact.Each declared claim still needs its own honest, statically affordable bound to inherit the runtime guarantee; other claims remain governed by the monitor alone.Source: Appendix F · pp. 62–63

Appendix G. Empirical Validation of Theorem 7.1

Theorem 7.1’s checker was empirically validated on fixed and tuned corpora: honest violations remained zero, including later claims after refusals and refunds, while dishonest bounds broke the guarantee. The experiments also showed that imprecise bounds impose either a resolution-driven cliff or a gradual certification slope.

Experimental design

  • The fixed corpus used 8 models on 15 paired coding tasks, while the tuned corpus used 150–400 synthetic tasks, planted effects, unbounded claims, and varied theorem parameters.The tuned design also included strongest-first programs, which are legitimate for this per-path theorem because it assumes no distributional claim-sequence hypothesis.Source: Appendix G · p. 63

Empirical validation

  • 1,120 of 2,367 honest-bound claims were certified in the tuned corpus, including 972 later-position claims and 566 after prior refusals, with zero violations in every stratum.The fixed corpus certified 18 claims, all at position 1; the tuned corpus tested the theorem across varied wealth trajectories, including programs rejected as a whole.Source: Appendix G · pp. 63–64
  • Dishonest bounds broke the guarantee on both corpora, while honest violations stayed at zero as required by Theorem 7.1.This negative control ensures the guarantee is tested against bounds that can actually violate it.Source: Appendix G · pp. 63–64

The cost of imprecision

  • On the tuned corpus, certification declined from 1,120 claims at slack 1.0 to 912 at slack 10, whereas the fixed corpus showed a cliff caused by limited p-value resolution.The fixed corpus certified claims within 1.5× at no cost but none at slack 3.0 or 10.0; its smallest available p-value was 0.0078, versus a 0.00417 requirement for a threefold overstatement.Source: Appendix G · p. 64

Appendix H. The Deletion Attack · Appendix I. Selection, Verification, and Accounting Side by Side

The appendices show that deleting failed tests can drive false-discovery control toward failure, especially under dependence, while the released selection, verification, and accounting tools remain separate interfaces. They also locate the attack’s crossing behavior empirically and clarify the current implementation seams.

Appendix H. The Deletion Attack

  • Under a complete null, the appendix measures the cost of an analyst running every pairwise model comparison but paying only for rejections.The honest analyst’s expected rejections saturate as wealth decays geometrically, whereas the deleting analyst’s expected rejections grow linearly.Source: Appendix H · p. 64
  • Table 9 estimates where the deleting analyst’s mFDR_η crosses α = 0.05 using null p-values from four sources, with five tests as the uniformity-based floor.The nulls preserve corpus-specific difficulty, cross-system correlation, and discordance structure while permuting real effects away; each row uses 4,000 Monte Carlo trials.Source: Appendix H · p. 64, Table 9 · p. 65
  • SWE-bench Verified crosses well above the five-test floor because permuted systems remain correlated through shared instance difficulty, so the uniform floor is not a severity bound.This exposes the corpus’s unverified (H3) dependence assumption as a higher-than-uniform per-test rejection rate.Source: Appendix H · p. 65
  • BIG-Bench Hard lands one test above the floor, while the 20-task synthetic sweep is conservative and understates the deletion effect threefold because McNemar’s exact test has too few discordant pairs.The BIG-Bench result is close to uniformity; the synthetic result reflects limited data rather than a weaker attack.Source: Appendix H · p. 65

Appendix I. Selection, Verification, and Accounting Side by Side

  • Figure 2 compares StatWhy, the released selection layer, and the released verification library on StatWhy’s two-drug example, showing architecture and seams rather than an integrated workflow.Neither released layer covers the paired-nominal instrument required by the leaderboard, and no software currently connects the three panes.Source: Appendix I · p. 65

Appendix J. Checker Runtime

The appendix measures Tacet’s checker and runtime-monitor costs, finding sub-second checking for large claim families but a cluster sign-flip computation that benefits substantially from dynamic-programming convolution at scale.

Measurement caveats

  • The runtime figures are orientation rather than a benchmark, because shared-machine between-invocation variance exceeds the in-process ranges and StatWhy’s solver timings measure a different operation.Tacet’s checker performs an AST walk and fold without calling a solver, whereas StatWhy’s seconds include SMT startup, verification-condition discharge, and proof production; raw ratios therefore do not represent a directly available speedup.Source: Appendix J · p. 65

Checker runtime

  • 10,000 claims complete in a fifth of a second on every measured invocation, despite fold time growing faster than linearly across the synthetic sweep.The sweep reports fold times of 0.62, 6.9, and 113 ms per decade of claims, with parsing contributing one-third to one-half of totals; 10,000 claims are comparable to the leaderboard’s 8,911-claim family.Source: Appendix J · pp. 66–67
  • About 180 ms is required to unroll 5,000 claims from one literal loop, motivating the stated cap on loop-unrolling size.Unrolling deep-copies and substitutes the loop body once per item, and its cost grows somewhat faster than linearly.Source: Appendix J · p. 67

Runtime monitor

  • Under two milliseconds replaces nearly a minute for BIG-Bench Hard’s pooled k = 26 cluster sign-flip computation, with identical p-values to enumeration.The two routes were cross-checked on 20 random configurations up to k = 12; at the leaderboard’s k = 12, 2^12 = 4,096 assignments finish in well under a millisecond.Source: Appendix J · p. 67

Related papers

Loading 2608.27451v1…