---
title: "非正式-形式化交错规划（Interleaved Informal-Formal Planning）"
created: 2026-07-03
updated: 2026-07-03
type: concept
tags: ["theorem-proving", "planning", "llm", "lean"]
sources: ["arxiv:2606.03303"]
---

# 非正式-形式化交错规划

> LLM 擅长非正式推理和策略生成，Lean 擅长严格验证——交错规划让二者各司其职。

## 核心定义

**非正式-形式化交错规划** 是 [[leap-agentic-atp|LEAP]] 的设计原则：在每个证明步骤中，先以自然语言做策略规划，再翻译为形式化 Lean 代码。这利用了 LLM 和 Lean 的互补优势。

## 两条路径中的体现

### 直接证明路径

1. LLM 生成**非正式论证**（自然语言）→ 翻译为 Lean 候选证明
2. Lean 编译器验证 → 失败则 LLM 修正非正式论证 → 重新翻译

### 分解路径（[[blueprint-driven-atp|蓝图驱动]]）

1. LLM 生成**非正式蓝图**（说明如何归约为子目标）
2. 翻译为 Lean 证明草图 → 记录依赖关系
3. 每个子目标递归进入非正式 → 形式化循环

## 为什么需要交错

- 形式化代码直接生成极脆弱：一步错误整个证明报废
- 非正式草图提供**规划空间**——在形式化之前先理顺策略
- 可解释性：每个形式化尝试都有对应的非正式理由，方便审查

## 参考

- [[leap-agentic-atp|LEAP]]
- [[blueprint-driven-atp|蓝图驱动 ATP]]
- [[autoformalization|自动形式化]]
- [[verification-guided-proof-search|验证引导证明搜索]]