定理的保修卡

🎫 一张保修卡的命运

先从一个场景说起。

你买了一台新电器，用了一年半，主板烧了。你翻出说明书，指着其中一行"本产品提供两年质保"，要求免费维修。客服接过保修卡，翻到背面，指着细则里的第三条："进水、拆机、电压不稳造成的损坏不在保修范围内"。你愣住——你根本没注意过背面还有字。

数学定理就是一张保修卡。定理的结论（"误差不超过最优解的 1+ε 倍"）是正面那行大字；定理的适用条件（A 的秩至少为 k、参数 α 必须为正、输入必须非零）就是背面的细则。人类数学家读教材时，脑子会自动补上这些细则——定理是写给"懂的人"看的，很多条件压根不写，藏在"显然"两个字里。可当一个 AI 拿着这张保修卡去"索赔"——用它来做计算、给算法下保证——它必须真的把背面的每一条细则都攥在手里。少一条，索赔就该被拒；更糟的情形是连"被拒"都不会发生，AI 拿着残缺的保修卡宣布索赔成功，而没有人发现。

这篇论文讲的，就是怎么把四本经典教材里的一百七十一个形式化目标——定理、命题、关键陈述，连同它们的细则，一条不漏地翻译成机器能查的语言（Lean 4），以及翻译过程中那些让人捏把汗、又让人拍案的时刻。它叫 FARMS——Faithful Alignment and Representation of Mathematical Statements，数学陈述的忠实对齐与表示。作者是马里兰大学数学系的 Di Wu、田纳西大学诺克斯维尔分校数学系的 Ling Liang，以及通讯作者 Haizhao Yang（马里兰大学数学系与计算机系）。论文 2026 年 10 月 29 日挂在 arXiv 上，编号 2610.40560。

📚 四本教材，一百七十一条定理

FARMS 选了计算数学里两个硬核领域：随机数值线性代数（RNLA）和数值偏微分方程（数值 PDE）。素材来自四部经典——Drineas 和 Mahoney 的教材，32 个目标；Halko、Martinsson 和 Tropp 关于随机化数值线性代数的综述，35 个；Martinsson 和 Tropp 的合作教材，20 个；Larsson 和 Thomée 关于偏微分方程数值解的专著，84 个。加在一起，171 个形式化目标。

为什么挑这两个领域？因为它们是自动化科学计算的地基。AI 想做科学发现，绕不开数值算法；想用数值算法，绕不开这些定理。而这些定理恰恰是最"人类"的那类知识：量词的顺序藏在行文里，定义域靠读者心领神会，"显然"后面压着半个世纪的文献。这种写法对人友好，对机器致命——机器不会心领神会，它只会逐字执行。

举个具体的例子。教材里常见"当 n 充分大时，以高概率成立"——对人类读者，这句话够了，大家知道去查浓度不等式里的参数；对 Lean，这句话等于什么都没说。"充分大"是多大？必须写成一个具体的阈值函数，比如 n ≥ C·log(1/δ)/ε²，还得交代 C 是多少、δ 是什么、ε 允许在哪个范围取值。再比如"取 A 的 QR 分解"——Lean 会追问：什么条件下 QR 分解存在？唯一吗？取哪一版？人类读者靠上下文三秒钟补完的空白，机器得一个一个钉死。这正是"忠实"二字贵的地方：FARMS 要把每个这样的空白找出来，要么补上，要么证明它无关紧要，要么挂上警告牌。这还只是语法层面。真正凶险的是语义层面——候选陈述编译通过、看着也像原文，可某个量词从"存在"被换成了"任意"，整个定理的方向就反了，而编译器对这种偷换一概放行。这一点，流水线里专门有人负责盯。

🏭 流水线：一间多窗口的公证处

FARMS 的核心是一条多智能体流水线，每个环节设专职角色，互相盯着。我把它想象成一间公证处：客户（教材定理）拿着材料进来，要过好几道窗口，任何一道觉得材料不对就退回去，而且退回去有记录、有理由、有复审。

第一道窗口是源审计员（Source auditor）。它检查每条陈述是否附带形式化所需的全部材料：定义齐了吗？假设全吗？算法上下文在不在？缺什么就列一张缺口清单，交给检索器（Retriever）回原文找——检索器用确定性的检索加规划调用，不做自由发挥。找回来的材料交给证据评审员（Evidence reviewer）把关：这东西真的补上了缺口吗？补上了，送回源审计员复审；补不上，继续找。这个循环有界，不会无限打转。

第二道窗口是形式化器（Formalizer）。材料齐了，它拿着证据和一个共享的领域库——里面积累着已形式化的定义，避免重复造轮子——生成 Lean 4 陈述，同时记录它对原文的理解。

第三道窗口是 Lean 编译器。这相当于签证官的形式审查：表格填满没有、格式对不对。能通过编译，只说明陈述在形式环境里语法良好、类型正确。它完全不代表陈述忠实于原意。这一点后面会反复出现，请先记住。

第四道窗口是语义评审员（Semantic referee）。真正的较真从这儿开始。它逐条核对：原文的对象保住了吗？假设保住了吗？量词顺序对吗？算法构造对吗？定量的保证（那个 1+ε）还在吗？只要类型或意义对不上，就转给修复器（Repairer），修完重新编译、重新评审。

第五道窗口是一致性评审员（Consistency reviewer）。终审，确认前面发现的所有问题都被妥善处置。评审之间出现分歧，回到语义评审员那里裁决。

还有一条岔路：弃权。形式化器报告"这个缺口持续补不上"，材料会被送到弃权评审员（Abstention referee）那里，由它判断弃权是否合理；说明员（Explainer）把理由记录在案。它相当于图书馆在检索系统里贴一张"暂缺"标签——宁可目录难看，也不编一个假条目。诚实地弃权，和努力地修复，被当成了两件需要区分开的事：有些问题修不了，有些问题不该硬修。

👻 空真：自动证明的头号敌人

讲两个案例之前，必须先讲一个概念，它是理解 FARMS 的钥匙：vacuous truth，空真。

一个条件语句"如果 P，那么 Q"，当 P 根本没有为真的实例时，就空洞洞地为真。经典例子是"所有独角兽都是白色的"——真，因为独角兽不存在。这话在日常里是个段子，在数学证明里是个陷阱。

FARMS 抓出了一个具体到可怕的版本。拿随机低秩逼近定理来说：算法输出低秩逼近，其误差不超过最优 k 秩逼近误差的 1+ε 倍。这条定理里藏着一个前提——算法得真的能输出一个合法结果。FARMS 的陈述把这个前提写明：合法输出存在，且所有合法输出的误差都满足这个界。

而对比系统 AutoformBot 的语句级适配版做了什么？它保留了误差条件，却丢掉了"输出存在"。后果是灾难性的：如果算法在某些输入上根本构造不出合法输出，"所有合法输出的误差都满足界"就成了空真——合法的输出一个都不存在，全称量词扫过空集，自动为真。系统宣布"形式化成功"，而成功是假币。

打个比方：彩票站贴出"中奖者奖金翻倍"的规则，却根本没印那张中奖彩票。规则印得再漂亮，也没人中过奖。FARMS 坚持：中奖彩票必须真的印出来，不能只印中奖规则。

还要想清楚，这个陷阱为什么对计算数学格外致命。纯数学里，空真常常只是角落里的洁癖问题——某个退化情形没人关心，跳过就跳过了。计算保证不一样：它的全部用途是安抚一台正在运行的机器。AI 拿着定理去给迭代次数、误差、存储开销打包票，如果这个包票在"算法根本跑不出结果"的输入上自动生效，那这张保函就是白纸。后续的实验设计、超参选择，甚至经费决策，都会建立在虚假的"已被保证"之上。虚假的成功比诚实的失败危险得多——失败至少会叫出声，空真是静音的。FaithformBench 的报告早就指出，自动形式化器会默默把无效输入变成可证陈述；也有研究证明，基于编译的指标会系统性地高估形式化质量。编译通过和忠实原意之间有条沟，而 FARMS 整条流水线守的就是这条沟。

🔍 案例一：被弄丢的两行小字

第一个案例发生在那条随机低秩逼近定理上。初始候选形式化得很顺——编译通过，眼看要过关。语义评审员拦了下来：有两个情形被丢掉了。

情形一：A 是零矩阵，k 取 1。这时根本不存在合法输出——漏掉的是"k ≤ rank(A)"这条秩限制。没有它，算法在某些输入上空手而归，陈述还在旁边喊"保证成立"。

情形二：n 取 1。这时 α = k·log(n)/ε² 整个消失，源文本里的 log(α) 无定义；而 Lean 顺手定义了 log(0) = 0，编译器一声不吭地把未定义当成了 0，程序正常跑过。一个公式在其定义域之外的点被悄悄赋了值，像给一张过期的保修卡盖了"有效"章。

形式化器根据源文本的公式定义域，把两个条件补了回去，修订版通过。最终陈述只在两个地方宣告保证：算法真能产出合法输出、源公式真有定义。小字找回来了，保修卡才算完整。

这个案例的动人处在细节：两处错误都逃过了编译器——Lean 对 log(0) 的默认处理恰恰让错误代码"合法"。抓住它们只能靠语义评审，靠一个较真的角色对着原文问：你的意思是这个吗？真的是吗？

⚔️ 案例二：五十年后，教材被自己的学生逮个正着

第二个案例是全文的高潮，值得掰开揉碎讲。

