用确定性验证约束大模型推理

在围绕大语言模型（LLM）构建生产级软件时，工程师会面临一个根本问题：LLM 生成的输出往往结构合理、看似可信，却经常暗藏细微的幻觉或无效逻辑。在低风险应用中，人工抽查通常已经足够。但在金融引擎计算、基础设施部署脚本或科学证明等高风险场景中，随机输出必须与确定性验证机制结合使用。

2026 年 8 月 1 日，OpenAI 发布了《数学与理论计算机科学的十项进展》，介绍了借助代号为“Astra”的内部推理系统解决的十个长期未解难题。抛开其中的具体成果主张，这次发布还给出了一套清晰的可验证软件架构蓝图：使用随机模型探索复杂的搜索空间，同时将真伪检查交给确定性验证器。

Astra 案例研究：机器检查的数学成果

OpenAI 表示，其 Astra 模型的内部多 Agent 版本解决了十个数学与理论计算机科学问题，这些问题此前至少已有十年未能解决。OpenAI 并没有要求公众或同行评审者直接相信 LLM 的原始输出，而是发布了一份长达 249 页的技术论文、推理过程解析，以及名为 openai/ten-proofs 的公开 GitHub 仓库。该仓库包含使用 Lean 4 交互式定理证明器编写、可由机器检查的形式化证明。

这十项成果横跨多个不同领域：

高维几何： 建立了球体堆积密度的新渐近上界，该上界达到了 Cohn–Elkies 阈值，是自 1978 年以来这一指数上的首次重大进展。

群论与算子代数： 构造了第一个显式的非 sofic 群，解决了一个自 1999 年以来一直悬而未决的存在性问题；同时推翻了 Connes 关于 property-(T) 群和 von Neumann 代数的刚性猜想。

理论计算机科学： 证明了算术电路复杂度中计算 permanent 的新下界——具体而言，得到了 $\Omega(n^4 / \log n)$ 的公式下界；同时还证明了有限双人纠缠量子博弈的指数级并行重复定理。

组合数学与格密码学： 解决了 Erdős 问题 146、180 和 183，其中包括为多色三角形 Ramsey 数建立超指数下界；此外，还证明了欧几里得最近向量问题（CVP）的多项式因子困难性。

与以往的 AI 成果主张相比，这次发布体现出了一种结构性变化。2025 年 10 月，OpenAI 曾遭到质疑：数学家 Thomas Bloom 指出，GPT-5 生成的一项数学成果实际上只是检索到了既有文献，而不是提出原创证明。针对 Astra 的发布，Bloom 公开表示，可验证的 Lean 证书让这次成果成为一个性质截然不同的里程碑。

OpenAI 根据 Sol API 的费率估算，推理成本约为 2,000 美元。不过，研究员 Noam Brown 澄清说，这一数字只涵盖成功的搜索路径，并不包括失败尝试所消耗的算力。

信任边界：模型探索与确定性验证

产生这些成果的技术工作流展示了一条由三个阶段组成的人类与 AI 协作流水线：

生成（模型）： Astra 多 Agent 系统在数小时乃至数天的超长时间跨度内，自主运行推理循环，生成候选证明、数学构造和逻辑步骤。

阐释（人类 + 模型）： 人类研究人员与模型协作，将原始论证整理成结构清晰、可读的技术论文。

形式化（模型 + 验证器）： 模型把非形式化的数学陈述和证明步骤转换成形式化的 Lean 4 代码。Lean 编译器依据 Lean 的公理基础检查每一步推导。

在这条流水线中，信任边界得到了谨慎而明确的划分。LLM 从未被当作判断正确性的最终权威。相反，它的职责被限定为生成候选方案和执行转换，正确性则严格由确定性运行的 Lean 4 kernel 确立。

OpenAI 明确认可 Astra 生成了核心数学论证，并引用 2026 年 6 月发布的《AI 与数学莱顿宣言》，指出如果声称这些证明由人类完成，将会产生误导。

生成器与验证器：形式化验证为何重要

对于构建 LLM 应用的软件工程师来说，理解证明生成器与证明验证器之间的差异至关重要。

LLM 是一种随机生成器。它擅长跨越不同的概念领域——例如将代数数论应用到几何堆积问题中——并提出可能的解题结构。然而，它无法保证输出中完全不存在逻辑缺陷。

相比之下，Lean 4 是一个确定性的交互式定理证明器。其可信 kernel 会依据基本逻辑规则，检查给定的形式化证明是否正确地从前提推导出结论。Lean 编译器并不关心证明是如何生成的——无论出自人类、启发式脚本还是 LLM。它只负责验证证明字符串能否通过有效的类型检查，并确保其中没有使用未经证明的假设（sorry 占位符）。

当 LLM 输出的代码能够在 Lean 4 中顺利编译，并且不存在任何被跳过的证明缺口时，验证器便能保证该形式化陈述在逻辑上的正确性，从而有效消除这一特定证明产物中的 LLM 幻觉风险。

开发者可以借鉴什么

你不需要研究尚未解决的数学猜想，也能应用这种架构模式。任何高风险软件系统——例如自动化代码重构、基础设施即代码部署或金融计算引擎——都可以采用生成器—验证器设计。

将生成与验证解耦： 永远不要依赖 LLM 评估自己的输出。应当为 LLM 生成器配备外部的非 LLM 验证器，例如编译器、静态分析器、linter、单元测试套件或 schema 验证器。

以机器可检查的中间格式为目标： 要求模型使用能够被严格工具解析和执行的格式输出结果，例如 Lean 代码、TypeScript 定义、SQL 查询或 OpenAPI 规范，而不是仅仅给出自然语言解释。

在重试循环中使用编译器反馈： 实现多 Agent 反馈流水线，将验证器产生的错误日志——例如 Lean 构建错误或编译器类型错误——重新放入模型的上下文，让模型能够自动修正输出。

明确形式化规范的边界： 必须意识到，自动验证器只能检查某个产物是否满足给定的形式化规范。形式化规范是否真正符合底层业务需求或技术需求，仍然需要人类领域专家进行审查。

局限性与系统层面的注意事项

尽管 Astra 的成果展示了机器检查工作流的强大能力，但仍然存在几项重要的局限：

形式化与对齐缺口： Lean 证书可以确认一个结论在指定公理下逻辑有效，但无法保证 Lean 代码准确表达了原始的非形式化问题。要确认二者是否对齐，仍然需要人工审查。

无法评估新颖性： 形式化验证器无法判断一项成果是否具有原创性，也无法判断它是否只是根据已知引理推导出的结果。

不透明的算力指标： 2,000 美元的成本数据只覆盖成功的搜索路径，不包括失败的推理轨迹和前期实验。

系统尚未发布： Astra 仍然是一个未公开发布的内部研究系统。由于底层模型并不开放，开发者无法独立评测其原始、无引导状态下的生成性能。

通过将随机探索与确定性检查分离，OpenAI 的 Astra 成果为 AI 工程提供了一种实用范式：让语言模型负责探索各种可能性，但把最终裁决权交给严格的确定性系统。

如需采取进一步措施，你可以考虑屏蔽此人和/或举报其滥用行为。