AI 时代，数值库正确性工作的耐久价值
问题
假设未来的 AI 已经能够按照要求完成下面的任务：
- 使用 Lean4 描述并证明
sin的正确舍入算法； - 将算法提取为 Rust 实现；
- 导出 C API；
- 使用 GMP 等高精度库进行随机测试和差分测试。
如果 AI 可以稳定、低成本地完成这些工作，那么单独“证明一个 sin 函数”就可能不再是一个足够耐久的研究或工程方向。今天积累的实现经验，明天可能只是一个提示词和自动化流水线的输出。
因此，更重要的问题不是“AI 能不能生成一个正确的函数”，而是：
如何选择一种工作，使 AI 能力增长后，已有投入不会全部变成普通的自动生成结果？
首先区分不同层次的正确性
“正确性”并不是一个单一目标。数值函数至少涉及以下层次：
数学语义
↓
算法与误差证明
↓
跨语言实现的一致性
↓
平台、编译器和实际库的持续验证
数学语义包括定义域、值域、分支、奇点、特殊值和异常行为。算法证明关注逼近、递推、范围规约以及误差界。实现一致性关注 Rust、C、Julia 等实现是否实现了同一个算法。最后一层还要处理浮点环境、编译器优化、FMA、SIMD、次正规数、异常标志以及不同硬件。
Lean 主要帮助解决前两层。形式化证明并不会自动覆盖所有提取代码、FFI 边界和具体平台行为；除非这些语义保留关系也被纳入可信边界，否则“证明过的算法”与“实际可调用的 C 函数”之间仍有工程间隙。
重写与等价性验证的价值
把大型 C 程序重写为 Rust，再使用 Kani 等工具逐个函数验证等价性，是很有价值的工程路线。它能够发现：
- 未定义行为；
- 内存安全问题；
- 整数溢出和边界错误；
- 分支条件不一致；
- 重写过程中暴露出的历史 bug。
但等价性验证有一个根本限制：
它证明的是“新实现与旧实现一致”，不一定证明“旧实现本身正确”。
如果原来的 C 程序已经包含错误，Rust 版本可能只是更安全地保留了同一个错误。因此理想的验证结构不是只有两个实现互相比较，而是加入数学规范或独立高精度 oracle：
数学规范 / 高精度 oracle
↓
Lean 或其他工具验证的参考算法
↓
Rust / C / Julia 实现
↓
等价性验证 + 性质测试 + 差分测试
↓
实际平台上的精度与性能报告
GMP 随机测试不是完整答案
GMP 等高精度库非常适合作为参考 oracle，但随机测试本身通常无法覆盖数值函数最危险的区域。需要额外关注：
- 正确舍入边界附近的输入；
- 大指数与尾数的组合；
- 范围规约的临界点；
- cancellation 严重的区域；
- 零、负零、无穷和 NaN；
- 奇点、分支切割以及接近极点的输入；
- 溢出、下溢和次正规数；
- 不同舍入模式；
- 编译器和硬件优化导致的结果变化。
因此测试系统应该结合：
- 随机高精度差分测试；
- 舍入边界附近的定向生成；
- 性质和 metamorphic testing；
- 多实现 differential testing；
- 已知最坏案例和历史 bug 回归测试；
- 不同编译器、CPU 和编译选项下的测试。
AI 可以生成大部分测试输入、性质和证明草稿，但必须由明确的验收协议决定什么算“通过”。
更耐久的目标：正确性基础设施
相比把成果定义为“证明了多少个函数”，更耐久的成果是建立一套持续审查 AI 生成数值代码的基础设施。
一个完整的工作单元不应只是一个实现，而应包括：
函数语义合同
+ 独立高精度 oracle
+ 多语言实现
+ 性质测试
+ 定向边界测试
+ 形式化证明或误差证明
+ 可复现报告
+ 历史失败案例
其中，AI 可以负责：
- 生成 Lean 定义、定理和证明草稿；
- 尝试多种算法与实现；
- 生成测试性质和输入分布；
- 分析反例并提出修复；
- 将实现提取到 Rust 或其他语言；
- 自动更新报告和回归测试。
人的主要工作则转移到：
- 设计语义合同；
- 规定可信边界；
- 判断 oracle 和假设是否独立可靠；
- 规定证明覆盖范围；
- 维护失败案例和验收标准；
- 选择哪些真实库、平台和版本需要持续验证。
这并不要求排斥 AI 驱动的形式化证明。相反，形式化证明本身也应该尽可能自动化。需要保护的不是手写证明文本，而是证明目标、假设、工具链、检查器和可重现过程。
对三个方向的重新判断
1. 以 Lean4 为基础生成指定语言代码
这是很好的内核技术路线，但单个函数的实现容易被未来 AI 自动化。它更适合作为正确性流水线的一环，而不是项目的全部价值。
2. 继续维护 Julia 数值库，并进行跨语言重写
这是最接近实际用户和真实 bug 的路线。Julia 版本可以继续提供生态兼容性，Rust 或其他语言则可以作为独立实现、验证载体或安全 kernel。它能够积累真实的失败案例和跨语言经验，短期收益也更明确。
3. 扩展 Julia 的形式化验证能力
直接修改语言本身的成本较高，也容易变成一个大型语言研究项目。更现实的起点是语义合同、测试生成器、验证报告工具和 Julia/Rust/Lean 之间的接口。当这些工具显示出稳定需求后，再考虑 Julia 原生的属性标注、数值 contract 或程序分析支持。
因此，优先级可以是：
2 + 1：现有库维护 + 选定函数的形式化验证
↓
跨语言正确性与回归验证基础设施
↓
必要时再增强 Julia 语言和工具链
建议的第一个试点
选择一个边界行为丰富、但仍能独立封装的特殊函数，建立完整闭环：
- 写出数学语义合同；
- 建立高精度参考实现；
- 记录现有 Julia 实现的精度基线；
- 编写独立的 Rust 实现；
- 用 Lean 验证局部算法或误差性质；
- 进行定向测试、随机测试和差分测试；
- 导出 C API 并检查 FFI 边界；
- 在不同编译器和硬件上生成可复现报告；
- 保存所有失败输入、修复记录和证明覆盖范围。
这个试点的目的不是证明 AI 能不能完成一个函数，而是找出长期系统真正的瓶颈：规范表达、浮点模型、证明库、跨语言语义、平台差异，还是测试 oracle。
结论
如果 AI 将来可以自动完成一个正确舍入的 sin，那么与 AI 竞争“生产一个 sin”确实没有长期优势。更值得投入的是建立一套能判断以下问题的系统：
- AI 生成的证明是否覆盖了实际目标；
- 提取后的代码是否保持了证明语义；
- 多语言实现是否符合同一个数学规范；
- 新平台和新编译器是否引入了回归；
- 旧库中哪些行为其实是历史 bug；
- 哪些失败案例值得进入长期测试集。
最终的耐久资产不是某段代码，也不是某个证明文件，而是语义合同、测试数据、验证工具、失败历史和可复现的验收协议。