Terence Tao gostou! O ChatGPT prova automaticamente um grande avanço e a IA dominará o mundo da matemática em 10 anos

**Fonte:**Xinzhiyuan

**Guia:**Embora muitas pessoas não queiram admitir, é muito provável que a IA ultrapasse os matemáticos humanos dentro de dez anos.

Há alguns dias, um artigo de pesquisadores do Caltech e do MIT usando o ChatGPT para provar teoremas matemáticos explodiu e atraiu grande atenção no meio matemático.

Jim Fan, o cientista-chefe da Nvidia, encaminhou-o com entusiasmo, dizendo que o copiloto de matemática da IA chegou e a próxima pessoa que descobrir novos teoremas será um matemático de IA totalmente automático!

O New York Times também publicou um artigo recentemente, dizendo que os matemáticos estão prontos e a IA alcançará ou até superará os melhores matemáticos humanos dentro de dez anos.

E o próprio Tao Zhexuan republicou este artigo.

Siobhan Roberts participou do workshop do IPAM deste ano realizado pela Machine Assisted Proofs e, em seguida, escreveu este artigo sobre IA e matemática com base em sua própria experiência e entrevistas

**A IA também está chegando para subverter o mundo da matemática! **

Hoje, os matemáticos precisam enfrentar a mais recente força revolucionária - a IA.

Em 2019, o cientista da computação Christian Szegedy, ex-funcionário do Google que agora trabalha em uma startup da Bay Area, previu que os sistemas de computador corresponderiam ou excederiam as habilidades de resolução de problemas dos melhores matemáticos humanos dentro de uma década. No ano passado, ele revisou a data prevista para 2026.

O lógico da Carnegie Mellon University Jeremy Avigad (em azul) com alunos da Formal Mathematics Summer School

Akshay Venkatesh, vencedor da Medalha Fields de 2018 e matemático do Instituto de Estudos Avançados de Princeton, atualmente não está interessado em usar a IA, mas está muito interessado em discutir tópicos relacionados à IA.

Em uma entrevista no ano passado, Venkatesh disse: "Quero que meus alunos percebam que esse campo vai mudar muito".

E recentemente sua atitude é: "Não tenho objeções ao uso deliberado, mesmo deliberado, da IA para auxiliar a compreensão humana. Mas acredito firmemente que precisamos estar atentos e cautelosos sobre a maneira como a usamos."

Em fevereiro deste ano, o Instituto de Matemática Teórica e Aplicada da UCLA realizou um workshop sobre "Demonstração assistida por máquina".

O principal organizador do seminário é Tao Terence, matemático que ganhou a Medalha Fields em 2006 e trabalha na UCLA.

Ele apontou que o uso de IA para auxiliar provas matemáticas é realmente um fenômeno digno de atenção.

Apenas nos últimos anos os matemáticos começaram a se preocupar com a ameaça potencial da IA, seja a destruição da estética matemática pela IA ou a ameaça aos próprios matemáticos.

E membros destacados da comunidade estão colocando essas questões na mesa e começando a explorar como "quebrar o tabu".

Os organizadores da escola de verão, da esquerda para a direita: Avigad, Patrick Massot e Heather Macbeth

Dos primitivos da geometria euclidiana ao código de computador

Por milênios, os matemáticos se adaptaram aos últimos avanços da lógica e do raciocínio. Mas eles estão prontos para a IA?

Retrato do matemático grego do século XVII Euclides no Getty Museum em Los Angeles: ele está vestido com trapos e segura seu tratado de geometria, Elements

Por mais de 2.000 anos, o texto de Euclides tem sido o paradigma do argumento e raciocínio matemático.

O lógico da Universidade Carnegie Mellon, Jeremy Avigad, diz que Euclides começou com uma "definição" quase poética sobre a qual construiu a matemática de seu tempo - usando conceitos básicos, definições e teoremas anteriores, cada um sucessivo. modo a provar as coisas.

Alguns reclamaram que alguns dos passos "óbvios" de Euclides não eram tão óbvios, mas o Dr. Avigad disse que o sistema funcionou.

Mas depois do século 20, os matemáticos não estavam mais dispostos a basear a matemática nessa base geométrica intuitiva.

Em vez disso, desenvolveram sistemas formais com representações simbólicas precisas e regras mecânicas.

Eventualmente, sob tal sistema, a matemática poderia ser traduzida em código de computador.

Em 1976, o teorema das quatro cores tornou-se o primeiro grande teorema a ser provado com a ajuda de cálculos de força bruta.

O teorema das quatro cores: quatro cores são suficientes para preencher um mapa de modo que não haja duas regiões adjacentes com a mesma cor

Reclamando AI: Desculpe, não consigo entender seu teorema

Existe um gadget de matemática chamado Proof Assistant ou Interactive Theorem Prover.

Passo a passo, os matemáticos convertem provas em código e, em seguida, usam programas de software para verificar se o raciocínio está correto.

O processo de verificação é acumulado em uma biblioteca de referência de especificação dinâmica, que está disponível para outros.

O Dr. Avigad, diretor do Hoskinson Center for Formal Mathematics, disse que esse tipo de formalização lançou as bases para a matemática de hoje, assim como Euclides tentou transcodificar a matemática daquela época, fornecendo assim uma base.

Recentemente, o Lean, um sistema assistente de prova de código aberto, mais uma vez atraiu muita atenção.

O Lean foi desenvolvido pelo atual cientista da computação da Amazon, Leonardo de Moura, enquanto trabalhava na Microsoft.

O Lean usa o raciocínio automatizado, alimentado pela velha escola AI GOFAI, uma IA simbólica inspirada pela lógica.

Até agora, Lean verificou um teorema interessante que transforma uma esfera de dentro para fora, bem como um teorema chave que unifica esquemas em toda a esfera matemática.

No entanto, o assistente de prova também tem deficiências: muitas vezes reclama que não entende as definições, axiomas ou etapas de raciocínio inseridas pelo matemático, por isso também é chamado de "reclamador de prova".

Essas reclamações tornariam a pesquisa incômoda, mas o tipo de funcionalidade que fornece feedback linha por linha também tornaria o sistema útil para o ensino, diz Heather Macbeth, matemática da Fordham University.

Nesta primavera, a Dra. Macbeth projetou um curso "bilíngue" Ela traduziu todos os problemas do quadro-negro em código Lean nas notas de aula, e os alunos precisam apresentar soluções em linguagem Lean e natural.

"Isso lhes deu confiança", disse Macbeth, porque eles receberiam feedback instantâneo sobre quando a prova estivesse completa e se cada passo ao longo do caminho estava certo ou errado.

E depois de participar de um workshop, a matemática Emily Riehl, da Universidade Johns Hopkins, deu uma chance.

Emily Riehl, matemática da Universidade Johns Hopkins, tem usado um assistente de prova experimental

Ela usou um miniaplicativo assistente de prova para provar os teoremas em seus artigos publicados anteriormente.

Depois de usá-lo, ela ficou chocada. "Agora entendo o processo de prova muito mais profundamente do que antes. Meu pensamento é tão claro que posso explicá-lo ao computador mais idiota."

Um projeto de grupo do qual os alunos participaram durante a Escola de Verão de Formalização Matemática

**Raciocínio violento - isso não é "matemático" **

Outra ferramenta que os cientistas da computação costumam usar para resolver alguns problemas matemáticos é chamada de "raciocínio violento", mas a comunidade matemática frequentemente zomba desse método.

No entanto, os cientistas da IA não parecem se importar muito com as ideias dos matemáticos e continuam a usar seus próprios métodos familiares para capturar as "terras altas" da matemática.

Heule, um cientista da computação da Carnegie Mellon University, usou um arquivo "SAT solver" 200T para resolver o "problema triplo booleano de Pitágoras" em 2016.

A revista "Nature" disse no artigo: "A prova de 200T é o maior processo de prova da história. É realmente matemática usar essas ferramentas para resolver problemas?"

Mas, na opinião do cientista da computação Heule, o próprio autor do artigo sobre a solução do problema, "essa abordagem é necessária para resolver problemas além do escopo das capacidades humanas".

