Resumo Técnico: Por que o Provedor de Teoremas Agêntico Funciona

Declaração do Problema

Provedores de teoremas agênticos recentes, que combinam modelos de linguagem de grande escala (LLMs) com recuperação, busca e verificadores de assistentes de prova, demonstraram sucesso empírico na geração de provas matemáticas verificadas. No entanto, os quadros teóricos existentes lutam para explicar esse sucesso. A teoria da prova clássica aborda a existência de provas, enquanto a teoria da complexidade aborda a dificuldade no pior caso. Nenhum dos dois explica adequadamente por que um algoritmo específico tem sucesso com alta probabilidade sob um orçamento fixo de computação para as distribuições específicas e enviesadas de teoremas encontrados na prática (por exemplo, teoremas de bibliotecas, famílias de benchmarks).

O artigo aborda a questão: Qual é a probabilidade de que um provedor agêntico específico gere uma prova aceita pelo verificador dentro de um orçamento fixo em um fluxo especificado de instâncias de teoremas? Os autores argumentam que compreender essa "provabilidade estatística" é essencial para explicar por que componentes como recuperação, feedback do verificador e decomposição melhoram o desempenho sem contradizer a indecidibilidade clássica ou limites inferiores do pior caso.

Metodologia

1. Formalização como um MDP de Alcançabilidade

Os autores modelam a busca por prova formal como um Processo de Decisão de Markov (MDP) de horizonte finito de alcançabilidade com dinâmicas determinísticas:

• Estado ($X$): A obrigação de prova atual (por exemplo, uma lista de objetivos abertos no Lean) mais o feedback do verificador.
• Ação ($A$): Movimentos do provedor, como táticas, regras de inferência ou comandos de recuperação.
• Transição ($F$): Um mapa de atualização determinístico do verificador $F: X \times A \to X$. Ações inválidas mapeiam para estados de falha; ações válidas transitam para novos estados de prova.
• Objetivo ($G$): O conjunto de estados resolvidos (listas de objetivos vazias).

Esta formulação trata a semântica operacional do verificador como o kernel de transição. Os autores provam que, sob uma abstração de estado fiel, a probabilidade de sucesso ótima do MDP coincide exatamente com a provabilidade sintática ordinária dentro do mesmo orçamento, preservando a integridade lógica enquanto permite análise estatística.

2. Definição de Provabilidade Estatística

A métrica central é a Provabilidade Estatística ($SP^\pi_B(q_0)$), definida como a probabilidade de que uma política de provedor $\pi$ alcance uma prova verificada dentro de $B$ chamadas ao verificador, média sobre uma distribuição inicial de teoremas $q_0$ e a aleatoriedade interna do provedor. Isso é contrastado com a probabilidade de sucesso ótima $SP^*_B(q_0)$.

Os autores também rastreiam o comprimento médio de prova truncado ($Len^\pi_B(q_0)$), definido como o número esperado de chamadas ao verificador antes do sucesso ou do esgotamento do orçamento. Esta métrica serve como um controle crítico de interpretabilidade em seus limites.

3. Análise do Pipeline de Aprendizado

O artigo analisa um pipeline alinhado com a prática atual:

1. Regressão Offline de Valor-Ação: Aprendizado de funções de valor-ação por profundidade ($Q^*_t$) a partir de simulações (rollouts) apoiadas por verificador em uma distribuição de treinamento.
2. Prova Gananciosa em Tempo de Teste: Uso das pontuações aprendidas para selecionar a melhor ação de forma gananciosa no momento do teste.

A análise depende da Hipótese 3.1, que postula:

• Conjuntos de concentração compactos ($C_t$) onde o treinamento e o teste ocorrem.
• Continuidade de Lipschitz da função de valor ótima e da classe de hipóteses.
• Cobertura suficiente do espaço de estado-ação pela distribuição de exploração.
• Disponibilidade de múltiplos rótulos de simulação independentes por consulta para reduzir o ruído.

Contribuições e Resultados Principais

1. O Teorema Principal (Limite de Provabilidade Estatística)

O resultado central (Teorema 3.1) limita a lacuna entre a probabilidade de sucesso do provedor aprendido e a probabilidade de sucesso do provedor ótimo. O limite é uma soma ponderada pela ocupação de erros uniformes de valor-ação:

$$SP^*_B(q_0) - SP^{\hat{\pi}}_B(q_0) \leq 2 \sum_{s=1}^B P^{\hat{\pi}}_{q_0}(T_G \geq s) \cdot \epsilon_{B-s+1}$$

Onde:

• $P^{\hat{\pi}}_{q_0}(T_G \geq s)$ é a probabilidade de que o provedor aprendido ainda não tenha resolvido o problema no passo $s$ (a curva de massa não resolvida).
• $\epsilon_t$ é o limite de erro uniforme no estimador de valor-ação aprendido na profundidade $t$.

Interpretação do Termo de Erro ($\epsilon_t$):
O erro se decompõe em três componentes:

1. Erro de Aproximação: A incapacidade da classe de hipóteses de representar a verdadeira função de valor.
2. Erro de Cobertura/Geometria: Dependente da dimensão local efetiva ($d_t$) e da constante de cobertura ($c_t$) da distribuição de treinamento.
3. Ruído de Simulação: Variância do número finito de rótulos de Monte Carlo ($m_t$) usados para regressão.

2. O Papel do Comprimento Médio de Prova

Uma ideia-chave é que o multiplicador de complexidade principal no limite é o comprimento médio de prova truncado do provedor aprendido ($Len^{\hat{\pi}}_B(q_0)$).
$$SP^*_B(q_0) - SP^{\hat{\pi}}_B(q_0) \lesssim \bar{\epsilon}_B \cdot Len^{\hat{\pi}}_B(q_0)$$
Isso implica que mecanismos que encurtam provas (por exemplo, decomposição eficaz, introdução de lemas) reduzem diretamente a perda de ponta a ponta, mesmo que o erro de estimativa de valor local ($\bar{\epsilon}_B$) permaneça constante.

3. Condições de Margem e Taxas Rápidas

Sob uma condição de margem (onde a lacuna entre os valores das melhores e segundas melhores ações é suficientemente grande com alta probabilidade), o limite melhora para uma taxa rápida:
$$SP^*_B(q_0) - SP^{\hat{\pi}}_B(q_0) \lesssim Len^{\hat{\pi}}_B(q_0) \cdot \bar{\epsilon}_B^{\beta+1}$$
Isso sugere que melhorar as lacunas de ação (tornando movimentos corretos claramente superiores aos incorretos) acelera significativamente a convergência.

4. Leis de Escala

O artigo deriva heurísticas de complexidade de amostra. Ignorando fatores logarítmicos, o erro escala como $n^{-1/(d+2)}$, onde $n$ é o orçamento de rótulos do verificador e $d$ é a dimensão local efetiva. Isso esclarece que os ganhos de "escala em tempo de teste" podem surgir de:

• Reduzir o horizonte efetivo (provas mais curtas).
• Reduzir a dimensão geométrica efetiva (melhor recuperação/representação).
• Aumentar a margem da lacuna de ação.

Significado e Afirmações

O artigo afirma fornecer uma conta sensível a componentes de por que provedores de teoremas agênticos funcionam em cargas de trabalho enviesadas. Ele preenche a lacuna entre lógica clássica e aprendizado estatístico, mostrando que:

1. Feedback do Verificador: Melhora a provabilidade ao reduzir o erro de aproximação, melhorar a cobertura e aumentar as lacunas de ação.
2. Recuperação e Representação: Ajudam ao suavizar a função de valor, concentrar o espaço de estado em regiões de dimensão mais baixa e podar escolhas ruins para aumentar as margens.
3. Encurtamento de Provas: Mecanismos como decomposição reduzem o "peso de ocupação" (comprimento médio de prova), que é o multiplicador primário de erro no limite.

Os autores enfatizam que esta teoria não contradiz a dificuldade do pior caso. Em vez disso, explica por que sistemas agênticos têm sucesso nas distribuições específicas e estruturadas de teoremas encontradas na prática (teoremas de bibliotecas, benchmarks), onde as provas são curtas, as lacunas são grandes e a cobertura é boa. O quadro trata o verificador como um canal de informação e o provedor como um aprendiz estatístico extraindo informações úteis sob um orçamento limitado, oferecendo uma justificativa rigorosa para as escolhas de engenharia (recuperação, decomposição, loops de verificador) prevalentes em sistemas agênticos modernos.