🤖 AI

Symbolic Informalization: Fluent, Productive, Multilingual

本文介绍了 Informath 项目，该项目利用构建在 Dedukti hub 和 Grammatical Framework 之上的符号非形式化框架，将来自 Agda、Lean 和 Rocq 等系统的形式化证明可靠地转换为流畅、精确且多语言的自然语言。

原作者： Aarne Ranta

发布于 2026-06-16

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Aarne Ranta

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

核心理念：数学机器人的“翻译官”

想象你拥有一个才华横溢、速度极快的机器人数学家。这个机器人使用一种非常严谨、精确的语言，叫做形式逻辑（例如 Agda、Lean 或 Rocq）。它能以 100% 的准确度证明定理，但它的输出看起来就像一堵代码墙：forall (a : Int), odd a -> even (a + 1)。

对于人类来说，这是无法阅读的。这就像是在读一本每个单词都是秘密代码的书。

非形式化（Informalization）是将这种严谨的机器人代码翻译回自然语言（英语、法语、德语等）的过程，以便人类能够阅读和理解它。

本文指出，虽然我们已经非常擅长教机器人如何通过 AI 从人类书籍中“学习”数学，但我们还没能很好地教它们如何向我们“解释”它们的工作，并让其听起来像是人类写的一样。本文介绍了一个名为 Informath 的系统来解决这个问题。

三大目标：“流利、高效、多语言”铁三角

作者认为，一个优秀的翻译系统需要具备三个要素，他称之为这个项目的“神圣三位一体”：

流利（听起来自然）：
- 问题： 旧的翻译器就像拙劣的机器人，会说：“整数的集合是一个集合。”这种表达生硬且机械。
- 目标： 新系统应该听起来像数学教科书。它应该知道什么时候该说“设 $x$ 为...”，而不是“假设 $x$ 是...”，并且它应该知道如何平滑地组合句子（例如，说“ $x$ 和 $y$ 是偶数”，而不是“ $x$ 是偶数且 $y$ 是偶数”）。
- 类比： 想想 GPS 导航说“左转。然后行驶 500 米。然后右转”与人类提供路线指引的区别：“向左转，走一个街区，然后右转。”两者都能带你到达目的地，但前者更容易跟随。
高效（易于构建）：
- 问题： 构建这些翻译器过去就像是靠手工雕刻字典里的每一个单词。这既耗时又需要语言学家和计算机科学家紧密协作。
- 目标： 让数学家只需在代码中添加一些注释，系统就能搞定剩下的工作。
- 类比： 与其从零开始一块砖一块砖地盖房子，不如使用一套“乐高组件包”（称为资源语法库）。你只需将零件拼装在一起，系统就会为你处理复杂的工程问题（如语法规则）。
多语言（通晓多种语言）：
- 问题： 通常，如果你想要一个英语翻译器，你就得造一个；如果你想要法语，你就得造一个完全不同的东西。
- 目标： 构建一个可以讲任何语言的“大脑”。
- 类比： 想象一个万用适配器插头。你把数学代码插入中间，只需更换“插头头”，它就可以输出英语、法语、德语或瑞典语。你不需要为每个国家重新制造整台机器。

它是如何工作的：“枢纽与辐射”系统

论文描述了一个巧妙的架构来实现这些目标。可以将其想象为一个繁忙的机场枢纽。

枢纽（Dedukti）：
- 这是中央机场。所有不同的“航空公司”（Agda、Lean、Rocq）都将它们的“飞机”（数学证明）飞往这里。
- Dedukti 是一种简单的通用语言，充当共同的基础。它剥离了每种特定语言的特性，并将一切转换为标准格式。
翻译（语法框架 - GF）：
- 一旦数学内容到达了枢纽，它就需要转化为人类语言。这就是 GF 发挥作用的地方。
- GF 就像是一个大师级厨师的厨房。它拥有一本“食谱书”（语法），知道如何将数学食材烹饪成任何语言的美味句子。
- 它处理棘手的细节：确保动词与主语一致、处理单复数变化（如“is”变为“are”），以及处理法语或德语中的性别问题。
菜单（符号表）：
- 这是秘方所在。数学家不需要重写整个食谱书。他们只需填写一张“菜单卡”（符号表），注明：
  - “当你看到代码 plus 时，请说 'sum'（和）。”
  - “当你看到 odd 时，请说 'odd'（奇数）。”
- 这使得系统可以轻松定制，而不会破坏底层的复杂语法。

让它听起来像人类的“魔法”

论文强调，让数学听起来自然比看起来要难得多。以下是 Informath 使用的技巧：

