GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving

O artigo apresenta o GAR, um quadro de aprendizado por reforço generativo-antagônico que treina conjuntamente a composição e a resolução de problemas em um loop adversarial, melhorando a eficiência do treinamento e o desempenho na prova de teoremas formais complexos.

O essencial

Imagine que você está tentando ensinar um robô superinteligente a resolver os problemas de matemática mais difíceis do mundo, como provar teoremas complexos que podem levar anos para humanos. O desafio é que, se você der a ele apenas exercícios fáceis, ele fica entediado e não aprende nada novo. Mas se você der problemas impossíveis de cara, ele desiste e fica frustrado.

O artigo que você enviou apresenta uma solução genial chamada GAR (Aprendizado por Reforço Adversarial Generativo). Pense no GAR não como um professor solitário, mas como um par de atletas olímpicos treinando juntos: um é o Atleta (o Provedor) e o outro é o Treinador de Obstáculos (o Fuser de Declarações).

Aqui está como funciona essa "dança" de treinamento, explicada de forma simples:

1. O Cenário: O Problema dos Exercícios Estáticos

Antes do GAR, os robôs de matemática eram treinados com uma lista fixa de problemas (como um livro de exercícios antigo).

• O problema: O robô resolvia os fáceis rapidamente e perdia tempo. Quando chegava nos difíceis, ele travava. O livro de exercícios nunca mudava, mesmo que o robô ficasse mais inteligente. Era como tentar correr em uma esteira que nunca acelera: você não melhora sua velocidade máxima.

2. A Solução GAR: O Treinamento em Dupla

O GAR cria um ciclo de treinamento onde dois modelos de IA aprendem um com o outro ao mesmo tempo:

• O Provedor (O Atleta): Sua tarefa é provar teoremas (resolver os problemas). Ele ganha pontos quando acerta.
• O Fuser (O Treinador de Obstáculos): Sua tarefa é criar novos problemas. Mas ele não cria qualquer problema; ele pega dois problemas existentes e os "funde" (mistura) para criar um novo problema mais difícil, mas que ainda seja possível de resolver.

3. A Magia do "Currículo Implícito"

Aqui está a parte brilhante: eles competem, mas cooperam.

• O Treinador quer: Criar um problema que o Atleta quase consiga resolver, mas que seja difícil o suficiente para exigir um esforço extra. Se o problema for muito fácil, o Treinador perde pontos. Se for impossível, ele também perde.
• O Atleta quer: Resolver esses problemas difíceis para ganhar pontos.

A Analogia do Jogo de Tênis:
Imagine um jogo de tênis onde você joga contra um parceiro.

• No começo, o parceiro bate a bola devagar (problemas fáceis). Você acerta tudo.
• O GAR faz com que o parceiro (o Treinador) perceba que você está acertando tudo e comece a bater a bola um pouco mais forte e com mais efeito (problemas mais difíceis).
• Você (o Atleta) é forçado a melhorar seu jogo para devolver a bola.
• Se você melhorar muito, o parceiro aumenta a dificuldade novamente.
• Resultado: Você nunca fica entediado (problemas fáceis demais) e nunca desiste (problemas impossíveis). Você evolui constantemente, subindo de nível automaticamente.

4. O Truque da "Fusão"

Como o Treinador cria esses problemas novos? Ele não inventa do nada. Ele pega dois problemas de matemática que já existem (por exemplo, um sobre preços de móveis e outro sobre geometria) e pede para a IA misturar as ideias principais deles em um único problema novo e mais complexo. É como pegar uma receita de bolo e uma de pizza e criar um "Bolo-Pizza" novo e desafiador.

5. O Resultado: Robôs Mais Inteligentes

Os autores testaram isso com dois robôs famosos (Goedel-Prover e DeepSeek-Prover).

• O que aconteceu? Depois de treinar com esse método, os robôs conseguiram resolver muito mais problemas difíceis do que antes.
• A prova: Em testes padrão de matemática, eles melhoraram significativamente. O DeepSeek-Prover, por exemplo, aumentou sua taxa de sucesso em problemas de nível universitário de 22% para quase 26% (o que é uma grande vitória nessa área).

Resumo em uma frase

O GAR é um sistema onde a IA que cria os problemas e a IA que resolve os problemas treinam juntas em uma competição saudável, garantindo que a dificuldade dos exercícios cresça exatamente na mesma velocidade que a inteligência do robô, criando um ciclo de aprendizado perfeito e contínuo.

É como ter um professor que sabe exatamente qual é o próximo passo ideal para você aprender, sem que você precise pedir ajuda.

Resumo técnico

1. O Problema

O provamento de teoremas formais em linguagens como Lean tem impactado significativamente a matemática e a ciência da computação. No entanto, os modelos de estado da arte (SOTA) atuais enfrentam limitações críticas:

• Dependência de Conjuntos de Dados Fixos: A maioria das abordagens de Aprendizado por Reforço (RL) ou iteração de especialistas utiliza conjuntos de problemas estáticos. Isso resulta em treinamento ineficiente, onde o modelo gasta recursos em tarefas triviais ou impossíveis, e limita a capacidade de resolver problemas complexos à medida que o modelo evolui.
• Falta de Curriculo Adaptativo: Métodos de RL avançados carecem de um mecanismo para ajustar a dificuldade dos problemas dinamicamente durante o processo de rollout, restringindo a exploração concentrada em teoremas desafiadores.
• Ambiguidade e Verificação: A linguagem natural (NL) é ambígua para verificação de passos intermediários, enquanto a linguagem formal (FL) exige expertise. A transição entre elas e a geração de novos problemas adaptados ao nível do modelo é um desafio não resolvido de forma sistemática.

