💻 computer science

Inference-Time Diversity in RL-Trained Lean Theorem Provers: A Diagnostic Study

Este estudo revela que os provadores de teoremas Lean treinados com RL sofrem de colapso de modo no tempo de inferência, o que pode ser efetivamente mitigado pela aplicação de um cronograma fixo de esqueletos de táticas diversos para recuperar ganhos significativos de desempenho, enquanto o parafraseamento de prompts e comentários irrelevantes provam ser ineficazes ou prejudiciais.

Autores originais: Zachary Burton

Publicado 2026-05-19

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Zachary Burton

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine um estudante brilhante que foi treinado para resolver quebra-cabeças matemáticos muito difíceis usando uma linguagem de computador especial chamada Lean. Este estudante, vamos chamá-lo de "DeepSeek", é incrivelmente inteligente, mas tem um hábito estranho: quando solicitado a resolver um quebra-cabeça, ele fica preso em uma rotina mental.

Este artigo é um relatório de diagnóstico sobre por que isso acontece e como corrigi-lo. Aqui está a história do que os pesquisadores descobriram, contada em termos do cotidiano.

1. O Problema: O Efeito "Disco Riscado"

Os pesquisadores notaram que, quando pediam ao DeepSeek para resolver o mesmo quebra-cabeça matemático repetidamente (apenas com sementes aleatórias ligeiramente diferentes, como rolar dados), o estudante continuava tentando exatamente o mesmo primeiro passo.

A Analogia: Imagine que você está tentando abrir uma porta trancada. Você tenta a chave na fechadura. Não funciona. Você tenta novamente. Ainda não funciona. Você tenta uma terceira vez, e uma centésima vez. Mesmo que você tente 64 vezes, você está apenas enfiando a mesma chave na mesma fechadura da mesma maneira. Você não está explorando outras chaves ou outras maneiras de abrir a porta.
O Resultado: No estudo, dobrar o número de tentativas de 32 para 64 não resolveu um único novo quebra-cabeça. O estudante sofreu um "colapso de modo"—ficou preso em um caminho estreito e não conseguia pensar em mais nada.

2. A Correção: Dar uma Dica de "Primeiro Passo"

Os pesquisadores perceberam que o estudante não era preguiçoso; ele estava apenas muito preso em sua rotina. Então, tentaram um novo truque: antes de pedir ao estudante para resolver o quebra-cabeça, deram-lhe uma instrução específica sobre como começar.

A Analogia: Em vez de apenas dizer "Resolva este quebra-cabeça", os pesquisadores disseram "Comece simplificando os números" ou "Comece introduzindo uma nova variável". É como dar ao estudante uma chave específica para tentar primeiro, em vez de deixá-lo adivinhar.
O Resultado: Este pequeno empurrão quebrou a rotina. O estudante de repente começou a resolver muitos mais quebra-cabeças. A "rotina" não era porque o estudante era ruim em matemática; era porque ele era muito rígido em como começava.

3. O "Porquê": É um Problema de Treinamento, Não de Cérebro

Os pesquisadores queriam saber: o estudante é naturalmente ruim em matemática, ou foi o treinamento que o tornou rígido?

O Experimento: Eles testaram o estudante antes de receber o treinamento matemático especial (o modelo "Base").
A Descoberta: O estudante não treinado não conseguia resolver nenhum quebra-cabeça. Ele apenas desistia ou repetia a pergunta.
A Conclusão: O treinamento especial (Aprendizado por Reforço) é o que ensinou o estudante a resolver quebra-cabeças em primeiro lugar. Mas, esse mesmo treinamento é também o que o tornou rígido e preso em uma rotina. O treinamento criou a habilidade, mas também criou o problema do "disco riscado".

4. Quem Mais Tem Este Problema?

Os pesquisadores testaram outros "estudantes" (diferentes modelos de IA) para ver se este era um problema universal.

O Estudante "SFT": Um estudante foi treinado de forma diferente (Ajuste Fino Supervisionado). Este estudante era na verdade melhor em resolver quebra-cabeças no geral, mas não tinha o problema de "rotina". Quando os pesquisadores deram dicas a ele, isso na verdade o tornou ligeiramente pior. Ele já era flexível o suficiente para encontrar seu próprio caminho.
Os Estudantes "RL": Os estudantes treinados com o método especial de "Aprendizado por Reforço" (como o DeepSeek) foram os que ficaram presos. Eles precisavam das dicas de "primeiro passo" para sair de seu pensamento estreito.

5. A Evidência do "Primeiro Movimento"

Para provar que isso não era apenas uma coincidência, os pesquisadores analisaram os reais "primeiros movimentos" que os estudantes fizeram.

A Descoberta: De 64 tentativas em um único quebra-cabeça, o estudante "preso em rotina" usou exatamente o mesmo primeiro movimento em quase metade dos casos. Eles eram incrivelmente previsíveis.
A Metáfora: Se você pedisse a um humano para escrever uma história 64 vezes, ele poderia começar com "Era uma vez", "O sol estava brilhando" ou "Era uma noite escura". Mas este estudante de IA começaria com "Era uma vez" 32 vezes e "O sol estava brilhando" 30 vezes. Eles tinham quase nenhuma variedade em sua abertura.

Resumo

O artigo conclui que o Aprendizado por Reforço (uma maneira específica de treinar IA) cria uma faca de dois gumes:

Ensina à IA como resolver provas matemáticas formais (algo que ela não conseguia fazer antes).
Mas também torna a IA tão focada em algumas estratégias "vencedoras" que ela para de explorar novas.

A solução não é dar à IA mais poder de processamento ou mais tempo para pensar; é dar a ela orientação estrutural—um pequeno empurrão sobre como começar a prova. Isso força a IA a quebrar sua rotina e explorar novos caminhos, desbloqueando soluções que ela era anteriormente teimosamente incapaz de encontrar.

Resumo Técnico: Diversidade em Tempo de Inferência em Provedores de Teoremas Lean Treinados com RL

Declaração do Problema

Provedores de teoremas neurais recentes, particularmente aqueles treinados com Aprendizado por Reforço (RL) e recompensas verificáveis (RLVR), alcançaram desempenho robusto em benchmarks de prova formal como miniF2F. A suposição predominante é que o treinamento suficiente com RL e o aumento da capacidade computacional em tempo de inferência (via amostragem i.i.d.) permitem que os modelos internalizem os priores estruturais necessários para provas formais.

Este artigo desafia essa suposição, diagnosticando um fenômeno de colapso de modo em tempo de inferência em provedores Lean treinados com RL. Especificamente, os autores observam que o aumento do orçamento de amostragem ( $k$ ) produz retornos decrescentes muito antes do esperado. No benchmark miniF2F-test com DeepSeek-Prover-V1.5-RL, dobrar o orçamento de amostragem de $k=32$ para $k=64$ produz zero teoremas adicionais resolvidos (estagnado em 42/244). O modelo converge para um conjunto estreito de estratégias de prova e falha em explorar alternativas, mesmo quando fornecido com amostras estocásticas adicionais.

Metodologia

O estudo emprega um framework de diagnóstico controlado usando DeepSeek-Prover-V1.5-RL e sua variante base não-RL, juntamente com comparações inter-modelo com DeepSeek-Prover-V2-7B (RL) e Goedel-Prover (apenas SFT).

1. A Intervenção do Cronograma de Esqueletos

Para testar se o platô é devido à falta de diversidade estrutural e não à falta de capacidade computacional, os autores introduzem um cronograma fixo e determinístico de 15 esqueletos de táticas.

Estrutura: Uma grade $15 \times 8 = 120$ combinando 15 esqueletos de táticas Lean selecionados manualmente (ex: simp, intro, constructor, aesop) com 8 comentários de dica de objetivo (sugestões em linguagem natural).
Execução: Para um orçamento $k$ , o modelo tenta as primeiras $k$ entradas desta grade. Isso força o modelo a iniciar provas com aberturas estratégicas específicas, em vez de depender de amostragem aleatória.
Ablações: Para isolar a fonte de melhoria, os autores comparam:
- B-RL (Esqueleto): O cronograma estruturado de 15 esqueletos.
- C1 (Paráfrase): 16 paráfrases semanticamente equivalentes de instruções (sem estrutura de tática).
- C2 (Comentários Irrelevantes): 16 comentários Lean sem conteúdo.
- C3 (NL-only): Uma condição dedicada usando apenas dicas em linguagem natural sem prefixos de tática.

2. Estratificação de Dificuldade

Os autores definem uma pontuação empírica de dificuldade de formalização ( $\sigma$ ) usando uma construção leave-one-out. Para um teorema alvo, $\sigma$ conta quantos outros modelos de linha de base (Goedel-Prover, V2-7B) o resolvem sem intervenção. Isso estratifica os teoremas em buckets: Fronteira (não resolvidos por outros), Difícil, Médio, Fácil e Trivial.

3. Medição Distribucional Direta

Para ir além dos platôs comportamentais, os autores analisam a diversidade do cabeçalho da primeira tática em 13.159 amostras estocásticas. Eles contam o número de identificadores de táticas líderes distintos (ex: have, rw, norm_num) gerados por teorema.

