Matemáticos se preparam para encarar a inteligência artificial

THE NEW YORK TIMES - Na coleção do Museu Getty em Los Angeles, EUA, há um retrato do século 17 do antigo matemático grego Euclides: desgrenhado, segurando folhas de “Elementos”, seu tratado sobre geometria, com as mãos sujas.

Por mais de 2 mil anos, o texto de Euclides foi o paradigma de argumentação e raciocínio matemático. “Euclides começa com ‘definições’ que são quase poéticas”, diz Jeremy Avigad, um lógico da Carnegie Mellon University em e-mail. “Depois, ele construiu a matemática da época com base nisso, provando coisas de tal maneira que cada passo sucessivo ‘segue claramente’ dos anteriores, usando noções básicas, definições e teoremas anteriores.” Havia reclamações de que alguns dos passos “óbvios” de Euclides eram menos do que óbvios, diz Avigad, mas o sistema funcionou.

Mas, no século 20, os matemáticos já não estavam dispostos a fundamentar a matemática nesta fundação geométrica intuitiva. Em vez disso, eles desenvolveram sistemas formais - representações simbólicas precisas, regras mecânicas. Eventualmente, essa formalização permitiu que a matemática fosse traduzida em código de computador. Em 1976, o teorema das quatro cores - que afirma que quatro cores são suficientes para preencher um mapa de forma que nenhuma região adjacente tenha a mesma cor - tornou-se o primeiro grande teorema a ser provado com a ajuda da força bruta computacional.

Agora, os matemáticos estão lidando com a mais recente força transformadora: a inteligência artificial (IA).

Em 2019, Christian Szegedy, cientista da computação que trabalhava no Google e agora em uma startup na região de São Francisco (EUA), previu que um sistema de computador igualaria ou superaria a capacidade de resolução de problemas dos melhores matemáticos humanos em uma década. No ano passado, ele revisou a data-alvo para 2026.

Akshay Venkatesh, matemático do Institute for Advanced Study em Princeton, EUA, e vencedor da Medalha Fields em 2018, atualmente não está interessado em usar IA, mas está interessado em falar sobre isso. “Quero que meus alunos percebam que o campo em que estão vai mudar muito”, disse ele em uma entrevista no ano passado. Ele acrescentou recentemente por e-mail: “Não sou contra o uso atencioso e deliberado da tecnologia para apoiar nosso entendimento humano. Mas acredito fortemente que a atenção sobre a forma como a usamos é essencial.”

Em fevereiro, Avigad participou de um workshop sobre “provas assistidas por máquinas” no Institute for Pure and Applied Mathematics, no campus da Universidade da Califórnia. O encontro reuniu uma mistura atípica de matemáticos e cientistas da computação. “Parece importante”, disse Terence Tao, matemático da universidade, vencedor de uma Medalha Fields em 2006 e principal organizador do workshop.

Tao observou que apenas nos últimos anos os matemáticos começaram a se preocupar com as possíveis ameaças da IA, seja para a estética matemática ou para eles próprios. O fato de membros proeminentes da comunidade agora abordarem as questões e explorarem o potencial “meio que quebra o tabu”, disse ele.

Um participante importante do workshop estava sentado na primeira fila: uma caixa trapezoidal chamada “robô levanta a mão” que emitia um murmúrio mecânico e levantava a mão sempre que um participante online tinha uma pergunta. “Ajuda se os robôs forem fofos e inofensivos”, disse Tao.

Hoje em dia, não há escassez de aparelhos para otimizar nossas vidas - dieta, sono, exercício. “Gostamos de conectar coisas a nós mesmos para tornar um pouco mais fácil acertar as coisas”, diz Jordan Ellenberg, matemático da Universidade de Wisconsin-Madison, EUA. A aparelhagem de IA pode fazer o mesmo pela matemática, acrescentou ele: “Está muito claro que a questão é: O que as máquinas podem fazer por nós, não o que as máquinas farão conosco.”

Um gadget matemático é chamado de assistente de prova ou verificador de teoremas interativo. (“Automath” foi uma das primeiras versões na década de 1960.) Passo a passo, um matemático traduz uma prova em código; então, um programa de software verifica se o raciocínio está correto. As verificações se acumulam em uma biblioteca, uma referência canônica dinâmica que outros podem consultar. Esse tipo de formalização fornece uma base para a matemática hoje, disse Avigad, que é diretor do Hoskinson Center for Formal Mathematics (financiado pelo empreendedor de criptografia Charles Hoskinson), “da mesma forma que Euclides estava tentando codificar e fornecer uma base para a matemática de seu tempo.”

Recentemente, o sistema de assistente de prova de código aberto Lean tem atraído atenção. Desenvolvido na Microsoft por Leonardo de Moura, cientista da computação agora na Amazon, Lean usa raciocínio automatizado, que é alimentado pelo que é conhecido como boa e velha inteligência artificial ou GOFAI - IA simbólica, inspirada pela lógica. Até agora, a comunidade Lean verificou um teorema intrigante sobre como virar uma esfera do avesso, bem como um teorema fundamental em um esquema para unificar reinos matemáticos, entre outras coisas.

Mas um assistente de prova também tem desvantagens: muitas vezes reclama que não entende as definições, axiomas ou etapas de raciocínio inseridas pelo matemático, e por isso foi apelidado de “reclamador de prova”. Tanto reclamar pode tornar a pesquisa complicada. Mas Heather Macbeth, matemática da Fordham University, EUA, disse que essa mesma característica - fornecer feedback linha por linha - também torna os sistemas úteis para o ensino.

Na primavera, Macbeth projetou um curso “bilíngue”: ela traduziu todos os problemas apresentados no quadro-negro para código Lean nas notas da palestra, e os alunos enviaram soluções para os problemas de casa tanto em Lean quanto em prosa. “Isso lhes deu confiança”, disse Macbeth, porque eles receberam feedback instantâneo sobre quando a prova estava terminada e se cada passo ao longo do caminho estava certo ou errado.

Desde que participou do workshop, Emily Riehl, matemática da Johns Hopkins University, EUA, usou um programa experimental de assistente de prova para formalizar provas que ela havia publicado anteriormente com um co-autor. No final de uma verificação, ela disse, “Eu realmente me aprofundo em entender a prova, muito mais do que eu jamais entendi antes. Estou pensando tão claramente que posso explicar para um computador realmente burro.”

Outra ferramenta de raciocínio automatizado, usada por Marijn Heule, cientista da computação da Carnegie Mellon University, EUA, e bolsista da Amazon, é o que ele chama coloquialmente de “raciocínio bruto” (ou, mais tecnicamente, um resolvedor de Satisfabilidade ou SAT). Ao simplesmente declarar, com uma codificação cuidadosamente elaborada, qual “objeto exótico” você deseja encontrar, disse ele, uma rede de supercomputadores vasculha um espaço de busca e determina se essa entidade existe ou não.

Pouco antes do workshop, Heule e um de seus alunos de doutorado, Bernardo Subercaseaux, finalizaram sua solução para um problema antigo com um arquivo de 50 terabytes. No entanto, esse arquivo mal se comparava com um resultado que Heule e colaboradores produziram em 2016: “Prova de matemática de duzentos terabytes é a maior de todos os tempos”, anunciou uma manchete na Nature. O artigo continuou perguntando se resolver problemas com tais ferramentas realmente contava como matemática. Na visão de Heule, essa abordagem é necessária “para resolver problemas que estão além do que os humanos podem fazer.”

Outro conjunto de ferramentas usa aprendizado de máquina, que sintetiza muitos dados e detecta padrões, mas não é bom em raciocínio lógico, passo a passo. O DeepMind do Google cria algoritmos de aprendizado de máquina para enfrentar desafios como dobrar proteínas (AlphaFold) e vencer no xadrez (AlphaZero). Em um artigo na Nature de 2021, uma equipe descreveu seus resultados como “avançando na matemática ao orientar a intuição humana com IA.”

Yuhuai “Tony” Wu, cientista da computação que trabalhou no Google, delineou um objetivo mais ambicioso para o aprendizado de máquina: “resolver matemática”. No Google, Wu explorou como os grandes modelos de linguagem que potencializam os chatbots podem ajudar com a matemática. A equipe usou um modelo treinado em dados da internet e depois refinado em um grande conjunto de dados rico em matemática, usando, por exemplo, um arquivo online de artigos de matemática e ciências. Quando solicitado em inglês comum a resolver problemas de matemática, este chatbot especializado, chamado Minerva, era “muito bom em imitar humanos”, disse o Wu no workshop. O modelo obteve pontuações melhores do que um estudante de 16 anos em exames de matemática do ensino médio.

Eventualmente, Wu disse que ele imaginou um “matemático automatizado” que tem “a capacidade de resolver um teorema matemático por conta própria.”

