别信任 AI：构建验证循环的架构设计

不要要求 AI 完全正确：建立验证循环

AI 不需要完全可信，只要它的重要输出是独立可验证的。

大语言模型在长链推理上的能力日益增强。

它们可以探索数学问题、编写复杂软件、构造科学假设，还能作为自主 agent 在长时间内运行。

但是在所有这些进展的底层，隐藏着一个根本的工程问题：

我们如何知道模型什么时候出错？

对于聊天机器人，错误的答案可能只是不便。

对于自主研究 agent，错误的证明、不安全的代码改动或虚假的科学结论可能成为系统级故障。

解决方案可能不是另一层 prompt。

可能是一个不同的架构。

传统工作流的问题

传统的 LLM 工作流是这样的：

Problem
   ↓
LLM
   ↓
Answer
   ↓
Human judgment

问题很明显。

最后的验证步骤通常是：

"这个答案看起来有说服力吗？"

这不是验证。

更强的架构

更强的架构将生成与接受分离：

flowchart TD
    A[Problem] --> B[LLM Reasoning]
    B --> C[Candidate Solution]
    C --> D[Human / AI Formalization]
    D --> E[Formal Artifact]
    E --> F[Machine Verification]
    F --> G{Valid?}
    G -->|Yes| H[Verified Artifact]
    G -->|No| I[Failure / Repair]
    I --> B

模型生成可能性。

形式化层将这些可能性转换为显式的制品。

验证器决定该制品是否通过形式检查。

这是一个根本上不同的信任模型。

Astra 和流水线模式

最近关于 OpenAI 下一代主要模型族（代号 Astra）的报道，吸引了人们对一个涉及推理、人类形式化和机器验证的流水线所产生的数学结果的注意。

这篇文章的重要问题不是独立实现是否能重现 Astra 本身。

模型还未发布，重现其报告的数学结果需要访问底层系统。

有趣的研究对象是流水线模式。

报告的结构可以表示为：

┌──────────────────────┐
│      Reasoning       │
│        LLM           │
└──────────┬───────────┘
           ↓
┌──────────────────────┐
│    Formalization     │
│    Human + AI        │
└──────────┬───────────┘
           ↓
┌──────────────────────┐
│     Verification     │
│      Lean 4          │
└──────────┬───────────┘
           ↓
     Certificate

这个区分很重要。

我们是在复制循环的形状，而不是模型。

LLM 的根本限制

LLM 是概率生成器。

即使推理轨迹看起来严谨，严谨的表象本身不是正确性的证据。

LLM 可能会：

跳过必要的假设

做出无效的代数变换

将相关性与因果关系混淆

生成看起来正确但在边界情况下失败的代码

增加模型的推理预算可能会改善性能。

它不会消除根本问题。

模型仍然是一个生成器。

新的工程要求

所以与其要求：

"永远不要犯错。"

我们改为要求：

"错误必须在接受之前被检测到。"

这是一个更可扩展的工程要求。

为了探索这个架构，一个小的三阶段项目可以使用现有模型和 Lean 复制流水线结构。

该原型刻意避免声称能重现 Astra 的能力。

其目的是衡量循环本身的工程权衡。

实现架构

该架构包括：

stage1_reasoning.py
        │
        ▼
   Candidate trace
        │
        ▼
stage2_formalize.md
        │
        ▼
    .lean proof
        │
        ▼
stage3_verify.py
        │
        ▼
 PASS / FAIL / SKIPPED
        │
        ▼
     report.py

该项目记录成功和失败。

一个只记录成功结果的验证系统很容易变成一个成功报告系统，而不是验证系统。

阶段一：生成候选

第一阶段要求 LLM 生成候选解。

最小实现可以是这样的：

from anthropic import Anthropic

client = Anthropic()

problem = """
Prove that the sum of the first n positive integers
is n(n+1)/2.
"""

response = client.messages.create(
    model="YOUR_MODEL",
    max_tokens=2000,
    messages=[
        {
            "role": "user",
            "content": problem
        }
    ]
)

print(response.content[0].text)

这个输出还不是一个证明。

这个区分在系统架构中应该是明确的。

流水线应该将其视为：

LLM 输出 = 候选

而不是：

LLM 输出 = 真理

阶段二：形式化

下一步将非形式的推理转换为形式制品。

这刻意是人在环中的。

因为自然语言是欠定义的。

考虑以下区别：

"这个序列显然通过归纳法成立。"

