---
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]]