Matemáticos reagiram a essas mudanças com diferentes níveis de preocupação.

Michael Harris, da Universidade Columbia, EUA, expressa suas dúvidas no seu site “Silicon Reckoner”. Ele está preocupado com os objetivos e valores potencialmente conflitantes da pesquisa matemática e das indústrias de tecnologia e defesa. Em um boletim recente, ele observou que um dos palestrantes em um workshop, “IA para Auxiliar o Raciocínio Matemático”, organizado pela Academia Nacional de Ciências (NAS), foi um representante da Booz Allen Hamilton, um contratado do governo para agências de inteligência e militares.

Harris lamentou a falta de discussão sobre as implicações mais amplas da IA na pesquisa matemática, particularmente “quando comparado com a conversa muito animada acontecendo” sobre a tecnologia “praticamente em todos os lugares, exceto na matemática.”

Geordie Williamson, da Universidade de Sydney e colaborador da DeepMind, falou no encontro da NAS e encorajou matemáticos e cientistas da computação a se envolverem mais nessas conversas. No workshop em Los Angeles, ele iniciou sua palestra com uma frase adaptada de “You and the Atom Bomb”, um ensaio de 1945 de George Orwell. “Dado o quão provável é que todos nós sejamos profundamente afetados nos próximos cinco anos,” Dr. Williamson disse, “o aprendizado profundo não despertou tanta discussão quanto poderia ter sido esperado.”

Williamson considera a matemática um teste decisivo do que o aprendizado de máquina pode ou não fazer. O raciocínio é essencial para o processo matemático, e é o problema crucial não resolvido do aprendizado de máquina.

No início da colaboração do Williamson com a DeepMind, a equipe encontrou uma simples rede neural que previa “uma quantidade em matemática pela qual eu me importava profundamente”, ele disse em uma entrevista, e fez isso “ridiculamente com precisão”. Williamson tentou arduamente entender por que - isso seria a base de um teorema - mas não conseguiu. Nem ninguém na DeepMind. Como o antigo geômetra Euclides, a rede neural de alguma forma intuiu uma verdade matemática, mas a lógica por trás disso estava longe de ser óbvia.

No workshop de Los Angeles, um tema proeminente foi como combinar o intuitivo e o lógico. Se a IA pudesse fazer ambos ao mesmo tempo, todas as apostas estariam encerradas.

Mas, aponta Williamson, há pouca motivação para entender a caixa-preta que o aprendizado de máquina apresenta. “É a cultura de fazer de qualquer jeito na tecnologia, onde, se funciona na maioria das vezes, isso é ótimo”, disse ele - mas esse cenário deixa os matemáticos insatisfeitos.

Ele acrescentou que tentar entender o que acontece dentro de uma rede neural levanta “questões matemáticas fascinantes” e que encontrar respostas apresenta uma oportunidade para os matemáticos “contribuírem significativamente para o mundo”./TRADUZIDO POR ALICE LABATE

THE NEW YORK TIMES - Na coleção do Museu Getty em Los Angeles, EUA, há um retrato do século 17 do antigo matemático grego Euclides: desgrenhado, segurando folhas de “Elementos”, seu tratado sobre geometria, com as mãos sujas.

Por mais de 2 mil anos, o texto de Euclides foi o paradigma de argumentação e raciocínio matemático. “Euclides começa com ‘definições’ que são quase poéticas”, diz Jeremy Avigad, um lógico da Carnegie Mellon University em e-mail. “Depois, ele construiu a matemática da época com base nisso, provando coisas de tal maneira que cada passo sucessivo ‘segue claramente’ dos anteriores, usando noções básicas, definições e teoremas anteriores.” Havia reclamações de que alguns dos passos “óbvios” de Euclides eram menos do que óbvios, diz Avigad, mas o sistema funcionou.

Mas, no século 20, os matemáticos já não estavam dispostos a fundamentar a matemática nesta fundação geométrica intuitiva. Em vez disso, eles desenvolveram sistemas formais - representações simbólicas precisas, regras mecânicas. Eventualmente, essa formalização permitiu que a matemática fosse traduzida em código de computador. Em 1976, o teorema das quatro cores - que afirma que quatro cores são suficientes para preencher um mapa de forma que nenhuma região adjacente tenha a mesma cor - tornou-se o primeiro grande teorema a ser provado com a ajuda da força bruta computacional.

Agora, os matemáticos estão lidando com a mais recente força transformadora: a inteligência artificial (IA).

Em 2019, Christian Szegedy, cientista da computação que trabalhava no Google e agora em uma startup na região de São Francisco (EUA), previu que um sistema de computador igualaria ou superaria a capacidade de resolução de problemas dos melhores matemáticos humanos em uma década. No ano passado, ele revisou a data-alvo para 2026.

Akshay Venkatesh, matemático do Institute for Advanced Study em Princeton, EUA, e vencedor da Medalha Fields em 2018, atualmente não está interessado em usar IA, mas está interessado em falar sobre isso. “Quero que meus alunos percebam que o campo em que estão vai mudar muito”, disse ele em uma entrevista no ano passado. Ele acrescentou recentemente por e-mail: “Não sou contra o uso atencioso e deliberado da tecnologia para apoiar nosso entendimento humano. Mas acredito fortemente que a atenção sobre a forma como a usamos é essencial.”

Em fevereiro, Avigad participou de um workshop sobre “provas assistidas por máquinas” no Institute for Pure and Applied Mathematics, no campus da Universidade da Califórnia. O encontro reuniu uma mistura atípica de matemáticos e cientistas da computação. “Parece importante”, disse Terence Tao, matemático da universidade, vencedor de uma Medalha Fields em 2006 e principal organizador do workshop.

Tao observou que apenas nos últimos anos os matemáticos começaram a se preocupar com as possíveis ameaças da IA, seja para a estética matemática ou para eles próprios. O fato de membros proeminentes da comunidade agora abordarem as questões e explorarem o potencial “meio que quebra o tabu”, disse ele.

Um participante importante do workshop estava sentado na primeira fila: uma caixa trapezoidal chamada “robô levanta a mão” que emitia um murmúrio mecânico e levantava a mão sempre que um participante online tinha uma pergunta. “Ajuda se os robôs forem fofos e inofensivos”, disse Tao.

Hoje em dia, não há escassez de aparelhos para otimizar nossas vidas - dieta, sono, exercício. “Gostamos de conectar coisas a nós mesmos para tornar um pouco mais fácil acertar as coisas”, diz Jordan Ellenberg, matemático da Universidade de Wisconsin-Madison, EUA. A aparelhagem de IA pode fazer o mesmo pela matemática, acrescentou ele: “Está muito claro que a questão é: O que as máquinas podem fazer por nós, não o que as máquinas farão conosco.”

Um gadget matemático é chamado de assistente de prova ou verificador de teoremas interativo. (“Automath” foi uma das primeiras versões na década de 1960.) Passo a passo, um matemático traduz uma prova em código; então, um programa de software verifica se o raciocínio está correto. As verificações se acumulam em uma biblioteca, uma referência canônica dinâmica que outros podem consultar. Esse tipo de formalização fornece uma base para a matemática hoje, disse Avigad, que é diretor do Hoskinson Center for Formal Mathematics (financiado pelo empreendedor de criptografia Charles Hoskinson), “da mesma forma que Euclides estava tentando codificar e fornecer uma base para a matemática de seu tempo.”

Recentemente, o sistema de assistente de prova de código aberto Lean tem atraído atenção. Desenvolvido na Microsoft por Leonardo de Moura, cientista da computação agora na Amazon, Lean usa raciocínio automatizado, que é alimentado pelo que é conhecido como boa e velha inteligência artificial ou GOFAI - IA simbólica, inspirada pela lógica. Até agora, a comunidade Lean verificou um teorema intrigante sobre como virar uma esfera do avesso, bem como um teorema fundamental em um esquema para unificar reinos matemáticos, entre outras coisas.

Mas um assistente de prova também tem desvantagens: muitas vezes reclama que não entende as definições, axiomas ou etapas de raciocínio inseridas pelo matemático, e por isso foi apelidado de “reclamador de prova”. Tanto reclamar pode tornar a pesquisa complicada. Mas Heather Macbeth, matemática da Fordham University, EUA, disse que essa mesma característica - fornecer feedback linha por linha - também torna os sistemas úteis para o ensino.

Na primavera, Macbeth projetou um curso “bilíngue”: ela traduziu todos os problemas apresentados no quadro-negro para código Lean nas notas da palestra, e os alunos enviaram soluções para os problemas de casa tanto em Lean quanto em prosa. “Isso lhes deu confiança”, disse Macbeth, porque eles receberam feedback instantâneo sobre quando a prova estava terminada e se cada passo ao longo do caminho estava certo ou errado.

Desde que participou do workshop, Emily Riehl, matemática da Johns Hopkins University, EUA, usou um programa experimental de assistente de prova para formalizar provas que ela havia publicado anteriormente com um co-autor. No final de uma verificação, ela disse, “Eu realmente me aprofundo em entender a prova, muito mais do que eu jamais entendi antes. Estou pensando tão claramente que posso explicar para um computador realmente burro.”

Outra ferramenta de raciocínio automatizado, usada por Marijn Heule, cientista da computação da Carnegie Mellon University, EUA, e bolsista da Amazon, é o que ele chama coloquialmente de “raciocínio bruto” (ou, mais tecnicamente, um resolvedor de Satisfabilidade ou SAT). Ao simplesmente declarar, com uma codificação cuidadosamente elaborada, qual “objeto exótico” você deseja encontrar, disse ele, uma rede de supercomputadores vasculha um espaço de busca e determina se essa entidade existe ou não.

Pouco antes do workshop, Heule e um de seus alunos de doutorado, Bernardo Subercaseaux, finalizaram sua solução para um problema antigo com um arquivo de 50 terabytes. No entanto, esse arquivo mal se comparava com um resultado que Heule e colaboradores produziram em 2016: “Prova de matemática de duzentos terabytes é a maior de todos os tempos”, anunciou uma manchete na Nature. O artigo continuou perguntando se resolver problemas com tais ferramentas realmente contava como matemática. Na visão de Heule, essa abordagem é necessária “para resolver problemas que estão além do que os humanos podem fazer.”

Outro conjunto de ferramentas usa aprendizado de máquina, que sintetiza muitos dados e detecta padrões, mas não é bom em raciocínio lógico, passo a passo. O DeepMind do Google cria algoritmos de aprendizado de máquina para enfrentar desafios como dobrar proteínas (AlphaFold) e vencer no xadrez (AlphaZero). Em um artigo na Nature de 2021, uma equipe descreveu seus resultados como “avançando na matemática ao orientar a intuição humana com IA.”

Yuhuai “Tony” Wu, cientista da computação que trabalhou no Google, delineou um objetivo mais ambicioso para o aprendizado de máquina: “resolver matemática”. No Google, Wu explorou como os grandes modelos de linguagem que potencializam os chatbots podem ajudar com a matemática. A equipe usou um modelo treinado em dados da internet e depois refinado em um grande conjunto de dados rico em matemática, usando, por exemplo, um arquivo online de artigos de matemática e ciências. Quando solicitado em inglês comum a resolver problemas de matemática, este chatbot especializado, chamado Minerva, era “muito bom em imitar humanos”, disse o Wu no workshop. O modelo obteve pontuações melhores do que um estudante de 16 anos em exames de matemática do ensino médio.

Eventualmente, Wu disse que ele imaginou um “matemático automatizado” que tem “a capacidade de resolver um teorema matemático por conta própria.”

Matemáticos reagiram a essas mudanças com diferentes níveis de preocupação.

Michael Harris, da Universidade Columbia, EUA, expressa suas dúvidas no seu site “Silicon Reckoner”. Ele está preocupado com os objetivos e valores potencialmente conflitantes da pesquisa matemática e das indústrias de tecnologia e defesa. Em um boletim recente, ele observou que um dos palestrantes em um workshop, “IA para Auxiliar o Raciocínio Matemático”, organizado pela Academia Nacional de Ciências (NAS), foi um representante da Booz Allen Hamilton, um contratado do governo para agências de inteligência e militares.

Harris lamentou a falta de discussão sobre as implicações mais amplas da IA na pesquisa matemática, particularmente “quando comparado com a conversa muito animada acontecendo” sobre a tecnologia “praticamente em todos os lugares, exceto na matemática.”

Geordie Williamson, da Universidade de Sydney e colaborador da DeepMind, falou no encontro da NAS e encorajou matemáticos e cientistas da computação a se envolverem mais nessas conversas. No workshop em Los Angeles, ele iniciou sua palestra com uma frase adaptada de “You and the Atom Bomb”, um ensaio de 1945 de George Orwell. “Dado o quão provável é que todos nós sejamos profundamente afetados nos próximos cinco anos,” Dr. Williamson disse, “o aprendizado profundo não despertou tanta discussão quanto poderia ter sido esperado.”

Williamson considera a matemática um teste decisivo do que o aprendizado de máquina pode ou não fazer. O raciocínio é essencial para o processo matemático, e é o problema crucial não resolvido do aprendizado de máquina.

No início da colaboração do Williamson com a DeepMind, a equipe encontrou uma simples rede neural que previa “uma quantidade em matemática pela qual eu me importava profundamente”, ele disse em uma entrevista, e fez isso “ridiculamente com precisão”. Williamson tentou arduamente entender por que - isso seria a base de um teorema - mas não conseguiu. Nem ninguém na DeepMind. Como o antigo geômetra Euclides, a rede neural de alguma forma intuiu uma verdade matemática, mas a lógica por trás disso estava longe de ser óbvia.

No workshop de Los Angeles, um tema proeminente foi como combinar o intuitivo e o lógico. Se a IA pudesse fazer ambos ao mesmo tempo, todas as apostas estariam encerradas.

Mas, aponta Williamson, há pouca motivação para entender a caixa-preta que o aprendizado de máquina apresenta. “É a cultura de fazer de qualquer jeito na tecnologia, onde, se funciona na maioria das vezes, isso é ótimo”, disse ele - mas esse cenário deixa os matemáticos insatisfeitos.

Ele acrescentou que tentar entender o que acontece dentro de uma rede neural levanta “questões matemáticas fascinantes” e que encontrar respostas apresenta uma oportunidade para os matemáticos “contribuírem significativamente para o mundo”./TRADUZIDO POR ALICE LABATE

THE NEW YORK TIMES - Na coleção do Museu Getty em Los Angeles, EUA, há um retrato do século 17 do antigo matemático grego Euclides: desgrenhado, segurando folhas de “Elementos”, seu tratado sobre geometria, com as mãos sujas.

Por mais de 2 mil anos, o texto de Euclides foi o paradigma de argumentação e raciocínio matemático. “Euclides começa com ‘definições’ que são quase poéticas”, diz Jeremy Avigad, um lógico da Carnegie Mellon University em e-mail. “Depois, ele construiu a matemática da época com base nisso, provando coisas de tal maneira que cada passo sucessivo ‘segue claramente’ dos anteriores, usando noções básicas, definições e teoremas anteriores.” Havia reclamações de que alguns dos passos “óbvios” de Euclides eram menos do que óbvios, diz Avigad, mas o sistema funcionou.

Mas, no século 20, os matemáticos já não estavam dispostos a fundamentar a matemática nesta fundação geométrica intuitiva. Em vez disso, eles desenvolveram sistemas formais - representações simbólicas precisas, regras mecânicas. Eventualmente, essa formalização permitiu que a matemática fosse traduzida em código de computador. Em 1976, o teorema das quatro cores - que afirma que quatro cores são suficientes para preencher um mapa de forma que nenhuma região adjacente tenha a mesma cor - tornou-se o primeiro grande teorema a ser provado com a ajuda da força bruta computacional.

Agora, os matemáticos estão lidando com a mais recente força transformadora: a inteligência artificial (IA).

Em 2019, Christian Szegedy, cientista da computação que trabalhava no Google e agora em uma startup na região de São Francisco (EUA), previu que um sistema de computador igualaria ou superaria a capacidade de resolução de problemas dos melhores matemáticos humanos em uma década. No ano passado, ele revisou a data-alvo para 2026.

Akshay Venkatesh, matemático do Institute for Advanced Study em Princeton, EUA, e vencedor da Medalha Fields em 2018, atualmente não está interessado em usar IA, mas está interessado em falar sobre isso. “Quero que meus alunos percebam que o campo em que estão vai mudar muito”, disse ele em uma entrevista no ano passado. Ele acrescentou recentemente por e-mail: “Não sou contra o uso atencioso e deliberado da tecnologia para apoiar nosso entendimento humano. Mas acredito fortemente que a atenção sobre a forma como a usamos é essencial.”

Em fevereiro, Avigad participou de um workshop sobre “provas assistidas por máquinas” no Institute for Pure and Applied Mathematics, no campus da Universidade da Califórnia. O encontro reuniu uma mistura atípica de matemáticos e cientistas da computação. “Parece importante”, disse Terence Tao, matemático da universidade, vencedor de uma Medalha Fields em 2006 e principal organizador do workshop.

