37 lines
1.5 KiB
Markdown
37 lines
1.5 KiB
Markdown
---
|
||
title: "自动形式化（Autoformalization）"
|
||
created: 2026-07-03
|
||
updated: 2026-07-03
|
||
type: concept
|
||
tags: ["mathematics", "formal-verification", "nlp", "lean"]
|
||
sources: ["arxiv:2606.03303"]
|
||
---
|
||
|
||
# 自动形式化
|
||
|
||
> 将自然语言数学证明自动翻译为机器可验证的形式化证明——弥合「非形式化推理」与「形式化验证」之间的鸿沟。
|
||
|
||
## 核心定义
|
||
|
||
**自动形式化** (Autoformalization) 是将人类可读的自然语言数学论证转化为 [[lean-proof-assistant|Lean]] 等 [[formal-theorem-proving|形式化定理证明]] 系统中的可验证代码。这是 LLM 在数学领域最具挑战性的任务之一。
|
||
|
||
## 挑战
|
||
|
||
- **语义鸿沟**：自然语言中的直觉跳跃无法直接对应形式化逻辑步骤
|
||
- **单次生成困难**：即使 LLM 能理解数学概念，一次性生成正确的形式化证明仍极难（[[leap-agentic-atp|LEAP]] 论文显示 direct formalization 在 Putnam 2025 上全军覆没）
|
||
- **反馈需求**：自然语言证明翻译为 Lean 后，Pass@128 的 Advanced 组得分仅 3.3%
|
||
|
||
## LEAP 的解法
|
||
|
||
[[leap-agentic-atp|LEAP]] 不依赖单次自动形式化，而是：
|
||
1. 先生成**非正式蓝图**（策略层面），再逐步翻译为 Lean
|
||
2. 利用编译错误反馈迭代修正
|
||
3. 将复杂问题分解为更小的子目标（[[blueprint-driven-atp|蓝图驱动]]）
|
||
|
||
## 参考
|
||
|
||
- [[formal-theorem-proving|形式化定理证明]]
|
||
- [[lean-proof-assistant|Lean 证明助手]]
|
||
- [[leap-agentic-atp|LEAP]]
|
||
- [[blueprint-driven-atp|蓝图驱动 ATP]]
|