Learning to Disprove: Formal Counterexample Generation with Large Language Models

Este artigo apresenta uma abordagem para aprimorar modelos de linguagem na geração de contraexemplos matemáticos, utilizando uma estratégia de mutação simbólica e um framework de iteração com múltiplas recompensas para treinar modelos que produzem contraexemplos com provas formais verificáveis no Lean 4.

O essencial

Imagine que você está tentando ensinar um robô superinteligente a resolver problemas de matemática. Até agora, a maioria dos robôs (Inteligências Artificiais) foi treinada apenas para uma coisa: provar que algo é verdadeiro. É como se eles fossem mestres em construir castelos de areia perfeitos, mas não soubessem como encontrar a onda que derruba o castelo.

Este artigo, chamado "Aprendendo a Refutar" (Learning to Disprove), apresenta uma nova abordagem para ensinar esses robôs a fazer o oposto: encontrar o "bug" ou o exemplo que prova que uma afirmação está errada.

Aqui está uma explicação simples, usando analogias do dia a dia:

1. O Problema: O Robô que só diz "Sim"

Na matemática, para provar que uma regra é falsa, você não precisa provar tudo; você só precisa de um único exemplo que quebre a regra.

• Exemplo: Se alguém diz "Todos os cisnes são brancos", você não precisa caçar todos os cisnes do mundo. Basta encontrar um cisne preto para derrubar a teoria.
• O que faltava: As IAs atuais são ótimas em construir argumentos longos para dizer "Sim, isso é verdade". Mas quando elas tentam dizer "Não, olhe aqui, existe um cisne preto", elas falham. Elas não têm prática em "caçar" esses exemplos. Além disso, faltam muitos "treinos" (dados) para elas aprenderem a fazer isso.

2. A Solução: O "Laboratório de Mutação"

Como não há muitos exemplos de "cisnes pretos" prontos para treinar o robô, os autores criaram um método genial chamado Mutação Simbólica.

Imagine que você tem uma receita de bolo infalível (um teorema provado) que diz: "Se você usar farinha, ovos e açúcar, o bolo fica bom."

• A Mutação: O robô pega essa receita e, de propósito, joga o "açúcar" fora.
• O Resultado: Agora a receita diz: "Se você usar farinha e ovos, o bolo fica bom."
• O Desafio: O robô precisa encontrar um caso onde, sem açúcar, o bolo fica horrível (o "contraexemplo").

Ao fazer isso sistematicamente com milhares de teoremas matemáticos, eles criaram um "superconjunto de dados" com 575.000 problemas novos. É como se eles tivessem criado um ginásio de exercícios onde o robô é forçado a encontrar falhas em regras que parecem certas, mas que estão incompletas.

3. O Treinamento: O Sistema de Dupla Recompensa

Treinar um robô para encontrar erros é difícil porque, se ele errar, ele não recebe nenhum feedback (é como tentar adivinhar um número e não saber se está perto ou longe).

Os autores criaram um sistema de dupla recompensa:

1. Recompensa 1 (O "Não"): O robô precisa provar que a parte que ele removeu (o açúcar) era, de fato, necessária. Ele deve mostrar: "Veja, sem açúcar, o bolo quebrou!"
2. Recompensa 2 (O "Sim"): O robô precisa provar que o bolo que ele criou (o exemplo específico) realmente funciona como um contraexemplo.

Se o robô conseguir fazer as duas coisas, ele ganha pontos. Isso ajuda o robô a aprender mesmo quando o problema é muito difícil, evitando que ele desista ou fique "preso" em soluções fáceis.

4. O Processo: Dois Passos (Chute e Verificação)

O robô aprende a pensar em duas etapas, como um detetive:

1. A Chute (Raciocínio Informal): "Hum, se eu tirar o açúcar e usar apenas farinha e ovos, talvez o bolo fique seco. Vou tentar imaginar um bolo específico com esses ingredientes."
2. A Verificação (Prova Formal): "Ok, agora vou escrever isso na linguagem matemática perfeita (Lean 4) para que o computador verifique se o meu bolo realmente não funciona."