2. Metodologia: O Framework GAR

Os autores propõem o GAR (Generative Adversarial Reinforcement Learning), um framework de treinamento que otimiza conjuntamente dois agentes em um loop adversarial: o Provedor (solver) e o Fusionador de Declarações (statement fuser/composer).

O processo ocorre em iterações, divididas em duas fases principais:

A. Fase de Geração (Statement Fusion)

• Fusão de Declarações: Em vez de apenas formalizar problemas existentes, o Fusionador (baseado em modelos de raciocínio como Qwen3 ou DeepSeek-R1) combina dois problemas naturais (NL) do repositório base para criar um novo problema mais desafiador.
• Separação NL-FL: O processo fusiona as declarações em Linguagem Natural primeiro e, em seguida, utiliza um autoformalizador para convertê-las em Lean (FL). Isso evita erros de compilação comuns quando se tenta fundir diretamente declarações formais.
• Reinicialização do Pensamento: Para evitar "superpensamento" (overthinking) e garantir foco, o processo de raciocínio do Fusionador é reiniciado com um token indicador dedicado (<analysis>).
• Geração de Provas: O Provedor gera múltiplas candidatas de prova para as novas declarações, que são verificadas pelo verificador Lean4.

B. Fase de Aprendizado por Reforço Adversarial

Ambos os modelos são otimizados usando uma variante do algoritmo GRPO (Group Relative Policy Optimization):

• Treinamento do Fusionador (Compositor): Recebe recompensa por gerar problemas que sejam difíceis, mas solucionáveis. O objetivo é reduzir a taxa de aprovação (pass rate) do provedor, mas não a zero (o que indicaria problemas insolúveis).
  • Mecanismo de Penalidade: Introduz-se uma penalidade suave para modificações de declaração (statement modification). Modelos com forte capacidade de auto-correção tendem a simplificar o problema para ganhar recompensa (reward hacking). O GAR penaliza essa alteração excessiva, mantendo a integridade do problema original.
• Treinamento do Provedor: Recebe recompensa por gerar provas corretas para problemas de dificuldade média e alta.
  • Filtragem de Dados: Problemas com taxa de aprovação 0 (impossíveis) ou > 0.5 (muito fáceis) são filtrados, garantindo que o provedor treine apenas em um "curriculo implícito" de desafios adequados.

3. Principais Contribuições

1. Framework GAR: Um novo paradigma de RL que estabelece um curriculo implícito, alinhando a dificuldade do problema com a capacidade evolutiva do provedor, eliminando o desperdício computacional em tarefas triviais.
2. Técnica de Fusão de Declarações: Uma metodologia inovadora para criar novos teoremas formais combinando conceitos de problemas existentes em NL, superando a simples formalização direta e gerando problemas melhor alinhados com a capacidade do modelo.
3. Paradigma Geral de Co-evolução: Demonstra que a co-evolução adversarial entre a geração de problemas e a resolução em ambientes verificáveis é uma estratégia eficaz, aplicável a outros domínios intensivos em raciocínio.

4. Resultados Experimentais

Os autores avaliaram o GAR treinando dois modelos base: Goedel-Prover-V2-8B e DeepSeek-Prover-V2-7B.

• MiniF2F-Test (Benchmark de Olimpíada):
  • O modelo DeepSeek-Prover-V2 melhorou sua taxa de sucesso (pass@32) de 70.49% para 74.18% (+5.23% relativo).
  • O modelo Goedel-Prover-V2 alcançou 80.33% (ganho de +3.16% relativo).
• ProofNet-Test (Matemática Universitária Avançada):
  • O DeepSeek-Prover-V2 aumentou sua performance de 22.58% para 25.81%, demonstrando capacidade de lidar com tópicos mais complexos (análise real, álgebra abstrata).
• Estudos de Ablação:
  • A remoção da penalidade de modificação de declaração levou a um aumento drástico na taxa de alteração de problemas (de ~30% para ~74%), confirmando a necessidade do mecanismo de penalidade para evitar reward hacking.
  • Comparado ao treinamento direto de RL (GRPO) em dados estáticos, o GAR superou consistentemente, enquanto o treinamento estático em modelos já fortemente treinados via RL tendeu a degradar o desempenho.

5. Significado e Impacto

O trabalho GAR representa um avanço significativo na automação de provação de teoremas ao resolver o problema de estagnação de dados. Ao invés de depender de conjuntos de dados fixos que se tornam obsoletos à medida que o modelo melhora, o GAR cria um ciclo de feedback dinâmico onde o "professor" (Fusionador) ajusta a dificuldade para manter o "aluno" (Provedor) em um estado de aprendizado ideal.

Isso não apenas melhora o desempenho em benchmarks existentes, mas oferece uma estrutura geral para o treinamento adversarial em ambientes verificáveis, permitindo que modelos de IA explorem estratégias de raciocínio mais profundas e resolvam teoremas de nível universitário e de competição que antes eram inatingíveis. O código de treinamento foi aberto para fomentar a pesquisa na área.