CS336 · 第 18 课

Guest Lecture：Daniel Selsam

形式化验证、程序合成与 LLM：当语言模型遇到绝对正确性。Daniel Selsam 分享形式化方法如何为 AI 系统提供数学级别的保证。

本讲问题：LLM 可以生成程序、证明和数学步骤，但语言流畅不等于正确；本讲关注怎样把 verifier 放进生成循环，让错误能够被机械检查并反馈。

informal intent → formal specification
                         ↓
generator → candidate proof/program → verifier
     ↑                           pass / diagnostic
     └──────── search / repair ────────┘

verifier soundness + specification coverage
→ define what “verified” actually guarantees

关于讲者

Daniel Selsam 是形式化验证和程序合成领域的研究者。他参与创建了 Lean 定理证明器，并致力于将形式化方法应用于 AI 系统。他的工作横跨：

• Lean 定理证明器：开源的形式化数学和验证平台
• 程序合成 (Program Synthesis)：从规范自动生成程序
• 形式化验证：数学证明程序/系统的正确性
• AI for Math：用 AI 辅助形式化推理

形式化验证基础

什么是形式化验证？

传统测试：运行程序，检查输出是否正确。只能证明存在 bug，不能证明没有 bug。

形式化验证：用数学方法证明程序满足规范。可以证明不存在特定类型的 bug。

# 例: 排序函数的规范

# 传统测试:
def test_sort():
    assert sort([3, 1, 2]) == [1, 2, 3]
    assert sort([]) == []
    assert sort([1]) == [1]
    # 测试通过 ≠ 所有输入都正确

# 形式化验证 (Lean 风格):
def sort (list : List Nat) : List Nat := ...

theorem sort_is_sorted (list : List Nat) :
  sorted (sort list) := by
  -- 证明: sort 的输出总是有序的
  ...

theorem sort_is_permutation (list : List Nat) :
  Permutation list (sort list) := by
  -- 证明: sort 的输出是输入的排列（没有丢元素）
  ...

Lean 定理证明器

Lean 是一个开源的编程语言和证明助手：

• 可以写程序、定义数学概念、陈述定理、构造证明
• 内核极小（trusted kernel），所有证明都被严格检查
• Mathlib：最大的形式化数学库之一（包含数万条定理）
• 被 AWS（Cedar 授权语言）、Google DeepMind（AlphaProof）等使用

形式化验证 vs 测试

程序合成

什么是程序合成？

从高层规范自动生成程序。LLM 是程序合成的一种实现方式。

LLM 用于程序合成

现代 LLM（如 Codex、DeepSeek-Coder）可以进行程序合成：

• 从自然语言描述生成代码
• 从类型签名推断实现
• 从测试用例反推实现

Verification-Guided Generation

核心思想

将 LLM 的生成能力与形式化验证的保证能力结合：

# Verification-Guided Generation:
#
# 1. LLM 生成候选程序
# 2. 形式化验证器检查正确性
# 3. 如果不通过，反馈给 LLM 重新生成
# 4. 重复直到通过或超时

# 伪代码:
def verify_guided_generate(spec, max_attempts=10):
    for attempt in range(max_attempts):
        # LLM 生成
        code = llm.generate(spec)

        # 验证器检查
        result = verifier.verify(code, spec)

        if result.is_valid:
            return code  # 通过！

        # 不通过，反馈错误信息
        feedback = result.error_message
        llm.add_feedback(feedback)

    return None  # 所有尝试都失败

优势

• 正确性保证：输出的代码被验证器证明是正确的
• 错误反馈：验证器可以指出哪里错了，帮助 LLM 改进
• 组合性：可以组合多个已验证的组件

挑战

• 规范难题：如何形式化"写一个排序函数"这样的自然语言需求？
• 验证成本：形式化验证可能非常耗时
• LLM 生成证明：让 LLM 生成可验证的证明仍然很困难
• 搜索空间：可能的程序空间巨大，LLM 可能找不到正确的

AI for Mathematics

AlphaProof (Google DeepMind)

AI 系统在数学竞赛中取得突破：

• 用 Lean 形式化数学问题
• LLM 生成证明候选
• Lean 验证证明是否正确
• 在国际数学奥林匹克 (IMO) 中获得银牌水平

Lean 作为验证平台

# Lean 在 AI for Math 中的角色:

# 1. 形式化问题陈述
-- 例: 费马大定理
theorem flt (n : Nat) (hn : n ≥ 3)
  (a b c : Nat) (ha : a > 0) (hb : b > 0) :
  a^n + b^n ≠ c^n := by
  -- ...
  sorry  -- 这里放证明

# 2. LLM 生成证明步骤
# 3. Lean 检查每一步是否正确
# 4. 如果所有步骤都通过，定理被证明

形式化数学库 (Mathlib)

• 包含数万条形式化定义的数学概念和定理
• 从基础（集合论、代数）到前沿（代数几何、分析）
• 社区驱动，持续扩展
• 为 AI 系统提供"已知知识"的基础

验证 LLM 输出

为什么需要验证 LLM？

LLM 在许多场景中被使用，其中错误代价很高：

• 代码生成：bug 可能导致安全漏洞
• 数学推理：错误推理导致错误结论
• 法律/医疗：错误建议可能导致伤害
• 金融：错误交易可能导致损失

验证方法

LLM 输出的形式化验证

# 例: 验证 LLM 生成的排序算法

# Step 1: LLM 生成代码
code = llm.generate("写一个快速排序")

def quicksort(arr):
    if len(arr) <= 1:
        return arr
    pivot = arr[0]
    left = [x for x in arr[1:] if x <= pivot]
    right = [x for x in arr[1:] if x > pivot]
    return quicksort(left) + [pivot] + quicksort(right)

# Step 2: 形式化规范
# 规范 1: 输出是有序的
# 规范 2: 输出是输入的排列
# 规范 3: 时间复杂度 O(n log n) 平均

# Step 3: 验证
# 用 Lean/Coq/Isabelle 证明代码满足规范
# 如果验证通过 → 数学保证正确

未来方向

1. LLM + 证明助手

让 LLM 直接生成形式化证明，由证明助手验证：

• LLM 生成证明步骤
• 证明助手检查每一步
• 错误反馈帮助 LLM 改进

2. 神经符号方法

结合神经网络（LLM）和符号推理（证明助手）：

• LLM 负责"直觉"和"搜索"
• 符号系统负责"验证"和"推理"
• 两者互补，取长补短

3. 可验证的 AI 系统

构建可以数学证明其行为正确的 AI 系统：

• 安全边界：证明 AI 不会做某些事
• 鲁棒性：证明 AI 对扰动的稳定性
• 公平性：证明 AI 不会对特定群体歧视

4. 形式化 LLM 行为

用形式化方法描述和验证 LLM 本身的行为：

• LLM 的哪些行为是可以证明的？
• 如何形式化"helpful, harmless, honest"？
• 能否证明 LLM 不会产生某些输出？

知识检查

如果只能记住 5 件事

延伸阅读