主要证据
- Autoformalization with Large Language ModelsS1 · 主要研究来源 · 论文 · 2022-05-25
- Autoformalization with Large Language Models — NeurIPS 2022S1 · 主要研究来源 · 论文
- Autoformalization with Large Language ModelsS2 · 官方机构来源 · 官方公告
大语言模型在数学自动形式化上展示实用进展
研究者通过 few-shot prompting 让大语言模型把非形式化数学陈述翻译为 Isabelle/HOL，并将生成的形式化结果进一步作为神经定理证明器的训练数据，把自然语言翻译与形式证明搜索连接到同一流程中。
发生了什么？
论文报告称，大语言模型能够将抽样数学竞赛题中的 25.3% 正确翻译为 Isabelle/HOL 形式规范；使用自动形式化生成的定理训练神经定理证明器后，其 miniF2F 证明率从 29.6% 提升到 35.2%。
为什么重要？
这一结果较早建立了现代语言模型与证明助手之间的经验性桥梁：自动形式化不仅以翻译准确率评估，而且被证明能够生成可提升下游证明器的数据，成为后来自动形式化基准与合成形式数学管线的重要前序。
重要性说明：该工作较早建立了从非形式化竞赛数学到证明助手形式规范的大语言模型路线，并展示生成的形式陈述可以提升后续定理证明，使自动形式化成为更具体的 AI4Math 研究方向。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E2 · 研究记录
- AI 角色
- AI 自主主导
- 形式保障
- 无形式保障
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 非形式化, 形式化, 混合
- AI 贡献
- 语言模型从非形式化题目陈述生成候选 Isabelle/HOL 形式规范，并将这些生成的形式陈述用于扩充定理证明器训练数据。
- 人类贡献
- 研究者设计提示与评测协议、判断形式化是否正确、将生成陈述接入定理证明器训练，并测量其在 miniF2F 上的表现。
- 验证状态
- 论文已发布 · E2 · 研究记录 · 无形式保障
- 最后审阅
- 2026-09-15
技术细节
- 系统
- isabelle-hol
- 机构
- google-research, university-of-cambridge
- 数学问题
- autoformalization, minif2f
- 方法
- large-language-model, few-shot-prompting, autoformalization, synthetic-training-data
全部来源与工件
- Autoformalization with Large Language ModelsS1 · 主要研究来源 · 论文 · 访问于 2026-09-11
- Autoformalization with Large Language Models — NeurIPS 2022S1 · 主要研究来源 · 论文 · 访问于 2026-09-11
- Autoformalization with Large Language ModelsS2 · 官方机构来源 · 官方公告 · 访问于 2026-09-11
验证历史
- 2022-05-25 · 论文已发布 · E2 · 研究记录
研究论文公开报告了 Isabelle/HOL 自动形式化与 miniF2F 结果。E2 表示已有公开研究记录，并不意味着已经获得独立复现或验证。
更正
当前没有记录的更正。