Resultados Chave

1. Quebrando o Platô via Orientação Estrutural

Colapso da Linha de Base: DeepSeek-Prover-V1.5-RL com amostragem i.i.d. resolve 38 teoremas em $k=16$ , 42 em $k=32$ e permanece em 42 em $k=64$ .
Eficácia do Esqueleto: O cronograma fixo de esqueletos quebra este platô, resolvendo 55 teoremas em $k=16$ (+45% de melhoria relativa) e continuando a encontrar novas provas até $k=64$ (60 no total).
Descobertas de Ablação:
- Estrutura vs. Diversidade: Paráfrases de instruções (C1) produzem o mesmo pass@16 que a linha de base (38/244), enquanto comentários irrelevantes (C2) degradam o desempenho para 25/244. Isso confirma que os ganhos são impulsionados por orientação estrutural, não mera diversidade de prompt.
- NL vs. Táticas: A condição NL-only (C3) resolve 48/244, intermediária entre a linha de base e os esqueletos completos. Isso indica que dicas em linguagem natural recuperam aproximadamente 58% da lacuna, enquanto prefixos literais de táticas contribuem com o restante.

2. Localização do Ganho

O ganho estrutural está concentrado nos buckets Fácil e Trivial (teoremas solucionáveis por outros provedores de código aberto, mas perdidos pela amostragem i.i.d. do V1.5-RL).

Na coluna combinada Fácil+Trivial, a intervenção de esqueleto produz um ganho líquido de +15, enquanto paráfrases produzem 0 e comentários irrelevantes produzem -14.
Nenhuma perturbação desbloqueia o bucket "Fronteira" (teoremas não resolvidos por nenhuma linha de base), sugerindo que a intervenção remedia a subexploração de problemas conhecidos como solucionáveis, em vez de expandir a fronteira de capacidade.

3. Especificidade do RL do Colapso de Modo

Contraste do Modelo Base: DeepSeek-Prover-V1.5-Base (não-RL) prova zero teoremas sob qualquer condição (i.i.d. ou esqueletos). Isso estabelece que o RL é o locus tanto da capacidade de prova quanto do subsequente colapso de modo. O modelo base carece da capacidade de gerar provas válidas; o estágio de RL cria a capacidade, mas a colapsa em uma política estreita.
Contraste Inter-Modelo:
- V2-7B (RL): Mostra um ganho agregado plano (+1), mas desbloqueia +3 teoremas de fronteira inacessíveis a qualquer linha de base i.i.d.
- Goedel-Prover (SFT): Mostra um ganho negativo (-10,0 $\pm$ 4,4) com esqueletos. Modelos treinados com SFT parecem já explorar um conjunto amplo de troncos de táticas, tornando o cronograma fixo de esqueletos redundante ou restritivo.

4. Evidência Direta de Colapso

A análise distribucional revela que o teorema mediano recebe apenas 2 cabeçalhos de primeira tática distintos em 64 amostras, com 49% do benchmark recebendo uma abertura estratégica única determinística. A entropia de Shannon observada é $\le 8\%$ da capacidade teórica, confirmando um colapso de modo severo.

Significado e Alegações

O artigo reestrutura a narrativa de "esqueletos de táticas melhoram o desempenho" para "provedores treinados com RL exploram severamente pouco o espaço de táticas em tempo de inferência".

RL como Agente Dual: Os autores afirmam que o RL desempenha um papel duplo: é o estágio que cria a capacidade de prova (já que o modelo base não possui nenhuma) e simultaneamente o estágio que colapsa essa capacidade em uma política estreita.
Escalonamento em Tempo de Inferência: Os resultados sugerem que simplesmente escalar a capacidade computacional de inferência via amostragem i.i.d. tem retornos decrescentes muito mais cedo do que assumido. A diversidade estrutural (variando estratégias de prova via prompts) é um eixo mais eficiente para escalonamento.
Remediabilidade: O colapso de modo é específico de modelos treinados com RL. Modelos treinados com SFT não exibem o mesmo colapso recuperável via dicas estruturais; de fato, eles sofrem com isso. Isso implica que intervenções futuras (regularização de entropia em tempo de treinamento ou recuperação de esqueletos em tempo de inferência) devem navegar o trade-off entre criar capacidade e manter a diversidade.

O estudo conclui que o "colapso de modo" é um fenômeno real, contingente ao pipeline, inerente ao processo de ajuste fino com RL em domínios de verificação formal, e que intervenções estruturais fixas podem efetivamente recuperar a exploração perdida sem exigir treinamento adicional.