As ferramentas de IA estão moldando os provadores de teoremas da próxima geração e, com eles, a relação entre matemática e máquina.
Na década de 1970, o falecido matemático Paul Cohen, a única pessoa a ganhar uma medalha Fields por trabalho em lógica matemática, supostamente fez uma previsão abrangente que continua a excitar e irritar os matemáticos – que “em algum momento futuro não especificado, os matemáticos seriam substituídos por computadores.” Cohen, lendário por seus métodos ousados na teoria dos conjuntos, previu que toda a matemática poderia ser automatizada, incluindo a redação de provas.
Uma prova é um argumento lógico passo a passo que verifica a verdade de uma conjectura ou proposição matemática. (Uma vez provado, uma conjectura se torna um teorema.) Ele estabelece a validade de uma afirmação e explica por que ela é verdadeira. Uma prova é estranha, no entanto. É abstrato e não está vinculado à experiência material. “Eles são esse contato louco entre um mundo imaginário, não físico e criaturas biologicamente evoluídas”, disse o cientista cognitivo Simon DeDeo, da Carnegie Mellon University, que estuda a certeza matemática analisando a estrutura das provas. “Não evoluímos para fazer isso.”
Os computadores são úteis para grandes cálculos, mas as provas exigem algo diferente. As conjecturas surgem do raciocínio indutivo – uma espécie de intuição sobre um problema interessante – e as provas geralmente seguem uma lógica dedutiva passo a passo. Eles geralmente exigem um pensamento criativo complicado, bem como o trabalho mais trabalhoso de preencher as lacunas, e as máquinas não conseguem essa combinação.
Os provadores de teoremas computadorizados podem ser divididos em duas categorias. Provadores de teoremas automatizados, ou ATPs, normalmente usam métodos de força bruta para processar grandes cálculos. Provadores de teoremas interativos, ou ITPs, atuam como assistentes de prova que podem verificar a precisão de um argumento e verificar se há erros nas provas existentes. Mas essas duas estratégias, mesmo quando combinadas (como é o caso com provadores de teoremas mais novos), não somam ao raciocínio automatizado.
Além disso, as ferramentas não foram recebidas de braços abertos, e a maioria dos matemáticos não as usa ou aceita. “Eles são muito controversos para os matemáticos” disse DeDeo. “A maioria deles não gosta da ideia.”
Um desafio aberto formidável no campo pergunta o quanto a produção de provas pode realmente ser automatizada: um sistema pode gerar uma conjectura interessante e prová-la de uma maneira que as pessoas entendam? Uma série de avanços recentes de laboratórios de todo o mundo sugere maneiras pelas quais as ferramentas de inteligência artificial podem responder a essa pergunta. Josef Urban, do Instituto Tcheco de Informática, Robótica e Cibernética em Praga, está explorando uma variedade de abordagens que usam o aprendizado de máquina para aumentar a eficiência e o desempenho dos provadores existentes. Em julho, seu grupo relatou um conjunto de conjecturas e provas originais geradas e verificadas por máquinas. E em junho, um grupo do Google Research liderado por Christian Szegedy postou resultados recentes de esforços para aproveitar os pontos fortes do processamento de linguagem natural para fazer as provas de computador parecerem mais humanas em estrutura e explicação.
Alguns matemáticos veem os provadores de teoremas como uma ferramenta potencialmente revolucionária para o treinamento de alunos de graduação em redação de provas. Outros dizem que fazer com que os computadores escrevam provas é desnecessário para o avanço da matemática e provavelmente impossível. Mas um sistema que pode prever uma conjectura útil e provar um novo teorema alcançará algo novo – alguma versão de máquina de compreensão, disse Szegedy. E isso sugere a possibilidade de automatizar a própria razão.
Máquinas Úteis
Matemáticos, lógicos e filósofos há muito discutem sobre que parte da criação de provas é fundamentalmente humana, e os debates sobre a matemática mecanizada continuam até hoje, especialmente nos vales profundos que conectam a ciência da computação à matemática pura.
Para cientistas da computação, os provadores de teoremas não são controversos. Eles oferecem uma maneira rigorosa de verificar se um programa funciona, e os argumentos sobre intuição e criatividade são menos importantes do que encontrar uma maneira eficiente de resolver um problema. No Massachusetts Institute of Technology, por exemplo, o cientista da computação Adam Chlipala projetou ferramentas de prova de teoremas que geram algoritmos criptográficos – tradicionalmente escritos por humanos – para proteger as transações na Internet. O código de seu grupo já é usado para a maioria das comunicações no navegador Chrome do Google.
“Você pode pegar qualquer tipo de argumento matemático e codificá-lo com uma ferramenta e conectar seus argumentos para criar provas de segurança”, disse Chlipala.
Na matemática, os provadores de teoremas ajudaram a produzir provas complicadas e pesadas em cálculos que, de outra forma, ocupariam centenas de anos da vida dos matemáticos. A conjectura do Kepler, que descreve a melhor maneira de empilhar esferas (ou, historicamente, laranjas ou balas de canhão), oferece um exemplo revelador. Em 1998, Thomas Hales, junto com seu aluno Sam Ferguson, completou uma prova usando uma variedade de técnicas matemáticas computadorizadas. O resultado foi tão complicado – os resultados ocuparam 3 gigabytes – que 12 matemáticos o analisaram por anos antes de anunciar que estavam 99% certos de que estava correto.
A conjectura de Kepler não é a única questão famosa a ser resolvida por máquinas. O teorema das quatro cores, que diz que você só precisa de quatro tons para colorir qualquer mapa bidimensional de modo que duas regiões adjacentes não compartilhem uma cor, foi estabelecido em 1977 por matemáticos usando um programa de computador que revolveu mapas de cinco cores para mostrá-los todos poderiam ser reduzidos a quatro. E em 2016, um trio de matemáticos usou um programa de computador para provar um desafio aberto de longa data chamado de problema dos triplos Booleanos Pitagóricos, mas a versão inicial da prova tinha 200 terabytes de tamanho. Com uma conexão de internet de alta velocidade, uma pessoa poderia baixá-lo em pouco mais de três semanas.
Sentimentos Complicados
Esses exemplos costumam ser alardeados como sucessos, mas também contribuíram para o debate. O código de computador que prova o teorema das quatro cores, que foi estabelecido há mais de 40 anos, era impossível para os humanos verificarem por conta própria. “Os matemáticos têm discutido desde então se é ou não uma prova”, disse o matemático Michael Harris, da Universidade de Columbia.
Outra queixa é que, se quiserem usar provadores de teoremas, os matemáticos devem primeiro aprender a codificar e então descobrir como expressar seu problema em uma linguagem amigável – atividades que prejudicam o ato de fazer matemática. “No momento em que reformulei minha pergunta em uma forma que pudesse se encaixar nessa tecnologia, eu teria resolvido o problema sozinho”, disse Harris.
Muitos simplesmente não veem a necessidade de solucionadores de teoremas em seu trabalho. “Eles têm um sistema, e é lápis e papel, e funciona”, disse Kevin Buzzard, um matemático do Imperial College London que três anos atrás transformou seu trabalho da matemática pura em provadores de teoremas e provas formais. “Os computadores fizeram cálculos incríveis para nós, mas nunca resolveram um problema difícil por conta própria”, disse ele. “Até que o façam, os matemáticos não vão acreditar nisso.”
Mas Buzzard e outros pensam que talvez devessem. Por um lado, “as provas de computador podem não ser tão estranhas quanto pensamos”, disse DeDeo. Recentemente, junto com Scott Viteri, um cientista da computação agora na Universidade de Stanford, ele fez a engenharia reversa de um punhado de provas canônicas famosas (incluindo uma de Euclid’s Elements) e dezenas de provas geradas por máquina, escritas usando um provador de teorema chamado Coq, para olhar para semelhanças. Eles descobriram que a estrutura em rede das provas de máquina era notavelmente semelhante à estrutura das provas feitas por pessoas. Essa característica compartilhada, disse ele, pode ajudar os pesquisadores a encontrar uma maneira de fazer os assistentes de prova, em certo sentido, se explicarem.
“As provas de máquina podem não ser tão misteriosas quanto parecem”, disse DeDeo.
Outros dizem que os provadores de teoremas podem ser ferramentas de ensino úteis, tanto em ciência da computação quanto em matemática. Na Universidade Johns Hopkins, a matemática Emily Riehl desenvolveu cursos nos quais os alunos escrevem provas usando um provador de teoremas. “Isso o força a ser muito organizado e pensar com clareza”, disse ela. “Os alunos que escrevem provas pela primeira vez podem ter problemas para saber o que precisam e entender a estrutura lógica.”
Riehl também diz que tem usado cada vez mais provadores de teoremas em seu próprio trabalho. “Não é necessariamente algo que você tem que usar o tempo todo e nunca substituirá rabiscar em um pedaço de papel”, disse ela, “mas usar um assistente de prova mudou minha maneira de pensar sobre escrever provas”.
Os provadores de teoremas também oferecem uma maneira de manter o campo honesto. Em 1999, o matemático russo-americano Vladimir Voevodsky descobriu um erro em uma de suas provas. Daí até sua morte em 2017, ele foi um defensor vocal do uso de computadores para verificar as provas. Hales disse que ele e Ferguson encontraram centenas de erros em sua prova original quando a verificaram com computadores. Mesmo a primeira proposição em Elementos de Euclides não é perfeita. Se uma máquina pode ajudar os matemáticos a evitar esses erros, por que não tirar proveito dela? (A objeção prática, justificada ou não, é aquela sugerida por Harris: se os matemáticos têm que gastar seu tempo formalizando matemática para serem entendidos por um computador, é o tempo que eles não gastam fazendo matemática nova.)
Mas Timothy Gowers, um matemático e medalhista de Fields na Universidade de Cambridge, quer ir ainda mais longe: ele prevê um futuro em que os provadores de teoremas substituam os árbitros humanos nas principais revistas. “Eu posso ver que está se tornando uma prática padrão se você quer que seu artigo seja aceito, você tem que passar por um verificador automático”, disse ele.
Falando para computadores
Mas antes que os computadores possam verificar universalmente ou mesmo inventar provas, os pesquisadores primeiro precisam superar um obstáculo significativo: a barreira de comunicação entre a linguagem dos humanos e a dos computadores.
Os provadores de teoremas de hoje não foram projetados para serem amigáveis ao matemático. ATPs, o primeiro tipo, geralmente são usados para verificar se uma declaração está correta, geralmente testando casos possíveis. Peça a um ATP para verificar se uma pessoa pode dirigir de Miami a Seattle, por exemplo, e pode pesquisar todas as cidades conectadas por estradas que saem de Miami e, eventualmente, encontrar uma cidade com uma estrada que leve a Seattle.
Com um ATP, um programador pode codificar em todas as regras, ou axiomas, e então perguntar se uma determinada conjectura segue essas regras. O computador então faz todo o trabalho. “Você apenas digita a conjectura que deseja provar e espera obter uma resposta”, disse Daniel Huang, um cientista da computação que recentemente deixou a Universidade da Califórnia, em Berkeley, para trabalhar em uma startup.
Mas aqui está o problema: o que um ATP não faz é explicar seu trabalho. Todo esse cálculo acontece dentro da máquina e, aos olhos humanos, pareceria uma longa sequência de 0s e 1s. Huang disse que é impossível escanear a prova e seguir o raciocínio, porque parece uma pilha de dados aleatórios. “Nenhum ser humano jamais olhará para essa prova e será capaz de dizer: ‘Entendi'”, disse ele.
ITPs, a segunda categoria, têm vastos conjuntos de dados contendo até dezenas de milhares de teoremas e provas, que podem digitalizar para verificar se uma prova é precisa. Ao contrário dos ATPs, que operam em uma espécie de caixa preta e apenas fornecem uma resposta, os ITPs exigem interação humana e até mesmo orientação ao longo do caminho, portanto, não são tão inacessíveis. “Um humano poderia sentar e entender quais são as técnicas de nível de prova”, disse Huang. (Esses são os tipos de provas de máquina que DeDeo e Viteri estudaram.)
ITPs têm se tornado cada vez mais populares nos últimos anos. Em 2017, o trio por trás do problema dos triplos booleanos pitagóricos usou Coq, um ITP, para criar e verificar uma versão formal de sua prova; em 2005, Georges Gonthier, da Microsoft Research Cambridge, usou Coq para formalizar o teorema das quatro cores. Hales também usou ITPs chamados HOL Light e Isabelle na prova formal da conjectura de Kepler. (“HOL” significa “lógica de ordem superior”.)
Os esforços na vanguarda do campo hoje visam combinar aprendizado com raciocínio. Eles geralmente combinam ATPs com ITPs e também integram ferramentas de aprendizado de máquina para melhorar a eficiência de ambos. Eles imaginam programas ATP / ITP que podem usar raciocínio dedutivo – e até mesmo comunicar ideias matemáticas – da mesma maneira que as pessoas fazem, ou pelo menos de maneiras semelhantes.
Os limites da razão
Josef Urban pensa que o casamento do raciocínio dedutivo e indutivo necessário para as provas pode ser alcançado por meio desse tipo de abordagem combinada. Seu grupo construiu provadores de teoremas guiados por ferramentas de aprendizado de máquina, que permitem que os computadores aprendam por conta própria por meio da experiência. Nos últimos anos, eles exploraram o uso de redes neurais – camadas de cálculos que ajudam as máquinas a processar informações por meio de uma aproximação aproximada da atividade neuronal de nosso cérebro. Em julho, seu grupo relatou novas conjecturas geradas por uma rede neural treinada em dados de prova de teoremas.
Urban foi parcialmente inspirado por Andrej Karpathy, que há alguns anos treinou uma rede neural para gerar disparates de aparência matemática que pareciam legítimos para não especialistas. Urban não queria tolices, entretanto – ele e seu grupo, em vez disso, projetaram sua própria ferramenta para encontrar novas provas após treinar em milhões de teoremas. Em seguida, eles usaram a rede para gerar novas conjecturas e verificar a validade dessas conjecturas usando um ATP chamado E.
A rede propôs mais de 50.000 novas fórmulas, embora dezenas de milhares fossem duplicatas. “Parece que ainda não somos capazes de provar as conjecturas mais interessantes”, disse Urban.
“[Máquinas] aprenderão como fazer suas próprias instruções.”
Timothy Gowers, University of Cambridge
Szegedy, do Google Research, vê o desafio de automatizar o raciocínio em provas de computador como um subconjunto de um campo muito maior: o processamento de linguagem natural, que envolve o reconhecimento de padrões no uso de palavras e frases. (O reconhecimento de padrões também é a ideia motriz por trás da visão computacional, o objeto do projeto anterior de Szegedy no Google.) Como outros grupos, sua equipe quer provadores de teoremas que possam encontrar e explicar provas úteis.
Inspirado pelo rápido desenvolvimento de ferramentas de IA como AlphaZero – o programa DeepMind que pode derrotar humanos no xadrez, Go e shogi – o grupo de Szegedy quer capitalizar os avanços recentes no reconhecimento de linguagem para escrever provas. Os modelos de linguagem, disse ele, podem demonstrar um raciocínio matemático surpreendentemente sólido.
Seu grupo no Google Research descreveu recentemente uma maneira de usar modelos de linguagem – que geralmente usam redes neurais – para gerar novas provas. Depois de treinar o modelo para reconhecer um tipo de estrutura semelhante a uma árvore em teoremas que são conhecidos como verdadeiros, eles executaram uma espécie de experimento de forma livre, simplesmente pedindo à rede para gerar e provar um teorema sem qualquer orientação adicional. Dos milhares de conjecturas geradas, cerca de 13% eram prováveis e novas (o que significa que não duplicavam outros teoremas no banco de dados). O experimento, disse ele, sugere que a rede neural pode ensinar a si mesma uma espécie de compreensão de como é uma prova.
“As redes neurais são capazes de desenvolver um estilo artificial de intuição”, disse Szegedy.
Claro, ainda não está claro se esses esforços cumprirão a profecia de Cohen de mais de 40 anos atrás. Gowers disse que acha que os computadores serão capazes de superar os matemáticos em 2099. No início, ele prevê, os matemáticos irão desfrutar de uma espécie de era de ouro, “quando os matemáticos fazem todas as partes divertidas e os computadores fazem todas as partes chatas. Mas acho que vai durar muito pouco tempo.”
Afinal, se as máquinas continuarem a melhorar e tiverem acesso a grandes quantidades de dados, elas também deverão se tornar muito boas em fazer as partes divertidas. “Eles aprenderão como fazer suas próprias instruções”, disse Gowers.
Harris discorda. Ele não acha que os provadores de computador são necessários, ou que eles inevitavelmente “tornarão os matemáticos humanos obsoletos.” Se os cientistas da computação algum dia forem capazes de programar um tipo de intuição sintética, diz ele, ainda não rivalizará com a dos humanos. “Mesmo que os computadores entendam, eles não entendem de uma maneira humana.”
Publicado em 30/08/2020 15h24
Artigo original:
Achou importante? Compartilhe!
Assine nossa newsletter e fique informado sobre Astrofísica, Biofísica, Geofísica e outras áreas. Preencha seu e-mail no espaço abaixo e clique em “OK”: