Resumo Técnico: Corrigindo FOLIO e MALLS

Declaração do Problema

A tradução de Linguagem Natural (NL) para Lógica de Primeira Ordem (FOL) é um componente crítico da IA neurosimbólica e da Inferência de Linguagem Natural (NLI). No entanto, a qualidade dos benchmarks existentes usados para treinar e avaliar esses sistemas não foi rigorosamente auditada. Este artigo identifica que conjuntos de dados amplamente utilizados, especificamente o FOLIO e o MALLS, contêm erros significativos de anotação e ambiguidades em seus rótulos de verdade fundamental (ground truth). Esses erros distorcem a avaliação de Grandes Modelos de Linguagem (LLMs) de última geração, levando a métricas de desempenho imprecisas. Além disso, a revisão manual exaustiva de grandes conjuntos de dados é proibitiva em termos de custo e não escala, necessitando de um método mais eficiente para a curadoria de conjuntos de dados.

Metodologia

1. Auditoria e Correção Humana Sistemática

Os autores conduziram uma inspeção humana sistemática da divisão de validação do FOLIO (275 instâncias) e de um subconjunto do conjunto de teste do MALLS (100 instâncias). Dois revisores experientes (estudante de doutorado e pesquisador) anotaram os dados de forma independente, cruzaram os resultados e resolveram conflitos via consenso.

• Tratamento de Ontologia: Como os conjuntos de dados carecem de ontologias explícitas, os autores extraíram assinaturas (predicados, aridades, constantes) das fórmulas FOL e usaram um LLM para atribuir significados em linguagem natural, seguido de verificação manual. Eles distinguiram entre inconsistências (conflitos de aridade/significado), que foram corrigidas, e imprecisão ontológica (ontological looseness — convenções não convencionais, mas consistentes), que foram preservadas para evitar a reescrita de todo o conjunto de dados.
• Classificação de Erros: A auditoria categorizou os erros em:
  • Erros Sintáticos: Descompassos de parênteses, erros de digitação, uso indevido de ontologia (10,5% no FOLIO, 3% no MALLS).
  • Erros Semânticos: Fórmulas válidas que representam incorretamente o significado da NL, incluindo erros de escopo de quantificador e informações ausentes (28,3% no FOLIO, 33% no MALLS).
  • Ambiguidades: Sentenças em NL que admitem múltiplas formalizações não equivalentes, mas defensáveis (16,4% no FOLIO, 48% no MALLS).
  • Inconsistências de Rótulo de NLI: Rótulos (Verdadeiro/Falso/Desconhecido) inconsistentes com as formalizações fornecidas (8,4% no FOLIO).
• Grupo de Controle: Os autores também revisaram 213 instâncias do conjunto de dados GGC (Barker-Plummer et al., 2011b), um corpus de alta qualidade validado por instrutores, para verificar se o framework de curadoria deles não introduz ruído em dados que já estão corretos.

2. Framework de Supervisão Assistida por LLM

Para abordar o problema de escalabilidade da revisão manual, os autores propõem um framework que utiliza LLMs para priorizar o esforço humano.

• Tarefa de Veredito e Refinamento (V&R): Um LLM é encarregado de avaliar uma tripla $(p, \Omega, \phi)$ — onde $p$ é uma sentença em NL, $\Omega$ é uma ontologia e $\phi$ é uma fórmula candidata em FOL. O LLM produz:
  1. Um veredito $v \in \{sim, não, ?\}$ (correto, incorreto ou ambíguo/incerto).
  2. Um refinamento $\psi$ (uma fórmula corrigida se $v \neq sim$).
• Pipelines: Dois designs de pipeline foram testados:
  • Pipeline 1 (V&R Direto): O LLM julga a fórmula original $\phi$ diretamente.
  • Pipeline 2 (Regeração): O LLM primeiro gera uma nova candidata $\hat{\phi}$ a partir de $p$ e $\Omega$, e então julga esta nova candidata.
