主要证据
- First Experiments with Neural Translation of Informal to Formal MathematicsS1 · 主要研究来源 · 论文 · 2018-05-10
- First Experiments with Neural Translation of Informal to Formal Mathematics — CICM 2018S1 · 主要研究来源 · 论文
神经翻译建立从非形式化数学文本到形式 Mizar 的早期路线
作者通过将 Mizar 陈述 informalize 为类似 LaTeX 的数学文本，构建大规模对齐语料，并训练序列到序列翻译模型重建形式语言。研究比较多种神经翻译配置，并通过案例分析模型能够正确恢复哪些数学结构。
发生了什么？
Qingxiang Wang、Cezary Kaliszyk 与 Josef Urban 在对齐的 informalized-LaTeX 文本与形式 Mizar 陈述上训练神经机器翻译模型。论文报告称，最佳模型配置在推理数据上的精确生成率为 65.73%，多种评测模型结果的并集覆盖率达到 79.17%。
为什么重要？
自动形式化是连接人类数学书写与机器可检查形式数学的关键接口问题。该工作在现代 LLM 时代之前就展示了学习式翻译能够把 informal-to-formal 方向转化为可实验评测的具体研究问题，而不仅是长期愿景。
重要性说明：这些实验是较早具有代表性的神经自动形式化里程碑：系统不再假设输入已经是形式定理陈述，而是训练神经机器翻译模型，把接近自然数学语言的文本映射为 Mizar 形式陈述。后来的自动形式化研究，包括 2022 年的大语言模型路线，也明确把该工作列为前序研究。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E2 · 研究记录
- AI 角色
- AI 自主主导
- 形式保障
- 无形式保障
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 非形式化, 形式化, 混合
- AI 贡献
- 神经序列到序列模型从 informalized 数学输入生成候选 Mizar 形式陈述，并承担研究所评测的核心翻译任务。
- 人类贡献
- 研究者构建 informal / formal 对齐语料、设计翻译实验与评测方法、选择模型配置，并分析生成的形式陈述。
- 验证状态
- 论文已发布 · E2 · 研究记录 · 无形式保障
- 最后审阅
- 2026-09-15
技术细节
- 系统
- mizar
- 机构
- university-of-innsbruck
- 数学问题
- mathematical-autoformalization
- 方法
- neural-machine-translation, sequence-to-sequence-learning, aligned-corpus-construction, autoformalization
全部来源与工件
- First Experiments with Neural Translation of Informal to Formal MathematicsS1 · 主要研究来源 · 论文 · 访问于 2026-09-15
- First Experiments with Neural Translation of Informal to Formal Mathematics — CICM 2018S1 · 主要研究来源 · 论文 · 访问于 2026-09-15
验证历史
- 2018-05-10 · 论文已发布 · E2 · 研究记录
arXiv 与 CICM 研究记录确认了神经 informal-to-formal 翻译实验及论文报告的 Mizar 结果。E2 表示已有公开研究记录，并不意味着全部生成陈述都获得了独立复现或语义验证。
更正
当前没有记录的更正。