💬 NLP

Fixing FOLIO and MALLS: Verified Annotations and an LLM-assisted Framework to Focus Human Relabeling

This paper reveals significant annotation errors in the FOLIO and MALLS NL-to-FOL benchmarks, releases corrected ground truths that substantially improve LLM evaluation metrics, and proposes an LLM-assisted framework that enables efficient human relabeling to achieve high dataset accuracy with minimal review effort.

Original authors: Andrea Brunello, Cristian Curaba, Luca Geatti, Michele Mignani, Angelo Montanari, Nicola Saccomanno

Published 2026-06-03

📖 4 min read☕ Coffee break read

CC BY 4.0

Original authors: Andrea Brunello, Cristian Curaba, Luca Geatti, Michele Mignani, Angelo Montanari, Nicola Saccomanno

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are trying to teach a robot to understand human logic. To do this, you give the robot a textbook full of stories written in plain English, paired with their "mathematical translations" into a strict language called First-Order Logic (FOL). The robot studies these pairs to learn how to translate new stories on its own.

This paper is about discovering that the textbook was full of typos and mistakes, and then building a smarter way to fix it without reading every single page by hand.

Here is the breakdown of what the researchers found and did:

1. The Problem: The "Textbook" Was Broken

The researchers looked at two popular datasets (FOLIO and MALLS) that everyone uses to test these AI robots. They acted like a team of strict editors going through the answer keys.

The Discovery: They found that about 39% of the answers in FOLIO and 36% in MALLS were actually wrong.
- Some translations were just gibberish (syntax errors).
- Some were logical nonsense (semantic errors).
- Some of the original English sentences were so vague that they could be interpreted in multiple ways, but the textbook only gave one answer.
The Consequence: Because the "answer key" was broken, the robots were being graded unfairly. A robot might have given a perfectly correct translation, but because it didn't match the wrong answer in the book, it got marked down.
The Fix: The team manually corrected these errors. When they re-tested the top AI models using the new, correct answer keys, the robots' scores jumped dramatically—by 9 to 22 percentage points. It turned out the robots were smarter than we thought; the test was just broken.

2. The Challenge: You Can't Read Every Page

Now that they knew the books were messy, the team faced a new problem: How do you fix a massive library of books without spending 100 years reading every single page?

If you hire a human to check every single translation, it costs too much time and money. If you let a computer check them, computers aren't perfect at understanding human nuance yet.

3. The Solution: The "Spot-Check" Strategy

The researchers invented a smart assistant system (an LLM-assisted framework) that acts like a metal detector for errors.

Instead of asking a human to check every single page, the system works like this:

The AI Scout: A powerful AI reads the translation and asks, "Does this look right to me?"
The Filter:
- If the AI says, "This looks perfect," the human skips it. (The researchers found the AI is very good at spotting correct answers; it rarely flags a good answer as bad).
- If the AI says, "This looks suspicious," or "I'm not sure," it puts a red flag on that page.
The Human Expert: The human reviewer only looks at the pages with red flags.

4. The Result: Doing Less, Getting More

This "spot-check" method was incredibly efficient.

Old Way (Random Checking): To get a dataset that is 90% accurate, a human would have to read through 70% to 74% of the entire library.
New Way (Smart Spot-Checking): By only looking at the pages the AI flagged as suspicious, the human reached 90% accuracy after reading only 13% to 24% of the library.

The Takeaway

Think of it like looking for a needle in a haystack.

Before: You were told to pull out every single piece of hay and check it to find the needles.
Now: You have a magnet (the AI) that pulls out the metal (the errors). You only have to inspect the metal the magnet found.

The paper concludes that by using AI to guide human attention toward the most likely mistakes, we can clean up massive datasets much faster and cheaper, ensuring that future AI systems are trained on high-quality, accurate information. They have released the corrected datasets and the code for this "spot-check" system so others can use it.

Technical Summary: Fixing FOLIO and MALLS

Problem Statement

The translation from Natural Language (NL) to First-Order Logic (FOL) is a critical component of neurosymbolic AI and Natural Language Inference (NLI). However, the quality of existing benchmarks used to train and evaluate these systems has not been rigorously audited. This paper identifies that widely used datasets, specifically FOLIO and MALLS, contain significant annotation errors and ambiguities in their ground truth labels. These errors distort the evaluation of state-of-the-art Large Language Models (LLMs), leading to inaccurate performance metrics. Furthermore, exhaustive manual review of large datasets is cost-prohibitive and does not scale, necessitating a more efficient method for dataset curation.

Methodology

1. Systematic Human Audit and Correction

The authors conducted a systematic human inspection of the FOLIO validation split (275 instances) and a subset of the MALLS test set (100 instances). Two experienced reviewers (PhD student and research fellow) independently annotated the data, cross-checked results, and resolved conflicts via consensus.

Ontology Handling: Since datasets lack explicit ontologies, the authors extracted signatures (predicates, arities, constants) from FOL formulas and used an LLM to assign natural language meanings, followed by manual verification. They distinguished between inconsistencies (conflicting arities/meanings), which were corrected, and ontological looseness (unconventional but consistent conventions), which were preserved to avoid rewriting the entire dataset.
Error Classification: The audit categorized errors into:
- Syntactic Errors: Parenthesis mismatches, typos, ontology misuse (10.5% in FOLIO, 3% in MALLS).
- Semantic Errors: Valid formulas that misrepresent NL meaning, including quantifier scope errors and missing information (28.3% in FOLIO, 33% in MALLS).
- Ambiguities: NL sentences admitting multiple non-equivalent but defensible formalizations (16.4% in FOLIO, 48% in MALLS).
- NLI Label Inconsistencies: Labels (True/False/Unknown) inconsistent with the provided formalizations (8.4% in FOLIO).
Control Group: The authors also reviewed 213 instances from the GGC dataset (Barker-Plummer et al., 2011b), a high-quality, instructor-validated corpus, to verify that their curation framework does not introduce noise into already-correct data.

2. LLM-Assisted Oversight Framework

To address the scalability issue of manual review, the authors propose a framework that uses LLMs to prioritize human effort.

Verdict-and-Refinement (V&R) Task: An LLM is tasked with evaluating a triplet $(p, \Omega, \phi)$ $(p, Ω, ϕ)$ —where $p$ $p$ is an NL sentence, $\Omega$ $Ω$ is an ontology, and $\phi$ $ϕ$ is a candidate FOL formula. The LLM produces:
1. A verdict $v \in \{yes, no, ?\}$ (correct, incorrect, or ambiguous/uncertain).
2. A refinement $\psi$ (a corrected formula if $v \neq yes$ ).
Pipelines: Two pipeline designs were tested:
- Pipeline 1 (Direct V&R): The LLM judges the original formula $\phi$ directly.
- Pipeline 2 (Re-generation): The LLM first generates a new candidate $\hat{\phi}$ from $p$ and $\Omega$ , then judges this new candidate.
Prioritization Strategy: The framework leverages the empirical finding that LLMs rarely flag correct formalizations as incorrect (false positive rate $\approx 3\%$ in FOLIO). By directing human reviewers to instances flagged as "no" (incorrect) or "?" (ambiguous) first, the framework aims to maximize accuracy gains per unit of human effort.

Key Contributions

Corrected Datasets: The authors released revised ground truths for the FOLIO validation split and a MALLS test subset, correcting 39% and 36% of entries respectively, along with corrected NLI labels where applicable.
Evaluation Impact Analysis: The paper demonstrates that annotation errors significantly penalize model evaluation. Re-evaluating three state-of-the-art LLMs (Gemma 4 31B-it, Qwen3-30B-A3B, GPT-4o-mini) against the corrected ground truths resulted in accuracy gains ranging from +9 to +22 percentage points.
LLM-Assisted Oversight Framework: A novel strategy that reduces the cost of dataset curation. By focusing human review on the subset of instances flagged as error-prone by the LLM, the framework achieves 90% dataset accuracy after reviewing only 24% of FOLIO instances and 13% of MALLS instances. This is a substantial reduction compared to unguided random review, which requires over 70% of instances to reach the same accuracy.

Results

Error Rates: The human audit confirmed that approximately 39% of FOLIO and 36% of MALLS instances contain incorrect FOL formalizations. Additionally, 16.4% of FOLIO and 48% of MALLS contain ambiguous NL sentences.
Performance Shifts: When tested on the curated datasets, all evaluated models showed improved translation accuracy. For example, Gemma 4 31B-it saw a +21.8% increase on FOLIO (all instances) and +18.0% on MALLS.
Efficiency of Oversight:
- Pipeline 1 outperformed Pipeline 2 and baseline methods (random review of original or regenerated data) across all metrics (Area Under the Curve, $T_{90}$ , $T_{95}$ ).
- Using the prioritization order (malformed outputs $\to$ ? $\to$ no $\to$ yes), the framework reached 90% accuracy with minimal human effort (24% for FOLIO, 13% for MALLS).
- On the high-quality GGC dataset, the framework introduced negligible noise (degradation $\le 5\%$ ), confirming its reliability when applied to data that is already largely correct.

Significance and Claims

The paper claims that the quality of NL-to-FOL benchmarks has been a "black box" that has distorted the evaluation of neurosymbolic AI systems. By providing corrected ground truths, the authors show that previous performance estimates were artificially suppressed by annotation noise.

The proposed LLM-assisted framework offers a practical solution to the "scaling" problem of dataset curation. It demonstrates that it is possible to achieve high-quality datasets without the prohibitive cost of exhaustive human review. The authors position this framework as a tool for:

Dataset Curation: Allowing curators to focus exclusively on suspicious instances.
Formal Methods: Acting as a warning layer for experts reviewing NL specifications.
Runtime Verification: Providing on-the-fly feedback on whether generated formulas capture intended requirements in scenarios where manual review is impossible.

The authors release the corrected datasets and code for the framework to support reproducibility, while noting that the conclusions are specific to the tested datasets and LLMs and may require adaptation for other logical formalisms or domains.