AI 时代数值代码的正确性来源

基于 idea/ 中的项目选择判据与手工艺讨论，延伸讨论广义代码正确性在 AI 时代的变化——以数值计算为具体抓手，但不限于此。

讨论日期：2026-06-14

〇、问题起点

AI 之前，正确性大致是这样流转的：

需求 → 规格 → 设计 → 实现 → 测试 → 部署 → 运维

每一层的人类投入大致均匀。AI 之后，实现的成本坍塌了，但规格和测试没有。这产生了一个不对称：

需求 → 规格 → [AI 实现] → 测试 → 部署 → 运维
         ↑ 瓶颈              ↑ 瓶颈

在 AI 时代，正确性工程的投资重点应该从"怎么写得对"完全转向"怎么知道它是对的"。

这个文档尝试回答三个问题：

什么是对的？——正确性锚点从哪来？
怎么知道它不对？——如何系统性地探测错误？
AI 在各层能做什么、不能做什么？——人类判断力的支点在哪？

一、正确性锚点的五种类型

"对"不是单一概念。数值代码的正确性至少可以锚定在五个不同的来源上，每个的保证强度和适用范围都不同。

1.1 标准文本（Specification-anchored）

来源： C23 Annex F/G、IEEE 754、DLMF、语言标准库文档。

特点： 正确性来自人类共识文本——这是最高层次的"对"的定义。

层级	例子	特点
数学定义	DLMF 定义 $J_\nu(z)$ 的数学含义	在抽象层面是权威的，但降到具体数值时不可执行—— $z=10^{308}$ 的 $J_\nu(z)$ 是多少？DLMF 只给公式，不给值
语言标准	C23 定义 `sin` 的语义为"无限精度+舍入"	依赖于"无限精度"这个理想概念——文本本身不能计算
实现级参考	Wolfram、NIST 物性数据	介于抽象定义和具体数值之间。Wolfram 在边界 case 上有已知 bug，作为 oracle 是一个足够好的近似，不是数学真理

关键洞察： 标准在抽象的数学层面是权威的，但降到具体数值时，它本身不可执行。标准的价值和标准的可执行性之间存在一道翻译裂缝——谁来做这个翻译，谁就在定义事实上的"对"。

这道裂缝在 AI 时代变宽了：AI 可以从标准文本直接生成实现，但 AI 无法判断自己翻译得对不对——标准文本在训练数据里，但正确的翻译不在。

1.2 高精度 Oracle（Oracle-anchored）

来源： MPFR、arb、高精度参考实现。

做法： 以远超目标精度（如 512-bit 中间精度）计算函数值，然后按目标舍入模式舍入到目标精度，得到"唯一正确答案"。

MPFR 本身怎么被验证？ 它建立在 GMP 的任意精度整数算术之上——底层只有整数算术，理论上可验证。但 MPFR 也在持续修 bug。它不是一个静态的"真理"，而是一个不断逼近真理的工程制品。

正确性工程的一个深刻原则：正确性不是来自单一来源的绝对可靠，而是来自多个独立来源的交叉一致。 如果一个实现、一个 oracle、和一个物理约束三者同时被满足，正确的置信度远超任何一个来源单独能提供的。

这就是为什么 oracle 必须独立于被验证对象。CORE-MATH 使用 MPFR 作为外部的"地面真相"——不是因为 MPFR 绝对不会错，而是因为 MPFR 不会和你的实现犯同样的错误（不同的作者、不同的算法、不同的假设）。

1.3 物理/数学约束（Constraint-anchored）

来源： 守恒定律、不等式、函数性质（单调性、对称性、函数方程、值域）。

特点： 这类锚点只定义"什么是错"，不定义"什么是对"。这恰好绕开了规格书写的困难，而且可以被自动检查，无需人工标注 ground truth。

数学约束举例：

约束类型	例子	可自动检查？
单调性	$\exp(x)$ 单调增， $\text{erf}(x)$ 单调增	✅ 随机采样可探测违反
对称性	$\sin(-x) = -\sin(x)$	✅
范围	$\text{erf}(x) \in (-1,1)$ ， $\exp(x) > 0$	✅
特殊值	$\exp(0)=1$ ， $\sin(0)=0$	✅ 快，适合 CI
函数方程	$\log(xy) = \log(x) + \log(y)$	⚠️ 浮点下近似成立，需要 ULP 容忍

