55 lines
2.1 KiB
Markdown
55 lines
2.1 KiB
Markdown
---
|
||
title: "Formal Verification (形式化验证)"
|
||
created: 2025-04-15
|
||
updated: 2025-04-15
|
||
type: concept
|
||
tags: [concept, mathematics, logic, ai-mathematics, verification]
|
||
sources: [raw/papers/tao-ai-mathematical-methods-2026.md]
|
||
---
|
||
|
||
# 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]] - "气味测试"概念
|