autoformalization

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辅助时，参与者的形式化准确率普遍更高，同时他们倾向于在证明发现过程中保持人类对高层决策的主导权。

ATLAS是一个大规模的Lean 4教科书数学库，由LLM自动形式化，涵盖26本书籍，超过46,000个声明。它为人机形式化提供了可重用的形式化构建块。

MathAtlas 是一个针对研究生级别数学的自动形式化的大规模基准测试，包含从103本教科书中提取的约5.2万个定理和定义，并附带一个包含约17.8万条关系的数学依赖图。实验表明，最先进的模型正确率最高仅为9.8%，凸显了其难度。