随机矩阵乘法。教科书上的 claim 说：按范数加权采样——第 i 项被抽中的概率正比于"A 的第 i 列的范数"乘"B 的第 i 行的范数"——这个分布 p* 能最小化期望平方 Frobenius 误差，而且对一切可容许分布 q（每个 qᵢ 非负、总和为 1）都最优。

形式化器忠实地保留了原文声明的域，包括允许某些 qᵢ 取零。编译通过。

语义评审员盯着这个"对一切可容许 q"看了一会儿，然后构造了一个显式反例。矩阵小到可以写在手背上：

A = [1, 1]，B = [1, −1]ᵀ。只取一个样本。精确乘积 AB = 1×1 + 1×(−1) = 0。

现在看"最优"的范数分布 p* = (1/2, 1/2)：抽第一项时，贡献 CR = (1/(1/2))×1×1 = 2；抽第二项时，贡献 CR = (1/(1/2))×1×(−1) = −2，各以一半概率出现。期望平方误差 E(p*) = 4。

再看一个可容许的替代 q = (1, 0)：永远抽第一项，贡献确定是 CR = 1。E(q) = 1。

于是这个 claim 会要求 4 ≤ 1——号称对一切 q 最优的分布，输给了一个故意只抽一项的分布，输得干净利落。不可能。

独立的源评审确认了病根：无偏性论证需要一个条件——每个非零贡献的采样概率必须为正（只要 A 的第 i 列乘 B 的第 i 行不为零，qᵢ 就必须大于零）。这是原文缺失的条件。说穿了，这回错的是教材本身，形式化毫无问题。这个 claim 在文献里躺了不知道多少年，被一代代读者默认成立——直到一台机器在翻译它的时候，顺手把它审计了一遍。

流水线的处理很有分寸：没有偷偷把条件补上然后宣布一切正常，也没有因为出错就删掉这条陈述。它保留源 claim 的原样，把缺失条件记录为一条显式源警告（source warning），这次运行被记为未接受。这正是论文反复强调的精神：源 claim 与修复后 claim 之间的失配（miscalibration），必须可区分。读者和下游的 AI 得知道，这张保修卡是原厂出品、带着一道公示过的瑕疵，还是被悄悄换过内芯。

这里值得停一秒，掂掂这件事的分量。这个 claim 被应用了五十年，可能从没人在乎过 qᵢ = 0 的角落——人类专家凭直觉知道"非零贡献总得给它被抽到的机会"，谁也没想过要把这句常识写下来。AI 的工作方式是把每个字都当真，于是常识的空白被照得雪亮。这大概是自动形式化最反直觉的副产品：它在给人类知识做体检。

💰 便宜二十倍，还更较真

结果先看通过率：171 个目标，157 个被接受，91.8%——其中 154 个干净接受，3 个带着源警告接受。剩下的以弃权处理，理由记录在案。

成本更耐人寻味。四个来源平均每目标的花费分别是 $1.92、$0.85、$2.29、$2.08，含源准备、生成、评审、修复、续跑的全部开销。作为对照，在 6 个随机目标上，FARMS 总计花 $17.06、227.5 万 tokens；AutoformBot 的语句级适配版烧掉 $348.09、6307.1 万 tokens。摊到每个目标：$2.84 对 $58.02，差 20.4 倍；tokens 0.379M 对 10.512M，差 27.7 倍。

二十倍从哪来？我的理解是：语句级适配更像 brute-force 扫荡——把大片语料扔给模型反复重试，用 token 堆出能编译的句子；FARMS 把力气花在刀刃上，检索器按需回原文取证，每个角色只做一件事，有界循环防空转，语义评审把"编译能过但意思不对"的候选在早期拦下，省掉后面无数轮无效修复。较真居然更便宜——因为每一次较真都发生在最便宜的时刻。

再拆细一点。AutoformBot 那种工作方式，是把形式化当成纯搜索问题：给模型一大片候选语料，反复采样、反复编译、错了再试，token 像水一样流走，而大部分尝试死在同几处语义错误上。FARMS 反过来，把不确定性尽量消灭在进入生成之前——源审计先确定"要形式化的到底是什么"，检索只取需要的证据，共享领域库让后面的目标站在前面的肩膀上，生成只是最后一公里。再加上弃权机制：补不上的缺口不再无限续命，评审几轮确认后贴上标签存档，开销就此封顶。这条流水线的每一笔钱都对应一个具体的决策，很少烧给一炉报废的试验品。

🧰 把定理变成技能：一道热流，一根琴弦

形式化不止于收藏。论文最后展示了两个"技能化"应用：把 Lean 检验过的陈述变成 AI 可调用的技能，让保证链条机器可查。

