Exponential Sample Complexity Separation between Flat and Hierarchical Agentic Theorem Provers

Título: Separação Exponencial na Complexidade de Amostragem entre Provedores de Teoremas Agênticos Planos e Hierárquicos

Autores: Sho Sonoda, Shunta Akiyama, Yuya Uezato
Afiliações: CyberAgent, RIKEN AIP
Data: 7 de maio de 2026

1. Declaração do Problema

Provedores de teoremas agênticos recentes frequentemente empregam estratégias de decomposição — como geração de lemas intermediários, esboços de prova ou decomposições de subobjetivos — antes de se engajar em buscas no nível de táticas. Embora a teoria da prova clássica sugira que lemas possam encurtar derivações, o custo de aprendizado estatístico de descobrir e provar esses passos intermediários permanece uma questão em aberto. Especificamente, se provar um lema é em si difícil, por que um provedor aprendido deveria despender esforço nele?

O artigo aborda o problema de aprendizado estatístico de saber se aprender uma estrutura de prova reutilizável (hierárquica) aumenta a probabilidade de encontrar uma prova verificada dentro de um orçamento de busca fixo, comparado a aprender a partir de traços de prova totalmente inlineados (planos). Os autores focam na distribuição de dados induzida por um provedor "professor", consistindo em estados iniciais de teoremas e traços de prova bem-sucedidos e verificados, em vez da complexidade de prova no pior caso sobre todas as fórmulas.

2. Metodologia

Os autores modelam a prova de teoremas como um Processo de Decisão de Markov (MDP) determinístico de horizonte finito, onde estados são estados de prova e ações são táticas, regras de inferência ou movimentos de decomposição de alto nível. Eles analisam o aprendizado por imitação offline a partir de traços bem-sucedidos de professores sob três configurações distintas:

• Configuração 1 (Plana): O professor gera traços de prova de baixo nível totalmente inlineados. O aluno imita esses traços sem previsão de grafos ou memorização. Subprovas repetidas aparecem como ocorrências distintas e copiadas nos dados de treinamento e teste.
• Configuração 2 (Hierárquica): O professor constrói um Grafo Acíclico Direcionado (DAG) de prova de alto nível, onde nós representam blocos de prova reutilizáveis. O aluno aprende um preditor de grafo e políticas para ações de grafo de alto nível (selecionar, expandir, reutilizar blocos) e resolução local de baixo nível. Os dados de treinamento consistem em traços inlineados, exigindo que o aluno infira a estrutura latente do DAG de prova.
• Configuração 3 (Comparação): Tanto um aluno plano quanto um aluno hierárquico são treinados na mesma fonte de dados gerada pelo professor hierárquico (traços inlineados). O aluno plano descarta a estrutura de grafo latente, enquanto o aluno hierárquico a infere. Esta configuração isola o efeito da representação na complexidade de amostragem.

A análise depende de três quantidades-chave:

1. $L$ (Comprimento Médio): O número médio de decisões em uma prova bem-sucedida.
2. $\eta$ (Perda Intrínseca de Busca): A massa de probabilidade perdida porque a próxima ação do professor não está na lista de $k$ melhores candidatos do aluno (previsibilidade local).
3. $e$ (Erro de Imitação): A divergência Kullback-Leibler (KL) entre a política do aluno e a política do professor.

Os autores assumem uma condição de margem do tipo Tsybakov para converter erro de imitação em probabilidade de omissão top-$k$ e assumem completude de busca se as ações do professor estiverem contidas na lista de top-$k$ do aluno.

3. Principais Contribuições