物理约束举例（ChemE/PSE）：

约束	含义	可自动检查？
质量守恒	流入 = 流出 + 积累	✅
能量守恒	入热 = 出热 + 积累	✅
热力学第二定律	孤立系统的熵不减	⚠️ 方向性可检查，量值需模型
摩尔分数	$x_i \in [0,1]$ 且 $\sum x_i = 1$	✅
Gibbs 自由能	平衡态时达极小值	⚠️ 需方向导数检查

数值陷阱： 浮点算术本身违反了很多数学恒等式。 $\log(xy) = \log(x) + \log(y)$ 在浮点下是不精确成立的。所以需要的是近似约束检查——不是 assert 等式成立，而是 assert 等式在合理误差范围内成立——而"合理"的定义本身需要领域判断。

1.4 对抗一致性（Adversarial-consistency）

来源： 多个独立实现的交叉验证。

做法： 同一输入喂给多个独立实现（自己的实现 + CORE-MATH + Julia Base.Math + glibc libm + MPFR），比较输出。多个独立来源对同一随机输入的一致结果，是极强的正确性信号。

与差分测试（differential testing）的关系： 差分测试是这类锚点的操作化。当实现成本趋零时，你能支付多个独立实现的成本，只需要人类的判断聚焦在一个问题上："它们都同意了吗？"

微妙之处——"正确的分歧"： 两个都可以是正确的实现（在 spec 范围内），但返回了不同的最后一位。这不是 bug——是精度上的合理差异。区别"正确的分歧"和"真正的 bug"需要领域知识。

这就是正确舍入（correctly rounded）路线的吸引力：以 MPFR 为绝对参考，按目标舍入模式舍入，得到唯一正确答案。一个函数要么返回了正确的舍入结果，要么没有——没有模糊地带。这在 AI 时代特别重要，因为你需要一个自动化的、无歧义的 pass/fail 判据——否则"差不多对"会积累成系统性的精度漂移。

正确舍入的代价： 某些函数在某些输入上极其困难（Table Maker's Dilemma）。对于基础函数（sin、cos、exp、log），hard-to-round cases 已被穷举。对于特殊函数（tgamma、Bessel），正确舍入仍然是开放问题。

1.5 经验数据（Empirically-anchored）

来源： 实验测量、工业标准（ASME 蒸汽表、NIST 物性数据）、已发表的 benchmark（Tennessee Eastman 过程）。

特点： 不定义"正确输出"，而是定义"输出必须符合的边界"。一个 P-V-T 计算不需要返回和 NIST 完全一致的值，但差异必须在设备精度的合理范围内——这个判断本身就嵌入了领域知识。

二、正确性的强度谱

综合以上五种锚点，存在一条从低强度到高强度的谱系：

强度         低                                        高

规格文本  →  经验数据  →  物理约束  →  高精度Oracle  →  对抗一致性  →  数学证明

AI可参与性   高 ←───────────────────────────────────────────── 低
成本         低 ←───────────────────────────────────────────── 极高
覆盖面       全（概念上）←─────────────────────────────────── 窄（个别函数）

三个值得注意的倒置：

高精度 Oracle 在 AI 时代反而变得更关键——不是因为 Oracle 本身变强了，而是因为 AI 生成的代码量暴增，自动化的、独立于实现的正确性检查需求暴增。Oracle 是少有的可以不依赖人类判断就能发出"这是错的"信号的方法。
物理约束具有新形态的价值——它们不需要人工标注，不需要"正确的输出"作为参考，只需要"不可能的输出"作为排除器。给你一百万个人工标注的参考值，AI 可以 fit 出所有已知 case；给你三条守恒定律，AI 无法绕过——因为守恒定律不是数据，是结构。
差分测试从锦上添花变成基础设施——当实现成本趋零，你可以负担多个独立实现的成本。这恰好是最适合 AI 自动化的部分（跑五个实现、比较、标记差异），也恰好需要人类判断收尾（差异是"正确的分歧"还是 bug？）。

三、如何测试数值代码：分层策略

将五种锚点转化为可操作的测试体系。以下分层承接 [[数值函数形式化验证-想法与约束.md]] 中的五级验证（L0–L4），在此处重新组织为更通用的框架。

Layer 0：编译期保证

手段： 类型系统 + lint + 静态分析。

禁止隐式转换、标注精度语义
禁止已知危险模式（等值比较浮点数、除零路径、未使用的数值结果）
deny(unsafe), clippy::float_cmp 等编译器级检查

AI 特有问题： AI 生成的代码经常在数值上"看起来对"但违反了语言的类型约束。类型系统应该被当作AI 生成代码的第一道安检。

AI 能做什么： ✅ 生成 lint 规则。AI 不能做什么： ❌ 定义危险模式（需要领域知识）。判定 pass/fail： ✅ 编译器判定，机械的。

Layer 1：特殊值快速测试

手段： CI 常驻的秒级测试。

规范要求的特殊值（±0、±∞、NaN、subnormal、overflow 边界）
已知的 hard-to-round cases
已知的历史 bug 回归 case

每一个手动添加的回归测试都是一个判断型资产——它编码了"这个 corner case 值得锁死"。

AI 能做什么： ⚠️ 生成测试格式，但会漏掉重要的特殊值。AI 不能做什么： ❌ 判断哪个 case 值得锁死。判定 pass/fail： ✅ 机械比较。

Layer 2：穷举/大规模对照测试

手段： 定期运行（nightly/cron），binary32 穷举或 binary64 大量采样。

f32 全输入域 ≈ 40 亿种输入 → 数小时可完成
正确性 oracle 用 MPFR 按目标舍入模式生成唯一期望值
任何差异要么是 bug，要么是 oracle 的 bug——没有"容忍度"的模糊地带

这就是正确舍入的 killer feature：穷举测试无歧义。binary64（ $2^{64}$ 种输入）无法穷举，需要随机采样 + 特殊值策略。

AI 能做什么： ✅ 生成框架代码。AI 不能做什么： ❌ 不能提供 oracle（它自己是待验证的，oracle 必须独立于被验证对象）。判定 pass/fail： ✅ 用外部 oracle 时判定机械。

Layer 3：约束/性质测试

手段： 随机采样 + 不变量检查，每次提交跑。

每个函数的数学约束（单调性、奇偶性、函数方程、值域）
物理约束（ChemE：质量守恒、能量守恒、Gibbs 自由能下降方向）
Differential testing（同一输入喂给多个独立实现）

这些都是"只要违反就是错"的不变量——不需要黄金参考值。 这恰好绕开了"规格本身可能错"的问题，也绕开了 AI 无法提供 oracle 的困境。

AI 能做什么： ✅ 生成检查函数体。AI 能做什么但有风险： ⚠️ 能从 spec 推断数学约束，但会遗漏、会幻觉出不存在的不变量。判定 pass/fail： ✅ 违反时清晰。

Layer 4：模糊测试

手段： 定期/按需跑。

输入空间遍历（包括 NaN、subnormal、异常值模式）
计时一致性（单次调用耗时不应有极端异常）
不崩溃/不 panic/不无限循环
对 NaN 和非正规输入的行为合理（不强求精确，但要求不 UB）

AI 能做什么： ✅ 天生的 fuzzer——生成各种输入。AI 不能做什么： ❌ 不知道什么是"合理的 NaN 行为"。判定 pass/fail： ⚠️ crash 可判定，精度退化不可判定。

Layer 5：形式化验证

手段： 按函数深度选择，不要求全覆盖。

Bounded model checking（Kani）验证不 panic、不溢出、不除零
Sollya/Gappa 为多项式逼近生成误差上界的机器可查证明
Coq/Flocq 为选定的函数提供完整的正确舍入证明

L5 是附加保险，不是基础要求。 AI 在证明搜索上是最短板——一个 lemma 卡几个小时是常态。

AI 能做什么： ❌ 证明搜索是 AI 最短板。AI 不能做什么： ❌ 不能写形式化规格（需要数学建模）。判定 pass/fail： ✅ 证明检查器是机械的。

四、AI 在各层的角色总结

一个清晰的分化模式：