聚合（“和”的技巧）：
- 机器人： “ $x$ 是偶数。 $x$ 能被 3 整除。”
- 人类： “ $x$ 是偶数且能被 3 整除。”
- 系统知道如何合并这些句子，使它们流动得更顺畅。

就地量化（“隐藏”变量）：
- 机器人： “对于所有数字 $n$ ， $n$ 是偶数或 $n$ 是奇数。”
- 人类： “每个自然数都是偶数或奇数。”
- 系统意识到你不需要每次都重复“数字”这个词。它会在显而易见的地方隐藏变量，就像人类一样。
符号 vs. 文字：
- 有时，用符号表示数学效果更好（如 $x + y = z$ ），而有时则用文字（“ $x$ 与 $y$ 的和”）。系统知道何时使用哪种方式。它甚至可以自动生成 LaTeX 代码（标准的数学排版格式）。

本文实际声称的内容（以及未声称的内容）

它确实做到了：

成功构建了一个系统（Informath），可以将形式化的数学证明转化为流畅、自然的文本，并支持多种语言。
证明了通过使用预构建的语法库和简单的符号表，可以使该系统具有“高效性”（易于使用）。
展示了该系统适用于本科水平的数学（算术、代数、拓扑学），甚至包括一些高级课题（同伦类型论），尽管高级课题的处理难度更大。
证明了该系统可以生成数据，以帮助训练 AI 模型（LLM）更好地处理数学。

它并没有声称（根据原文）：

它并未声称该系统目前已能完美处理“所有”数学。作者承认，覆盖“所有日常数学语言”是一个宏大且持续进行的目标。
它并未声称目前可以完美处理“每一个”证明系统。像 Isabelle 或 Mizar 这样的系统被提及为未来的挑战，因为它们的工作方式不同。
它并未声称该系统会取代人类数学家。它是一个帮助人类理解计算机所做工作的工具。

总结

论文得出结论：非形式化并不容易。它不仅仅是形式化的逆过程。虽然形式化（人类到机器人）可以自动检查错误，但非形式化（机器人到人类）却非常复杂，因为“听起来自然”是具有主观性和复杂性的。

然而，通过使用“枢纽”系统（Dedukti）和“通用语法”（GF），作者展示了我们可以构建一个既可靠（不会产生幻觉）、又灵活（能讲多种语言）、且高效（不需要语言专家团队来构建）的翻译器。它将机器人冰冷的代码转回了温暖、可读的故事。

技术摘要：符号化非形式化 (Symbolic Informalization)

问题陈述

本文探讨了符号化非形式化（symbolic informalization）的挑战：即如何可靠地将形式化数学（机器检查的证明和定理）转换为流畅的自然语言，且不损失精度。虽然神经方法（大语言模型）在自动形式化（从非形式化到形式化）方面取得了进展，但它们存在“幻觉”问题，且无法保证形式化定理与原始文本完全匹配。相反，虽然形式化结果可以被自动验证，但逆向过程——非形式化——往往难以通过符号化手段实现自动化。

先前的符号化非形式化尝试被批评存在三个主要缺陷，本文将其确定为成功系统的核心要求：

流畅度 (Fluency)： 输出结果往往缺乏自然语言的多样性和灵活性，显得僵硬。
生产力 (Productivity)： 系统设计和实现难度较大。
多语言性 (Multilinguality)： 方法往往难以扩展到不同的形式化语言或自然语言。

本文认为，非形式化不仅仅是简单的“翻译”，而是一个复杂的科研问题，需要在语义完备性（保持意义）与语言完备性（覆盖数学表达的全范围）之间取得平衡。

方法论：Informath 系统

本文介绍了 Informath，这是一个基于中间语言架构 (interlingual architecture) 构建的系统，旨在解决流畅度、生产力和多语言性这三个目标。

1. 架构

Informath 利用了两阶段中间语言方法：

形式中间语言 (Dedukti)： 作为各种证明系统（Agda, Lean, Rocq）之间的枢纽。Dedukti 是一个极简的逻辑框架，具有依赖类型和重写规则。它作为形式内容的“事实来源”。
语言中间语言 (Grammatical Framework - GF)： 处理自然语言侧。GF 是一种基于逻辑框架（类似于 Dedukti）的语法形式化工具，专为多语言翻译而设计。

其工作流为：证明系统 $\to$ Dedukti $\to$ GF 抽象语法 $\to$ 自然语言。

2. 多语言性

通过将 Dedukti 抽象语法映射到 GF 抽象语法，进而将其线性化为具体的自然语言，从而实现多语言性。

