Formal Verification (形式化验证)

定义

Formal Verification 是使用形式化方法（如一阶逻辑、集合论）来验证数学证明或计算机程序正确性的过程。

历史背景

数学传统上有客观的证明标准：

从欧几里得到二十世纪初的基础
尽管如此，人类数学家的论证通常不达到完美严格的理想
错误是常见的，有些被修正，有些成为 "folklore"

形式化验证的局限

terence-tao 在其论文中指出了形式化验证的两个关键局限：

1. 翻译问题

Formal verification only certifies that a formalized argument establishes a formal mathematical statement, but does not rule out errors in translation between the formal statement and the original intended statement.

Example (陶哲轩的费马大定理例子)：

费马大定理断言：对于 $n > 2$，方程 a^n + b^n = c^n 没有自然数解
隐含假设：自然数从 1 开始，而非 0
如果 AI 错误地允许 a, b, c 为 0，可能"证明"费马大定理是错误的！

2. 无法捕捉 "Penumbra"

即使形式化验证可以确保推理的正确性，它无法捕捉：

Heuristics 启发式 - 为什么这个方法有效
Motivation 动机 - 为什么要研究这个问题
Context 背景 - 如何广泛地理解这个结果
Narrative 叙事 - 证明的策略和构思

AI 时代的意义

terence-tao 认为：

AI 可以自动化形式化证明的生成
但这可能产生 "odorless proofs"（无味证明）：技术上正确，但缺乏启发性
人类数学家需要专注于那些不容易自动验证的方面

关联页面

tao-klowden-ai-mathematical-methods - 详细讨论
terence-tao - 该概念的主要阐述者
automated-theorem-proving - 论文提及的大型形式化数学库
spurious-predictability - "气味测试"概念

2.1 KiB Raw Blame History Unescape Escape