来源： Invited Talk 05 · Yinya Huang 播客： ICML 2026 · AI4Math 分类： AI 研究 原文发表： 2026-07-11 纪要生成： 2026-07-13
针对 LLM 定理证明的"非形式—形式鸿沟"，从两端发力：其一，用依赖感知（dependency-aware）的 premise selection——借 Lean Blueprint 项目的丰富依赖数据，去够到稀有/新颖前提；其二，为自动形式化的忠实性建立细粒度错误分类（28 类）与四子任务评测（判定→归类→定位→纠正），并发现1.7B 小模型经训练即可胜任评测。
理想场景：用 LLM 做端到端自然语言定理证明——给一个非形式问题（如 Erdős 问题），喂给 LLM，希望它给出非形式证明，然后判断其正确，从而"用 LLM 成功解决了开放问题"。但如何验证这个非形式证明？现状：要么请数学专家看、要么用很花哨的 LLM-as-judge。可是我们并不总有数学专家，也不总信任 LLM judge。
一个常见解法：把非形式证明在一定程度上形式化（如到 Lean），则可验证。另一问题：端到端自然语言推理时，如何控制逐步推理过程？形式路径给出思路——从最开始就把问题形式化为形式陈述，再用 LLM 形式证明技术（如 premise selection、proof search）得到形式证明，则逐步推理与最终证明都可验证。但这条流水线里有一个形式化步骤，由此产生两大主问题：(1) 如何保证形式化是忠实的；(2) 在"非形式问题"场景下，如何应用这些形式证明技术、如何联结形式与非形式各自优势。
解开放问题（如 Erdős 问题）或新提出的猜想时，常需要新颖前提——这些前提新、模型很少见过。相关工作 LeanDojo、miniCTX 观察到：当证明需要"搜索空间中不常见的新颖前提"时，模型通常吃力；而当特意给出相关前提与额外上下文信息（自然语言注释、或同文件中结构类似的其他证明）时，模型表现会提升，尤其对重依赖定理的问题（如 PFR 猜想，polynomial Freiman–Ruzsa conjecture）。
当前 premise selection 通常从 mathlib 训练、以"定理语义相似"为目标，这忽略了：
一个答案：真正利用 mathlib 中丰富的依赖关系，而不仅看每个节点/定理的语义。
另有一个含大量"新定理依赖"的资源——Lean Blueprint 项目：数学专家写下互相交叉引用的定理、以 LaTeX 写、用于证明新猜想；写时会把每个定理逐点形式化以便在 Lean 实现。借 blueprint 工具，这些 LaTeX 定理会自动转成一个有向无环图（DAG），图记录了这些"新定理依赖"，每个节点记录定理的 LaTeX 版本、以及（若专家已形式化的）配对 Lean 代码。于是 blueprint 提供了自然语言的丰富上下文、作为 mathlib 的补充；而且有趣的是这些 blueprint 依赖能通过"共享的形式定理"与 mathlib 相接——这给了"用依赖数据训练选择器、以应对新颖/罕见前提"的机会。
数据规模：先尽量挖掘线上开源 blueprint 项目，再用规则过滤掉无意义/低质项目，最终得 53 个项目、约 3800 定理、约 4600 依赖。其中约 30% 节点未形式化（无 Lean 版、只有 LaTeX 描述），但它们仍有依赖，故仍在训练中利用、并把其非形式语义编码为训练特征。
评测集含团队自建的多个数据集：用 mathlib 4.22.0，自定义划分出 mathlib-random 与 mathlib-held-out（held-out 的查询全来自训练未见的文件）；还有 dep-collection（从开源 Lean 训练集收集查询、候选也从 mathlib 抽）与 dep-blueprint（测从 blueprint 的选择）。结果：
回到"用形式化帮助非形式证明"这条流水线，其自动形式化不总被保证忠实。问题：如何评价"忠实性"、如何判断自动形式化中形式与非形式两部分是否对齐？因为即使人类专家也会下意识犯错——例如在广泛使用的 PutnamBench 中就存在一些小错误。
"对齐（alignment）"的含义：形式陈述需保留自然语言陈述里的所有数学约束、保持相同逻辑、且不引入自然语言中没有的额外约束。但我们缺乏检测并纠正这类错位的评测器/工具：现有手段要么借神经机器翻译的现成指标（tree edit distance、BLEU），要么只看"形式化部分是否过 Lean"；也在尝试用神经模型给错位打分，但当前只能判"是否对齐"，无法告诉你：错在哪个确切位置、是哪一类错误、以及如何纠正。
本工作定义了一套全面的错位错误类型，含语义（semantic）、约束（constraint）、实现（implementation）三大类：
数据：从多个已有数据集/基准取得一批对齐的种子数据，再用 LLM 注入错位，最终得含训练集 + held-out 测试集的大规模数据集。
Q1（某 blueprint 项目作者）： 我是你取用了部分陈述的某 blueprint 项目作者，其中有相当一部分（"a good third"）尚未形式化；那些非形式陈述我当初没投入足够精力，很可能有不少是错的。你的数据集是否也包含 blueprint 中这些非形式（未形式化）部分？还是只取有形式陈述的部分？ A1： 感谢提问。我们没有联系所有项目作者，方法上假设那里的依赖都是正确的来构建方法。但既然有了这套方法论，这确实是很好的建议——未来可以更仔细审视数据集、并与作者合作以获得更好的数据源。
Q2： 关于你流水线的 verdict（判定）部分：你是仅靠 LLM 本身来发现语义错位，还是有别的技术参与？如果只靠 LLM，你认为前沿 LLM 有能力发现你案例里所有语义错位吗？ A2： 你是问我们构建数据集时？流水线是：先用 LLM 做一轮粗筛（rough curation），然后由多名专家非常仔细地多轮检查，确保数据正确。 Q2 追问： 那你有没有发现 LLM 检查/判定的失败模式？还是说 LLM 在这任务上已经做得不错？ A2 追问： 当前 LLM 在该任务上并不完美，有很多不同的错误模式与情形；我们在稿件里有大量 case study，可以去看。
Q3： 如果我理解没错，你在训练一些定制（bespoke）小模型做这些任务。问题是：前沿模型在这些任务上表现如何？在那些前沿模型更强的情形下，你是否想过如何改造你的技术去提升前沿模型的能力（如 in-context learning、prompt engineering）？因为训练自定义模型常有个问题：哪怕你把能力提升了 10%，可能仍不如前沿模型做同样任务——这样"改进"并没真正推动 SOTA；那么在无法重训前沿模型时，能否实现你的想法去提升前沿模型？ A3： 很好的问题，我个人也在想。但我认为不只是 SOTA 之争——在学术界算力有限，仍有有趣的研究问题：比如我们第二项工作，观察到形式/非形式的错位，并发现"不仅要检测错位本身、还需更细粒度地看它"，于是提出方法去 benchmark 它。这类问题足够通用——对任意规模的模型、乃至超越 LLM 的方法论都成立；这些问题对我个人很有趣，也可能是对工业研究的很好补充。