和一个明确定义以下内容的形式证明：

• 归纳假设
• 变量范围

形式化将隐藏的假设公之于众。

结果可能变成一个 Lean 定理，例如：

theorem sum_first_n (n : Nat) :
  2 * (∑ k in Finset.range (n + 1), k) = n * (n + 1) := by
  ...

确切的证明在这里不如架构转变重要：

自然语言论证
          ↓
形式命题
          ↓
机器可检查的制品

现在制品到达信任边界。

Lean 没有被要求：

"这个解释听起来合理吗？"

它被要求检查一个形式证明。

阶段三：验证

一个简单的验证包装器可以显式地处理结果：

import subprocess

result = subprocess.run(
    ["lake", "env", "lean", "proof.lean"],
    capture_output=True,
    text=True
)

if result.returncode == 0:
    print("PASS")
else:
    print("FAIL")
    print(result.stderr)

重要的不是 Python。

重要的是状态机。

             ┌──────────┐
             │ Candidate│
             └────┬─────┘
                  ↓
             ┌──────────┐
             │ Formalize│
             └────┬─────┘
                  ↓
             ┌──────────┐
             │  Verify  │
             └────┬─────┘
                  ↓
       ┌──────────┴──────────┐
       ↓                     ↓
     PASS                   FAIL
       ↓                     ↓
  Certificate             Repair

还有第三个状态，它出奇地重要：

SKIPPED

如果 Lean 没有安装，系统不能报告：

VERIFIED

它应该报告：

SKIPPED_NO_LEAN_INSTALLED

未知不是成功。

这是核心设计原则。

验证边界

LLM 在一个概率环境中运行。

验证器定义了一个边界，在这个边界之外，一个制品必须满足明确的规则。

flowchart LR
    subgraph P[Probabilistic Layer]
        A[LLM]
        B[Search]
        C[Agent]
        D[Reasoning]
    end

    subgraph V[Verification Boundary]
        E[Formal Specification]
        F[Lean / Compiler / Tests]
    end

    subgraph T[Trusted Output]
        G[Verified Artifact]
    end

    A --> E
    B --> E
    C --> E
    D --> E
    E --> F
    F --> G

这个模式可以变得远比简单地增加模型智能更强大。

验证器不一定是 Lean。

架构可以是领域特定的。

LLM
 ↓
Code
 ↓
Compiler
 ↓
Static Analysis
 ↓
Tests
 ↓
Validated Build

AI
 ↓
Threat Hypothesis
 ↓
Formal Constraints
 ↓
Sandbox / Testing
 ↓
Security Decision

AI
 ↓
Scientific Hypothesis
 ↓
Simulation
 ↓
Statistical Validation
 ↓
Experimental Confirmation

Agent
 ↓
Plan
 ↓
Policy Constraints
 ↓
Execution
 ↓
Observed Outcome
 ↓
Validation

实现会改变。

原则不会。

API 契约观点

还有另一种思考这个架构的方式。

验证器可以被视为 API 约定。

LLM 被允许返回：

{
  "type": "candidate",
  "artifact": "...",
  "confidence": 0.87
}

但系统不会仅仅因为信心度高就接受候选。

它必须最终产生类似这样的内容：

{
  "type": "verified_artifact",
  "status": "PASS",
  "verifier": "Lean",
  "proof_hash": "..."
}

这在以下方面创建了清晰的分离：

• LLM 产生的候选制品
• 已验证的制品

这些不是同一回事。

一个模型可以 99% 确信但仍然是错误的。

一个已验证的制品可以被接受，而无需验证器理解模型为什么确信。

衡量流水线

如果这个架构将成为一个严肃的研究方向，仅有的基准准确性是不够的。

我们需要衡量整个流水线。

推理 token
API 成本
尝试次数
形式化时间
人类干预
验证时间
修复迭代
证明大小
验证结果
失败类别

一个有用的实验表可能包含这些指标。

现在我们可以提出更好的问题。

不是：

"哪个模型更聪明？"

而是：

"哪个系统最有效地产生已验证的制品？"

成本分析

一个报告的 API 成本，例如：

$200 / problem

不足以描述验证流水线的经济学。

实际成本应该包括：

推理
+
人类形式化
+
验证计算
+
失败的尝试
+
修复迭代

一个更有意义的度量是：

总验证成本
────────────────────
成功验证的问题

当人类干预很大时，这变得特别重要。

