Resumo Técnico: OProver: Uma Estrutura Unificada para Prova Formal de Teoremas Agêntica

Declaração do Problema

Avanços recentes na prova formal de teoremas, particularmente no ecossistema Lean 4, têm aproveitado a geração de provas em grande escala e o treinamento consciente do verificador para melhorar o desempenho em benchmarks como MiniF2F e PutnamBench. No entanto, uma limitação crítica persiste: as capacidades de prova agêntica (recuperação, feedback do compilador e reparo iterativo) são tipicamente tratadas como heurísticas aplicadas no momento da inferência a um provador fixo, em vez de políticas aprendidas integradas ao processo de treinamento.

Isso cria uma incompatibilidade entre treinamento e inferência. Modelos treinados principalmente em provas finalizadas e bem-sucedidas encontram feedback do compilador e contexto recuperado apenas durante a implantação, em distribuições para as quais nunca foram otimizados. Além disso, os corpora formais existentes focam em produtos finais (enunciados e provas verificadas), omitindo os históricos de interação de múltiplas rodadas — tentativas falhas, contexto recuperado e diagnósticos do compilador — essenciais para aprender a reparar provas. Consequentemente, o sinal de supervisão que impulsiona o reparo de provas na prática permanece amplamente subutilizado no treinamento de modelos.

Metodologia

O artigo apresenta o OProver, uma estrutura unificada que integra recuperação, feedback do compilador e reparo iterativo diretamente na política do provador por meio de um pipeline de treinamento coevolutivo.

1. A Estrutura OProver

O OProver trata a prova de teoremas como um loop de refinamento limitado e de múltiplas rodadas. Em cada rodada $t$, a política $\pi$ condiciona-se a um estado compacto $X_t = (s, R_t, p_{t-1}, f_{t-1})$, onde:

• $s$: O enunciado do teorema alvo.
• $R_t$: As top-$k$ provas recuperadas e verificadas pelo compilador de uma memória $M$.
• $p_{t-1}$: A tentativa de prova anterior.
• $f_{t-1}$: O feedback textual bruto do compilador (diagnósticos) do verificador Lean 4.

A política gera uma tentativa revisada $p_t$. Se a verificação falhar, o feedback bruto é passado de volta à política para a próxima rodada. Crucialmente, a política condiciona-se apenas à tentativa e ao feedback mais recentes, preservando sinais de correção locais enquanto mantém o estado compacto.

2. OProofs: Um Corpus de Treinamento Unificado

Para suportar essa estrutura, os autores constroem o OProofs, um corpus em grande escala projetado especificamente para prova agêntica. Diferentemente de conjuntos de dados anteriores que preservam apenas provas finais, o OProofs registra trajetórias serializadas incluindo:

• Contexto recuperado.
• Tentativas falhas.
• Feedback bruto do compilador.
• Reparos subsequentes.

O OProofs é construído a partir de três fontes: recursos Lean públicos, síntese de prova em grande escala (autoformalização + verificação) e rastros da prova agêntica do próprio OProver. Ele contém 1,77 milhão de enunciados Lean únicos e 6,86 milhões de provas verificadas pelo compilador, emparelhados com 1,07 milhão de trajetórias agênticas.

3. Pipeline de Treinamento Coevolutivo

O processo de treinamento segue um loop iterativo (Algoritmo 1) onde o provador e o corpus coevoluem:

1. Pré-treinamento Contínuo (CPT): Um modelo base é treinado em uma mistura de código Lean, matemática e dados de raciocínio de longo contexto para criar o OProver-Base.
2. Pós-treinamento Iterativo:
   • Execuções Agênticas: A política atual realiza prova de múltiplas rodadas em um pool de teoremas, recuperando da memória atual $M_k$ e verificando com o compilador Lean.
   • Coleta de Dados: Novas provas verificadas são adicionadas ao corpus e indexadas na memória de recuperação. Tentativas falhas e reparos bem-sucedidos são decompostos em exemplos por nível de rodada $(s, R_t, p_{t-1}, f_{t-1}) \to p_t$.
   • Ajuste Fino Supervisionado (SFT): O modelo é atualizado usando os exemplos de reparo coletados.
   • Aprendizado por Reforço (RL): A Otimização de Política de Sequência em Grupo (GSPO) é aplicada a casos não resolvidos mais difíceis, usando um sinal de recompensa baseado no sucesso da verificação e na correção do formato.
   • Recirculação: O corpus e a memória atualizados alimentam a próxima iteração, permitindo que a política aprenda com suas próprias provas melhoradas.