共享抽象语法： 核心数学概念在 GF 的语言无关抽象语法树 (AST) 中定义。
资源语法库 (RGL)： Informath 利用了 GF 的 RGL，该库提供了大约 40 种语言的预定义语言结构（包括屈折、一致性、句法规则）。这使得相同的抽象语法可以被正确地渲染为英语、法语、德语、瑞典语等，并自动处理语法变化（如性别、格、数）。

3. 生产力

为了解决实现难度问题，Informath 采用了一个部署栈 (deployment stack)，为最终用户屏蔽了 GF 和 Haskell 代码的复杂性：

符号表 (.dkgf)： 最高级且最易访问的层级。用户定义词汇注释，将 Dedukti 常量映射到 GF 函数或字符串模板。这使得非语言学家无需编写语法规则即可将系统扩展到新的数学概念。
智能范式 (Smart Paradigms)： RGL 从基础词形生成屈折表，减少了手动录入词汇的需求。
模块化代码： 系统将稳定的核心（MathCore，处理语义完备性）与可扩展的扩展部分（MathExtensions，处理语言完备性）分离。

4. 流畅度与自然语言生成 (NLG)

为了实现流畅度，Informath 超越了基础的受控自然语言 (CNL)，实现了一个多步 NLG 流水线：

内容确定与文本规划： 决定说什么以及以何种顺序说。
聚合 (Aggregation)： 合并原子事实（例如，将“x 是偶数且 x 是素数”转换为“x 是偶数且为素数”）。
词汇选择： 通过符号表选择合适的词汇。
表面实现： 使用 GF 线性化生成最终字符串。
排序 (Ranking)： 系统会为单个形式化陈述生成数千个变体表达式。这些变体根据树大小、深度、标记计数和风格规则（例如，避免以符号开头的句子）进行惩罚函数排序。这确保了输出既紧凑又自然。

语法分为 MathCore（涵盖所有 Dedukti 结构的极简 CNL）和 MathExtensions（近似完整的数学语言）。系统支持复杂功能，例如：

变量绑定常量： 通过高阶抽象语法 (HOAS) 处理量词和积分。
原位量化 (In situ quantification)： 将量词置于谓词之中（例如，“每个自然数都是偶数”）。
符号表示： 生成用于符号部分的 LaTeX 宏，同时保持文字部分的自然性。

核心贡献

Informath 系统： 一个可运行的实现，证明了符号化非形式化可以具备流畅性、生产力和多语言性。
中间语言架构： 创新性地使用 Dedukti 和 GF 作为双重中间语言，将形式逻辑与语言变化解耦。
低代码扩展： 一种基于符号表的机制，允许用户在不修改核心语法或编译器代码的情况下，将系统扩展到新的数学领域。
处理歧义： 一种管理自然语言固有歧义（如量词作用域、连词）的策略，即通过生成多个变体并使用类型检查或排序来解决歧义，而不是强制执行牺牲流畅性的僵化、无歧义规则。

结果

论文报告了 Informath 的现状：

覆盖范围： 系统涵盖了本科数学内容（算术、集合论、代数、拓扑学），并在“100 个定理”项目中进行了测试。
多语言输出： 它能成功地从同一个 Dedukti 源生成流畅的英语、法语、德语和瑞典语文本。
案例研究：
- 同伦类型论 (HoTT)： 对 Hoott 著作的案例研究揭示了第三方转换器（Agda 到 Dedukti）面临的挑战，即由于宇宙层级 (universe levels) 导致代码复杂度爆炸。然而，一旦完成转换，Informath 能够成功处理非形式化过程，包括复杂的“命题即类型”场景。
- 合成数据： Informath 被用于生成合成数据以微调大语言模型 (Qwen2.5-7B-Instruct)，使其自动形式化性能较基准模型有所提升。
局限性： 系统尚未达到语言完备性（即尚未覆盖所有普通数学语言），且证明的非形式化仍处于研究阶段，特别是在步骤的排序和省略方面。

重要性与主张

本文主张，符号化非形式化是神经自动形式化的必要补充。虽然 LLM 可以生成形式化代码，但它们无法保证正确性；符号化非形式化提供了一个可靠且可解释的桥梁，允许人类用户通过自然语言与形式化系统进行交互，而无需接触底层代码。

作者谦逊地总结道，尽管 Informath 实现了超越基础 CNL 的流畅度，但实现对普通数学语言的完全覆盖仍是一个遥远的目标。主要的开放性挑战在于对日益增长的生成变体进行排序以及证明的非形式化。论文强调，与可以自动验证的“形式化”不同，“非形式化”需要内在的可靠性和专家知识，这使得开发此类工具成为未来人类可读的机器检查数学的重要且必要的任务。