A Google DeepMind anunciou que seus sistemas de inteligência artificial (IA), AlphaProof e AlphaGeometry 2, resolveram quatro dos seis problemas da Olimpíada Internacional de Matemática (IMO) deste ano, alcançando uma pontuação equivalente a uma medalha de prata.
A gigante da tecnologia afirma que esta é a primeira vez que uma IA atinge este nível de desempenho na prestigiada competição de matemática, mas, como é habitual na IA, as reivindicações não são tão claras quanto parecem.
A primeira IA a chegar ao pódio na IMO
A Google afirma que o AlphaProof utiliza aprendizagem por reforço para provar declarações matemáticas na linguagem formal chamada Lean. O sistema treina-se a si mesmo gerando e verificando milhões de provas, abordando progressivamente problemas mais difíceis.
Enquanto isso, o AlphaGeometry 2 é descrito como uma versão atualizada do modelo anterior de resolução de geometria da Google, agora alimentado por um modelo de linguagem baseado em Gemini e treinado com muito mais dados.
Segundo a Google, os proeminentes matemáticos Sir Timothy Gowers e Dr. Joseph Myers avaliaram as soluções do modelo de IA usando as regras oficiais da IMO. A empresa relata que o seu sistema combinado obteve 28 dos 42 pontos possíveis, ficando aquém do limite de 29 pontos para a medalha de ouro.
Isto incluiu uma pontuação perfeita no problema mais difícil da competição, que a Google afirma que apenas cinco concorrentes humanos resolveram este ano.
Um feito impressionante, mas com nuances
A IMO, realizada anualmente desde 1959, coloca matemáticos de elite em idade pré-universitária contra problemas excecionalmente difíceis em álgebra, combinatória, geometria e teoria dos números. O desempenho nos problemas da IMO tornou-se um ponto de referência reconhecido para avaliar as capacidades de raciocínio matemático de um sistema de IA.
A Google afirma que o AlphaProof resolveu dois problemas de álgebra e um problema de teoria dos números, enquanto o AlphaGeometry 2 abordou a questão da geometria. O modelo de IA não conseguiu resolver os dois problemas de combinatória. A empresa afirma que os seus sistemas resolveram um problema em minutos, enquanto outros levaram até três dias.
Tradução para linguagem formal: um passo crucial
A Google diz que primeiro traduziu os problemas da IMO para linguagem matemática formal para que o seu modelo de IA os processasse. Este passo difere da competição oficial, onde os concorrentes humanos trabalham diretamente com as declarações dos problemas durante duas sessões de 4,5 horas.
A Google relata que, antes da competição deste ano, o AlphaGeometry 2 podia resolver 83% dos problemas históricos de geometria da IMO dos últimos 25 anos, acima da taxa de sucesso de 53% do seu antecessor. A empresa afirma que o novo sistema resolveu o problema de geometria deste ano em 19 segundos após receber a versão formalizada.
Limitações e o futuro da IA na matemática
Apesar das afirmações da Google, Sir Timothy Gowers ofereceu uma perspetiva mais matizada sobre os modelos da Google DeepMind numa thread publicada no X (antigo Twitter). Embora reconhecendo a conquista como “muito além do que os demonstradores automáticos de teoremas podiam fazer antes”, Gowers apontou várias qualificações importantes.
“A principal qualificação é que o programa precisou de muito mais tempo do que os concorrentes humanos — para alguns dos problemas mais de 60 horas — e, claro, uma velocidade de processamento muito mais rápida do que o pobre e velho cérebro humano”, escreveu Gowers. “Se os concorrentes humanos tivessem tido esse tipo de tempo por problema, eles, sem dúvida, teriam pontuado mais alto.”
Gowers também observou que os humanos traduziram manualmente os problemas para a linguagem formal Lean antes do modelo de IA começar seu trabalho. Ele enfatizou que, embora a IA tenha realizado o raciocínio matemático central, este passo de “autoformalização” foi feito por humanos.
Relativamente às implicações mais amplas para a pesquisa matemática, Gowers expressou incerteza. “Estamos perto do ponto em que os matemáticos são redundantes? É difícil dizer. Eu diria que ainda estamos a uma ou duas descobertas disso”, escreveu. Ele sugeriu que os longos tempos de processamento do sistema indicam que ele não “resolveu a matemática”, mas reconheceu que “claramente há algo interessante acontecendo quando ele opera”.
Mesmo com estas limitações, Gowers especulou que tais sistemas de IA poderiam tornar-se ferramentas de pesquisa valiosas. “Então, poderíamos estar perto de ter um programa que permitiria aos matemáticos obter respostas para uma ampla gama de perguntas, desde que essas perguntas não fossem muito difíceis — o tipo de coisa que se pode fazer em algumas horas. Isso seria extremamente útil como ferramenta de pesquisa, mesmo que não fosse capaz de resolver problemas em aberto.”
Outros artigos interessantes:
