NeuroProlog: Multi-Task Fine-Tuning for Neurosymbolic Mathematical Reasoning via the Cocktail Effect

O NeuroProlog é um framework neurosimbólico que utiliza uma estratégia de treinamento multi-tarefa "Cocktail" para compilar problemas matemáticos em programas Prolog verificáveis, resultando em ganhos significativos de precisão e capacidade de auto-correção em modelos de linguagem de diferentes escalas.

O essencial

🧠 O Problema: O "Gênio" que Alucina

Imagine que você tem um estudante muito inteligente (um Modelo de Linguagem Grande, ou LLM) que leu todos os livros do mundo. Ele escreve textos lindos e responde perguntas com fluência. Mas, quando você pede para ele resolver um problema de matemática, ele às vezes inventa uma resposta que parece correta, mas está totalmente errada.

É como se ele estivesse adivinhando a resposta baseada em como as palavras soam, em vez de realmente fazer as contas. Ele é um "alucinador" confiante: a resposta flui bem, mas a lógica está quebrada.

🛠️ A Solução: NeuroProlog (O "Arquiteto" e o "Engenheiro")

Os autores criaram um novo sistema chamado NeuroProlog. Eles decidiram não deixar o computador apenas "adivinhar". Em vez disso, eles ensinaram o modelo a agir como um arquiteto que desenha um plano rigoroso (em uma linguagem de programação chamada Prolog) e depois deixa um engenheiro (um executor de código) verificar se o plano funciona de verdade.

Se o plano tiver um erro, o engenheiro avisa exatamente onde está o problema, e o arquiteto conserta.

🍹 O Segredo: O "Efeito Coquetel"

A grande inovação deste trabalho é a forma como eles treinaram o modelo. Eles usaram uma estratégia chamada Treinamento Multi-tarefa em Coquetel.

Imagine que você está ensinando alguém a cozinhar:

1. Método Antigo (Tarefa Única): Você só dá receitas de pratos complexos para a pessoa tentar fazer. Ela aprende a seguir o passo a passo, mas não entende por que o sal faz a comida ficar salgada.
2. Método NeuroProlog (O Coquetel): Você mistura três coisas na mesma aula:
   • A Teoria (KB): Ensinar a química dos ingredientes (o que é sal, o que é açúcar).
   • A Prática (SOLVE): Pedir para cozinhar pratos reais usando essa teoria.
   • O Degustação (Verificação): Provar o prato e ver se o sabor bate com a teoria.

Ao fazer tudo isso ao mesmo tempo (o "Coquetel"), o modelo aprende a conectar a teoria com a prática. Ele não apenas memoriza receitas; ele entende a lógica por trás delas.

🔄 O Ciclo de Correção: O "Detetive"

Quando o modelo tenta resolver um problema, ele não para na primeira tentativa. O sistema funciona assim:

1. O modelo escreve o código (o plano).
2. O computador executa o código.
3. Se der erro: O computador não apenas diz "errou". Ele diz: "Ei, você tentou dividir por zero!" ou "Você usou uma palavra onde deveria usar um número!".
4. O modelo recebe essa dica específica, corrige o código e tenta de novo.

Isso é como um detetive que não apenas vê o crime, mas aponta a pista exata para o suspeito se corrigir.

📊 O Que Eles Descobriram? (O Tamanho Importa)

O estudo testou modelos de tamanhos diferentes (de "pequenos" a "gigantes") e encontrou algo fascinante:

• Modelos Gigantes (32 Bilhões de parâmetros): Eles são como gênios maduros. Com o treinamento "Coquetel", eles aprenderam a entender a lógica profunda. Quando erram, o erro é fácil de consertar (como um erro de cálculo simples). A taxa de acerto subiu muito.
• Modelos Pequenos (8 Bilhões de parâmetros): Eles são como crianças aprendendo a escrever. O treinamento "Coquetel" ajudou a escrever as letras bonitas (a sintaxe do código), mas eles ainda não entendem o significado das palavras. Eles escrevem frases gramaticalmente corretas, mas que não fazem sentido lógico.
  • Analogia: É como um aluno que aprendeu a escrever "2 + 2 = 5" com uma caligrafia perfeita, mas ainda não sabe que a conta está errada.

