多语种数学自动形式化
原文中文，约300字，阅读约需1分钟。发表于：。通过使用语言模型将正式数学陈述翻译为相应的非正式陈述，我们创建了一个大型、灵活、多语言和多领域的非正式 - 正式对数据集 MMA，实验证明在 MMA 上对语言模型进行微调可以产生 16-18％的陈述，仅需进行最小的修正即可达到 miniF2F 和 ProofNet 标准，这也证明了在单语言任务中部署多语言正式数据进行微调可以得到更有能力的自动形式化模型。
研究使用Codex探讨将自然语言书写的数学转化为可以被程序检查正确性的形式语言的能力。Codex可以以近75％的准确率进行短数学陈述的形式化，并以自然语言形式翻译本科水平的13个定理的证明。大型语言模型是完全或部分自动化形式化的有前景的途径。