Tao observou que apenas nos últimos anos os matemáticos começaram a se preocupar com as possíveis ameaças da IA, seja para a estética matemática ou para eles próprios. O fato de membros proeminentes da comunidade agora abordarem as questões e explorarem o potencial “meio que quebra o tabu”, disse ele.

Um participante importante do workshop estava sentado na primeira fila: uma caixa trapezoidal chamada “robô levanta a mão” que emitia um murmúrio mecânico e levantava a mão sempre que um participante online tinha uma pergunta. “Ajuda se os robôs forem fofos e inofensivos”, disse Tao.

Hoje em dia, não há escassez de aparelhos para otimizar nossas vidas - dieta, sono, exercício. “Gostamos de conectar coisas a nós mesmos para tornar um pouco mais fácil acertar as coisas”, diz Jordan Ellenberg, matemático da Universidade de Wisconsin-Madison, EUA. A aparelhagem de IA pode fazer o mesmo pela matemática, acrescentou ele: “Está muito claro que a questão é: O que as máquinas podem fazer por nós, não o que as máquinas farão conosco.”

Um gadget matemático é chamado de assistente de prova ou verificador de teoremas interativo. (“Automath” foi uma das primeiras versões na década de 1960.) Passo a passo, um matemático traduz uma prova em código; então, um programa de software verifica se o raciocínio está correto. As verificações se acumulam em uma biblioteca, uma referência canônica dinâmica que outros podem consultar. Esse tipo de formalização fornece uma base para a matemática hoje, disse Avigad, que é diretor do Hoskinson Center for Formal Mathematics (financiado pelo empreendedor de criptografia Charles Hoskinson), “da mesma forma que Euclides estava tentando codificar e fornecer uma base para a matemática de seu tempo.”

Recentemente, o sistema de assistente de prova de código aberto Lean tem atraído atenção. Desenvolvido na Microsoft por Leonardo de Moura, cientista da computação agora na Amazon, Lean usa raciocínio automatizado, que é alimentado pelo que é conhecido como boa e velha inteligência artificial ou GOFAI - IA simbólica, inspirada pela lógica. Até agora, a comunidade Lean verificou um teorema intrigante sobre como virar uma esfera do avesso, bem como um teorema fundamental em um esquema para unificar reinos matemáticos, entre outras coisas.

Mas um assistente de prova também tem desvantagens: muitas vezes reclama que não entende as definições, axiomas ou etapas de raciocínio inseridas pelo matemático, e por isso foi apelidado de “reclamador de prova”. Tanto reclamar pode tornar a pesquisa complicada. Mas Heather Macbeth, matemática da Fordham University, EUA, disse que essa mesma característica - fornecer feedback linha por linha - também torna os sistemas úteis para o ensino.

Na primavera, Macbeth projetou um curso “bilíngue”: ela traduziu todos os problemas apresentados no quadro-negro para código Lean nas notas da palestra, e os alunos enviaram soluções para os problemas de casa tanto em Lean quanto em prosa. “Isso lhes deu confiança”, disse Macbeth, porque eles receberam feedback instantâneo sobre quando a prova estava terminada e se cada passo ao longo do caminho estava certo ou errado.

Desde que participou do workshop, Emily Riehl, matemática da Johns Hopkins University, EUA, usou um programa experimental de assistente de prova para formalizar provas que ela havia publicado anteriormente com um co-autor. No final de uma verificação, ela disse, “Eu realmente me aprofundo em entender a prova, muito mais do que eu jamais entendi antes. Estou pensando tão claramente que posso explicar para um computador realmente burro.”

Outra ferramenta de raciocínio automatizado, usada por Marijn Heule, cientista da computação da Carnegie Mellon University, EUA, e bolsista da Amazon, é o que ele chama coloquialmente de “raciocínio bruto” (ou, mais tecnicamente, um resolvedor de Satisfabilidade ou SAT). Ao simplesmente declarar, com uma codificação cuidadosamente elaborada, qual “objeto exótico” você deseja encontrar, disse ele, uma rede de supercomputadores vasculha um espaço de busca e determina se essa entidade existe ou não.

Pouco antes do workshop, Heule e um de seus alunos de doutorado, Bernardo Subercaseaux, finalizaram sua solução para um problema antigo com um arquivo de 50 terabytes. No entanto, esse arquivo mal se comparava com um resultado que Heule e colaboradores produziram em 2016: “Prova de matemática de duzentos terabytes é a maior de todos os tempos”, anunciou uma manchete na Nature. O artigo continuou perguntando se resolver problemas com tais ferramentas realmente contava como matemática. Na visão de Heule, essa abordagem é necessária “para resolver problemas que estão além do que os humanos podem fazer.”