💡 Conclusão Simples

O NeuroProlog mostrou que, para fazer matemática com inteligência artificial, não basta apenas pedir para o modelo "pensar". É preciso:

1. Ensinar a lógica (teoria) junto com a aplicação (exercícios).
2. Dar feedback imediato quando o modelo erra, para que ele aprenda a se corrigir sozinho.
3. Entender que modelos muito pequenos podem ter dificuldade em entender a "alma" da matemática, mesmo que escrevam o código perfeitamente.

Com essa abordagem, eles conseguiram que modelos de tamanho médio (20 bilhões de parâmetros) superassem modelos gigantes de outros métodos, provando que ensinar a pensar de forma estruturada é mais importante do que apenas ter um cérebro gigante.

Resumo técnico

Título: NeuroProlog: Ajuste Fino Multi-Tarefa para Raciocínio Matemático Neurosimbólico via Efeito Coquetel

1. O Problema

Os Grandes Modelos de Linguagem (LLMs) demonstraram desempenho robusto em tarefas de linguagem natural, mas continuam a ser pouco confiáveis no raciocínio matemático. Eles frequentemente geram soluções fluentes, mas logicamente inconsistentes, baseando-se em correspondência de padrões probabilísticos em vez de inferência lógica formal.

• Limitações Atuais: Abordagens tradicionais (como Chain-of-Thought) sofrem de fragilidade sob perturbações e não conseguem verificar passos intermediários. Métodos neurosimbólicos existentes geralmente aplicam a verificação simbólica apenas no momento da inferência (post-hoc), o que impede que o modelo internalize estruturas simbólicas durante o treinamento.
• Necessidade: Há uma lacuna na capacidade dos modelos de aprenderem simultaneamente a mapear linguagem natural para lógica formal, gerar programas executáveis e alinhar saídas simbólicas com verificação numérica.

2. Metodologia: NeuroProlog

O NeuroProlog é um framework neurosimbólico unificado que garante raciocínio verificável compilando problemas matemáticos em programas Prolog executáveis. A abordagem central baseia-se em três pilares:

A. Construção do Dataset (Corpus Unificado)

O treinamento utiliza um corpus combinado de duas fontes complementares:

1. Base de Conhecimento Matemático (KB): 200 entradas que formalizam conceitos matemáticos fundamentais (ex: estatística, lógica, geometria) como predicados Prolog executáveis. Cada entrada inclui comentários em linguagem natural para alinhamento semântico.
2. Dataset de Resolução de Problemas (SOLVE): 310 exemplos de problemas baseados na KB, mais 7.476 entradas do GSM8K-Prolog. Estes exemplos demonstram a aplicação procedural dos conceitos declarativos para resolver problemas específicos.

B. Treinamento Multi-Tarefa "Cocktail"

Em vez de treinar em tarefas isoladas, o modelo é submetido a um objetivo de "Cocktail" que otimiza conjuntamente três objetivos sinérgicos em um espaço de representação simbólico unificado:

1. Tradução Fórmula-Regra (KB): Mapear descrições de fórmulas para regras Prolog.
2. Síntese Linguagem-Programa (SOLVE): Gerar programas Prolog a partir de problemas de palavras.
3. Alinhamento Programa-Resposta: Garantir que a execução do programa produza a resposta numérica correta.

A função de perda combina as tarefas com pesos ajustáveis ($\lambda_{kb}$ e $\lambda_{solve}$), induzindo transferência positiva onde o conhecimento simbólico da KB melhora a capacidade de raciocínio composicional na tarefa de resolução.

C. Decodificação Guiada por Execução (Pipeline de Auto-Debug)

No momento da inferência, o sistema utiliza um pipeline iterativo:

1. O LLM gera um programa Prolog inicial.
2. Um executor Prolog (SWI-Prolog) executa o código.
3. Se houver erro, o sistema classifica o erro em uma taxonomia de 5 classes (Sintaxe, Tipo, Domínio, Instanciação, Lógica).
4. Um prompt de reparo direcionado é gerado com base no tipo de erro específico, permitindo que o modelo corrija o código iterativamente (até 3 tentativas) sem necessidade de treinamento específico para correção (zero-shot self-debugging).

