Melhorando a Prova de Teoremas com Algoritmos Avançados

Nos últimos anos, teve bastante interesse em usar computadores pra ajudar a provar teoremas matemáticos. Uma abordagem chamada Monte Carlo Tree Search (MCTS) permite que os computadores tomem decisões explorando várias opções, bem parecido com o que os jogadores fazem em jogos. O MCTS foi usado em programas populares como o AlphaGo, que ficou famoso por vencer campeões humanos no jogo Go.

Outro exemplo de ferramenta que usa MCTS é o Holophrasm, um programa criado pra automatizar a prova de teoremas. O Holophrasm combina MCTS com redes neurais pra melhorar seus processos de decisão e avaliação. Neste papo, a gente vai ver como melhorar o desempenho do Holophrasm usando métodos de busca diferentes.

#O que é Metamath?

Antes de entrar em detalhes, é importante entender o Metamath, que é o sistema do qual o Holophrasm depende. O Metamath é uma linguagem formal para matemática. Ele opera com um princípio chamado substituição lógica. Quando você tenta provar um teorema, muitas vezes precisa aplicar algumas proposições, que exigem ajustar suas variáveis pra combinar com o contexto atual da prova.

O Holophrasm representa provas matemáticas como árvores. No topo da árvore tá a conclusão que a gente quer provar, e os ramos mostram os passos que foram tomados. Esses ramos são divididos em dois tipos de nós: nós OR e nós AND. Nós OR representam diferentes caminhos pra prova, enquanto os nós AND mostram os passos ou suposições necessários pra provar o nó OR.

Uma prova é construída começando pela conclusão e trabalhando pra trás, avaliando se cada passo pode ser alcançado. O Holophrasm tem um conjunto de teoremas pra testar, e pra nossa análise, vamos focar só nos primeiros 200 teoremas dessa lista.

#Como o Holophrasm Funciona

O Holophrasm busca através da árvore de provas visitando nós pra ver se eles podem ser provados. O processo é parecido com a estratégia que os jogadores usam em jogos. Ao olhar pra um nó OR, o Holophrasm tenta descobrir a chance de prová-lo com base nas previsões das redes neurais.

Quando um nó OR é visitado, o próximo passo é explorar o nó AND correspondente, que é uma proposição que precisa ser provada. Cada vez que um nó AND é criado, seus nós filhos também são explorados. Se uma proposição é confirmada por todas as hipóteses necessárias, o nó AND é considerado provado. Por outro lado, se alguma hipótese falha, o nó AND é refutado.

O sistema dá valores iniciais com base em redes neurais. A rede de pagamento prevê as chances de prova, enquanto a rede de previsão direciona quais proposições considerar. Se todos os nós filhos de um nó OR são refutados ou se o nó OR atingiu seu limite de visitas, ele é marcado como refutado.

#Resultados dos Testes do Holophrasm

Nos nossos testes, vimos como o Holophrasm se saiu nos primeiros 200 teoremas. Sem entrar em muitos detalhes nos resultados, só vamos notar que o método do Holophrasm serve como uma base pra comparar outros algoritmos.

#Usando Métodos de Busca Tradicionais

Pra melhorar o Holophrasm, precisávamos considerar métodos de busca tradicionais. Um método bem conhecido é o Minimax, usado na estratégia de jogos. Ele alterna entre minimizar as possíveis perdas e maximizar os potenciais ganhos.

Ao testar o Minimax no contexto do Holophrasm, percebemos que ele tinha limitações. Principalmente, um nó OR poderia ter um número infinito de filhos. Pra lidar com isso, restringimos o número de filhos a uma contagem fixa baseada em scores de probabilidade. Apesar dessas mudanças, os resultados mostraram que uma abordagem de busca mais ampla resultou em resultados melhores.

#Algoritmos Avançados de Busca em Árvore

Além do Minimax, estudamos outros métodos avançados, como PUCT, Propagação de Produto e Busca por Número de Prova (PNS). Esses métodos visam refinar a busca, permitindo que um computador encontre respostas sem precisar explorar todos os caminhos possíveis na árvore de prova.

PUCT governa como a busca seleciona o próximo nó AND a ser visitado. Ele se baseia em ideias da teoria dos jogos, gerenciando a incerteza ajustando os parâmetros de busca. Quando o PUCT foi comparado ao Holophrasm, notamos que ele costumava se sair melhor sob condições menos restritas.

Em seguida, exploramos a Propagação de Produto, que muda como os valores são atribuídos aos nós durante a busca. Nesse método, os nós AND são avaliados com base na força coletiva de seus filhos enquanto os nós OR refletem seu melhor filho. Nossos testes mostraram que a Propagação de Produto teve melhor eficiência do que o PUCT quando o número de passagens foi limitado.

O PNS tem uma abordagem diferente, enfatizando as contagens de folhas que ainda precisam ser provadas. Achamos que ele foi menos eficaz em comparação com a Propagação de Produto, mas vale a pena explorar mais.

#Busca de Prova HyperTree

Também testamos um algoritmo conhecido como Busca de Prova HyperTree. Esse método adota uma visão mais ampla, focando em subárvores em vez de ramos individuais. Ele expande todas as folhas possíveis de um nó selecionado e depois atualiza seus valores. Embora esse método tenha enfrentado dificuldades no início, mostrou melhorias com o tempo, sugerindo vantagens potenciais a longo prazo, apesar de seu começo mais lento.

#Novas Direções para Prova de Teoremas

Com uma boa compreensão dos métodos existentes, tentamos criar novos algoritmos que aproveitassem os pontos fortes das abordagens anteriores. Uma ideia foi combinar a Propagação de Produto com o PUCT. Ao aproveitar as melhores características de ambos, esperamos obter resultados melhores.

Nos nossos testes iniciais, percebemos que essa combinação realmente trouxe algumas melhorias. O que foi especialmente empolgante foi um método que permitiu uma abordagem modificada no PUCT, levando a gente a romper barreiras previamente estabelecidas na prova de teoremas.

#Conclusões e Trabalhos Futuros

No geral, analisamos como diferentes algoritmos poderiam ser aplicados pra melhorar a prova de teoremas no Metamath. O algoritmo Minimax destacou a necessidade de uma ampliação progressiva nas buscas. Enquanto isso, algoritmos como PUCT, PNS e Propagação de Produto contribuíram pra uma melhor compreensão de quais métodos funcionam melhor nesse contexto.

Nossos experimentos com a combinação de técnicas são promissores, embora ainda haja espaço pra melhorias. Pra frente, planejamos aplicar nossos novos algoritmos a um conjunto de dados maior pra ver como eles se saem em diferentes condições. Essa exploração vai permitir que a gente refine nossas técnicas e possivelmente descubra formas mais eficazes de automatizar a prova de teoremas.