Resumo Técnico: Aprendizado por Reforço Verificado por Processo para Demonstração de Teoremas via Lean

Definição do Problema

A Demonstração Automática de Teoremas (ATP) visa gerar provas formais para teoremas matemáticos. Embora os Grandes Modelos de Linguagem (LLMs) tenham avançado em tarefas de raciocínio, eles geralmente dependem de linguagem natural (NL) ou recompensas binárias (correto/incorreto) durante o Aprendizado por Reforço (RL). Isso cria uma lacuna:

1. Feedback Esparso: Abordagens padrão de RL frequentemente utilizam apenas um sinal binário final (prova passou/falhou), o que fornece atribuição de crédito esparsa e tem dificuldade em guiar o modelo através de longas cadeias de raciocínio.
2. Não Estruturado vs. Estruturado: Ao contrário dos assistentes de prova simbólicos (ex: Lean, Coq, Isabelle), que oferecem verificação de tipo refinada de cada passo do raciocínio, os LLMs são treinados em sequências de tokens com recompensas escalares.
3. Modelos de Recompensa de Processo (PRMs): Embora trabalhos recentes utilizem PRMs para fornecer recompensas ao nível do passo, estes frequentemente exigem grandes conjuntos de dados anotados ou dependem de supervisão de CoT baseada em NL, carecendo da correção rigorosa da verificação simbólica.

O desafio central abordado é como alavancar o feedback rico e estruturado de um assistente de prova simbólico (Lean) para treinar LLMs sem depender de PRMs externos potencialmente ruidosos ou anotações humanas.

Metodologia

O artigo propõe o Aprendizado por Reforço Verificado por Processo, um framework que integra o feedback simbólico do Lean diretamente em um objetivo de Otimização de Política Relativa de Grupo (GRPO). O método consiste em três componentes principais:

1. Oráculo de Processo Simbólico

Em vez de tratar o Lean meramente como um verificador final, os autores o utilizam como um oráculo de processo durante o treinamento.

• Parsing: As provas geradas são analisadas em sequências de táticas ($T_1, \dots, T_N$) baseadas na Árvore de Sintaxe Abstrata (AST).
• Verificação: O processo de elaboração do Lean fornece dois tipos de sinais:
  • Sinal de Resultado: Um escore binário global $g(Y) \in \{0, 1\}$ indicando se toda a prova é válida.
  • Sinal de Processo: Feedback detalhado para cada tática, identificando passos localmente válidos e a localização específica do primeiro erro.

2. Estratégia de Atribuição de Crédito

Para preencher a lacuna entre o feedback simbólico e o RL ao nível de token, os autores introduzem regras de atribuição específicas:

• Propagação do Primeiro Erro: Se uma tática $T_j$ falha, todas as táticas subsequentes ($T_k$ onde $k \ge j$) são tratadas como errôneas. Isso reflete a natureza causal das provas: um prefixo inválido invalida toda a cadeia de raciocínio subsequente.
• Pontuação ao Nível de Tática ($\phi$):
  • Se a prova passa ($g(Y)=1$), todas as táticas recebem um escore positivo (1).
  • Se a prova falha ($g(Y)=0$):
    • As táticas antes do primeiro erro recebem um escore parcial ($d_1$).
    • A primeira tática errônea e todas as subsequentes recebem um escore de penalidade ($d_2$).
• Mapeamento ao Nível de Token: A vantagem ao nível de tática é atribuída apenas ao primeiro token de cada tática (a palavra-chave, ex: intro, apply). Isso alinha-se ao ponto de decisão semântica onde a estratégia de prova é determinada.

3. Objetivo de RL (Integração GRPO)

O framework combina vantagens de resultado e de processo em um único objetivo GRPO:

• Vantagem de Resultado ($A_{outcome}$): Calculada com base no status global de passagem/falha em relação à média do grupo.
• Vantagem de Processo ($A_{process}$): Calculada com base nos escores de tática, normalizados pela média de resultado do grupo para considerar a dificuldade do problema.
• Vantagem Combinada: Para um token $t$ pertencente ao primeiro token da tática $j$ na resposta $i$:
  $$A_{i,t} = A_{outcome, i, t} + A_{process, i, j}$$
  Para tokens não-primeiros, apenas a vantagem de resultado é aplicada. Esta formulação evita a necessidade de um modelo de valor ou de um PRM auxiliar, baseando-se exclusivamente no ground truth do verificador.

Principais Contribuições

1. Formalização do Feedback Simbólico: Os autores formalizam o feedback de nível de tática do Lean em sinais de treinamento escalares, permitindo atribuição de crédito refinada ao nível de token sem orientação em linguagem natural.
2. RL Guiado por Verificador Simbólico: Eles integram recompensas de resultado e de tática derivadas diretamente do Lean em um framework de RL, fornecendo atribuição de crédito densa e verificável.
3. Melhorias Estáveis em Benchmarks: A abordagem demonstra melhorias consistentes nos benchmarks MiniF2F e ProofNet, superando o RL de apenas resultado e os baselines vanilla sem exigir PRMs externos ou notação de NL.

Resultados Experimentais

Os experimentos foram conduzidos utilizando STP-Lean e DeepSeek-Prover-V1.5 (modelos de 7B) nos benchmarks MiniF2F-Test e ProofNet-Test.

• Ganhos de Desempenho:
  • STP-Lean: O método proposto melhorou o pass@64 do MiniF2F em +2.5% (de 56.7% para 59.2%) e o pass@32 do ProofNet em +1.4%.
  • DeepSeek-Prover-V1.5: Melhorias consistentes, embora marginais, foram observadas em todas as configurações.
• Comparação com Baselines:
  • O método superou o GRPO de "Apenas Resultado", que mostrou instabilidade e falhou em melhorar no ProofNet em algumas configurações.
  • Alcançou resultados competitivos contra fortes baselines de busca em árvore (ex: InternLM2.5-StepProver, DeepSeek-Prover-RL+RMaxTS) usando uma abordagem de geração de disparo único sem orçamentos massivos de busca em tempo de inferência.
• Estudos de Ablação:
  • Atribuição de Token: Atribuir crédito ao primeiro token de uma tática rendeu os resultados mais estáveis em comparação com a distribuição de crédito por todos os tokens ou pelo último token.
  • Propagação do Primeiro Erro: Remover esta regra degradou significativamente o desempenho, confirmando a necessidade de tratar os passos subsequentes como inválidos após um erro.
  • Timeouts: Um timeout de verificação de 15 segundos proporcionou o melhor equilíbrio, incentivando provas concisas sem descartar provas complexas válidas.

Significância e Alegações

O artigo alega que os assistentes de prova simbólicos não devem ser vistos apenas como ferramentas de avaliação, mas como oráculos ativos de recompensa de processo durante o treinamento. Ao alavancar o "feedback estruturado rico e detalhado" inerente aos sistemas de raciocínio formal, os autores demonstram um caminho para frameworks de RL que combinam a escalabilidade de LLMs com a confiabilidade da verificação simbólica.

O estudo destaca que:

• Sinais Densos e Verificáveis: O uso dos logs de erro e árvores de elaboração do próprio prover fornece um sinal de recompensa denso e sólido que é superior a resultados binários esparsos ou PRMs aprendidos.
• Estabilidade: A combinação de recompensas de resultado global e recompensas de tática local estabiliza o treinamento, evitando a convergência prematura vista no treinamento apenas de táticas e os problemas de esparsidade do treinamento de apenas resultado.
• Eficiência: Esta abordagem alcança um desempenho de estado da arte ou competitivo sem o overhead computacional de busca em árvore ou os requisitos de dados para treinar PRMs separados.

Os autores mantêm modéstia quanto às limitações, observando que seu método depende de escores de recompensa fixos ($d_1, d_2$) em vez de estimadores de vantagem aprendidos e atualmente foca em provas puras de Lean sem CoT, deixando aberto o design de recompensas para raciocínio de linguagem natural de longo formato.