Contribuições Principais

1. Estrutura Unificada para Prova Agêntica: O OProver unifica recuperação, feedback e reparo iterativo em uma única política aprendida, eliminando a incompatibilidade entre treinamento e inferência ao treinar o modelo para usar esses sinais como parte de sua estratégia central, em vez de heurísticas externas.
2. Corpus OProofs: A construção de um corpus em grande escala (1,77 milhão de enunciados, 6,86 milhões de provas) que preserva explicitamente históricos de interação de múltiplas voltas, incluindo tentativas falhas e feedback bruto do compilador, fornecendo supervisão anteriormente indisponível em conjuntos de dados formais.
3. Pipeline Coevolutivo: Uma metodologia de treinamento onde o provador gera novos dados (provas verificadas e trajetórias de reparo) que são imediatamente incorporados ao corpus de treinamento e à memória de recuperação, criando um loop de autoaperfeiçoamento.
4. Desempenho de Ponta: O OProver alcança resultados de primeiro escalão entre provadores de prova inteira com pesos abertos, demonstrando que estratégias de refinamento agêntico podem superar modelos significativamente maiores.

Resultados Experimentais

O OProver foi avaliado em cinco benchmarks Lean 4: MiniF2F, MathOlympiadBench, ProofNet, ProverBench e PutnamBench.

• Desempenho: O modelo OProver-32B alcançou as melhores pontuações Pass@32 em três benchmarks (MiniF2F: 93,3%, ProverBench: 58,2%, PutnamBench: 11,3%) e o segundo melhor nos outros dois (MathOlympiad: 22,8%, ProofNet: 33,2%).
• Eficiência: O OProver-32B (32B parâmetros) superou o DeepSeek-Prover-V2 de 671B e o LongCat-Flash-Prover de 560B (com TIR) na maioria dos benchmarks, apesar de ter significativamente menos parâmetros. Até mesmo a variante de 8B superou o Goedel-Prover-V2 de 32B em todos os benchmarks.
• Escalonamento no Tempo de Teste: O desempenho melhorou consistentemente com orçamentos de computação aumentados (mais amostras ou rodadas de refinamento), embora com retornos decrescentes. A alocação ótima entre profundidade de refinamento e largura de amostragem variou conforme a dificuldade do benchmark.
• Estudos de Ablação: A remoção do feedback do compilador de múltiplas voltas causou a degradação de desempenho mais significativa, confirmando o refinamento iterativo como o principal motor de ganhos. A remoção da augmentação por recuperação também causou quedas consistentes, embora menores, destacando o valor complementar da fundamentação por recuperação.

Significado e Alegações

O artigo afirma que o OProver demonstra que a prova formal de teoremas agêntica pode ser aprendida efetivamente como uma política unificada, em vez de ser montada a partir de módulos separados no momento da inferência. Ao treinar na trajetória completa de construção de prova, falha e reparo, o modelo aprende a aproveitar o feedback do compilador e o contexto recuperado como partes intrínsecas de seu processo de raciocínio.

Os autores enfatizam que os ganhos de desempenho não são meramente resultado da escala do modelo, mas derivam da sinergia entre fundamentação aumentada por recuperação e refinamento iterativo guiado por compilador. A coevolução da política OProver e do corpus OProofs permite que o sistema melhore continuamente suas capacidades de prova, aprendendo com suas próprias tentativas bem-sucedidas e falhas, estabelecendo um novo paradigma para o treinamento de sistemas de raciocínio formal.