修正FOLIO和MALLS：经过验证的标注与聚焦人工重标的LLM辅助框架

# 经过验证的标注与面向人工重新标注的LLM辅助框架
来源：https://arxiv.org/html/2606.02837
Michele Mignani1∗Angelo Montanari1Nicola Saccomanno1 1意大利乌迪内大学，email\.surname@uniud\.it ∗通讯作者

###### 摘要

从自然语言到一阶逻辑（NL\-to\-FOL）的精确翻译是神经符号AI系统和自然语言推理（NLI）的基础，这使得NL\-to\-FOL基准测试集的质量至关重要——然而这些数据集从未经过严格审计。我们的第一个贡献是对FOLIO验证集和MALLS测试集子集进行了系统性人工检查，发现分别约有39%和36%的条目包含错误的FOL形式化（即真实标签），此外还有一定比例的歧义NL句子（16.4%和48%）以及FOLIO中错误的NLI标签（8.4%）。我们的第二个贡献是开发并发布了这些数据集的修正真实标签，表明标注误差会在参考基准任务上扭曲模型评估：使用修正后的真实标签测试三个最先进的大语言模型（Gemma 4 31B\-it、Qwen3\-30B\-A3B和GPT\-4o\-mini），准确率提升了9到22个百分点。受这些发现的启发，我们提出了一种基于LLM的框架，以支持人工审查NL\-to\-FOL数据集。通过将审查者引导至最易出错的实例，我们经验性地证明，在审查少于24%的实例后即可达到90%的数据集准确率，而未经引导的审查则需要超过70%。我们发布了所有经过人工验证的标注以及我们框架的代码。

修复FOLIO与MALLS：经过验证的标注与面向人工重新标注的LLM辅助框架

Andrea Brunello1Cristian Curaba1Luca Geatti1

Michele Mignani1∗Angelo Montanari1Nicola Saccomanno11意大利乌迪内大学，email\.surname@uniud\.it∗通讯作者。

## 1引言

将自然语言（NL）自动翻译成机器可读的形式化语言——通常称为自动形式化——是神经符号AI的基本构建块，其应用范围从自然语言推理（NLI）DBLP:conf/nips/YeCDD23;DBLP:conf/emnlp/OlaussonGLZSTL23;DBLP:conf/emnlp/PanAWW23到运行时验证和AI安全Toward\_guaranteed\_safe\_AI。在目标形式化语言中，一阶逻辑（FOL）因其表达能力和计算易处理性而脱颖而出。然而，NL\-to\-FOL翻译¹仍然是人类和自动化系统长期面临的挑战barker2009difficulty;singh2020exploring。

为了支持该领域的进展，人们开发了数据集以促进NL\-to\-FOL翻译系统的训练并支持系统化比较。然而实际中，公开可用的、经过部分人工整理的数据集数量有限，最著名的是FOLIODBLP:conf/emnlp/HanS0QRZCPQBSWS24和MALLSDBLP:conf/acl/YangXPSF24。先前的工作考察了评估指标和任务设计中的局限性brunello2026llms，但参考标注本身很少受到系统性的关注。

在本文中，我们证明这些标注包含显著错误。我们对FOLIO验证集和MALLS测试集子集进行了系统性人工审计，发现分别有39%和36%的样例包含错误的FOL形式化。此外，16.4%的FOLIO和48%的MALLS包含允许多种非等价但合理的解释的NL陈述（第2节）。这些标注错误直接影响评估：使用我们修正后的真实标签重新评估最先进模型（Gemma 4 31B\-it、Qwen3\-30B\-A3B、GPT\-4o\-mini），准确率提升了9到22个百分点（第2.3节）。

然而，详尽的人工审查无法扩展到大型数据集或实际部署场景。因此，我们引入了一个LLM辅助的监督框架，将人力集中在最可能出错的实例上。该方法利用了一个关键的实证发现：LLM很少将正确的形式化标记为错误——在FOLIO验证集中，Gemma仅将约3%的正确实例标记为错误（见附录I）。引导标注者关注模型认为错误的实例，我们的框架在仅需审查约24%的FOLIO验证实例和约8%的MALLS测试子集的情况下，即可实现90%的标注准确率。此外，当应用于高质量私有数据集GGcbarker2011student时，它引入了可忽略的额外噪声，证实了其在错误罕见时的可靠性。