• Estratégia de Priorização: O framework aproveita a descoberta empírica de que os LLMs raramente sinalizam formalizações corretas como incorretas (taxa de falso positivo $\approx 3\%$ no FOLIO). Ao direcionar os revisores humanos para instâncias sinalizadas como "não" (incorreto) ou "?" (ambíguo) primeiro, o framework visa maximizar os ganhos de precisão por unidade de esforço humano.

Principais Contribuições

1. Conjuntos de Dados Corrigidos: Os autores lançaram versões revisadas das verdades fundamentais para a divisão de validação do FOLIO e um subconjunto do teste do MALLS, corrigindo 39% e 36% das entradas respectivamente, juntamente com rótulos de NLI corrigidos onde aplicável.
2. Análise de Impacto na Avaliação: O artigo demonstra que erros de anotação penalizam significativamente a avaliação de modelos. A reavaliação de três LLMs de última geração (Gemma 4 31B-it, Qwen3-30B-A3B, GPT-4o-mini) contra as verdades fundamentais corrigidas resultou em ganhos de precisão variando de +9 a +22 pontos percentuais.
3. Framework de Supervisão Assistida por LLM: Uma estratégia inovadora que reduz o custo da curadoria de conjuntos de dados. Ao focar a revisão humana no subconjunto de instâncias sinalizadas como propensas a erros pelo LLM, o framework atinge 90% de precisão no conjunto de dados após revisar apenas 24% das instâncias do FOLIO e 13% das instâncias do MALLS. Isso representa uma redução substancial em comparação com a revisão aleatória não guiada, que exige mais de 70% das instâncias para atingir a mesma precisão.

Resultados

• Taxas de Erro: A auditoria humana confirmou que aproximadamente 39% do FOLIO e 36% do MALLS contêm formalizações FOL incorretas. Além disso, 16,4% do FOLIO e 48% do MALLS contêm sentenças em NL ambíguas.
• Mudanças de Desempenho: Ao serem testados nos conjuntos de dados curados, todos os modelos avaliados mostraram melhoria na precisão de tradução. Por exemplo, o Gemma 4 31B-it teve um aumento de +21,8% no FOLIO (todas as instâncias) e +18,0% no MALLS.
• Eficiência da Supervisão:
  • O Pipeline 1 superou o Pipeline 2 e os métodos de base (revisão aleatória de dados originais ou regenerados) em todas as métricas (Área Sob a Curva, $T_{90}$, $T_{95}$).
  • Usando a ordem de priorização (saídas malformadas $\to$ ? $\to$ não $\to$ sim), o framework atingiu 90% de precisão com esforço humano mínimo (24% para FOLIO, 13% para MALLS).
  • No conjunto de dados de alta qualidade GGC, o framework introduziu ruído negligenciável (degradação $\le 5\%$), confirmando sua confiabilidade quando aplicado a dados que já são amplamente corretos.

Significância e Alegações

O artigo afirma que a qualidade dos benchmarks de NL-para-FOL tem sido uma "caixa preta" que distorceu a avaliação de sistemas de IA neurosimbólica. Ao fornecer verdades fundamentais corrigidas, os autores mostem que as estimativas de desempenho anteriores foram artificialmente suprimidas pelo ruído de anotação.

O framework assistido por LLM proposto oferece uma solução prática para o problema de "escala" da curadoria de conjuntos de dados. Ele demonstra que é possível obter conjuntos de dados de alta qualidade sem o custo proibitivo de uma revisão humana exaustiva. Os autores posicionam este framework como uma ferramenta para:

1. Curadoria de Conjuntos de Dados: Permitindo que curadores foquem exclusivamente em instâncias suspeitas.
2. Métodos Formais: Atuando como uma camada de aviso para especialistas que revisam especificações em NL.
3. Verificação em Tempo de Execução: Fornecendo feedback imediato sobre se as fórmulas geradas capturam os requisitos pretendidos em cenários onde a revisão manual é impossível.

Os autores disponibilizam os conjuntos de dados corrigidos e o código do framework para apoiar a reprodutibilidade, observando que as conclusões são específicas para os conjuntos de dados e LLMs testados e podem exigir adaptação para outros formalismos lógicos ou domínios.