Se o computador (o "Juiz") aprovar, o robô aprende. Se não, ele tenta de novo.

5. Os Resultados: O Detetive Matemático

Os autores testaram esse novo robô em três bancas de prova diferentes.

• O Resultado: O robô treinado com esse método ficou muito melhor do que os modelos mais inteligentes do mundo (como o GPT-4 ou o DeepSeek-R1) na tarefa de encontrar erros matemáticos.
• A Melhoria: Em alguns testes, ele acertou 47% a 74% mais problemas do que os concorrentes.

Resumo em uma frase

Os autores ensinaram a IA a não ser apenas um "construtor de castelos", mas também um "caçador de falhas", criando um método para gerar milhões de exercícios de "onde está o erro?" e treinando o robô a encontrar esses erros com precisão cirúrgica, usando a linguagem matemática formal para garantir que a resposta seja 100% correta.

Isso é crucial porque, na ciência e na matemática, saber o que não funciona é tão importante quanto saber o que funciona.

Resumo técnico

Título: Aprendendo a Refutar: Geração de Contraexemplos Formais com Grandes Modelos de Linguagem

1. O Problema

O raciocínio matemático exige duas habilidades complementares: a construção de provas rigorosas para afirmações verdadeiras e a descoberta de contraexemplos para refutar afirmações falsas. Embora os esforços atuais de IA em matemática se concentrem quase exclusivamente na construção de provas formais, a tarefa de encontrar contraexemplos permanece subexplorada.

Existem dois desafios principais que impedem o avanço nesta área:

1. Escassez de Dados de Treinamento: Não existem grandes conjuntos de dados específicos para contraexemplos formais. O único dataset existente (CounterMath) contém apenas cerca de 1.200 problemas em linguagem natural, insuficientes para treinar modelos de linguagem (LLMs) modernos.
2. Sinais de Recompensa Esparsos: Em problemas complexos, se o LLM falha em gerar um contraexemplo correto, não há sinal de recompensa (o gradiente desaparece), impedindo o aprendizado contínuo. A maioria dos modelos atinge um platô de baixa taxa de sucesso.

Além disso, a geração de contraexemplos difere da prova tradicional: enquanto a prova segue uma dedução lógica linear, a geração de contraexemplos segue um paradigma de "adivinhar e verificar" (guess-and-check), onde o modelo deve propor uma instância específica e depois provar formalmente que ela viola a conjectura.

2. Metodologia Proposta

Os autores propõem um framework integrado que combina síntese de dados simbólicos e treinamento guiado por múltiplas recompensas. O processo divide-se em duas fases principais:

A. Síntese de Problemas de Contraexemplo (Mutação Simbólica)
Para resolver a escassez de dados, os autores desenvolveram uma estratégia de mutação que transforma teoremas prováveis em problemas de contraexemplo:

1. Coleta de Sementes: Reúnem teoremas formalmente prováveis em formato universal (ex: $\forall x, H_1(x) \land H_2(x) \to C(x)$) a partir de bibliotecas como Mathlib, Leanworkbook e provas geradas por LLMs.
2. Mutação: O sistema remove deliberadamente uma hipótese necessária (ex: $H_1$) do teorema original. Se a hipótese era essencial, o novo teorema (agora $\exists x, H_2(x) \to C(x)$) torna-se falso, indicando a existência de um contraexemplo.
3. Validação: O provador de teoremas Lean 4 é usado para garantir que a hipótese removida era de fato necessária e que o novo problema é sintaticamente correto.
4. Resultado: Esta estratégia gerou 575.000 instâncias de contraexemplos a partir de cerca de 322.000 teoremas semente.

B. Treinamento Guiado por Múltiplas Recompensas (Multi-Reward)
Para superar o problema da recompensa esparsa, os autores introduzem um esquema de recompensa dupla baseado na lógica do contraexemplo:

1. Geração: O LLM propõe um candidato a contraexemplo ($x^*$).
2. Verificação Dupla: O modelo deve gerar duas provas formais no Lean 4:
   • Prova do Teorema Mutado: Provar que $x^*$ satisfaz a conclusão do teorema modificado ($H_2(x^*) \to C(x^*)$).
   • Prova da Hipótese Removida: Provar que $x^*$ viola a hipótese que foi descartada ($\neg H_1(x^*)$).
3. Cálculo de Recompensa: A recompensa total é a soma ponderada das duas verificações. Como provar a violação da hipótese removida é geralmente mais fácil do que provar o teorema mutado complexo, a primeira recompensa garante que o modelo receba feedback mesmo quando falha na parte mais difícil.
4. Iteração de Especialistas: O modelo é refinado iterativamente (Expert Iteration), usando as soluções bem-sucedidas (com suas recompensas) para fine-tuning supervisionado.

3. Contribuições Principais

• Novo Paradigma de Treinamento: Estabelece um pipeline de "raciocínio informal para formal" específico para contraexemplos, onde o modelo primeiro propõe uma instância concreta em linguagem natural e depois a formaliza.
• Estratégia de Mutação Simbólica: Uma técnica robusta para gerar automaticamente um dataset massivo e diversificado de problemas de contraexemplo, superando a dependência de dados manuais.
• Mecanismo de Recompensa Dupla: Resolve o problema da esparsidade de recompensas ao garantir que o modelo receba feedback válido mesmo em etapas intermediárias do raciocínio, acelerando a convergência.
• Benchmarks Novos: Criaram três novos benchmarks para avaliar a tarefa:
  1. FOR-COUNTER: Identificação de contraexemplos.
  2. VERI-REASON: Verificação de erros em passos de raciocínio.
  3. VERI-FORMALIZE: Verificação de erros em resultados de autoformalização.

4. Resultados Experimentais

Os experimentos foram conduzidos em servidores com GPUs de alto desempenho, utilizando modelos base como Qwen3 8B (para raciocínio informal) e DeepSeek-Prover-v2 7B (para provas formais).

• Eficiência da Mutação: A estratégia de mutação alcançou uma taxa de sucesso de 1,65 a 2,48 (gerando mais de 1 problema de contraexemplo por teorema semente) com um tempo de execução médio de 0,3 a 0,7 segundos por teorema.
• Desempenho de Treinamento: O treinamento com múltiplas recompensas convergiu mais rápido e atingiu um desempenho superior comparado ao treinamento com recompensa única.
  • No conjunto de validação, o modelo com múltiplas recompensas atingiu 49% de sucesso em pass@1, contra 43% do baseline de recompensa única.
• Comparação com o Estado da Arte (SOTA): O modelo ajustado (Ours) superou significativamente tanto modelos proprietários (como GPT-4.1, Gemini-2.5, Grok-3) quanto provadores de teoremas de código aberto (como Leanabell, Goedel, DeepSeek-Prover).
  • Em pass@1, o modelo proposto resolveu 95 a 78 problemas a mais do que o baseline mais forte em diferentes benchmarks.
  • Houve uma melhoria relativa de 47% a 74% na taxa de sucesso pass@1 em comparação com os melhores baselines existentes.

5. Significado e Impacto

Este trabalho preenche uma lacuna crítica na pesquisa de IA matemática, demonstrando que a capacidade de "refutar" é tão vital quanto a de "provar".

• Automação da Pesquisa Matemática: A ferramenta permite que LLMs atuem como copilotos práticos para validar conjecturas, identificando rapidamente casos onde uma hipótese pode estar faltando ou sendo falsa.
• Melhoria do Raciocínio: Ao forçar os modelos a pensarem em casos de borda e exceções (contraexemplos), o framework melhora a capacidade de autoverificação e a confiabilidade lógica dos LLMs.
• Escalabilidade de Dados: A metodologia de síntese de dados via mutação simbólica oferece um caminho viável para gerar dados de treinamento de alta qualidade para tarefas formais complexas onde a anotação humana é inviável.

Em resumo, o artigo demonstra que, ao combinar a síntese de dados inteligente com um esquema de recompensa robusto, é possível treinar modelos de linguagem para dominar a arte de encontrar e provar formalmente contraexemplos, elevando o estado da arte em raciocínio matemático formal.