我们的框架在多个需要高质量FOL语料但全面人工验证成本高昂的场景中具有自然应用。首先，在*数据集整理*中，整理者无需对每个实例进行昂贵的专家审阅，而只需专注于被标记为可疑的一小部分，从而使过程变得更为可控。其次，在*形式化方法*和验证中，该框架可通过识别自然语言规范中可能错误的形式化来协助专家，充当预警层。最后，在*运行时验证*场景DBLP:journals/corr/abs\-2504\-21022中，新定义的行为约束必须立即对照实时数据检查，没有时间进行人工审查；该框架可对生成的公式是否忠实捕获预期需求提供即时反馈。

#### 贡献。

1. 1\.修正后数据集：针对FOLIO验证集（275个实例）和MALLS测试子集（100个实例）修正后的FOL形式化及NLI标签（如适用）（第2节）。
2. 2\.评估影响：使用修正后的真实标签评估最先进LLM时，准确率提升（从9到22个百分点）（第2.3节）。
3. 3\.LLM辅助监督框架：一种将人工标注工作引导至最可能包含错误的实例的新策略，大幅降低审查成本而不牺牲修正质量（第3节）。

为支持可重复性和促进未来研究，我们公开发布了修正后的数据集，地址为https://huggingface.co/DSAVlab-UNIUD；代码目前尚未发布。

## 2数据集及其质量分析

我们分析了FOLIO验证集DBLP:conf/emnlp/HanS0QRZCPQBSWS24和MALLS测试集子集DBLP:conf/acl/YangXPSF24中的错误和歧义，并描述了人工验证和修正的方法。如表1所示，约39%的FOLIO和36%的MALLS实例包含标注错误，这对模型评估产生直接影响（第2.3节）。

表1：人工整理过程中发现的错误和歧义。不正确的FOL句子统计了原始数据集中错误的形式化；子类别并非互斥。
### 2.1数据集

FOLIO是一个基于FOL的NLI基准测试集：每个实例包含一个多句子故事（前提）和一个结论，均以NL和FOL形式给出，并配有一个NLI标签（True/False/Unknown），指示结论是否被前提蕴含、与前提矛盾或独立于前提。该数据集随机分为训练集、验证集和测试集（约1360/275/275个实例）。² FOLIO是NL\-to\-FOL翻译MALLS;brunello2026llms和神经符号推理DBLP:conf/emnlp/OlaussonGLZSTL23;DBLP:conf/iclr/RyuKLY25的主要基准测试集。我们验证其验证集（FOLIO\_validation）。

MALLS是一个由GPT\-4合成生成的大规模NL\-FOL对自动形式化数据集，常用于训练自动形式化器journals/corr/abs\-2509\-22338;DBLP:journals/corr/abs\-2409\-16461。完整数据集包含约28K个实例；其中1000个被声明为经过人工检查并保留为测试集。我们考虑其中的前100个（MALLS\_test）。³

我们还包含来自GGCbarker2011student的213个实例作为对照，以验证我们的整理框架不会向已正确的标注引入噪声。GGC包含学生针对《语言、证明与逻辑》（LPL）中《塔斯基的世界》练习提交的FOL答案，经教师通过自动工具验证，提供了语法和语义正确性的强有力保证。⁴

### 2.2质量分析

先前的工作DBLP:conf/emnlp/OlaussonGLZSTL23;brunello2026llms已注意到FOLIO和MALLS中存在错误；本文旨在量化它们对评估结果的影响。

在两个数据集中，我们都识别出*翻译错误*和*歧义NL句子*。这两种现象都可能惩罚产生正确形式化的模型：翻译错误导致有效公式被与错误参考进行评分，而歧义句子允许多种合理的解释，但真实值中只编码了其中一种。GGC未显示显著错误，只有一小部分歧义句子（约8.5%）。

原始的FOLIO\_validation中还包含与提供的形式化不一致的*NLI标签*；我们修正了17个这样的标签（约占数据集的8.4%），并重新对照NL推理进行了验证。

下面，我们详细说明标注协议、整理过程中发现的问题以及为解决这些问题所做的选择。

#### 标注协议。

整理工作由两位经验丰富的评审者进行：一位博士生和一位研究员，均具有数学或计算机科学背景。对于每个数据集，实例平均分配给两位标注者，每位首先独立审阅自己的一半，然后交叉检查另一半。冲突通过讨论解决直至达成共识。审阅过程中未参考任何LLM输出，唯一的例外是自动将谓词和常量符号映射到自然语言解释以辅助理解；这些映射随后由标注者手动验证。

#### 本体问题。

由于没有数据集提供显式本体，我们自动从FOL公式中提取签名——谓词、元数和常量——然后使用LLM为每个符号分配自然语言含义，最后手动验证其一致性。

我们遇到两类不同的本体问题。第一类是*不一致性*：当一个符号在同一故事的前提和结论之间或同一公式内以矛盾的元数或含义出现时，我们手动修正本体以恢复一致性。在MALLS\_test中，我们经常发现复合关系符号（例如，WorksInNewsIndustryAndReportsOnEvents）掩盖了逻辑结构。在这种情况下，我们将谓词分解为其组成部分（例如，WorksInNewsIndustry和ReportsOnEvents）以恢复组合本体。

第二类是*本体松散性*：在整个形式化中统一应用的非常规但内部一致的逻辑约定。一个具体例子如下：NL表达式school events被编码为常量schoolEvent，尽管FOL常量通常表示特定个体而非类别。更标准的表示应使用谓词SchoolEvent(x)对个体进行限定。这种模式在几个FOLIO故事中反复出现。

与第一类不同，本体松散性案例在整理后的版本中被*故意保留*，因为它们不损害推理的有效性。修正它们还需要重写所有依赖公式，产生一个新数据集而非原数据的整理版本；而且由于本体设计本身具有真正的自由度，任何此类修订都会用另一种合法的建模选择替代一种，在没有额外上下文信息的情况下，没有原则性依据偏好更细或更粗的粒度。

#### 翻译错误。

我们识别出损害真实标签正确性的反复出现的错误。*语法错误*（括号不匹配、符号拼写错误、本体误用和自由变量）影响FOLIO中10.5%的实例和MALLS中3%的实例。*语义错误*，即语法正确的公式错误表示NL含义，更为普遍（FOLIO中约28.3%，MALLS中约33%），且更难自动检测。它们包括量词辖域错误、遗漏NL句子中明确陈述的信息、错误实体相对化以及更广泛的逻辑结构失败。

这些发现的总结见表1。附录B讨论了如何将这些发现与文献中报道的看似矛盾的LLM逻辑翻译性能比率相协调。整理后的数据集版本包括修正的本体（见附录C），以及修正的形式化及其每个修正的解释（详见附录D、E和F）。

#### 歧义。

NL句子固有的歧义对NL\-to\-FOL形式化构成了根本性挑战DBLP:journals/aiopen/YadavPS21：当被承认时，通常通过要求句子明确陈述解释所需的所有背景信息或避免模糊术语来解决。由于先前没有工作为识别NL\-to\-FOL基准测试集中的歧义提供系统化标准，我们采用一个操作定义，并在人工整理阶段明确标注歧义实例。我们认为，当给定固定本体时，存在多个非等价的合理形式化，则该句子是歧义的。

歧义对评估有直接影响：由于所有NL\-to\-FOL基准测试集仅提供一个参考公式，基于等价性的评分会在模型提出正确的替代形式化时对其进行惩罚。因此，显式歧义标注具有双重目的：它使得下游分析能够解释这一混淆因素，并促进对模型能力的更清晰评估。关于跨数据集遇到的歧义类型的定性分类，见附录G。

#### FOLIO的NLI标签不一致性。

如前所述，FOLIO也是一个NLI数据集。对于每组前提\{p1,...,pn\}和结论c，还有一个标签 l ∈ \{True, False, Unknown\}，反映c是被p1,...,pn蕴含（True）、与它们矛盾（False）还是无法演绎地确定其真值（Unknown）。FOLIO提供了形式