💬 NLP

MioFFAn: an Annotation Software for Formula Formalization with LLM Automation Capabilities

本文介绍了 MioFFAn，这是一个开源且可定制的标注框架，它通过结合人工标注与模块化大语言模型自动化，扩展了 MioGatto 架构，旨在促进用于公式形式化的高质量数据集的创建。

原作者： Nicolas Sibuet, Horacio Saggion, Riccardo Rossi

发布于 2026-07-28

📖 1 分钟阅读☕ 轻松阅读

原作者： Nicolas Sibuet, Horacio Saggion, Riccardo Rossi

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

想象一下，你是一名试图破解谜团的侦探，但线索是用只有计算机才能读懂的秘密代码编写的，而故事本身是用只有人类才能理解的语言书写的。这正是科学家们在撰写充满复杂数学公式的论文时所面临的日常困境。他们使用优美、优雅的公式来描述世界的运作方式，但这些公式往往只是数学的“图像”——就像一张桥梁的图画。要真正建造这座桥，计算机需要的是蓝图：即那些能告诉机器如何精确计算钢材应力的具体指令、变量和逻辑。将这种数学“图像”转化为计算机“蓝图”的过程，被称为公式形式化（Formula Formalization）。

问题在于，即使是那些由人工智能（AI）驱动的超级智能计算机，也完全无法自主阅读这些蓝图。它们需要一个海量的示例库——成千上万对“数学图像”与“计算机蓝图”的配对——来学习如何进行翻译。但问题的关键在于：目前还没有人建立起这样一个库，因为创建它的过程极其困难且枯燥。人类必须坐下来，将论文中的每一个数学符号手动重写为代码，这项任务如此乏味，以至于拖慢了科学进步的步伐。这就像试图教机器人做菜，却要为世界上每一道菜从头开始手写每一个食材一样。

这就是名为 MioFFAn 的新工具发挥作用的地方。把它想象成一个高科技、交互式的笔记本，旨在让枯燥的数学转码工作变得更快、更轻松。研究人员不仅仅构建了一个静态工具；他们构建了一个“人机协同（human-in-the-loop）”系统。这意味着该软件就像一个智能助手，利用 AI 来猜测翻译结果，然后请求人类专家进行检查并修正错误。这就像有一个机器人可以为你起草信件，但你仍然需要签字并确保事实无误后才能将其发出。通过这种团队协作的方式，作者展示了我们可以比以前更快地构建这个至关重要的数学到代码的示例库，从而为计算机最终理解并运行驱动现代科学的复杂数学奠定基础。

论文的故事：搭建数学与代码之间的桥梁

这篇论文介绍了 MioFFAn，这是一个旨在帮助研究人员标注科学文档的开源软件。其主要目标是促进公式形式化，即把科学论文中的数学表达式转化为可执行的符号代码（例如你会使用的计算机代数系统代码）。作者认为，虽然我们拥有优秀的文档扫描和文本识别（OCR）工具，但我们缺乏将这些扫描出的公式转化为计算机可运行代码的“语义深度”。

为了解决这个问题，作者在名为 MioGatto 的旧工具之上构建了 MioFFAn。他们意识到旧工具在识别单个数学符号（如字母 $x$ ）方面表现出色，但在处理复杂的符号组合（如整个函数 $f(x)$ 或张量 $\delta u_i$ ）时表现糟糕，且无法实现现实科学研究中所需的灵活的层次化标注。MioFFAn 通过引入以下几项关键升级解决了这一问题：

分组与层次结构： MioFFAn 不再仅仅标记单个字母，它允许用户将公式的整个区块作为一个单一单元进行选择。它将复杂的表达式视为一个“组”，如果需要，该组仍可以被拆解为各个部分。
可定制规则： 该软件像变色龙一样灵活。它允许用户为不同的科学领域定义自己的“分类法”（规则和类别）。例如，物理学家可能需要将一个变量标记为“向量”，而生物学家可能需要将其标记为“浓度”。该工具可以适应这些需求。
easily 适应这些需求。
上下文关联： 它有助于将数学符号链接回文档中解释它们的文本。如果论文说“设 $v$ 为速度”，该工具可以帮助你高亮显示这句话，并将它与公式中的符号 $v$ 联系起来。
“人机协同”自动化： 这是最令人兴奋的部分。软件包含一个功能，其中 AI（具体来说是大语言模型，或 LLM）会首先尝试进行标注。它会建议公式的各个部分分别是什么、变量的含义以及它们在文中的定义位置。然而，人类用户并未被取代；他们扮演着监督者的角色。他们负责审查 AI 的建议，修正错误，并确认最终结果。