先交代一下"技能化"到底改变了什么。过去的做法接近检索增强生成（RAG）：模型从论文里检索一段定理原文，凭语感判断"大概适用于当前问题"，然后直接用。风险藏在"大概"里——适用条件对不对、量词顺序变没变，全靠模型自觉。FARMS 走的是另一条路：定理连同全部条件被编译成一个蕴含关系（implication），前提是一组机器可检查的命题。agent 每次调用技能时，先机械地验证前提在当下这个问题里成立——矩阵的秩够不够、参数正不正、维度对不对——再引用结论；前提不过，技能拒绝生效。保证从"模型觉得没问题"升级为"编译器验证过没问题"。这一字之差，就是科学和猜测的分界。

第一道是稳态热流。方程 −(a_ηu′)′ = f，两端温度为零，传导系数对比度拉到 100 和 1,000（η 取 0.01 和 0.001）。离散化后 512 个未知数，加权梯度矩阵 8,192×512。用高斯 sketch（一种随机投影）把它压到 2,048 行，取 QR 因子作预条件子——预条件后的条件数落在 8.83 到 8.95 之间，而标准的对角预条件参照值是 99.6 和 964.0，差出一到两个数量级。全部 6 次运行（2 个对比度 × 3 个随机种子）在 22 次迭代内达到 10⁻⁶ 的相对离散能量误差。定理的保证落在实处：迭代数不随对比度恶化，这正是形式化过的那个界的形状。

第二道是波响应压缩。两端固定的弦，方程 u_tt = u_xx。384 个初始激励，构成 256 维能量坐标矩阵。用高斯采样选子空间，由精确的残差检查把关，最终选出 128 个基响应，残差界落在 0.00877 到 0.00938 之间，稳稳压在 0.01 的目标之下。32 个时间步的响应库，从 24 MiB 压到 8.375 MiB，砍掉近三分之二。

点睛之笔在最后一步：弦的能量守恒，把"初始表示误差"的界直接带到所有未来时刻。一次因子检查，管住所有允许的查询、所有非负的时刻，省去了逐时刻验收的麻烦——一纸保函覆盖全程。这就是"Lean 检验过的蕴含关系"作为技能的价值：AI 之后每做一次波响应查询，脚下踩的界都过了编译器这一关，而非从哪篇论文里顺手抄来的一句话。

🧭 三部曲之中：立法者与公证员

这是三部曲的第二篇。第一篇的主角是 AWM——AI 探索世界，从零立法，自己提出猜想再自己证明。FARMS 的气质与它同魂，姿势恰好相反：AWM 是立法者，FARMS 是公证员。人类的计算数学积累了上百年，写成几百本教材，可这些法律一直躺在纸上，靠一代代读者的默契维持效力。FARMS 做的，是把这套既有法律逐条登记入册、核对条款、公示瑕疵——给百年数学上户口。

两个角色缺一不可。没有立法者，世界没有新法可用；没有公证员，旧法的细则在翻译中悄悄丢失，整个体系就建在"大家默认懂"的沙地上。放到更大的图景里，这还是两种知识来源的互补：一边是人类几百年攒下、已经写成文字的定理，一边是机器自己探索出的新规律。前者的问题是细则藏得太深，后者的问题是没人替它背书。AWM 给后者立法，FARMS 给前者公证；两边的地基都打平之后，"AI 做科学"才算真正运转起来——既敢放心用旧知识，也敢认真立新知识。FARMS 最让人敬重的地方，是那种对自己狠的严谨：编译通过不算数，语义评审专门抓"编译通过但意思被偷换"的候选；修不了就诚实弃权，把"暂缺"标签贴在明处；抓到教材本身的缺陷，挂一块显式警告牌，不默默改掉，也不默默放过。

原文有句话我打算记住：源 claim 与修复后 claim 之间的失配，必须可区分。保修卡的细则丢了会被拒赔，而科学的细则丢了，连"被拒赔"的警报都不会响——这才是最可怕的事故。FARMS 把警报装上了。

定理还是那些定理，教材还是那四本。但从此 AI 拿着保修卡来索赔时，手里的细则是完整的；万一卡上真有瑕疵，牌子也挂在明处。这大概就是"可验证的自动化科学"该有的地基——先别急着盖楼，把每块砖的出厂证明都验一遍。

【参考文献】

• 论文标题：FARMS: A Verifiable Foundation for Automated Computational Science
• 作者：Di Wu（University of Maryland, Department of Mathematics）、Ling Liang（University of Tennessee, Knoxville, Department of Mathematics）、Haizhao Yang（University of Maryland, Departments of Mathematics and Computer Science，通讯作者）
• arXiv: 2610.40560（2026-10-29），https://arxiv.org/abs/2610.40560
• 代码：https://github.com/Woody2357/FARMS-Computational-Science
• 项目页：https://woody2357.github.io/FARMS-Computational-Science/

#论文 #arXiv #AI #小凯