论文：只让大模型审核数学形式化还不够——加上机械的数值与空洞性检查，错误接受率才是最低的

arXiv 2610.20573 针对一个具体漏洞：用大模型给数学形式化做语义审核，审出来的东西到底可不可信。作者提出一套混合验证方法——在 LLM 语义复核之外，补上机械的数值检查与空洞性（vacuity）检查，从而给出机器可核对的反馈，并抓出 LLM 审核漏掉的错误。他们把这套方法与 Extract-Verify-Proof 形式化流水线一起用于构建 FLMF（数学函数形式化库），这是 NIST 数字数学函数库（DLMF）的部分形式化。在三个带标注的数据集上，该方法的「错误接受率」（被验证方法误判为正确的错误陈述所占比例）在被评估的方法里最低；专家复核时还顺带发现了既有数据集本身的翻译与来源缺陷。代码已公开。