层次	AI 能生成测试吗？	AI 能定义"对"吗？	AI 能判定 pass/fail 吗？
L0 编译期	✅ 生成 lint 规则	❌ 不能定义危险模式	✅ 编译器机械判定
L1 特殊值	⚠️ 生成格式，漏掉重要的	❌ 不能判断哪个 case 值得锁死	✅ 机械比较
L2 穷举对照	✅ 生成框架代码	❌ 不能提供 oracle	✅ 外部 oracle 时机械判定
L3 约束检查	✅ 生成检查函数	⚠️ 会遗漏、会幻觉	✅ 违反时清晰
L4 模糊测试	✅ 天生的 fuzzer	❌ 不知何为合理行为	⚠️ crash 可判，精度退化不可判
L5 形式化验证	❌ 最短板	❌ 不能写形式化规格	✅ 证明检查器机械判定

AI 在"生成测试"有用，在"判断什么值得测试"无用，在"提供正确答案"不可靠（oracle 和被验证对象同源则无意义），但在"机械判定 pass/fail"完全胜任。

这意味着正确性工程的人类瓶颈是三个判断问题：

定义"对"的语义——选择正确性锚点，设定验收标准
选定/构建 oracle——确保 oracle 独立于被验证对象
判断哪个 corner case 值得锁死——测试即规格，规格即判断

这三个恰好是 AI 最不擅长的。

五、关于跨平台一致性与精确舍入

5.1 为什么跨平台一致性在 AI 时代更重要

AI 之前，数值代码的"跨平台"通常意味着"不同系统上结果差不多"。AI 之后，三个新因素使一致性成为硬需求：

AI 生成的代码可能混入多个来源：一部分来自你的手写实现，一部分来自 AI 生成的算法，一部分来自不同语言的 FFI 调用。它们在不同平台上的行为必须一致到你可以在本地验证 CI，然后部署到服务器时得到相同结果。
规格的价值取决于它的可重复性：如果 sin(x) 在你的笔记本和 CI 服务器上返回不同的最后一位，你的穷举测试就没法写——因为没有单一的"正确答案"。
差分测试要求 bit-exact 的实现：如果你在三个参考实现之间做差分测试，而你的实现因为平台差异返回了不同的结果，差分测试就被噪音淹没了。

5.2 精确舍入作为可判定性标准

精确舍入不只是关于精度，更是关于正确性的可判定性。

方案	承诺	可自动验证？	可跨平台？
A: ULP 容忍	"误差 ≤ 2 ULP"	❌ f64 有 $2^{64}$ 种输入，穷举不完	❌ 允许多个"正确"答案
B: 正确舍入	"返回唯一正确的舍入结果"	✅ binary32 穷举可验证（40 亿种输入，数小时）	✅ 唯一正确答案，所有平台应一致

精确舍入是唯一可以在数学上严格判定的正确性标准。方案 A 允许多个不同的"正确"答案，无法区分"平台差异"和"精度退化"。

5.3 正确舍入 vs 足够好的精度：分层选择

不是所有场景都需要正确舍入：

场景	推荐标准	验证方法
科学计算的中间步骤	2-4 ULP 足够	采样 + MPFR 对照
可复现性关键的基准测试	正确舍入	binary32 穷举 / binary64 特殊值
安全/财经/法律责任相关	正确舍入 + 指定舍入模式	穷举 + 形式化验证
ChemE 过程模拟	2-4 ULP 通常足够	物理约束 + 采样对照
编译器常数折叠	正确舍入（常量求值必须确定）	穷举

不是一条标准适用所有场景。而是需要根据正确性的后果——错了会怎样？——来选择适当的标准。 这个"按场景定义足够好"的决策本身，就是 AI 时代人需要做的判断。

六、正确性的成本分布变化

AI 之前，正确性的总成本大致是：

规格 10% + 实现 40% + 测试 30% + 审查 10% + 运维 10%

AI 之后：

规格 30% + 实现 5% + 测试 30% + 审查 25% + 运维 10%

实现成本坍塌了，但规格、测试、审查的相对权重翻倍了。 这意味着在 AI 时代：