Outro conjunto de ferramentas usa aprendizado de máquina, que sintetiza muitos dados e detecta padrões, mas não é bom em raciocínio lógico, passo a passo. O DeepMind do Google cria algoritmos de aprendizado de máquina para enfrentar desafios como dobrar proteínas (AlphaFold) e vencer no xadrez (AlphaZero). Em um artigo na Nature de 2021, uma equipe descreveu seus resultados como “avançando na matemática ao orientar a intuição humana com IA.”

Yuhuai “Tony” Wu, cientista da computação que trabalhou no Google, delineou um objetivo mais ambicioso para o aprendizado de máquina: “resolver matemática”. No Google, Wu explorou como os grandes modelos de linguagem que potencializam os chatbots podem ajudar com a matemática. A equipe usou um modelo treinado em dados da internet e depois refinado em um grande conjunto de dados rico em matemática, usando, por exemplo, um arquivo online de artigos de matemática e ciências. Quando solicitado em inglês comum a resolver problemas de matemática, este chatbot especializado, chamado Minerva, era “muito bom em imitar humanos”, disse o Wu no workshop. O modelo obteve pontuações melhores do que um estudante de 16 anos em exames de matemática do ensino médio.

Eventualmente, Wu disse que ele imaginou um “matemático automatizado” que tem “a capacidade de resolver um teorema matemático por conta própria.”

Matemáticos reagiram a essas mudanças com diferentes níveis de preocupação.

Michael Harris, da Universidade Columbia, EUA, expressa suas dúvidas no seu site “Silicon Reckoner”. Ele está preocupado com os objetivos e valores potencialmente conflitantes da pesquisa matemática e das indústrias de tecnologia e defesa. Em um boletim recente, ele observou que um dos palestrantes em um workshop, “IA para Auxiliar o Raciocínio Matemático”, organizado pela Academia Nacional de Ciências (NAS), foi um representante da Booz Allen Hamilton, um contratado do governo para agências de inteligência e militares.

Harris lamentou a falta de discussão sobre as implicações mais amplas da IA na pesquisa matemática, particularmente “quando comparado com a conversa muito animada acontecendo” sobre a tecnologia “praticamente em todos os lugares, exceto na matemática.”

Geordie Williamson, da Universidade de Sydney e colaborador da DeepMind, falou no encontro da NAS e encorajou matemáticos e cientistas da computação a se envolverem mais nessas conversas. No workshop em Los Angeles, ele iniciou sua palestra com uma frase adaptada de “You and the Atom Bomb”, um ensaio de 1945 de George Orwell. “Dado o quão provável é que todos nós sejamos profundamente afetados nos próximos cinco anos,” Dr. Williamson disse, “o aprendizado profundo não despertou tanta discussão quanto poderia ter sido esperado.”

Williamson considera a matemática um teste decisivo do que o aprendizado de máquina pode ou não fazer. O raciocínio é essencial para o processo matemático, e é o problema crucial não resolvido do aprendizado de máquina.

No início da colaboração do Williamson com a DeepMind, a equipe encontrou uma simples rede neural que previa “uma quantidade em matemática pela qual eu me importava profundamente”, ele disse em uma entrevista, e fez isso “ridiculamente com precisão”. Williamson tentou arduamente entender por que - isso seria a base de um teorema - mas não conseguiu. Nem ninguém na DeepMind. Como o antigo geômetra Euclides, a rede neural de alguma forma intuiu uma verdade matemática, mas a lógica por trás disso estava longe de ser óbvia.

No workshop de Los Angeles, um tema proeminente foi como combinar o intuitivo e o lógico. Se a IA pudesse fazer ambos ao mesmo tempo, todas as apostas estariam encerradas.

Mas, aponta Williamson, há pouca motivação para entender a caixa-preta que o aprendizado de máquina apresenta. “É a cultura de fazer de qualquer jeito na tecnologia, onde, se funciona na maioria das vezes, isso é ótimo”, disse ele - mas esse cenário deixa os matemáticos insatisfeitos.

Ele acrescentou que tentar entender o que acontece dentro de uma rede neural levanta “questões matemáticas fascinantes” e que encontrar respostas apresenta uma oportunidade para os matemáticos “contribuírem significativamente para o mundo”./TRADUZIDO POR ALICE LABATE