• Formalização: O artigo formula a prova de teoremas guiada por verificador como um MDP de horizonte finito e define "provabilidade estatística" como a probabilidade média de encontrar uma prova verificada dentro de um orçamento sobre uma distribuição de estados iniciais.
• Garantias de Sucesso: Os autores derivam limites de sucesso de amostra finita tanto para alunos planos (treinados em traços inlineados) quanto para alunos hierárquicos (treinados para prever DAGs reutilizáveis). Os limites separam explicitamente o número de decisões, a perda intrínseca top-$k$ e o erro de classificação aprendido.
• Separação Exponencial: O resultado teórico primário é uma separação exponencial na complexidade de amostragem suficiente. Quando um DAG de prova reutilizável é achatado em uma árvore, subprovas idênticas são duplicadas exponencialmente muitas vezes. O artigo prova que o certificado de amostra suficiente para o aprendiz hierárquico pode ser exponencialmente menor que o do aprendiz plano, mesmo quando treinado na mesma fonte de dados.
• Aprendizado de Grafo Latente: O artigo fornece taxas de aprendizado para um aluno hierárquico que deve inferir DAGs de prova latentes a partir de traços inlineados usando uma abordagem ponderada por posterior estilo EM, contabilizando erros de previsão de grafo e incompatibilidade de posterior.

4. Resultados

O resultado central é apresentado no Teorema 6, que compara as contagens de amostras suficientes certificadas ($\bar{N}$) requeridas para os alunos plano e hierárquico alcançarem um nível de falha alvo $\delta$.

• Limite Plano: $\bar{N}_{flat}(\delta) \propto (L_{flat}/\delta)^{1/(p\gamma)}$
• Limite Hierárquico: $\bar{N}_{hier}(\delta) \propto \max(L_{hi}, L_{lo}/\delta)^{1/(p\gamma)}$

Onde $L_{flat}$ é o comprimento do traço desdobrado e $L_{hier} = L_{hi} + L_{lo}$ é o comprimento da representação hierárquica.

O artigo demonstra que, para uma família de teoremas indexada por um parâmetro de tamanho/profundidade $D$, se o processo de achatamento causar o crescimento exponencial do comprimento da prova ($L_{flat}/L_{hier} = \exp(\Omega(D))$), então a razão de amostras necessárias também cresce exponencialmente:
$$\bar{N}_{flat}(\delta) / \bar{N}_{hier}(\delta) \geq \exp(\Omega(D))$$

Essa separação surge porque o aprendiz plano deve aprender o mesmo argumento local difícil independentemente para cada ocorrência, enquanto o aprendiz hierárquico aprende o bloco compartilhado uma vez e o reutiliza. O artigo usa um exemplo de eliminação de corte (Apêndice G) para ilustrar como remover lemas intermediários (achatamento) pode causar uma explosão exponencial no tamanho da prova, inflando assim a complexidade de amostragem para aprendizes planos.

5. Significado e Alegações

O artigo alega fornecer um mecanismo estatístico concreto explicando por que a prova hierárquica ajuda, distinto de argumentos de complexidade de prova no pior caso. O significado reside em identificar que o benefício da decomposição não é meramente sobre encurtar a derivação lógica, mas sobre reduzir o ônus estatístico sobre o aprendiz.

• Consciência da Distribuição de Dados: O resultado destaca que a eficiência do aprendizado depende da estrutura da distribuição de dados. Se provas bem-sucedidas reutilizam argumentos intermediários, uma representação hierárquica captura esse compartilhamento, enquanto uma representação plana o destrói, levando a tarefas de aprendizado redundantes.
• Limitações: Os autores são modestos em suas alegações. Eles afirmam que isso não é um limite inferior no pior caso e não exclui aprendizes planos que possam alcançar uma canonicidade perfeita (reconhecimento perfeito de subproblemas idênticos sem hierarquia explícita). A separação vale especificamente quando o achatamento destrói a estrutura de prova reutilizável e a distribuição de dados contém provas onde tal compartilhamento é prevalente.
• Implicação Prática: As descobertas sugerem que, para prova de teoremas baseada em verificador, aprender a prever estruturas de prova reutilizáveis (lemas, subobjetivos) pode reduzir exponencialmente a complexidade de amostragem necessária para alcançar uma determinada probabilidade de sucesso, desde que o preditor de grafo possa cobrir o certificado do professor com alta probabilidade.

O artigo conclui que o "desvio caro" de provar lemas é estatisticamente justificado quando esses lemas são reutilizáveis, pois o custo de aprendê-los uma vez é muito menor que o custo de redescobri-los repetidamente em um framework plano.