3. Contribuições Principais

1. Treinamento Neurosimbólico Multi-Tarefa: Introdução de um objetivo "Cocktail" que combina conhecimento declarativo (KB) e resolução procedural (SOLVE), demonstrando que a mistura de modalidades de raciocínio dentro de um espaço simbólico unificado induz transferência cruzada superior.
2. Decodificação Guiada por Execução: Um pipeline de refinamento iterativo que utiliza taxonomias de erros formais para permitir auto-correção com taxa de sucesso de 92,7% em modelos de grande escala, sem treinamento adicional para correção.
3. Descoberta de Limiar de Capacidade Dependente de Escala: Evidência empírica de que o treinamento "Cocktail" transforma qualitativamente a distribuição de erros dependendo do tamanho do modelo:
   • Escala Grande (32B): Transforma erros de tipo não corrigíveis (semânticos) em erros de domínio corrigíveis.
   • Escala Pequena (8B): Elimina erros de sintaxe, mas introduz erros semânticos, revelando um limiar de capacidade (~10B parâmetros) necessário para o entendimento de tipos simbólicos.
4. Avaliação Abrangente e Código Aberto: Experimentos rigorosos em 12 configurações (4 modelos x 3 configurações) e liberação pública do dataset, código de treinamento e adaptadores LoRA.

4. Resultados Experimentais

Os experimentos foram conduzidos no conjunto de dados GSM8K (1.319 problemas) em quatro modelos com escalas de 3B a 32B parâmetros.

• Ganhos de Precisão: O treinamento "Cocktail" superou consistentemente as linhas de base de ajuste único (Prolog FT) e modelos base:
  • Qwen-32B: +5,23% de acurácia (atingindo 85,52%).
  • GPT-OSS-20B: +3,43% de acurácia (atingindo 88,34%).
  • Llama-3B: +5,54% de acurácia (atingindo 27,07%).
• Eficiência de Parâmetros: A melhor configuração (GPT-OSS-20B com 20B parâmetros) superou sistemas de síntese de programas maiores, como ToRA-Code-34B (80,7%) e OpenMath-70B (84,6%), demonstrando superior eficiência de parâmetros.
• Análise de Erros e Escala:
  • No modelo Qwen-32B, o treinamento reduziu erros finais de 39 para 9, transformando erros de tipo (87,2% dos erros base, 12% corrigíveis) em erros de domínio (55,6% dos erros, 96% corrigíveis).
  • No modelo Qwen3-8B, o ajuste fino melhorou a sintaxe, mas degradou a capacidade de correção (de 70,7% para 24,1%), resultando em uma queda líquida de acurácia, indicando que modelos abaixo de ~10B parâmetros não conseguem internalizar a semântica de tipos necessária para o auto-debug eficaz.
• Taxa de Correção: O modelo Qwen-32B com treinamento Cocktail alcançou uma taxa de correção de 92,7% após 3 iterações, demonstrando capacidade de auto-debug sem treinamento específico para correção.

5. Significado e Conclusão

O trabalho NeuroProlog estabelece que o treinamento multi-tarefa neurosimbólico é uma abordagem promissora para tornar o raciocínio matemático em LLMs mais robusto, interpretável e verificável.

• Mudança de Paradigma: Demonstra que a integração de conhecimento simbólico durante o treinamento (e não apenas na inferência) permite que os modelos internalizem padrões de raciocínio sistemático em vez de depender de heurísticas superficiais.
• Limitações de Capacidade: Revela um limiar crítico de capacidade (~10B parâmetros) para o aprendizado de raciocínio simbólico seguro a tipos. Modelos menores podem aprender sintaxe, mas falham na semântica profunda necessária para correção de erros.
• Aplicabilidade: A abordagem oferece uma base escalável para IA simbólica, com potencial para aplicações em domínios de alto risco (finanças, saúde) onde a verificação formal é obrigatória, superando as limitações de métodos puramente baseados em prompt ou verificação post-hoc.

Em suma, o NeuroProlog prova que a combinação de conhecimento declarativo e demonstrações procedurais, supervisionada por execução de código, cria modelos de linguagem matematicamente mais competentes e confiáveis.