证明自动形式化（proof autoformalization）的目标，是把用自然语言书写的非形式化数学证明，翻译成 Lean 4 等形式化语言中的形式化证明。近年来，已有若干工作开发了基于大语言模型（LLM）的证明自动形式化模型，但现有评测通常只关注如何翻译来自精心整理数据集的、格式良好的非形式化证明。这篇于 2026 年 6 月 12 日提交的预印本论文指出，一个稳健的证明自动形式化器即使面对偏离这些理想化样本的非形式化证明，也必须保持忠实，并据此提出了首个针对证明自动形式化模型稳健性的研究。
论文将扰动划分为两大类，并分别评估模型在两类扰动下的稳健性。第一类是全局扰动：它用不同风格对非形式化证明进行改写，在这种情况下，形式化结果本应保持一致，也就是说改写不应改变最终形式化证明的正确性。第二类是局部扰动：它改动证明中的某个数值、符号或证明步骤，有时甚至以反事实的方式进行改动，而一个稳健的形式化结果应当忠实反映这一改动，而不是回退到原始版本，或自行推断出另一个不同的结论。
为开展评测，作者在 miniF2F 和 MATH-500 两个数据集上构建了同时包含两类扰动的基准，并设计了自动化的度量方法：在全局扰动下衡量证明自动形式化结果的正确性有多稳定，在局部扰动下衡量其输出对扰动的反映有多忠实。
作者随后评测了七个近期的模型。结果显示，所有模型都对全局扰动敏感，即在证明被改写风格后难以维持原有正确性；而在局部扰动下，大多数模型也无法保持忠实，往往没有如实反映被改动的数值、符号或证明步骤。这一发现表明，当前基于 LLM 的证明自动形式化系统在面对非理想化输入时仍存在明显短板。
论文的代码与数据已通过 https://github.com/ucr-rai/robust-proof-autoformalization 公开。该论文为预印本，作者为 Zhengtao Gui 等三人，提交历史显示 v1 版本于 2026 年 6 月 12 日 18:10:21 UTC 发布，全文约 246 KB，主题归类为计算与语言（cs.CL），并涉及人工智能（cs.AI）与机器学习（cs.LG）。论文的 DOI 为 https://doi.org/10.48550/arXiv.2606.14867，arXiv 编号为 arXiv:2606.14867v1。