AI 系统下一阶段的质量差距，正在从“能否给出一个像样答案”，转向“能否交出一条可检查、可拒绝、可复现的证据链”。这不是模型能力退居次席，而是模型开始进入科研、代码和深度检索之后，流畅表达已经不再是足够的质量标准。
最近出现的几组信号指向同一个变化：数学研究尝试把模型生成的证明交给形式化工具检查，Coding Agent 开始把规格与机器可验证证明放进开发流程，搜索 Agent 的评测则开始主动注入不可靠证据。它们共同补的是模型最薄弱的一层——让结论经得起外部验证，而不是继续依赖模型自我确认。
从“生成证明”到“验证命题”
一篇关于无导数凸优化的新预印本引发了广泛讨论。论文证明，在只能查询精确函数值的条件下，确定性算法需要接近二次规模的查询复杂度，把一个可追溯至 1996 年的上下界差距缩小到 polylog 因子。作者公开说明研究过程得到 GPT-5.6 辅助，并使用 Lean 做形式化验证。
这件事最值得关注的，不是给模型贴上“解决开放问题”的标签。真正可复用的是一条研究流水线：模型负责搜索思路、拆解引理和草拟证明；形式化语言把自然语言主张转换为精确定义；证明器只接受能够通过检查的步骤；研究者还必须额外确认，被证明的形式化命题没有悄悄偏离原问题。
因此，“Lean 通过”不是事实正确性的万能印章。它能保证形式系统内部的推导成立，却不能自动保证前提选得合理、命题忠实对应研究问题。这恰好说明可验证 AI 的核心不是增加一个验证按钮，而是把结论、规格、证据和验证器之间的映射全部暴露出来。
代码 Agent 需要独立裁判，而不是更多自信
同样的变化正在进入软件开发。开源项目 Forall 尝试让 Coding Agent 同时生成规格驱动的代码与机器可检查证明，并提供 verify-only 的 MCP 接口，可接入 Cursor、Claude Code 和 Codex 等既有工作流。它的产品意义不在于替换所有测试，而在于把“生成者”和“裁判”分离：模型可以提出实现，确定性工具负责拒绝不满足规格的结果。
这对权限系统、计费逻辑、协议解析和状态机尤其重要。传统单元测试只能覆盖列举出来的样例，机器证明则有机会检查更一般的不变量。但边界仍然明确：错误规格也可以被正确证明。可靠工作流应当是规格评审、机器证明、属性测试、集成测试与人工审查的叠加，而不是用一种新工具替代全部质量控制。
验证还要覆盖证据环境
深度研究 Agent 面临的风险不同：它未必推理错误，而可能从一开始就拿到了低质量材料。DeepStress 提出用可控合成环境替换检索模块，分别调节证据的可信度、相关性和事实性，再观察搜索 Agent 面对冲突、误导或不可靠信息时如何失效。
这比只在干净 benchmark 上统计最终准确率更接近真实工作。公开网络中充满过时页面、SEO 内容、二手转述和彼此冲突的一手来源。一个研究 Agent 即使能检索更多页面，也可能只是更高效地积累错误。产品团队因此需要记录来源层级、发布时间、冲突点、被排除证据和结论置信度，并把“遇到证据污染时能否降级表达”纳入验收。
对工作流意味着什么
对科研团队，模型输出应拆成自然语言结论、结构化中间表示、独立验证结果和命题对齐检查；对软件团队，高风险变更应先定义可验证的不变量，再让 Agent 编码；对研究与情报团队，评测集应主动加入过时、矛盾和高相关假证据，而不是只测试理想检索环境。
我的判断是，未来高价值 Agent 的护城河不会只是“更会回答”，而是能否稳定地产生可追溯证据，并允许外部系统明确地说“不”。当生成成本快速下降，真正稀缺的将是可信的拒绝机制：什么被验证了、由谁验证、验证覆盖了哪些边界，以及失败后能否回到具体步骤重新处理。