Resumo Técnico: Melhorando a Tradução Simbólica de Modelos de Linguagem para Raciocínio Lógico

Declaração do Problema

A integração de Grandes Modelos de Linguagem (LMs) com resolvedores simbólicos externos (ex: Z3, Prover9) oferece um caminho verificável para o raciocínio lógico dedutivo. Este paradigma requer a tradução de Linguagem Natural (NL) para Lógica de Primeira Ordem (FOL). Embora eficaz para modelos grandes, os LMs menores e mais acessíveis enfrentam dificuldades significativas nesta tarefa de tradução. Eles frequentemente produzem saídas simbólicas incorretas devido a erros de formatação, violações de sintaxe e inconsistências semânticas. Abordagens existentes muitas vezes dependem de loops de autocorreção impulsionados pelo feedback do resolvedor, mas esses métodos dependem fortemente da capacidade do modelo subjacente de interpretar mensagens de erro e regenerar código preciso, uma força tipicamente reservada para modelos maiores e mais caros. Além disso, há uma escassez de dados simbólicos de alta qualidade para realizar o ajuste fino (fine-tuning) de modelos menores de forma eficaz.

Metodologia

Os autores propõem uma abordagem de três frentes para aumentar o desempenho de LMs menores (3B–4B de parâmetros) na tradução NL-para-FOL:

1. Síntese de Dados e Ajuste Fino Supervisionado (SFT)

Para abordar a falta de dados de treinamento simbólico, os autores sintetizam um conjunto de dados usando um grande modelo de linguagem (GPT-4o) sobre o dataset ProofWriter. Este processo envolve:

• Geração: Criação de pares NL-para-FOL.
• Filtragem: Um pipeline de múltiplos estágios incluindo correção de formato, validação de sintaxe usando Prover9 e filtragem semântica para garantir traduções de alta qualidade.
• Treinamento: Os dados sintetizados são combinados com datasets simbólicos existentes (FOLIO) para realizar o Ajuste Fino Supervisionado (SFT) em quatro modelos pequenos: Gemma-3-4B, Phi-4-mini, Qwen2.5-3B e Qwen3-4B. A entrada de treinamento concatena a sentença NL, o conjunto de predicados gerado e a representação FOL para impor padrões de geração estruturados.

2. Inferência Incremental

O artigo identifica que a inferência padrão de "próximo-token" frequentemente leva à propagação de erros, onde um único erro ao nível de token (ex: um erro de formatação) faz com que o modelo entre em loops repetitivos ou gere saídas malformadas. Para mitigar isso, os autores introduzem a Inferência Incremental, um processo de dois estágios:

• Estágio 1 (Geração de Predicados): O modelo primeiro produz um conjunto consistente de predicados ($\hat{P}$) necessários para todo o contexto do problema.
• Estágio 2 (Tradução FOL): Usando a entrada aumentada (sentenças NL + $\hat{P}$), o modelo gera as sentenças FOL completas.
  Esta decomposição impõe consistência de predicados entre as sentenças e permite a interrupção precoce, reduzindo significativamente os erros de formatação.

3. Módulo de Verificação

Aproveitando a separação da geração de predicados da geração de sentenças completas, os autores integram um Verificador leve. Este módulo, implementado como um pequeno LM com exemplos de poucos disparos (few-shot), verifica o conjunto de predicados gerado quanto a erros de aridade (ex: usar um predicado com contagens de argumentos inconsistentes) antes da etapa de tradução FOL. Se erros forem detectados, o verificador produz um conjunto de predicados corrigido; caso contrário, ele passa o conjunto original.

Principais Contribuições

• Taxonomia de Erros: Os autores categorizam erros comuns de tradução NL-para-FOL em quatro tipos: Parsing (falta de quantificadores, erros de parênteses), NoneType (localização de quantificadores, variáveis ausentes), Token (tokens especiais, operadores desconhecidos) e Predicado (incompatibilidade de aridade, conflitos sujeito-predicado).
• Pipeline de Síntese de Dados: Um framework robusto para gerar dados simbólicos de alta qualidade e verificados para treinar modelos menores, preenchendo a lacuna causada pela escassez de tais dados.
• Framework de Inferência Incremental: Uma estratégia de inferência inovadora que desacopla a geração de predicados da tradução de sentenças, melhorando a estabilidade da saída e a adesão ao formato sem exigir instruções adicionais no momento da inferência.
• Métricas de Predicado: Introdução de Cobertura (fração de predicados usados presente no conjunto inicial) e Uso (fração de predicados gerados que são realmente usados) para avaliar a consistência semântica, juntamente com taxas de execução padrão.

Resultados

O estudo avalia os métodos propostos através de quatro datasets de raciocínio lógico: ProofWriter, FOLIO, ProntoQA e ProverQA.

• Ganhos de Desempenho: O Ajuste Fino Supervisionado (SFT) melhora significativamente tanto as taxas de execução (a porcentagem de sentenças FOL válidas) quanto a precisão do raciocínio em comparação com as linhas de base de Aprendizado em Contexto (ICL) em todas as famílias de modelos.
• Redução de Erros: A combinação de SFT e Inferência Incremental leva a reduções substanciais em erros de formatação e sintaxe. Por exemplo, no dataset FOLIO, o modelo Qwen3-4B mostrou uma queda de 57,4% no total de erros.
• Fidelidade de Predicado: A inferência incremental melhora substancialmente a cobertura de predicados, particularmente em datasets fora da distribuição (OOD) como ProntoQA e ProverQA, ao garantir que o modelo defina explicitamente o conjunto de predicados antes de gerar a lógica.
• Impacto da Verificação: Adicionar o módulo de verificação de aridade melhora ainda mais a precisão do raciocínio, particularmente para modelos que lutam com conceitos abstratos (ex: ProntoQA), embora os ganhos sejam modestos comparados às melhorias provenientes do S SFT e da inferência incremental.
• Sensibilidade do Modelo: Os resultados indicam que o desempenho é altamente sensível à arquitetura específica do modelo e à natureza do dataset. Por exemplo, o Qwen3-4B mostrou ganhos significativos em datasets OOD, enquanto o Phi-4-mini teve dificuldades com a retenção de contexto em conjuntos de premissas longas sob inferência padrão.

Significância e Alegações

O artigo afirma mover o campo para mais perto do desenvolvimento de sistemas de raciocínio simbólico confiáveis e acessíveis. Ao demonstrar que modelos menores e de baixo custo podem alcançar raciocínio lógico de alta fidelidade através de síntese de dados estruturada e decomposição de inferência, os autores argumentam que a barreira para implantar sistemas neuro-simbólicos em ambientes com restrição de recursos é reduzida.

Os autores mantêm um tom modesto em relação às limitações:

• Os dados sintetizados, embora curados, podem conter inconsistências menores.
• O framework aborda a robustez sintática e de formatação, mas não garante totalmente a correção semântica (ou seja, a FOL pode ser sintaticamente válida, mas ainda assim representar incorretamente o significado pretendido da NL).
• O módulo de verificação introduz latência adicional de inferência, embora o processo de inferência incremental em si não aumente a latência além da contagem de tokens.
• Comparações comportamentais diretas entre modelos são difíceis devido à opacidade dos dados de pré-treinamento.

Em última análise, o trabalho sugere que a categorização sistemática de erros, o ajuste fino direcionado e a inferência estruturada são críticos para permitir que LMs menores funcionem efetivamente como componentes em pipelines de raciocínio lógico verificáveis.