autoformalization

作者们提出 Choir——一个用于分布式多智能体自动形式化的开放、模块化协议，将项目拆解为基于 GitHub 的任务，并通过确定性的信任门验证机制进行审核，支持 Lean 4、Isabelle 和 Rocq；该项目包含一篇预印本以及一个由 DARPA expMath 项目资助的开源代码仓库。

这篇 arXiv 论文研究了语言模型在着手化解矛盾之前，如何判断两项科学发现是否具有可比性。在一个受控任务中，不可满足的 XOR 约束被翻译成实验报告；当约束条件显式给出时，GPT-5.6 Sol 和 Claude Opo 5 都能很好地还原出最有力支持的赋值方案，但当研究发现以科学散文的形式呈现时，模型往往倾向于遵从生物学上的既有预期。

华为 Lagrange 数学计算研究中心提出 Sage，一个四阶段分解生成管线加双重信号语义校正循环的自动形式化框架，将答案泄漏率从 70.9% 降至 2.7%，在 Omni-MATH NP 上达到 73.3% pass@4，并在新提出的 IMO-Unformalized 基准上零样本达到 87.4% 验证保真度。

本文提出生成式验证（GenV），一种使用生成式奖励模型检测自动形式化中参考等价性失败的方法，解决神经符号系统的漏洞并提高验证准确性。

本文介绍了SA-Pass，一种用于评估自动形式化中语义对齐的方法，并提出了ShadowBench，一个包含178个问题的Lean 4基准测试，展示了与专家判断的高度一致性。

FormalTCS是一个用于评估大型语言模型在端到端理论计算机科学研究上的基准，揭示了显著局限性，尤其是在自动形式化方面。

MathForm引入了一个利用知识检索和验证引导优化的数学自动形式化框架，产生了FormalVerse数据集和一个8B模型，该模型在性能上优于专业基线模型。

LeanFlow是一个LLM智能体系统，用于将数学论文转化为形式化的Lean项目，通过案例研究和与Kimi-K2.6及GPT-5.5的基准测试进行评估，在预算限制内实现了高完成率。

这篇立场论文主张理论级别的自动形式化，即将包括公理、定义和引理在内的整个理论形式化为一致的库，而不是孤立的陈述。它讨论了这种转变的重要性、不同观点、开放挑战，并为形式化研究中的这一转变提出了前进方向。

提出了一种智能体框架，利用通用编码大语言模型将研究级数学自动形式化为Lean 4代码，并在Putnam问题和STOC会议论文上进行了评估。

Mistral AI 发布了 Leanstral 1.5，这是更新的 Lean 4 形式化证明工程模型，针对自动定理证明和自动形式化进行了优化，总参数为 119B，活跃参数为 6.5B。

本文介绍了 SD-GPS，一个求解器驱动的几何问题求解框架，利用求解器反馈引导的自动形式化和经过验证的定理提出，来克服神经符号系统中的瓶颈。

本文介绍了一种信号-覆盖矩阵，它将自动形式化中的类型正确性改进分解为四个层级，揭示了LLM改进背后的机制，并表明标题指标可能掩盖实际解决了哪些错误。

本文提出了一种自动形式化流水线，该流水线使用基于LLM的生成-批评循环，将智能体提示、MCP工具描述和自然语言策略文档转换为经过形式化验证的策略，在MedAgentBench上实现了比手工编码执行更好的覆盖度。

本文提出了一种架构，该架构使用形式化验证的法律作为训练法律AI的奖励信号，自适应地将法律规则自动形式化为形式化演算，并采用验证器确保可证明的正确性，在德国和美国法律示例上进行了演示。

本文评估了在全局和局部扰动下，Lean 4中证明自动形式化模型的鲁棒性，发现当前基于LLM的模型对扰动敏感，且常常无法忠实地反映局部变化。

介绍了PrologMCP，这是一个开源服务器，通过模型上下文协议（MCP）将Prolog暴露为有状态工具，使LLM代理能够将推理委托给符号求解器。评估表明，在前沿推理LLM中，该工具在演绎推理任务上具有竞争力或更高的准确性。

本文提出了一种用于在 Lean 4 中形式化数值分析教材的智能体流水线，并引入了一个超越内核接受的质量审计框架，用于评估语义正确性和库复用情况，揭示了常见的不忠实形式化模式。

本文介绍了一项案例研究，使用大型语言模型（Claude Code）在Lean定理证明器中形式化格罗滕迪克消失定理。研究发现，虽然智能体可以生成经验证的代码，但在定义和API设计方面存在困难，强调了超越单纯编译的专家评审需求。

来自牛津、剑桥、MIT、CMU等机构的研究人员开展了一项混合方法研究，考察人们如何将AI工具融入数学证明形式化工作流程。研究发现，借助AI辅助时，参与者的形式化准确率普遍更高，同时他们倾向于在证明发现过程中保持人类对高层决策的主导权。