Towards a Common Framework for Autoformalization¶

会议: AAAI 2026
arXiv: 2509.09810
代码: 无
领域: 人体理解
关键词: autoformalization, 形式化, LLM, 语义解析, 形式验证

一句话总结¶

本文系统回顾了"自动形式化"（autoformalization）在数学证明、逻辑推理、规划和知识表示等领域的现有工作，提出了一个统一的跨学科定义框架，将自动形式化定义为从非形式语言到形式推理语言的语义等价转换，旨在促进不同研究社区间的方法共享并加速下一代 AI 推理系统的发展。

研究背景与动机¶

问题定义¶

自动形式化（autoformalization）最初在 2018 年被引入，指使用交互式定理证明器（如 Isabelle/HOL、Lean、Rocq、Mizar）将非形式数学自动转化为可机器验证的形式语言。随着 LLM 的快速发展，该术语已超越数学领域，泛指将自然语言输入转化为形式逻辑表示的更广泛任务。

核心矛盾¶

尽管自动形式化在多个领域都有研究，但各自独立发展导致了显著问题：

定义不统一：不同社区对"自动形式化"的理解存在微妙差异，有些研究甚至不认为自己的工作属于自动形式化范畴

方法难以复用：各领域独立开发导致共享方法论、基准和理论框架的机会有限

评估标准缺失：缺乏跨领域的统一评估标准，难以比较不同方法的效果

LLM 推理可靠性差：LLM 作为通用推理器存在幻觉问题，而自动形式化可以利用 LLM 擅长的"翻译"能力，将推理交给形式工具

现有方法的局限¶

当前的思维链（Chain-of-Thought）和强化学习增强的"推理"模型在复杂逻辑推断上仍不可靠
推理过程难以或无法形式化验证，在高风险应用中存在信任问题
自动形式化通过将非形式语言映射为形式表示，提供了一种更高效、更可解释的替代方案

方法详解¶

整体框架¶

作者系统回顾了 81 篇研究论文，涵盖四个子领域，然后提出统一定义。

关键设计¶

1. 文献综述与分类：系统梳理自动形式化的应用分类¶

作者将综述的论文分为四类：

数学形式化（32 篇）：使用交互式定理证明器（Isabelle/HOL、Lean 等），所有论文都使用"autoformalization"术语
逻辑推理与声明式编程（30 篇）：目标形式主义包括一阶逻辑、Prolog、ASP、时序逻辑（LTL、CTL），仅 8 篇使用该术语
规划（16 篇）：将自然语言翻译为 PDDL 规划语言，无一使用该术语
知识表示：将自然语言翻译为 OWL/RDF 本体，无一使用该术语

尽管术语使用不同，跨领域的定义表现出显著相似性——核心都是将自然语言自动翻译为支持逻辑推理和自动推理的目标语言。

2. 统一定义：形式化从非形式语言 \(L_i\) 到形式推理语言 \(L_f\) 的转换¶

定义 1（形式化）：

从非形式语言 \(L_i\) 到形式推理语言 \(L_f\)、关于语义等价准则 \(E\) 的形式化，是将 \(L_i\) 的一个领域特定子集中的表达式转化为 \(L_f\) 中的一个良构且有效表达式，并在 \(E\) 下语义等价。自动形式化即由计算系统自动执行的形式化。

定义涉及四个核心参数：

参数	含义	示例
非形式语言 \(L_i\)	有意义表达式的集合	英语、数学语言
\(L_i\) 的领域子集	感兴趣的特定表达式子集	博弈论描述、规划场景
形式推理语言 \(L_f\)	由语法或形成规则定义的可枚举表达式集	Lean、FOL、PDDL、OWL
语义等价准则 \(E\)	非形式和形式表达"含义相同"的标准	定理语句保留所有重要数学细节

关键的形式推理语言 \(L_f\) 必须满足两个条件： - 能够表示领域特定子集中所有相关信息 - 支持推理，允许以可接受的计算复杂度验证感兴趣的性质

