# 自动形式化

这篇综述系统梳理了 AI for Mathematics（AI4Math）的进展、挑战与前景，将研究分为面向特定问题的建模（引导直觉、构造反例、封闭系统形式推理）与通用建模（自然语言推理、形式推理、数学信息检索）两条互补路线，并报告了作者自建的 PKU 本科与博士资格考试评测：GPT-4 平均分低于 60，而 o1、DeepSeek-R1、o3-mini、Gemini 2.5 Pro 等推理增强模型多数超过 90，o3-mini 在 58 道博士资格考试题上平均 84.4 分，同时指出研究级数学仍是开放难题。

这篇综述系统梳理了 AI for Mathematics（AI4Math）的进展、挑战与前景，将研究分为面向特定问题的建模（引导直觉、构造反例、封闭系统形式推理）与通用建模（自然语言推理、形式推理、数学信息检索）两条互补路线，并报告了作者自建的 PKU 本科与博士资格考试评测：GPT-4 平均分低于 60，而 o1、DeepSeek-R1、o3-mini、Gemini 2.5 Pro 等推理增强模型多数超过 90，o3-mini 在 58 道博士资格考试题上平均 84.4 分，同时指出研究级数学仍是开放难题。

该工作提出 Proof-Sketch-Guided Formal Model Synthesis（ProGS），一种以基于模型的证明草图为中心的自动形式化方法：草图把目标形式系统的证明结构表示为树，内部节点对应情况划分与归纳推理步骤，叶节点对应实现各子目标的具体状态转移事件，LLM 负责生成与修复这些草图，验证失败被映射回特定节点与子树以提供结构化修复指导；在 27 个形式系统基准上的评估显示，ProGS 在语法有效性、演绎可验证性与行为正确性上优于当前最先进的智能体式形式化建模方法。

该工作提出 Proof-Sketch-Guided Formal Model Synthesis（ProGS），一种以基于模型的证明草图为中心的自动形式化方法：草图把目标形式系统的证明结构表示为树，内部节点对应情况划分与归纳推理步骤，叶节点对应实现各子目标的具体状态转移事件，LLM 负责生成与修复这些草图，验证失败被映射回特定节点与子树以提供结构化修复指导；在 27 个形式系统基准上的评估显示，ProGS 在语法有效性、演绎可验证性与行为正确性上优于当前最先进的智能体式形式化建模方法。