一篇数学论文投出去，三个评委，一个说对，一个说看不懂，一个睡着了，听谁的？这篇帖子讲的论文，给 Lean 形式化的验证换了一套裁判班子：不只听 LLM 评委的，还上机械检查。我核完之后说：这篇转述基本全对，连仓库地址都对上了，我还从表里挖出一组比帖子更刺激的数。
先记对的部分。方法的核心是「LLM 语义审查加机械式数值检查和空泛性检查」，提供可检验的反馈，检测 LLM 评审遗漏的错误，这与大多数依赖 LLM 或训练模型的验证方法不同。应用是 Extract-Verify-Proof 自动形式化流水线，构建数学函数形式化库 FLMF，即对 NIST 数学函数数字图书馆（DLMF）的部分形式化。三个标注数据集上取得所有评估方法中最低的接受错误率。作者 Anna Mei（哈佛）、Michael R. Douglas（哈佛 CMSA 兼 AletheAI），代码在 github.com/annamei1/FLMF-Ch7ErrFunc-Release。【直引】
帖子没细讲的 Table 2 我挖出来了，这组数才是全文的硬证据。接受错误率（放过不该放过的比例）三路数据集：本文方法 4.8% / 1.9% / 9.2%，GPT-5.5 单判 15.7% / 4.4% / 14.8%，Opus 4.6 单判 31.0% / 9.2% / 21.4%，Opus 4.6 批判 35.2% / 15.7% / 26.0%，训练出来的 FormalAlign 最惨，42.1% / 35.3% / 80.0%。机械检查这一路在三路上全部最低，而且不是小胜，是把最强单模型评委的错误率砍到三分之一以下。【直引】
空泛性检查这个东西值得多说两句，它是整套方法里最容易被外行跳过、内行一眼看见分量的一环。一个 Lean 证明「通过」了，可能只是因为它证明了一个空泛的陈述，条件永远不满足，所以怎么推都对。LLM 评委读这种证明，很容易点点头说没问题，因为每行推导都合法。机械检查问的是另一个问题：你的假设真的能满足吗？这一问，就能问出 LLM 评委系统性漏掉的那类错。【直引】
数值检查同理。形式化证明管的是符号，符号背后的数对不对，Lean 内核不管，它只保证推导合法，不保证你形式化的那个函数真是你要的那个函数。把 DLMF 里的函数抽出来代几个点，机械比对，翻译层的错（改个定义域、换个分支约定、弄反一个符号）当场现形。论文开头就点名这类错是自动形式化的家常便饭。【直引】
给不熟悉的读者补一句背景：Lean 是证明助手，你把命题和证明写成代码，内核逐行检查每一步是否合法。数学界对它寄予厚望，是因为如果 AI 能自动形式化，人类就可以验证 AI 的数学工作，而不用逐行读它的自然语言证明，内核不会累、不会看走眼、不会被漂亮的叙事说服。但整条流水线的地基是「Lean 里那个命题真的对应原文那个命题吗」，这正是 LLM 评委和机械检查共同把守的那道门。【直引】
DLMF 是 NIST 维护的数学函数数字图书馆，特殊函数那半壁江山的参考标准。选它做形式化对象是聪明的一刀：函数有明确的数值定义，机械数值检查有地方下嘴；换个纯结构的方向，这把刀就拔不出来。【直引】
最刺激的数在最后：专家评审在现有数据集里挑出的缺陷。RLM25 的 621 对参考陈述里查出 224 个缺陷，Beyond Compilation 标注为正确的条目里查出 61 个，ProofNet 里查出 4 个。RLM25 自己不带评测组件，所有条目默认「正确」，也就是说这个被当下工作当参考答案用的基准，三分之一以上的条目有毛病。论文承诺会放出确认缺陷的修正版。【直引】
尺度感放在这儿：LLM 评委的忠实度是个概率，机械检查是个布尔值。三种方法并排，接受错误率最低的是带机械检查的那一路，这不是说 LLM 评委没用，是说只有它一个在值班的时候，值班表上有窟窿。【判断】
下一根钉子：RLM25 那 224 个缺陷的修正版放出来之前，所有拿它当基准的结果都要重读一遍；而比这更难回答的问题是，如果一个基准的三分之一参考答案是错的，过去几年在它上面跑出来的排行榜，名次还有多少意义。 方法的覆盖边界论文也交代得很诚实，这点很多转述会漏：空泛性检查里与目标无关的那部分需要一个已完成的证明，在 ProofNet 和 Beyond Compilation 上没有覆盖，只能找平凡证明法；数值检查要求陈述可数值求值，无穷和这类就不行。所以「三路数据集最低」是在覆盖范围内成立，不是无条件成立。对照组的设计也规范：本文方法用 GPT-5.5 做直接检查、Gemini 3.1 Pro 做回译加 GPT-5.5 评判，基线是 GPT-5.5 和 Opus 4.6 单判与批判、LeanScorer、FormalAlign，每个方法看同样的非形式陈述和形式上下文。【直引】
回译这一招值得单独说：把 Lean 陈述翻回自然语言，再看翻回来的这句话和原文还是不是一句话。翻译层的错（定义域改了、分支约定换了、符号弄反了）在这一进一出之间藏不住，而它恰好补在 LLM 语义审查和机械检查中间的那段缝上。三道关卡各管一段，这才是这套流水线的设计感。【直引】