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

MioFFAn：一款具备大语言模型自动化能力的公式形式化标注软件

The automatic translation of mathematical expressions in scientific literature into executable symbolic code (a process we refer to as Formula Formalization) is hindered by a severe scarcity of high-quality, ground-truth datasets specialized for technical scientific domains. 将科学文献中的数学表达式自动转换为可执行的符号代码（我们称之为“公式形式化”的过程）受到严重阻碍，原因在于缺乏针对技术科学领域的高质量、真实标注数据集。

In this paper, we present MioFFAn, an open-source, document-centric, and customizable framework designed to facilitate rapid annotation for this task. Building upon the MioGatto architecture, we extend existing features to overcome structural limitations and pivot its scope by introducing specific functionalities for Formula Formalization, such as selection of equations of interest and aided symbolic code specification. 在本文中，我们介绍了 MioFFAn，这是一个开源的、以文档为中心的、可定制的框架，旨在促进该任务的快速标注。基于 MioGatto 架构，我们扩展了现有功能以克服结构性限制，并通过引入公式形式化的特定功能（如感兴趣方程的选择和辅助符号代码规范）来调整其应用范围。

By allowing users to configure custom taxonomies and properties for identified symbols, and compatible symbolic operators, we ensure the framework is adaptable to diverse specialized scientific fields. 通过允许用户为识别出的符号配置自定义分类法和属性，以及兼容的符号运算符，我们确保了该框架能够适应各种专业的科学领域。

Furthermore, MioFFAn is designed to incorporate partial automation via Large Language Models. By defining a modular set of automated sub-tasks with strict output formats, we enable researchers to iteratively refine automation capabilities and evaluate competing strategies using standard NLP metrics. 此外，MioFFAn 的设计旨在通过大语言模型实现部分自动化。通过定义一组具有严格输出格式的模块化自动化子任务，我们使研究人员能够迭代地改进自动化能力，并使用标准的自然语言处理（NLP）指标来评估不同的竞争策略。

We specify the current automation methodology and perform a preliminary evaluation that demonstrates the efficacy of this human-in-the-loop approach. 我们详细说明了当前的自动化方法，并进行了初步评估，证明了这种“人在回路”（human-in-the-loop）方法的有效性。