一个花费 20 美元推理但需要两小时专家形式化的系统可能实际上不比花费 100 美元推理但只需要五分钟人类干预的系统便宜。

故障分类

这个架构最强的属性之一是故障变得可衡量。

不是这样：

AI 失败了。

而是这样：

GENERATION_FAILURE
FORMALIZATION_FAILURE
TYPE_ERROR
PROOF_FAILURE
MISSING_LEMMA
RESOURCE_LIMIT
VERIFIER_UNAVAILABLE

这给了我们一个更有信息的研究循环。

flowchart TD
    A[Problem] --> B[Generate]
    B --> C[Formalize]
    C --> D[Verify]
    D --> E{Result}

    E -->|PASS| F[Verified]
    E -->|Proof Failure| G[Repair]
    E -->|Formalization Failure| H[Reformulate]
    E -->|Generation Failure| I[Regenerate]
    E -->|Verifier Unavailable| J[SKIPPED]

    G --> B
    H --> C
    I --> B

系统变成一个实验工具，而不仅仅是一个 AI 包装器。

科学谨慎

科学谨慎在这里很重要。

该原型没有声称：

• 重现 Astra 的模型架构
• 重现其报告的数学结果
• 匹配其推理能力
• 建立等效的成本-性能
• 独立验证关于 Astra 的所有外部声称

它复制了验证循环架构。

那是一个更窄——也更可防御的——声称。

优化目标的转变

多年来，AI 进展主要围绕以下框架：

更大的模型
      ↓
更多计算
      ↓
更多推理
      ↓
更好的答案

另一个范式是可能的：

更好的生成器
      ↓
更好的候选制品
      ↓
更好的验证
      ↓
更好的修复循环
      ↓
更可信的系统

模型仍然极其重要。

但它不再是整个系统。

这改变了优化目标。

与其最大化：

每个参数的智能

我们可以开始思考：

每单位计算和人类工作的已验证能力

这是一个更有趣的系统问题。

未来的研究 Agent

想象一个未来的研究 agent。

它收到一个科学目标。

它生成假设。

它编写模拟。

它提出数学论证。

它测试自己的假设。

每个重要的制品必须跨越验证边界才能成为系统可信状态的一部分。

flowchart TD
    A[Research Objective] --> B[AI Research Agents]

    B --> C[Hypotheses]
    B --> D[Mathematical Arguments]
    B --> E[Code]
    B --> F[Simulations]

    C --> G[Evidence / Validation]
    D --> H[Formal Proof]
    E --> I[Compiler + Tests]
    F --> J[Statistical Validation]

    G --> K[Trusted Research State]
    H --> K
    I --> K
    J --> K

这不是一个聊天机器人。

它更接近一个面向验证的研究操作系统。

核心思想

核心思想可以用一句话总结：

不要让概率系统负责完全正确。让它们负责生成可独立检查的制品。

这不会消除幻觉。

它改变了它们的后果。

一个错误的假设可以被拒绝。

一个失败的证明可以被修复。

损坏的代码可以测试失败。

一个无效的计划可以被约束阻止。

系统变得能够说：

"我无法验证这个。"

或者，更重要的是：

"我不知道。"

这可能是自主 AI 系统能拥有的最重要的能力之一。

从理论到实验

下一步不是另一个理论图。

它是实验。

一个严格的评估应该：

• 选择一个受控问题集
• 生成多个独立候选解
• 记录确切的 token 使用和成本
• 测量人类形式化工作量
• 将候选转换为形式制品
• 运行 Lean 验证
• 记录每个失败模式
• 测量修复迭代
• 计算总验证成本
• 发布可重现的制品和结果

到那时，验证循环变得可衡量。

一旦它变得可衡量，我们可以开始优化它。

下一代的定义

下一代 AI 可能不仅由模型能推理多少来定义。

它可能由模型推理之后发生的事情来定义。

未来的架构可能是：

AI 生成。
人类结构化。
机器验证。
系统从失败中学习。

这是一个对可信 AI 的不同设想。

不是永不出错的 AI。

而是一个 AI 系统，在这个系统中，重要的错误很难被不经意地接受。

这可能是朝向可靠的长链推理智能的一条更现实的道路。

设计原则

本文中描述的原型围绕以下原则设计：

• 确定性验证
• 明确的失败状态
• 成本和 token 仪表化

实现在架构层级上是有意的与提供商无关。

模型可以改变。

验证边界保持不变。

由 Seyed Alireza Alhosseini Almodarresieh 创建