Aprendizado por imitação faz provador de teoremas resolver 46% mais problemas

Provar teoremas automaticamente é um dos sonhos mais antigos da inteligência artificial. O gargalo sempre foi a busca: em um espaço enorme de passos possíveis, como decidir qual movimento tentar em seguida? Um preprint do arXiv mostra que um provador guiado por aprendizado de imitação resolveu até 46% mais problemas que a referência leanCoP, usando uma ordem de magnitude menos passos.

Uma política que aprende a escolher o próximo passo

O estudo usa aprendizado por imitação para treinar uma política que, em cada etapa, escolhe entre as edições válidas de uma prova em um sistema formal chamado “tableau de conexão”. Um grafo neural (GNN) pontua cada movimento possível, já que a estrutura de uma prova é naturalmente um grafo.

Foram comparadas três políticas aprendidas — πmarkov, πdfs e πid — que expõem interfaces de ação e memória progressivamente mais restritivas, criando diferentes equilíbrios entre liberdade de busca, retenção das soluções da referência e número de passos.

Cobertura com compensações

No conjunto MPTP, as políticas se separaram em perfis distintos. A πdfs resolveu 363 problemas (94 que a referência não achava), mas a πmarkov fez as corridas mais curtas — média de apenas 11,9 passos — embora tenha perdido 27 soluções da referência. A πid resolveu 340 problemas perdendo apenas uma solução, porém com média de 158,7 passos.

Estendendo o treinamento até a convergência, a πdfs chegou a 396 problemas resolvidos (118 novos), com média de 26,6 passos. O dado mais relevante: as três políticas já superavam a referência desde a primeira iteração de agregação, sugerindo que o aprendizado captura padrões de prova transferíveis entre problemas — inclusive de forma zero-shot em problemas nunca vistos.

O que fica em aberto

O artigo é transparente sobre limites. O sinal de imitação rotula apenas os caminhos de prova bem-sucedidos; ações de desfazer (undo) e estados que não aparecem nesses caminhos ficam sem rótulo — deixando em aberto se treinar com tentativas falhas melhoraria as decisões de retrocesso. A figura de 46% não vem acompanhada de intervalo de incerteza nem de variabilidade entre repetições. O código está disponível no GitHub.

Para o campo do raciocínio matemático e da verificação formal, o resultado reforça uma tendência: aprendizado de máquina como “piloto” da busca, deixando para o provador formal apenas a verificação — o que mantém a correção garantida enquanto acelera a descoberta.