投资重点从"怎么写得对"转向"怎么知道它是对的"
规格撰写、测试设计、审查判断——这三个的能力变得比编码能力更重要
一个精心构造的测试集（判断型资产）比一个精心手写的实现（代码型资产）更值钱，因为实现可以无限再生，测试集的判断不能

七、ChemE/PSE 领域的特殊性

7.1 物理约束作为天然的正确性锚点

化工/PSE 比其他计算领域有一个结构性优势：系统中的正确性锚点天然来自物理定律，不依赖于人工规格。

质量守恒、能量守恒不是"应该"满足，而是"必须"满足
违反物理约束 = 确定性的错误，不论算法输出什么值
这些约束可以在 L3 层自动检查，无需黄金参考值

7.2 正确性的"足够好"有行业标准

化工模拟中，"对"的标准通常锚定在：

实验精度（温度 ±0.1K？±1K？取决于场景）
工业标准（ASME 蒸汽表对 IAPWS-IF97 的精度要求）
经济后果（相平衡计算误差对全流程优化的利润影响）

这为正确性分级提供了天然框架——不是一刀切追求最高精度，而是根据经济后果决定精度投资。

7.3 面向 ChemE 的正确性研究机会

物理约束自动验证框架——将质量守恒、能量守恒等编码为 CI 中自动运行的测试
ChemE oracle 构建方法论——对于没有现成高精度 oracle 的新模型（如新状态方程），如何从零构建可信的正确性链条
过程模拟的正确性分级标准——什么环节需要正确舍入（编译器常数折叠），什么环节 2 ULP 就够（求解器中间步骤）

八、开放问题

本文档的讨论现状是阶段性的，以下问题有待深入：

全新函数的 Oracle 构建——如果你的函数在现有任何库中都没有参考实现，你怎么办？从数学定义 → 符号计算 → 任意精度实现 → 交叉验证——这条链条怎么建、每一环怎么验证？
正确性成本的经济学——AI 让测试生成趋近免费，但让测试判断依然昂贵。如何在无限 AI 能力下更精确地对代码做正确性分级？
规格语言的选择——形式化规格（TLA+、Coq）vs 可执行规格（QuickCheck 性质）vs 自然语言规格 + AI 翻译 + 人类审查——哪条路对数值/PSE 领域最实用？
形式化验证的务实切入点——对于 PureLibm-rs，L0-L4 现在就可以做；L5 应该从哪些函数切入？哪些值得做完整证明，哪些不值得？
ChemE 正确性的基准建设——PSE 领域缺乏系统性的数值正确性基准。有没有机会构建一个 ChemE 版的"SPEC CPU"——一组标准化工过程模拟的参考输入和期望输出？

九、相关文档

[[项目选择判据-双视角.md]] — 判断 vs 代码的区分框架
[[数值函数形式化验证-想法与约束.md]] — PureLibm-rs 设计与 L0-L4 五级验证
[[Rust科学计算生态调研.md]] — LLVM 浮点约束与 Rust libm 现状
[[项目诊断.md]] — 手工艺项目选择与正确性方向评估
[[个人项目选择规则.md]] — 项目优先级分层

〇、问题起点​

一、正确性锚点的五种类型​

1.1 标准文本（Specification-anchored）​

1.2 高精度 Oracle（Oracle-anchored）​

1.3 物理/数学约束（Constraint-anchored）​

1.4 对抗一致性（Adversarial-consistency）​

1.5 经验数据（Empirically-anchored）​

二、正确性的强度谱​

三、如何测试数值代码：分层策略​

Layer 0：编译期保证​

Layer 1：特殊值快速测试​

Layer 2：穷举/大规模对照测试​

Layer 3：约束/性质测试​

Layer 4：模糊测试​

Layer 5：形式化验证​

四、AI 在各层的角色总结​

五、关于跨平台一致性与精确舍入​

5.1 为什么跨平台一致性在 AI 时代更重要​

5.2 精确舍入作为可判定性标准​

5.3 正确舍入 vs 足够好的精度：分层选择​

六、正确性的成本分布变化​

七、ChemE/PSE 领域的特殊性​

7.1 物理约束作为天然的正确性锚点​

7.2 正确性的"足够好"有行业标准​

7.3 面向 ChemE 的正确性研究机会​

八、开放问题​

九、相关文档​