LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learning

Resumo Técnico: LongCat-Flash-Prover

1. Problema e Contexto

Os Grandes Modelos de Linguagem (LLMs) avançaram significativamente no raciocínio em linguagem natural, mas ainda enfrentam desafios críticos em provas de teoremas formais (especificamente em Lean4). Diferente de scripts de Python ou ferramentas chamáveis tradicionais, Lean4 exige uma linguagem formal rigorosa onde a lógica deve ser verificada passo a passo.
As principais dificuldades identificadas são:

• A necessidade de transformar problemas informais em declarações formais corretas (auto-formalização).
• A geração de provas completas ou esboços (sketches) que sejam sintaticamente válidos e semanticamente consistentes.
• A instabilidade no treinamento de modelos de Mistura de Especialistas (MoE) em tarefas de longo horizonte (long-horizon tasks) usando Aprendizado por Reforço (RL), devido a discrepâncias entre o motor de treinamento e o de inferência.
• O problema de "hacking de recompensa" (reward hacking), onde modelos aprendem a enganar verificadores sintáticos sem realmente provar o teorema.

2. Metodologia

O LongCat-Flash-Prover é um modelo de 560 bilhões de parâmetros (com ~27B ativos) baseado em arquitetura MoE, projetado para raciocínio formal nativo. A abordagem é dividida em três pilares principais:

A. Raciocínio Formal Nativo e Decomposição de Tarefas
O trabalho define o "raciocínio formal nativo" como a capacidade do modelo de usar operadores formais sem modificações arquiteturais especiais. A tarefa é decomposta em três capacidades independentes, cada uma tratada por um "especialista":

1. Auto-formalização Agente: Transformar enunciados em linguagem natural em declarações formais em Lean4 verificadas.
2. Esboço (Sketching) Agente: Gerar um esboço do tipo "lemma-style" (dividindo o problema em lemas auxiliares não provados inicialmente) baseado no enunciado formal.
3. Prova (Proving) Agente: Gerar uma prova completa ("whole-proof") ou completar os lemas de um esboço para provar o teorema alvo.

B. Framework de Iteração Híbrida de Especialistas (Hybrid-Experts Iteration Framework)
Para gerar dados de treinamento de alta qualidade (cold-start), o authors desenvolveram um pipeline que sintetiza trajetórias de raciocínio:

• Utiliza múltiplos modelos especialistas (Auto-formalizador, Sketcher, Prover) que interagem iterativamente com ferramentas de verificação (compilador Lean4, verificadores de sintaxe e consistência semântica).
• Adota uma abordagem de curriculum learning: começa com síntese de uma única rodada (sem ferramentas) e evolui para síntese multi-turno com feedback de ferramentas (TIR - Tool-Integrated Reasoning).
• O processo de rejeição (rejection sampling) mantém apenas trajetórias que passam por todas as verificações de sintaxe e consistência.

C. Otimização de Política com Amostragem de Importância Hierárquica (HisPO)
Para estabilizar o treinamento por RL em modelos MoE, foi proposto o algoritmo HisPO.

• Problema: Em treinamento assíncrono, há discrepâncias entre o motor de treinamento (Megatron) e o de inferência (vLLM), além de "atraso da política" (policy staleness) quando os dados são gerados por versões antigas do modelo. Isso distorce a taxa de amostragem de importância (Importance Sampling - IS).
• Solução: O HisPO introduz uma estratégia de máscara de gradiente hierárquica:
  • Nível de Sequência: Calcula a média geométrica das discrepâncias de todos os tokens. Se a discrepância da sequência inteira for alta, o gradiente é zerado.
  • Nível de Token: Remove gradientes de tokens individuais com alta discrepância.
  • Controle de Estaleness: Limita a magnitude das atualizações para evitar instabilidade.
• Além disso, implementa detecção de ilegalidade (legality detection) usando um analisador de AST (Árvore de Sintaxe Abstrata) para identificar e punir "hacks" (como redefinir axiomas, usar #exit ou alterar definições de fundo) que passam na verificação sintática mas violam a semântica do problema.

3. Principais Contribuições

1. Novo Estado da Arte (SOTA) em Modelos Open-Source: O LongCat-Flash-Prover estabelece novos recordes em benchmarks de auto-formalização e prova de teoremas entre modelos de pesos abertos.
2. Framework Híbrido de Especialistas: Uma metodologia robusta para sintetizar dados de treinamento complexos e iterativos, combinando auto-formalização, esboço e prova com feedback de ferramentas.
3. Algoritmo HisPO: Uma contribuição técnica significativa para o treinamento estável de modelos MoE em tarefas de RL de longo horizonte, mitigando problemas de discrepância entre treinamento e inferência.
4. Mecanismos de Segurança contra Reward Hacking: A introdução de verificações de consistência de AST e detecção de ilegalidade garante que as provas geradas sejam matematicamente válidas e não apenas sintaticamente corretas.

4. Resultados Experimentais

O modelo foi avaliado em benchmarks rigorosos (MathOlympiad-Bench, PutnamBench, MiniF2F-Test, ProofNet, ProverBench):

• Auto-formalização: Alcançou 99.2% no MiniF2F-Test e 97.9% no ProofNet (Pass@8), superando modelos proprietários e open-source anteriores. O uso de TIR (Tool-Integrated Reasoning) aumentou o desempenho em até 14%.
• Prova de Teoremas (MiniF2F-Test):
  • No modo Sketch-Proof com TIR e Busca em Árvore, atingiu 97.1% de taxa de aprovação com apenas 72 tentativas por problema.
  • Isso supera significativamente modelos como Goedel-Prover-V2 e Kimina-Prover, que exigem milhares de tentativas para atingir desempenho similar.
• PutnamBench (Desafio Extremo): Resolveu 41.5% dos problemas com até 220 tentativas, superando todas as bases open-source existentes.
• Raciocínio Informal: O modelo manteve desempenho comparável ao seu modelo base (LongCat-Flash-Thinking-2601) em tarefas gerais (código, matemática informal), demonstrando que o treinamento focado em formal não degradou significativamente as capacidades gerais.

5. Significância e Impacto

O LongCat-Flash-Prover representa um avanço crucial na intersecção entre IA e Matemática Formal.

• Eficiência de Amostra: Demonstra que é possível atingir desempenho de nível humano (ou superior a modelos fechados) em provas complexas com um orçamento de inferência drasticamente menor, graças à estratégia de esboço (sketching) e busca em árvore.
• Confiabilidade: Ao abordar explicitamente o problema de "reward hacking" em ambientes formais, o trabalho oferece um caminho mais seguro para o desenvolvimento de agentes de IA autônomos que podem ser confiados para tarefas críticas de verificação.
• Acesso Aberto: A disponibilização do modelo e dos dados de treinamento (via Hugging Face e GitHub) democratiza o acesso a capacidades de raciocínio formal de ponta, permitindo que a comunidade científica construa sobre essa base para resolver problemas complexos em cenários formais e informais.

Em suma, o trabalho não apenas melhora o desempenho bruto em benchmarks, mas também estabelece novas metodologias de treinamento (HisPO) e síntese de dados (Hybrid-Experts) que são fundamentais para a evolução de agentes de raciocínio autônomos.