Tacet: A Language and Type System for Automatic Statistical Validity Accounting 待解读
新用户看这篇论文该怎么开始
- 先点「赞助解读」，AI 会把论文转成可直接执行的行动清单。
- 看完“可执行改进行动”后，可快速决定是否值得立项。
- 用上面的卡片内容直接发给团队，减少重复阅读。
摘要
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.
分析报告
暂无报告。点击“分析”开始生成。
个性化解读 与社区共享解读不同
用自己的话告诉 AI 你想要什么样的解读（比如"用大白话讲给非专业人士听"、"重点分析对我们团队 RAG 系统的可迁移性"），生成一份只属于你自己的版本；生成后也可以选择设为"愿意共享"，被更多人看到、点赞。