Resource-Aware Neuro-Symbolic Reasoning for Local Small Language Models

Resumo Técnico: Raciocínio Neuro-Simbólico Consciente de Recursos para Modelos de Linguagem Pequenos Locais

Definição do Problema
Modelos de Linguagem Pequenos (SLMs) oferecem as vantagens da execução local, incluindo privacidade, disponibilidade offline e redução de custos operacionais. No entanto, sua capacidade limitada muitas vezes exige estratégias como a amostragem repetida (autoconsistência) para alcançar um raciocínio confiável, o que multiplica as chamadas ao modelo local, a geração de tokens e a latência serial. Embora existam abordagens neuro-simbólicas, elas frequentemente assumem capacidades gerais de prova de teoremas ou ignoram as restrições de recursos específicas do hardware do consumidor. O problema central abordado é se um pipeline neuro-simbólico limitado e verificável pode substituir a amostragem neural local repetida para tarefas de raciocínio estruturado sem sacrificar a precisão, especificamente dentro das restrições de SLMs locais.

Metodologia: O Pipeline VFR-LLM
Os autores propõem o pipeline Verifiable Formalization and Repair (VFR-LLM), uma arquitetura de cinco estágios projetada para transferir o raciocínio do modelo neural para um solver determinístico:

1. Formalização: O SLM traduz um problema de linguagem natural em uma representação de regras e restrições de domínio finito tipada. Esta linguagem intermediária inclui fatos fundamentados, regras do tipo Horn seguras e restrições de domínio finito (ex: ordenação, posições absolutas). Crucialmente, o modelo deve fornecer intervalos de origem (source spans) vinculando cada restrição extraída ao texto original.
2. Verificação de Cobertura: Uma camada de verificação inspeciona a formalização para garantir que cada restrição esteja fundamentada no texto de origem e que não existam regras não suportadas ou entidades desconhecidas.
3. Execução do Solver: Um solver determinístico (um solver enumerativo exato para as tarefas avaliadas) processa o programa formalizado para encontrar uma atribuição satisfatória (ex: uma ordenação total de entidades).
4. Reparo: Se o solver falhar ou se diagnósticos indicarem erros de formalização (ex: argumentos invertidos ou problemas de sintaxe), um módulo de reparo determinístico aplica edições locais baseadas apenas nos intervalos de origem e nos diagnósticos do solver. Nenhuma chamada adicional ao modelo ou respostas de referência (gold answers) são utilizadas durante esta etapa.
5. Geração de Resposta: A resposta final é derivada da saída do solver, vinculada às restrições verificadas.

O formalismo alvo é intencionalmente modesto: uma linguagem semelhante ao Datalog com domínios finitos, excluindo símbolos de função e quantificação ilimitada para garantir que o fardo da tradução permaneça gerenciável para modelos pequenos.

Principais Contribuições

1. Representação Rastreável: Definição de um formalismo de regras e restrições de domínio finito tipado que exige intervalos de origem para cada fato extraído, permitindo a auditabilidade da etapa de tradução.
2. Loop de Verificação e Reparo: Implementação de um pipeline que utiliza validação fundamentada na origem e reparo determinístico para identificar e corrigir falhas de formalização antes da execução do solver, em vez de depender de amostragem repetida.
3. Matriz de Avaliação Local: Uma avaliação abrangente usando LM Studio em Apple Silicon (M3 Pro) com três famílias de modelos: Qwen3-4B, Microsoft Phi-4-mini-reasoning e Gemma-3n-E4B. Os benchmarks incluem tarefas de precedência pura geradas, tarefas de precedência tipada geradas e dois subconjuntos derivados de BIG-Bench Hard (BBH) Logical Deduction (pareamento e estendido).
4. Comparação Consciente de Recursos: Uma comparação rigorosa contra a autoconsistência serial ($k=5$) e uma linha de base de autoconsistência adaptativa consciente de custo, medindo precisão, chamadas de modelo, total de tokens e latência serial.

Resultos
Os resultados empíricos revelam uma eficácia limitada e dependente do modelo para a abordagem VFR-LLM:

• Desempenho do Qwen3-4B:

  • Precedência Pura: Alcançou 0,983 de precisão com uma chamada de modelo, superando significativamente a autoconsistência serial (0,700 de precisão, 5 chamadas) e reduzindo o total de tokens em 34,4%.
  • BBH-Extended (Fonte Pública): Alcançou 0,933 de precisão contra 0,283 para autoconsistência e 0,317 para resposta direta. Embora o total de tokens tenha aumentado ligeiramente devido à extensão da formalização, o método reduziu as chamadas de modelo (1 vs. 5) e a latência serial (11,32s vs. 16,54s).
  • Restrições Tipadas: O desempenho foi "bloqueado" pela resposta direta, que permaneceu mais precisa e barata nestes estratos específicos.

• Desempenho do Gemma-3n-E4B:

  • Mostrou melhorias fortes em tarefas de precedência pura (0,683 vs. 0,367 para autoconsistência).
  • Os resultados em tarefas BBH-extended foram marginais (0,375 vs. 0,350 para resposta direta), onde o ganho de precisão não foi estatisticamente significativo.
  • As restrições tipadas mostraram resultados mistos, com a latência sendo frequentemente maior que a da resposta direta.

• Phi-4-mini-reasoning:

  • Demonstrou falhas severas de formalização em restrições tipadas, resultando em resultados negativos comparados à resposta direta.

• Testes de Robustez:

  • Linha de Base Adaptativa: Mesmo quando comparado a uma linha de base de autoconsistência adaptativa consciente de custo (que reduz as chamadas de 5 para ~4,2), o VFR-LLM manteve uma vantagem significativa de precisão em tarefas de precedência e BBH-extended para o Qwen.
  • Rastreabilidade: A alta precisão correlacionou-se fortemente com altas taxas de "totalmente rastreável" (restrições fundamentadas na origem). O Qwen alcançou uma taxa rastreável de 0,942 no BBH-extended, enquanto o Gemma alcançou apenas 0,292, explicando a lacuna de desempenho.
  • Ablações Determinísticas: O solver de domínio finito tipado resolveu 100% das instâncias de BBH-extended, enquanto um solver de apenas precedência resolveu apenas 20,8%, confirmando a necessidade do formalismo estendido para estas tarefas.

Significância e Alegações
O artigo evita explicitamente alegar que o raciocínio simbólico melhora universalmente o desempenho de LLMs locais ou reduz o computo para todas as tarefas. Em vez disso, estabelece uma alegação limitada:

1. Redução de Recursos Condicional: O VFR-LLM é uma alternativa viável e consciente de recursos à autoconsistência serial para tarefas estruturadas com restrições explícitas (especificamente ordenação e lógica de domínio finito) onde a resposta direta é insuficientemente precisa.
2. Dependência de Modelo: O sucesso do pipeline depende fortemente da capacidade do SLM em produzir formalizações fiéis e fundamentadas na origem. O método funciona bem para o Qwen em estratos específicos, mas falha ou oferece apenas ganhos marginais para o Phi e Gemma em cenários tipados mais complexos.
3. Auditabilidade: A principal contribuição não é apenas a precisão, mas a capacidade de fornecer um traço de raciocínio auditável e diagnosticar falhas (ex: distinguir erros de tradução de falhas do solver) sem o overhead de geração neural repetida.
4. Não Redução Geral de Computo: O artigo conclui que adicionar uma camada simbólica não reduz automaticamente os custos de computação; em muitos casos (ex: tarefas tipadas com Qwen), a resposta direta continua sendo a opção mais eficiente e precisa. O método é melhor visto como uma ferramenta de diagnóstico e uma alternativa especializada à amostragem repetida para classes específicas e limitadas de problemas.