> 假阳性和好习惯相关时,它就不是噪声,是对好习惯的系统性罚分
假阳性通常被当成噪声:有个比例,忍一忍,慢慢降。 但有一类假阳性不是随机分布的——它只打在那些把事情做对了的输入上。 那它就不是噪声,是一个把作者往反方向推的梯度。
结论先行¶
假阳性通常被当成噪声:有个比例,忍一忍,慢慢降。 但有一类假阳性不是随机分布的——它只打在那些把事情做对了的输入上。 那它就不是噪声,是一个把作者往反方向推的梯度。
同一个工具里的三个例子:
① 把每个数都由脚本生成的论文,100% 的数被毁掉;把数硬写在正文里的论文,一个都不少。
提取器遇到自定义宏时只剥掉反斜杠,于是 29 个生成出来的数以裸名字的形式到了读者手里
(HefixCanonPct、ProvHistLateBoundHi、LeanTheoremCount…)。
已编译的 PDF 里这些位置是 81.1、6.4、23,一个裸名字都没有。
后果是读者的"无法反驳的一句"变成"这份稿子没写完——几十个 LaTeX 宏没有解析",
还有两道题(追踪摘要里每个数、核对正文算术)从根上答不了。
用
\newcommand把每个数字和它的生成脚本绑死,是数字卫生最好的做法。 而它在这个工具下的得分,严格低于把数字手抄进正文。
② 把测量程序写清楚的句子,被当成"在吹自己干了多少活"。
"每一行都在同一个协议下测得"、"七行是重测的而不是沿用的"、"每个数值主张都重新生成"—— 全被列为 effort-boasting。而这些句子恰恰是它们缺席时审稿人会抱怨缺的东西。
③ 把定理结论在引用它的那句话里写出来的论文,被判"读者在这里必须跳走"。
自包含性检查把 thm:/cor:/lem: 当作浮动体处理。
表格的证据无法内联,定理的结论routinely 可以——而工具自己的修法文本就提供了这条分支。
那次运行的 5 条定理 STOPS 里,4 条已经满足了那个修法。
为什么¶
普通假阳性的代价是时间:看一眼,丢掉。 跟着好习惯走的假阳性,代价是方向:
- 它作用于"听工具的话"的那部分人,而那部分人恰好是会照着改的人。
- 它作用的方向和正确方向相反。①的最短路径是把生成的数字改回硬写; ②的最短路径是删掉方法句;③的最短路径是把那句已经写好的结论删掉,改成"见定理 3"。
- 它不会自我纠正。作者改完之后警报真的消失了,所以这次修改被确认为"对"。
而且这类缺陷有一个很好用的可测特征: 拿两份同样正确、但在某个维度上做法相反的输入过一遍,比较报警数。 ①里就是"生成数字的稿子"对"硬写数字的稿子"——同一篇论文的两个版本, 报警数差了几十条,而两份 PDF 逐字相同。差值不为零,就说明工具在给一种做法打分。
这件事和"检查器只用通过的样本定标"是两种不同的偏差: 那一种让工具看不见某类缺陷(见 只用"通过"的样本定标,19 次修改全是降噪——而加了对抗样本之后,第一条被抓到的检查是死代码), 这一种让工具反向激励。后者更难发现,因为它的输出是"发现",不是沉默。
怎么用¶
- 分流假阳性时,多问一句"被误报的那些输入有什么共同点"。 如果共同点是一种好做法,这条的优先级要跳到最前面——它不是 minor。
- 拿一对"同样正确、做法相反"的输入做差分测试。 生成数字 vs 硬写数字、 写方法句 vs 不写、结论内联 vs 只给引用。报警数应该相等;不相等就是一个激励泄漏。
- 这类缺陷修不动的时候(比如宏展开有真实的技术约束), 至少把它变成可见的:报出"有 29 个宏未展开,所有与数字有关的回答作废"。 一个声明了自己失效范围的工具,不会把作者推向错误方向。
- 相关:一次变换的两个消费者需求相反,见 为保住行号而做的填充,让一个宏的值能不能到达下游取决于宏名有多长; 残渣按可见性分级,见 预处理残渣有三种,而守卫只有两道——被剥成普通单词的那一种无人可见。
出处¶
~/Tools/nonexpert-review 的 feedback/:①是 2026-09-25 的一条 critical
(29 个宏名、PDF 对照已由回报者核过),②③是 2026-09-24/25 的两条。
"差分测试一对做法相反的输入"是我这次总结的判别法。