作者使用一个名为**有限元方法（FEM）**的特定科学领域对该系统进行了测试，该方法用于模拟诸如汽车碰撞或桥梁弯曲等情况。他们为软件设定了理解 FEM 特定数学规则的规则，然后进行了一次“概念验证”实验。他们向软件输入了一些科学论文，让 AI 尝试进行标注，然后将 AI 的工作成果与人类专家创建的“金标准”进行了对比。

结果既展现了前景，也反映了现实。AI 在某些方面表现得非常出色，但在另一些方面则显得力不从心。例如，当 AI 被允许看到原始数学符号（如希腊字母 $\lambda$ ）时，它识别公式组成部分的表现（约 57.7% 的覆盖率）明显优于将符号替换为长文本名称时的表现（覆盖率降至 36.2%）。然而，AI 仍不完美；它经常难以精准定位文档中的文本定义位置，有时会高亮显示整个段落而非仅仅是特定的句子。

论文明确排除了 AI 目前能够完美独立完成这项工作的可能性。作者指出，自动化的结果“远非理想”，只能作为人类专家快速完善的“基准”。他们认为，如果尝试在没有人工检查的情况下使用 AI 进行完全自动化的端到端翻译，可能会导致难以察觉的错误。

在评估中，作者发现“原始字符（Original Characters）”方法（保留数学符号原貌）最有利于 AI 理解数学结构。他们还对比了三种不同的 AI 模型（NVIDIA 的 Nemotron、Google 的 Gemma 和阿里巴巴的 Qwen），并发现 Qwen3-4B-Instruct-2507 模型的表现显著优于其他模型，其符号识别的覆盖率达到了 57.7%，而排名第二的模型仅约为 33.9%。

最终，论文表明 MioFFAn 是开发更好自动化策略的一个强大的“游乐场”。它并不声称已经永久解决了数学到代码的翻译问题。相反，它提供了一个灵活的框架，研究人员可以在其中测试不同的 AI 策略，观察哪些有效，并逐步改进系统。作者总结道，虽然目前的自动化仅仅是一个“临时性”的步骤，但这种人类与 AI 的协作是构建训练未来更智能系统所需的高质量数据集的最有效途径。他们展望的未来是，这个工具将有助于建立一个庞大的、共享的数学到代码的翻译库，使计算机能够更容易地协助科学家解决世界上最复杂的难题。

技术摘要：MioFFAn

问题陈述

将科学文献中发现的数学表达式自动转化为可执行的符号代码（在本研究中定义为公式形式化，Formula Formalization）目前正受到技术瓶颈的阻碍，其核心原因在于缺乏高质量、针对特定技术科学领域的基准真值数据集。虽然光学字符识别（OCR）系统可以提取如 LaTeX 或 MathML 等表现形式，但它们缺乏实现这些公式所需的语义和计算深度。尽管大语言模型（LLMs）为这种转换提供了极具前景的编排机制，但由于缺乏能够捕捉特定上下文信息（如变量定义、算子属性和领域特定约束）的基准语料库，其发展进程陷入停滞。现有的标注工具通常侧重于单个符号的识别或指代消解，而非生成用于编排这些元素的符号代码。

方法论

作者提出了 MioFFAn（Math identifier-oriented Formula Formalization Annotator，面向数学标识符的公式形式化标注器），这是一个开源、以文档为中心且可定制的框架，旨在促进公式形式化的快速标注。该系统基于 MioGatto 架构构建，但引入了显著的结构性和功能性扩展，以解决原工具的局限性。

框架架构与增强功能

MioFFAn 是一个基于客户端-服务器架构（TypeScript/Python）的应用，使用 HTML 和 MathML 实现动态 Web 端交互。相较于 MioGatto 的主要架构增强包括：

