No começo deste ano, o estudante de pós-graduação em matemática Sidharth Hariharan, da Universidade Carnegie Mellon (Estados Unidos), recebeu uma notícia que o levou às pressas e com lágrimas nos olhos ao escritório de seu orientador, .
Ele acabara de receber um email de Maryna Viazovska, professora da École Polytechnique Fédérale de Lausanne, na Suíça, e vencedora da Medalha Fields de 2022, a maior honraria da matemática.
Durante mais de dois anos, a dupla liderou uma equipe de seis matemáticos em um esforço para decompor uma das mais célebres demonstrações de Viazovska em uma sequência de etapas lógicas rigorosamente definidas, um processo conhecido como formalização.
Poucas horas antes, Viazovska recebera uma mensagem de um colega: alguém tinha chegado lá primeiro.
Ou, como ela logo passou a dizer com humor, eles haviam sido “gaussados”.
O responsável foi Gauss, um sistema de inteligência artificial (IA) desenvolvido pela Math, Inc., uma startup sediada na Califórnia. Alimentado com o roteiro elaborado pela equipe para formalizar o resultado de Viazovska —a solução para o problema do empacotamento de esferas em oito dimensões, isto é, o arranjo mais denso possível de esferas nesse espaço—, o sistema concluiu a tarefa em apenas cinco dias.
Embora a IA seja associada com frequência a tropeços em aritmética —como a falha que virou meme quando o ChatGPT não conseguiu contar corretamente o número de letras “r” em strawberry (morango, em inglês)—, as empresas de tecnologia vêm investindo grandes volumes de recursos no desenvolvimento de sistemas de raciocínio capazes de enfrentar problemas matemáticos ainda sem solução. Os avanços recentes deram origem a uma espécie de corrida armamentista entre os concorrentes da IA ansiosos para demonstrar as capacidades de seu modelo em um campo muitas vezes considerado o ápice do intelecto humano.
No fim de maio, a OpenAI anunciou que um de seus modelos refutara um teorema de 80 anos que os matemáticos consideravam verdadeiro havia décadas. Pouco mais tarde, o Google DeepMind divulgou soluções para outros nove problemas.
Dias depois que a OpenAI publicou seus resultados, uma equipe de matemáticos empregou as mesmas técnicas para resolver mais um teorema em aberto, reforçando a ideia de que a IA pode se tornar uma ferramenta valiosa —ou até uma parceira intelectual— para matemáticos que buscam explorar novas ideias.
“Há cerca de 12 meses, ainda se poderia dizer que essas são curiosidades ou exageros que não têm utilidade. Agora já não dá para sustentar essa posição”, disse o matemático Terence Tao, da Universidade da Califórnia em Los Angeles, ganhador da Medalha Fields.
Para os milhares de estudantes de pós-graduação nos Estados Unidos que almejam um futuro na matemática pura —e que aprendem o ofício desenvolvendo muitas das mesmas habilidades e enfrentando muitos dos mesmos problemas que a IA está começando a dominar—, é difícil não vislumbrar um cenário preocupante.
O artigo da OpenAI foi um “choque”, afirmou o estudante de pós-graduação Carl Schildkraut, da Universidade Stanford, participante do trabalho subsequente que ampliou a técnica. Segundo ele, seus colegas de pós-graduação “não estão, em geral, muito otimistas” em relação às próprias perspectivas profissionais. Mas, ao examinar o resultado mais de perto, Schildkraut também percebeu os limites da matemática produzida pela IA.
“Quando nós, humanos, fazemos matemática, estamos constantemente nos perguntando coisas como: ‘que ideias estou desenvolvendo?’ ou ‘o que de fato está acontecendo aqui?'”
No começo de junho, um grupo internacional de matemáticos publicou uma declaração reconhecendo os benefícios da IA e pedindo cautela ao mesmo tempo. Eles estão preocupados com a relutância das companhias de IA em revelar informações básicas sobre seus métodos, a falha em dar o devido crédito aos autores humanos e a ânsia de confundir proeza matemática com a ideia de superinteligência artificial. O slogan da empresa Math, Inc., por exemplo, é este: “Resolva a matemática, resolva tudo”.
‘A gente se pergunta se tudo foi em vão’
O problema do empacotamento de esferas é fácil de visualizar em três dimensões: imagine uma pilha de laranjas em uma banca de feira. Qual é a configuração mais compacta possível? A resposta, proposta pela primeira vez há 400 anos, é exatamente a pilha de frutas que você imaginou, mas é difícil descartar todas as outras possibilidades. A comprovação escapou aos matemáticos até 1998.
O empacotamento de esferas em dimensões superiores, como a oitava, é mais difícil de visualizar, envolvendo pontos no espaço definidos por mais de três números. A prova de Viazovska estabeleceu ligações surpreendentes entre dois subcampos diferentes da matemática: a geometria e a teoria dos números —conexões que a equipe esperava explorar com mais detalhes à medida que formalizava a comprovação.
Quando Hariharan a procurou para formalizar sua solução, ela encarou isso como uma oportunidade de aprendizado. “Talvez a maneira mais fácil fosse formalizar algo menor sozinha. Mas isso não é muito divertido”, afirmou Viazovska. No início, ela lhe ensinou os conceitos de alto nível enquanto ele a ensinava a usar o software, chamado Lean, que usariam em seu trabalho. A seguir, com outros quatro matemáticos, desenvolveram um roteiro para detalhar a lógica da prova dela, passo a passo.
Depois de cerca de um ano de trabalho, o grupo abriu o projeto para colaboradores externos. O fato de várias empresas de IA, que usam o Lean para ensinar matemática a seus sistemas, terem se prontificado para ajudar não causou surpresa. Na época, porém, os melhores sistemas conseguiam produzir apenas trechos pequenos de código útil.
Então, no outono passado, quando a Math, Inc. informou o grupo de que o Gauss havia resolvido cerca de 30 partes inacabadas da comprovação, Hariharan e seus colegas ficaram entusiasmados e pediram à companhia que compartilhasse os resultados completos. Em vez disso, a startup deixou de dar notícias.
Auguste Poiroux, aluno de doutorado na École Polytechnique que também trabalha para a Math, Inc., declarou que a corporação havia voltado seu foco para uma nova versão do Gauss. A empresa decidiu voltar ao problema do empacotamento de esferas apenas meses depois, usando-o como um caso de teste para seu sistema atualizado.
Poiroux disse que, para surpresa geral, o Gauss aprimorado concluiu toda a demonstração.
Viazovska ficou ainda mais surpresa quando Poiroux, entusiasmado, lhe deu um vislumbre da solução “acidental”, como ele a descreveu. “Percebi rapidamente que a empolgação não era recíproca”, disse ele. Pediu então a Viazovska que esperasse para informar Hariharan, a quem ela enviou um email logo em seguida.
A próxima ligação de Hariharan foi para seus pais em Dubai. “A gente se pergunta se tudo foi em vão. E por que razão gastou dois anos da vida nisso”, questionou. E seus pais o aconselharam: “Confie no seu guru. Confie no processo”.
Naquela noite, Jesse Han, diretor-executivo da Math, Inc., enviou uma mensagem a Hariharan: embarcaria em um voo noturno para Pittsburgh. Eles se encontraram em um Starbucks na manhã seguinte, em companhia do orientador de Hariharan, Jeremy Avigad, que saiu correndo da academia depois do “banho mais rápido da minha vida”, como ele se lembrou. Quando Han propôs divulgar o resultado imediatamente e passar para um projeto de formalização relacionado, os acadêmicos se revoltaram, argumentando que o objetivo original do projeto —compreender melhor a prova de Viazovska— estava longe de ter sido alcançado.
“O resultado em si é certamente muito impressionante, mas também não é o que queríamos para nosso projeto”, afirmou Hariharan afirmou.
Contudo, depois de conversarem com outros matemáticos e revisarem o código, eles acabaram concordando com uma declaração que reconhecia que o Gauss produzira uma formalização correta meses antes do previsto.
Também concluíram que ainda havia meses de trabalho pela frente para tornar aquele código realmente utilizável pelas pessoas. “Ainda queríamos levar isso adiante”, afirmou Hariharan.
A pressa de ‘declarar vitória’
Uma maneira de encarar a situação enfrentada pelos jovens matemáticos é como uma versão em alta velocidade da automação que afeta o trabalho em outros setores, trazendo tanto oportunidades quanto o medo da obsolescência.
“Por experiência própria, eu sabia como era ser um aluno de doutorado e ter toda a sua identidade atrelada a um projeto como esse”, observou Han, que formalizou um resultado importante durante seu doutorado. Mas, por mais que tenha aprendido durante esse processo, ele diz acreditar que teria ido muito mais longe com a assistência da IA. “Eu teria ficado muito contente se esse tipo de resultado tivesse acontecido.”
Han afirmou que a revelação não foi intencional, mas sim uma consequência das melhorias vertiginosas na IA, e que esperava uma reação comemorativa. Contou que, em vez disso, sentiu-se emboscado pelas mensagens irritadas de ex-colegas, que começaram a chegar assim que desembarcou naquela manhã em Pittsburgh e que não pararam de ser enviadas desde então.
Segundo Vaughan McDonald, doutorando em matemática em Stanford, o desejo das empresas de IA de “declarar vitória” sobre certos problemas significa que o trabalho humano que tornou a automação possível geralmente não chega às manchetes, mesmo quando é reconhecido. Isso contribuiu para gerar certa dose de satisfação com o infortúnio alheio em relação a um campo acadêmico tão conceituado.
“As pessoas começaram a dizer: ‘Não deveria haver emprego para os matemáticos. Que eles se lixem.’ É uma coisa terrível”, afirmou McDonald.
Os matemáticos apontam para um desequilíbrio de poder entre departamentos de matemática em declínio e startups bem financiadas, que podem optar por gastar quantias equivalentes ao financiamento anual de vários alunos de pós-graduação em um único problema. Um funcionário da Math, Inc. disse à equipe de Hariharan que a companhia gastara mais de US$ 100 mil no cálculo da solução de empacotamento de esferas.
Mas, de acordo com McDonald, os matemáticos trazem “um valor tremendo” para a IA no trabalho intelectual que executam para viabilizar a automação. “E eles não estão sendo devidamente reconhecidos ou remunerados por isso.”
A equipe de Hariharan está usando ferramentas de IA para otimizar o código da Math, Inc. relativo à demonstração do empacotamento de esferas, colaborando com Poiroux para remover afirmações redundantes (como teoremas que provam por que 2 + 2 = 4) e converter as seções mais complexas em linguagem legível. Embora às vezes tenha sido um trabalho árduo, Hariharan disse que o processo rendeu uma “quantidade significativa de conhecimento”, tanto sobre a matemática de Viazovska quanto sobre o funcionamento da IA.
Neste verão do hemisfério norte, Hariharan também está estagiando na Axiom Math, outra startup de matemática baseada em IA, embora não tenha certeza do papel que essa tecnologia desempenhará nos seus planos de longo prazo. No entanto, quando regressar aos estudos no outono setentrional, seu próximo projeto não se concentrará na formalização.
“O próximo teorema que eu formalizar quero tê-lo provado eu mesmo”, declarou.
Fonte ==> Folha SP – TEC