3. 验证准则 \(V\)：语义等价的可计算近似¶

由于 \(E\) 涉及非形式语言含义，天然具有模糊性，作者引入验证准则 \(V\) 作为 \(E\) 的可计算近似：

\(E\) 定义了非形式和形式表达"含义相同"的语义标准
\(V\) 提供了验证给定对是否满足此等价的实际手段

不同领域的验证方式各异： - 数学：BLEU 分数 + 人工评估（成本高、不可扩展） - 逻辑推理：比较推导答案与正确答案（自动化但不保证语义等价） - 博弈论：查询所有行动组合并比较收益值（自动化且保证实际语义等价，但仅适用于窄类问题） - 规划：跨验证计划有效性（松弛但实用的等价概念） - 知识表示：本体工程师人工验证 + 自动一致性检查

案例研究¶

作者通过 5 个案例展示定义的灵活性：

案例	\(L_i\)	\(L_f\)	验证方式
数学证明	数学自然语言	Isabelle/HOL	BLEU + 人工
一阶逻辑	关于物体/形状的问题	Prover9 (FOL)	答案比较
逻辑编程	博弈描述	SWI-Prolog	博弈查询验证
规划	自然语言动作描述	PDDL	计划跨验证
知识表示	领域描述	OWL	人工 + 推理器

损失函数 / 训练策略¶

本文是综述/框架论文，不涉及模型训练。核心贡献是概念性框架的提出。

实验关键数据¶

主实验¶

本文是综述框架论文，不包含传统意义上的定量实验。核心"实验"是对 81 篇论文的系统综述分析。

子领域	论文数量	使用"autoformalization"术语	目标语言示例
数学形式化	32	全部	Isabelle, Lean, Rocq, Mizar
逻辑推理	30	8 篇	FOL, Prolog, ASP, LTL, CTL
规划	16	0	PDDL
知识表示	若干	0	OWL, RDF, RDFS

消融实验¶

定义参数	去掉后的问题	说明
领域子集	范围过大，无法评估	实际中只形式化特定领域的表达式
语义等价 \(E\)	无法判断正确性	"看起来对"不等于语义忠实
验证准则 \(V\)	无法实际检验	\(E\) 通常不可计算，需要近似

关键发现¶

跨领域一致性：尽管术语使用不同，四个子领域的定义在核心上具有显著相似性
语义验证是根本挑战：完全自动化的语义等价验证原则上不可能（因为自然语言天然非形式化），但可以通过元级推理显著减少人工监督
LLM 的角色：自动形式化利用 LLM 擅长的翻译能力，而非让它直接做推理，是一种更可靠的方案

亮点与洞察¶

观察深刻：指出不同社区其实在做同一件事但互不认识，这种跨领域视角非常有价值
定义精准：提出的四参数定义（\(L_i\), 子集, \(L_f\), \(E\)）既足够通用又够具体，能覆盖现有所有子领域
实际意义：框架可以促进方法迁移——例如规划领域的 PDDL 验证方法可能启发数学形式化的评估
战略眼光：将自动形式化定位为连接 LLM 和形式推理工具的桥梁，而非让 LLM 直接推理，思路清晰

局限与展望¶

缺少定量验证：纯概念框架，没有通过实验验证该框架是否真能促进跨领域方法迁移
综述完整性：作者承认综述不声称穷尽所有相关工作
定义的可操作性：虽然定义通用，但在具体领域落地时仍需大量领域知识来实例化参数
语义验证仍是开放问题：作者承认完全自动化的语义验证原则上不可能，但未提出具体的推进路径
可扩展性：当前系统在策划基准上表现可以，但在真实世界实践中常常失败

评分¶

新颖性: ⭐⭐⭐⭐ （统一框架视角新颖，但无技术创新）
实验充分度: ⭐⭐⭐ （综述性质，案例分析充分但无定量实验）
写作质量: ⭐⭐⭐⭐⭐ （结构清晰，定义严谨，案例丰富）
价值: ⭐⭐⭐⭐ （对促进跨领域交流有重要意义）