层级化与复合标识符管理： 系统将数学标识符（MIs）的定义从单一的 <mi> 标签扩展到支持复合结构（例如下标、上标）以及用户定义的组（Groups）。这使得复杂的符号（如 $\delta u_i$ 或 $f(x)$ ）可以被视为单一实体，同时保留了对组成部分进行标注的能力。
解耦的属性模式： 框架将不变语义属性（分配给“概念”，例如“速度向量”）与变体属性（分配给“出现实例”，例如“转置”）分离。这使得概念可以在不同的符号表示和实现模态中被复用。
灵活的溯源（Grounding）： 溯源源（Sources of Grounding, SoG）现在支持跨多个 HTML 节点的跨跨度高亮，并与“概念”而非单个“出现实例”相关联，从而允许选择整个显示的公式或跨节点的文本段落。
以文档为中心的流程： 用户可以在单次会话中无需重启服务器即可在多个文档样本之间进行导航，并且系统支持通过 JSON 配置动态填充标注模式。

公式形式化特性

为了专门针对公式形式化，MioFFAn 引入了三个核心特性：

感兴趣的方程（Equations of Interest, EoI）： 用户指定特定的表达式进行形式化，这会在标注模式中初始化一个专用条目。
规范变量名（Canonical Variable Names）： 每个“概念”都映射到一个唯一的变量名，以确保在生成的符号代码中具有无歧义的表示。
集成的符号代码构建： 一个交互式环境提供了一套定义的变量名和领域特定算子（如 grad(), div()）调色板，以辅助用户合成最终的符号代码，最大限度地减少手动语法错误。

自动化流水线

MioFFAn 通过 LLM 集成了一个模块化的“人机协同”（human-in-the-loop）自动化流水线。该自动化过程与核心应用解耦，允许研究人员更换策略。该流水线由三个子任务组成：

符号分割（Symbol Segmentation）： LLM 识别 MathML 元素或应作为唯一出现实例进行分组的复合结构。
概念分配（Concept Assignment）： LLM 建议“概念”（带有变量名和描述）并将它们映射到分割出的符号上。
SoG 识别（SoG Identification）： LLM 识别作为这些概念证据的文本跨度或公式。

系统强制执行严格的输出格式（包括组、概念列表等），以便使用标准的 NLP 指标进行与方法论无关的评估。

用例与评估

该框架针对**有限元方法（FEM）**进行了配置，该领域需要对高维张量和变分形式进行精确表征。研究定义了一个自定义的分类法和算子库（针对 KratosMultiphysics 的 Sympy 编译器）。

研究人员使用本地 Qwen3-4B-Instruct 模型对 6 个精选的 FEM 样本进行了初步的概念验证评估。评估比较了两种自动化变体：

原始字符（Original Characters）： LLM 处理包含非标准 Unicode 字符的原始 HTML。
显式名称（Explicit Names）： LLM 处理将 Unicode 字符替换为显式名称（例如“GREEK SMALL LETTER LAMBDA”）后的 HTML。

结果：

在符号分割任务中，“原始字符”变体显著优于“显式名称”变体（覆盖率 57.7% 对 36.2%；CoNLL 指标 36.8% 对 26.9%）。
“显式名称”变体在概念分配和 SoG 识别方面表现出边际改进。
定性分析显示，虽然模型通常能识别正确的语义上下文，但在 SoG 识别任务中，它在精确指定标签 ID 方面存在困难，经常高亮整个段落而非特定的句子。

核心贡献

MioFFAn 框架： 一种专门的开源标注工具，弥合了数学符号与可执行符号代码之间的鸿沟，解决了公式形式化领域缺乏真值数据的难题。
架构扩展： 对 MioGatto 基准进行了显著改进，包括支持复合标识符、解耦的属性模式以及灵活的溯源机制。
模块化自动化： 一种流水线设计，允许通过模块化子任务（分割、分配、溯源）迭代优化 LLM 策略，从而实现对竞争性自动化方法的评估。
领域适应性： 通过将其应用于有限元方法（包括自定义分类法和算子集），展示了该框架的可配置性。

意义与主张

本文将 MioFFAn 定位为而非一个完全自动化的解决方案，而是一个人机协同的开发实验场。作者声称，该框架的核心价值在于其能够：

促进创建用于训练和基准测试公式形式化 LLM 所需的高质量、领域特定数据集。
使研究人员能够通过隔离特定子任务（分割、分配、溯源）并使用标准指标进行评估，从而迭代地改进自动化能力。
为自动化提供一个基准，该基理可以被人类专家快速优化，同时也承认目前的 LLM 能力尚不足以实现复杂科学领域的完全自主形式化。

作者总结道，虽然目前的自动化尚不理想，但 MioFFAn 的模块化设计有效地支持了未来更复杂自动化工作流的发展，最终解决科学代码生成中数据匮乏的瓶颈问题。