Da mesma forma, depois de derrotar humanos em um jogo de xadrez (AlphaZero), a DeepMind projetou algoritmos de aprendizado de máquina para resolver o dobramento de proteínas (AlphaFold).

A DeepMind publicou um artigo argumentando que a maneira como eles alcançaram esses resultados foi usando IA para guiar a intuição humana para o avanço da matemática.

Yuhuai Wu, um ex-cientista da computação do Google que agora está abrindo um negócio na Bay Area, também disse que a direção de seu negócio é usar o aprendizado de máquina para resolver problemas matemáticos.

Seu projeto atual, Minerva, é um grande modelo de linguagem ajustado para resolver modelos matemáticos.

No futuro, ele espera que o projeto se transforme em um "matemático automatizado" que possa "resolver problemas de matemática independentemente" como assistente de pesquisa geral.

Matemática é um teste decisivo

Por outro lado, muitos matemáticos que tiveram contato profundo com a tecnologia de IA também levantaram preocupações de que a IA não é levada a sério na pesquisa matemática.

Eles acreditam que a tecnologia de inteligência artificial muitas vezes pode "diretamente" ajudar os matemáticos a "encontrar" as respostas que desejam.

Embora matemáticos ou especialistas em IA não tenham ideia de como a IA encontrou essa resposta.

Geordie Williamson, um matemático que trabalhou com DeepMind, uma vez compartilhou uma experiência de trabalho com DeepMind.

No processo de sua cooperação com DeepMind, uma rede neural descoberta por DeepMind pode prever o valor dos dados que ele considera muito importante e é extremamente preciso.

Ele está se esforçando muito para entender como a IA faz isso, porque isso pode ser a base para um teorema.

Mas ele ainda não conseguia entender a lógica da IA no final, e o pessoal da DeepMind também não conseguia.

Como Euclides, as redes neurais de alguma forma encontram a verdade, mas as razões lógicas são difíceis de entender.

A inferência, por outro lado, do ponto de vista do matemático, é a essência da matemática, mas uma peça que falta no quebra-cabeça do aprendizado de máquina.

No mundo da tecnologia, o mundo da tecnologia ficaria perfeitamente satisfeito se houvesse uma caixa preta que fornecesse uma solução para um problema na maioria das vezes.

A IA é uma caixa preta.

Mas os matemáticos não estão satisfeitos com esta situação.

Segundo o matemático, tentar entender como as redes neurais funcionam levanta questões matemáticas fascinantes.

E resolver esses problemas permitirá que os matemáticos "façam contribuições significativas para o mundo".

Se a IA puder provar teoremas matemáticos

O que faríamos se o mundo fosse inundado com hipóteses geradas por IA?

Os internautas enviaram a tortura da alma para isso, e tenho dúvidas sobre a nova hipótese/fórmula do sistema de IA como primeiro passo, porque o DeepMind já fez isso na teoria dos nós.

Eu me pergunto como a comunidade responderá à enxurrada de novas suposições geradas pela IA. Uma coisa é verificar um argumento lógico criado por uma IA; outra é ser dominado por milhões de sugestões do tipo “oh, isso pode ser verdade”. Não acho que nossos sistemas existentes de revisão e publicação estejam prontos para isso.

Como isso afeta a confiança das pessoas na matemática?

Tem sido argumentado que as máquinas não serão capazes de fazer matemática tão cedo, mas pode ser visto mudando a forma como a pesquisa é feita da mesma forma que os modelos de aprendizado de máquina e o poder computacional mudaram o campo da biologia.

Alguns internautas disseram que desde o AlphaDev, tenho pensado sobre esse problema, mas o mesmo programa pode construir algoritmos de classificação e também pode usar verificadores automáticos de prova para provar teoremas matemáticos. A verdadeira questão é se ela pode ser usada para provar algo importante, não apenas uma descoberta trivial.

No entanto, alguns internautas ainda estão céticos sobre se as ferramentas do tipo GPT podem realmente descobrir verdades valiosas.

Alguns internautas também apontaram que pode haver uma diferença entre humanos e IA na compreensão e atenção à matemática. A IA prova o que é verdade, enquanto os humanos sempre se concentram no porquê disso ser verdade.

Referências: