A IA é ‘burra’ com matemática e cientistas estão tentando mudar isso


Modelos de linguagem ampla ainda têm dificuldades com tarefas básicas de raciocínio, mas isso pode estar para mudar

Por Kevin Hartnett
Atualização:

QUANTA MAGAZINE - O mundo aprendeu duas coisas nos últimos meses sobre os modelos de linguagem ampla (LLMs) – os mecanismos de inteligência artificial (IA) por trás de programas como o ChatGPT e Dall-E. A primeira é que esses modelos parecem ter a inteligência e a criatividade de um ser humano. Eles dão respostas detalhadas e claras para as perguntas feitas ou criam imagens fascinantes com apenas algumas palavras.

A segunda é que eles não são confiáveis. Às vezes fazem afirmações ilógicas ou declaram sem titubear mentiras como se fossem fatos.

“Eles falam de unicórnios, mas depois esquecem que há apenas um único chifre, ou contam uma história e depois mudam as informações ao longo dela”, disse Jason Rute, da IBM Research.

continua após a publicidade

Isso é mais do que apenas um bug – pois comprova como os LLMs têm dificuldade para reconhecer seus erros, o que limita seu desempenho. O problema não é inerente aos sistemas de inteligência artificial. Os modelos de aprendizado de máquina se baseiam em uma técnica chamada aprendizado por reforço que permite aos computadores aprender com seus erros para se tornarem prodígios em jogos como xadrez e GO. Embora esses modelos costumem ser mais limitados em suas habilidades, eles demonstram um tipo de aprendizado que o LLMs ainda não dominam.

“Não queremos criar um modelo de linguagem que apenas converse como um ser humano”, disse Yuhuai (Tony) Wu, da Google AI. “Queremos que ele entenda do que está falando.”

Wu é coautor de dois artigos recentes que sugerem um caminho para conseguir isso. À primeira vista, eles falam de um uso muito específico: treinar sistemas de IA em matemática. O primeiro artigo descreve o treinamento de um LLM para traduzir afirmações matemáticas simples em códigos que um computador pode executar e verificar. O segundo treinou um LLM não apenas para entender problemas de matemática escritos em linguagem natural, mas para resolvê-los de verdade, usando um sistema chamado Minerva.

continua após a publicidade
A tecnologia está crescendo em muitas direções diferentes, e todas elas podem trabalhar juntas

Siddhartha Gadgil, matemático do Instituto Indiano de Ciência em Bangalore

Juntos, os artigos sugerem a forma do modelo de IA do futuro, no qual os LLMs podem aprender a raciocinar por meio do pensamento matemático.

“Temos coisas como aprendizado profundo, aprendizado por reforço, AlphaGo e agora os modelos de linguagem”, disse Siddhartha Gadgil, matemático do Instituto Indiano de Ciência em Bangalore, que trabalha com sistemas matemáticos de IA. “A tecnologia está crescendo em muitas direções diferentes, e todas elas podem trabalhar juntas.”

continua após a publicidade

Traduções não tão simples

Há décadas, os matemáticos traduzem provas em código de computação, um processo chamado formalização. O recurso é simples: se você escrever uma prova como código e um computador executá-lo sem erros, ela está correta. Mas formalizar uma única prova pode levar centenas ou milhares de horas.

Recentemente, Yuhuai (Tony) Wu foi coautor de dois artigos que ensinaram grandes modelos de linguagem a traduzir e resolver problemas matemáticos escritos em linguagem natural Foto: Christophe Testi/CreativeShot
continua após a publicidade

Nos últimos cinco anos, pesquisadores de IA começaram a ensinar os LLMs a formalizar automaticamente, ou “autoformalizar”, afirmações matemáticas na “linguagem formal” do código de computação. Os LLMs já podem traduzir de um um idioma para outro, como do português para o inglês. Mas traduzir da matemática para o código de programação é um desafio mais difícil. Há bem menos traduções de exemplo para treinar um LLM, para começar, e as linguagens formais nem sempre contêm todo o vocabulário necessário.

“Quando você traduz a palavra ‘queijo’ do português para o inglês, existe uma palavra em inglês para queijo”, disse Rute. “O problema está na matemática, não existe nem mesmo o conceito certo na linguagem formal.”

É por isso que os sete autores do primeiro artigo, profissionais do mercado e da academia, escolheram autoformalizar afirmações matemáticas curtas em vez de provas inteiras. Os pesquisadores trabalharam principalmente com um LLM chamado Codex, que tem como base o GPT-3 (o primeiro “cérebro” do ChatGPT), mas com treinamento extra em material técnico de fontes como o GitHub. Para fazer o Codex entender matemática bem o suficiente para autoformalizar, os pesquisadores deram a ele apenas dois exemplos de problemas matemáticos em linguagem natural e as suas traduções formais em código.

continua após a publicidade

Depois do breve tutorial, eles alimentaram o Codex com afirmações em linguagem natural de aproximadamente quatro mil problemas matemáticos de competições do ensino médio. A princípio, o desempenho dele pode parecer decepcionante: o Codex traduziu os problemas para a linguagem de um programa de matemática chamado Isabelle/HOL com uma taxa de precisão de pouco menos de 30%. Quando não conseguia fazer isso, inventava termos para preencher as lacunas com seu léxico de tradução.

“Às vezes, ele simplesmente não sabe a palavra que precisa saber – qual é o nome no Isabelle para ‘número primo’ ou o nome no Isabelle para “fatorial’ – e apenas inventa o termo, o que é o maior problema com esses modelos”, disse Rute. “Eles fazem suposições demais.”

Mas para os pesquisadores, o importante não era que o Codex havia falhado 70% das vezes, mas que tinha tido sucesso em 30% das vezes depois de ter acesso a um número tão limitado de exemplos.

continua após a publicidade

“Eles conseguiram fazer todas essas tarefas diferentes com apenas algumas demonstrações”, disse Wenda Li, cientista da computação da Universidade de Cambridge e coautor do artigo.

Cientistas tentam ensinar matemática para sistemas de IA Foto: Valentin Tkach/Quanta Magazine

Li e os demais coautores do artigo veem o resultado como característico do tipo de habilidade latente que os LLMs podem adquirir com dados gerais de treinamento suficientes. Antes dessa pesquisa, o Codex nunca tinha tentado traduzir da linguagem natural para o código matemático formal. Mas o Codex estava familiarizado com o código devido ao seu treinamento com o material do GitHub e com a matemática em linguagem natural da internet. Para aproveitar essa base, os pesquisadores apenas tiveram que mostrar a ele alguns exemplos do que queriam e o Codex poderia começar a ligar os pontos.

“Em muitos aspectos, o que é surpreendente nesse artigo é que [os autores] não fizeram muito”, disse Rute. “Esses modelos tinham essa capacidade natural de fazer isso.”

Os pesquisadores observaram o mesmo acontecer quando tentaram ensinar os LLMs não apenas a como traduzir problemas de matemática, mas também resolvê-los.

A matemática do Minerva

O segundo artigo, apesar de independente do trabalho anterior com autoformalização, chegou a uma conclusão semelhante. A equipe de pesquisadores do Google treinou um LLM para responder, em detalhes, questões de matemática de uma competição para estudantes do ensino médio, como “uma reta paralela a y = 4x + 6 passa pelo ponto (5, 10). Qual é a coordenada y do ponto onde esta reta passa pelo eixo y?”.

Os autores começaram com um LLM chamado PaLM, que tinha sido treinado com conteúdo geral em linguagem natural, semelhante ao GPT-3. Então eles treinaram o LLM com material matemático de sites como o arxiv.org e outros materiais técnicos, simulando as origens do Codex. Eles chamaram esse modelo ampliado de Minerva.

Os pesquisadores mostraram ao Minerva quatro exemplos do que queriam. Neste caso, isso significou soluções passo a passo para problemas de matemática em linguagem natural.

Em seguida, eles testaram o modelo com várias questões de raciocínio quantitativo. O desempenho do Minerva variava de acordo com o assunto: ele respondia corretamente às perguntas um pouco mais que a metade das vezes para alguns assuntos (como álgebra) e um pouco menos que a metade das vezes para outros (como geometria).

Uma das preocupações dos autores – comum em muitas áreas da pesquisa em IA – era que o Minerva respondesse às questões corretamente apenas porque já tinha visto elas, ou outras semelhantes a elas, em seus dados de treinamento. Esse problema é chamado de “poluição” e dificulta saber se um modelo está mesmo resolvendo os problemas ou apenas copiando o trabalho de outra pessoa.

“Há tantos dados nesses modelos que, a não ser que você esteja tentando evitar colocar alguns dados no conjunto de treinamento, se for um problema padrão, é muito provável que já tenha sido visto”, disse Rute.

Jason Rute, cientista da computação da IBM Research, vê potencial em modelos de linguagem grandes, mas também conhece seus pontos fracos. "Eles fazem muitas suposições", disse ele Foto: IBM

Para se protegerem dessa possibilidade, os pesquisadores submeteram o Minerva ao Exame Nacional de Matemática de 2022 da Polônia, realizado depois dos dados de treinamento do Minerva terem sido definidos. O sistema acertou 65% das questões, uma pontuação aceitável para um estudante de carne e osso e particularmente boa para um LLM, disse Rute. Mais uma vez, os resultados positivos depois de tão poucos exemplos sugeriram uma habilidade inerente para modelos bem treinados na execução dessas tarefas.

“Esta é uma lição que continuamos aprendendo no aprendizado profundo, que o volume ajuda surpreendentemente bastante em muitas tarefas”, disse Guy Gur-Ari, pesquisador que trabalhava no Google e é um dos coautores do artigo.

Os pesquisadores também descobriram maneiras de melhorar o desempenho do Minerva. Por exemplo, em uma técnica chamada “majority voting” (maioria absoluta), o Minerva resolveu o mesmo problema várias vezes, contabilizou os diferentes resultados e determinou como sua resposta final aquele que havia ocorrido na maioria das vezes (já que existe apenas uma resposta certa, mas inúmeras possíveis respostas erradas). Fazer isso aumentou sua pontuação em certos problemas de 33% para 50%.

Também foi importante ensinar o Minerva a explicar como chegou à solução dos problemas em etapas, um método conhecido como sugestão de cadeia de pensamento. Isso teve os mesmos benefícios para o Minerva que tem para os alunos: obrigou o modelo a desacelerar antes de dar uma resposta e permitiu que ele dedicasse mais tempo computacional a cada parte da tarefa.

“Se você pedir a um modelo de linguagem para explicar passo a passo, a precisão aumenta imensamente”, disse Gadgil.

Uma ponte necessária

Embora impressionante, o trabalho do Minerva chega com uma ressalva fundamental, que também foi reconhecida pelos autores: o Minerva não tem como verificar automaticamente se respondeu de forma correta a uma pergunta. E mesmo que tenha respondido a uma pergunta corretamente, não consegue verificar se os passos seguidos para chegar até ela são válidos.

“Ele às vezes apresenta falsos positivos, dando razões capciosas para respostas corretas”, disse Gadgil.

Em outras palavras, o Minerva pode mostrar seu trabalho, mas não pode verificá-lo, o que significa que depende do feedback humano para melhorar – um processo lento que talvez limite o quanto ele possa ser aprimorado.

“Realmente duvido que essa metodologia possa ser ampliada para problemas complexos”, disse Christian Szegedy, pesquisador de IA do Google e coautor do artigo anterior.

Em vez disso, os pesquisadores por trás de ambos os artigos esperam começar a ensinar matemática às máquinas usando as mesmas técnicas que permitiram a elas serem boas em jogos. O mundo está repleto de problemas de matemática, que poderiam funcionar como material de treinamento para sistemas como o Minerva, mas o Minerva não consegue reconhecer uma “boa” jogada em matemática do jeito que o AlphaGo faz quando está jogando bem Go.

“Por um lado, se você trabalha com linguagem natural ou com o tipo de raciocínio do Minerva, há muitos dados disponíveis por aí, toda a internet da matemática, mas, resumindo, você não consegue fazer o aprendizado por reforço com isso”, disse Wu. Por outro lado, “os assistentes de prova oferecem um ambiente fundamentado, porém têm poucos dados para serem treinados. Precisamos de uma espécie de ponte para ir de um lado ao outro.”

A autoformalização é essa ponte. As melhorias na autoformalização poderiam ajudar os matemáticos a automatizar aspectos da forma como eles escrevem provas e verificam se o trabalho deles está correto.

Ao combinar os avanços dos dois artigos, sistemas como o Minerva poderiam primeiro autoformalizar os problemas de matemática em linguagem natural, depois resolvê-los e verificar seu trabalho usando um assistente de prova como o Isabelle/HOL. Essa verificação instantânea ofereceria o feedback necessário para o aprendizado por reforço, permitindo a esses programas aprender com seus erros. Por fim, eles chegariam a uma resposta comprovadamente correta, com uma lista de etapas lógicas – combinando na prática o poder dos LLMs e do aprendizado por reforço.

Os pesquisadores de IA têm objetivos ainda maiores em mente. Eles veem a matemática como o campo de provas perfeito para desenvolver as habilidades de raciocínio da IA, porque ela é possivelmente a tarefa de raciocínio mais difícil de todas. Se uma máquina pode raciocinar de forma eficaz sobre matemática, segundo essa visão, ela deve naturalmente adquirir outras habilidades, como a capacidade de escrever código de computação ou dar diagnósticos médicos – e talvez até mesmo acabar com aquelas informações inconsistentes em uma história de unicórnios. /TRADUÇÃO ROMINA CÁCIA

História original republicada com permissão da Quanta Magazine, uma publicação editorialmente independente apoiada pela Simons Foundation. Leia o conteúdo original em To Teach Computers Math, Researchers Merge AI Approaches.

QUANTA MAGAZINE - O mundo aprendeu duas coisas nos últimos meses sobre os modelos de linguagem ampla (LLMs) – os mecanismos de inteligência artificial (IA) por trás de programas como o ChatGPT e Dall-E. A primeira é que esses modelos parecem ter a inteligência e a criatividade de um ser humano. Eles dão respostas detalhadas e claras para as perguntas feitas ou criam imagens fascinantes com apenas algumas palavras.

A segunda é que eles não são confiáveis. Às vezes fazem afirmações ilógicas ou declaram sem titubear mentiras como se fossem fatos.

“Eles falam de unicórnios, mas depois esquecem que há apenas um único chifre, ou contam uma história e depois mudam as informações ao longo dela”, disse Jason Rute, da IBM Research.

Isso é mais do que apenas um bug – pois comprova como os LLMs têm dificuldade para reconhecer seus erros, o que limita seu desempenho. O problema não é inerente aos sistemas de inteligência artificial. Os modelos de aprendizado de máquina se baseiam em uma técnica chamada aprendizado por reforço que permite aos computadores aprender com seus erros para se tornarem prodígios em jogos como xadrez e GO. Embora esses modelos costumem ser mais limitados em suas habilidades, eles demonstram um tipo de aprendizado que o LLMs ainda não dominam.

“Não queremos criar um modelo de linguagem que apenas converse como um ser humano”, disse Yuhuai (Tony) Wu, da Google AI. “Queremos que ele entenda do que está falando.”

Wu é coautor de dois artigos recentes que sugerem um caminho para conseguir isso. À primeira vista, eles falam de um uso muito específico: treinar sistemas de IA em matemática. O primeiro artigo descreve o treinamento de um LLM para traduzir afirmações matemáticas simples em códigos que um computador pode executar e verificar. O segundo treinou um LLM não apenas para entender problemas de matemática escritos em linguagem natural, mas para resolvê-los de verdade, usando um sistema chamado Minerva.

A tecnologia está crescendo em muitas direções diferentes, e todas elas podem trabalhar juntas

Siddhartha Gadgil, matemático do Instituto Indiano de Ciência em Bangalore

Juntos, os artigos sugerem a forma do modelo de IA do futuro, no qual os LLMs podem aprender a raciocinar por meio do pensamento matemático.

“Temos coisas como aprendizado profundo, aprendizado por reforço, AlphaGo e agora os modelos de linguagem”, disse Siddhartha Gadgil, matemático do Instituto Indiano de Ciência em Bangalore, que trabalha com sistemas matemáticos de IA. “A tecnologia está crescendo em muitas direções diferentes, e todas elas podem trabalhar juntas.”

Traduções não tão simples

Há décadas, os matemáticos traduzem provas em código de computação, um processo chamado formalização. O recurso é simples: se você escrever uma prova como código e um computador executá-lo sem erros, ela está correta. Mas formalizar uma única prova pode levar centenas ou milhares de horas.

Recentemente, Yuhuai (Tony) Wu foi coautor de dois artigos que ensinaram grandes modelos de linguagem a traduzir e resolver problemas matemáticos escritos em linguagem natural Foto: Christophe Testi/CreativeShot

Nos últimos cinco anos, pesquisadores de IA começaram a ensinar os LLMs a formalizar automaticamente, ou “autoformalizar”, afirmações matemáticas na “linguagem formal” do código de computação. Os LLMs já podem traduzir de um um idioma para outro, como do português para o inglês. Mas traduzir da matemática para o código de programação é um desafio mais difícil. Há bem menos traduções de exemplo para treinar um LLM, para começar, e as linguagens formais nem sempre contêm todo o vocabulário necessário.

“Quando você traduz a palavra ‘queijo’ do português para o inglês, existe uma palavra em inglês para queijo”, disse Rute. “O problema está na matemática, não existe nem mesmo o conceito certo na linguagem formal.”

É por isso que os sete autores do primeiro artigo, profissionais do mercado e da academia, escolheram autoformalizar afirmações matemáticas curtas em vez de provas inteiras. Os pesquisadores trabalharam principalmente com um LLM chamado Codex, que tem como base o GPT-3 (o primeiro “cérebro” do ChatGPT), mas com treinamento extra em material técnico de fontes como o GitHub. Para fazer o Codex entender matemática bem o suficiente para autoformalizar, os pesquisadores deram a ele apenas dois exemplos de problemas matemáticos em linguagem natural e as suas traduções formais em código.

Depois do breve tutorial, eles alimentaram o Codex com afirmações em linguagem natural de aproximadamente quatro mil problemas matemáticos de competições do ensino médio. A princípio, o desempenho dele pode parecer decepcionante: o Codex traduziu os problemas para a linguagem de um programa de matemática chamado Isabelle/HOL com uma taxa de precisão de pouco menos de 30%. Quando não conseguia fazer isso, inventava termos para preencher as lacunas com seu léxico de tradução.

“Às vezes, ele simplesmente não sabe a palavra que precisa saber – qual é o nome no Isabelle para ‘número primo’ ou o nome no Isabelle para “fatorial’ – e apenas inventa o termo, o que é o maior problema com esses modelos”, disse Rute. “Eles fazem suposições demais.”

Mas para os pesquisadores, o importante não era que o Codex havia falhado 70% das vezes, mas que tinha tido sucesso em 30% das vezes depois de ter acesso a um número tão limitado de exemplos.

“Eles conseguiram fazer todas essas tarefas diferentes com apenas algumas demonstrações”, disse Wenda Li, cientista da computação da Universidade de Cambridge e coautor do artigo.

Cientistas tentam ensinar matemática para sistemas de IA Foto: Valentin Tkach/Quanta Magazine

Li e os demais coautores do artigo veem o resultado como característico do tipo de habilidade latente que os LLMs podem adquirir com dados gerais de treinamento suficientes. Antes dessa pesquisa, o Codex nunca tinha tentado traduzir da linguagem natural para o código matemático formal. Mas o Codex estava familiarizado com o código devido ao seu treinamento com o material do GitHub e com a matemática em linguagem natural da internet. Para aproveitar essa base, os pesquisadores apenas tiveram que mostrar a ele alguns exemplos do que queriam e o Codex poderia começar a ligar os pontos.

“Em muitos aspectos, o que é surpreendente nesse artigo é que [os autores] não fizeram muito”, disse Rute. “Esses modelos tinham essa capacidade natural de fazer isso.”

Os pesquisadores observaram o mesmo acontecer quando tentaram ensinar os LLMs não apenas a como traduzir problemas de matemática, mas também resolvê-los.

A matemática do Minerva

O segundo artigo, apesar de independente do trabalho anterior com autoformalização, chegou a uma conclusão semelhante. A equipe de pesquisadores do Google treinou um LLM para responder, em detalhes, questões de matemática de uma competição para estudantes do ensino médio, como “uma reta paralela a y = 4x + 6 passa pelo ponto (5, 10). Qual é a coordenada y do ponto onde esta reta passa pelo eixo y?”.

Os autores começaram com um LLM chamado PaLM, que tinha sido treinado com conteúdo geral em linguagem natural, semelhante ao GPT-3. Então eles treinaram o LLM com material matemático de sites como o arxiv.org e outros materiais técnicos, simulando as origens do Codex. Eles chamaram esse modelo ampliado de Minerva.

Os pesquisadores mostraram ao Minerva quatro exemplos do que queriam. Neste caso, isso significou soluções passo a passo para problemas de matemática em linguagem natural.

Em seguida, eles testaram o modelo com várias questões de raciocínio quantitativo. O desempenho do Minerva variava de acordo com o assunto: ele respondia corretamente às perguntas um pouco mais que a metade das vezes para alguns assuntos (como álgebra) e um pouco menos que a metade das vezes para outros (como geometria).

Uma das preocupações dos autores – comum em muitas áreas da pesquisa em IA – era que o Minerva respondesse às questões corretamente apenas porque já tinha visto elas, ou outras semelhantes a elas, em seus dados de treinamento. Esse problema é chamado de “poluição” e dificulta saber se um modelo está mesmo resolvendo os problemas ou apenas copiando o trabalho de outra pessoa.

“Há tantos dados nesses modelos que, a não ser que você esteja tentando evitar colocar alguns dados no conjunto de treinamento, se for um problema padrão, é muito provável que já tenha sido visto”, disse Rute.

Jason Rute, cientista da computação da IBM Research, vê potencial em modelos de linguagem grandes, mas também conhece seus pontos fracos. "Eles fazem muitas suposições", disse ele Foto: IBM

Para se protegerem dessa possibilidade, os pesquisadores submeteram o Minerva ao Exame Nacional de Matemática de 2022 da Polônia, realizado depois dos dados de treinamento do Minerva terem sido definidos. O sistema acertou 65% das questões, uma pontuação aceitável para um estudante de carne e osso e particularmente boa para um LLM, disse Rute. Mais uma vez, os resultados positivos depois de tão poucos exemplos sugeriram uma habilidade inerente para modelos bem treinados na execução dessas tarefas.

“Esta é uma lição que continuamos aprendendo no aprendizado profundo, que o volume ajuda surpreendentemente bastante em muitas tarefas”, disse Guy Gur-Ari, pesquisador que trabalhava no Google e é um dos coautores do artigo.

Os pesquisadores também descobriram maneiras de melhorar o desempenho do Minerva. Por exemplo, em uma técnica chamada “majority voting” (maioria absoluta), o Minerva resolveu o mesmo problema várias vezes, contabilizou os diferentes resultados e determinou como sua resposta final aquele que havia ocorrido na maioria das vezes (já que existe apenas uma resposta certa, mas inúmeras possíveis respostas erradas). Fazer isso aumentou sua pontuação em certos problemas de 33% para 50%.

Também foi importante ensinar o Minerva a explicar como chegou à solução dos problemas em etapas, um método conhecido como sugestão de cadeia de pensamento. Isso teve os mesmos benefícios para o Minerva que tem para os alunos: obrigou o modelo a desacelerar antes de dar uma resposta e permitiu que ele dedicasse mais tempo computacional a cada parte da tarefa.

“Se você pedir a um modelo de linguagem para explicar passo a passo, a precisão aumenta imensamente”, disse Gadgil.

Uma ponte necessária

Embora impressionante, o trabalho do Minerva chega com uma ressalva fundamental, que também foi reconhecida pelos autores: o Minerva não tem como verificar automaticamente se respondeu de forma correta a uma pergunta. E mesmo que tenha respondido a uma pergunta corretamente, não consegue verificar se os passos seguidos para chegar até ela são válidos.

“Ele às vezes apresenta falsos positivos, dando razões capciosas para respostas corretas”, disse Gadgil.

Em outras palavras, o Minerva pode mostrar seu trabalho, mas não pode verificá-lo, o que significa que depende do feedback humano para melhorar – um processo lento que talvez limite o quanto ele possa ser aprimorado.

“Realmente duvido que essa metodologia possa ser ampliada para problemas complexos”, disse Christian Szegedy, pesquisador de IA do Google e coautor do artigo anterior.

Em vez disso, os pesquisadores por trás de ambos os artigos esperam começar a ensinar matemática às máquinas usando as mesmas técnicas que permitiram a elas serem boas em jogos. O mundo está repleto de problemas de matemática, que poderiam funcionar como material de treinamento para sistemas como o Minerva, mas o Minerva não consegue reconhecer uma “boa” jogada em matemática do jeito que o AlphaGo faz quando está jogando bem Go.

“Por um lado, se você trabalha com linguagem natural ou com o tipo de raciocínio do Minerva, há muitos dados disponíveis por aí, toda a internet da matemática, mas, resumindo, você não consegue fazer o aprendizado por reforço com isso”, disse Wu. Por outro lado, “os assistentes de prova oferecem um ambiente fundamentado, porém têm poucos dados para serem treinados. Precisamos de uma espécie de ponte para ir de um lado ao outro.”

A autoformalização é essa ponte. As melhorias na autoformalização poderiam ajudar os matemáticos a automatizar aspectos da forma como eles escrevem provas e verificam se o trabalho deles está correto.

Ao combinar os avanços dos dois artigos, sistemas como o Minerva poderiam primeiro autoformalizar os problemas de matemática em linguagem natural, depois resolvê-los e verificar seu trabalho usando um assistente de prova como o Isabelle/HOL. Essa verificação instantânea ofereceria o feedback necessário para o aprendizado por reforço, permitindo a esses programas aprender com seus erros. Por fim, eles chegariam a uma resposta comprovadamente correta, com uma lista de etapas lógicas – combinando na prática o poder dos LLMs e do aprendizado por reforço.

Os pesquisadores de IA têm objetivos ainda maiores em mente. Eles veem a matemática como o campo de provas perfeito para desenvolver as habilidades de raciocínio da IA, porque ela é possivelmente a tarefa de raciocínio mais difícil de todas. Se uma máquina pode raciocinar de forma eficaz sobre matemática, segundo essa visão, ela deve naturalmente adquirir outras habilidades, como a capacidade de escrever código de computação ou dar diagnósticos médicos – e talvez até mesmo acabar com aquelas informações inconsistentes em uma história de unicórnios. /TRADUÇÃO ROMINA CÁCIA

História original republicada com permissão da Quanta Magazine, uma publicação editorialmente independente apoiada pela Simons Foundation. Leia o conteúdo original em To Teach Computers Math, Researchers Merge AI Approaches.

QUANTA MAGAZINE - O mundo aprendeu duas coisas nos últimos meses sobre os modelos de linguagem ampla (LLMs) – os mecanismos de inteligência artificial (IA) por trás de programas como o ChatGPT e Dall-E. A primeira é que esses modelos parecem ter a inteligência e a criatividade de um ser humano. Eles dão respostas detalhadas e claras para as perguntas feitas ou criam imagens fascinantes com apenas algumas palavras.

A segunda é que eles não são confiáveis. Às vezes fazem afirmações ilógicas ou declaram sem titubear mentiras como se fossem fatos.

“Eles falam de unicórnios, mas depois esquecem que há apenas um único chifre, ou contam uma história e depois mudam as informações ao longo dela”, disse Jason Rute, da IBM Research.

Isso é mais do que apenas um bug – pois comprova como os LLMs têm dificuldade para reconhecer seus erros, o que limita seu desempenho. O problema não é inerente aos sistemas de inteligência artificial. Os modelos de aprendizado de máquina se baseiam em uma técnica chamada aprendizado por reforço que permite aos computadores aprender com seus erros para se tornarem prodígios em jogos como xadrez e GO. Embora esses modelos costumem ser mais limitados em suas habilidades, eles demonstram um tipo de aprendizado que o LLMs ainda não dominam.

“Não queremos criar um modelo de linguagem que apenas converse como um ser humano”, disse Yuhuai (Tony) Wu, da Google AI. “Queremos que ele entenda do que está falando.”

Wu é coautor de dois artigos recentes que sugerem um caminho para conseguir isso. À primeira vista, eles falam de um uso muito específico: treinar sistemas de IA em matemática. O primeiro artigo descreve o treinamento de um LLM para traduzir afirmações matemáticas simples em códigos que um computador pode executar e verificar. O segundo treinou um LLM não apenas para entender problemas de matemática escritos em linguagem natural, mas para resolvê-los de verdade, usando um sistema chamado Minerva.

A tecnologia está crescendo em muitas direções diferentes, e todas elas podem trabalhar juntas

Siddhartha Gadgil, matemático do Instituto Indiano de Ciência em Bangalore

Juntos, os artigos sugerem a forma do modelo de IA do futuro, no qual os LLMs podem aprender a raciocinar por meio do pensamento matemático.

“Temos coisas como aprendizado profundo, aprendizado por reforço, AlphaGo e agora os modelos de linguagem”, disse Siddhartha Gadgil, matemático do Instituto Indiano de Ciência em Bangalore, que trabalha com sistemas matemáticos de IA. “A tecnologia está crescendo em muitas direções diferentes, e todas elas podem trabalhar juntas.”

Traduções não tão simples

Há décadas, os matemáticos traduzem provas em código de computação, um processo chamado formalização. O recurso é simples: se você escrever uma prova como código e um computador executá-lo sem erros, ela está correta. Mas formalizar uma única prova pode levar centenas ou milhares de horas.

Recentemente, Yuhuai (Tony) Wu foi coautor de dois artigos que ensinaram grandes modelos de linguagem a traduzir e resolver problemas matemáticos escritos em linguagem natural Foto: Christophe Testi/CreativeShot

Nos últimos cinco anos, pesquisadores de IA começaram a ensinar os LLMs a formalizar automaticamente, ou “autoformalizar”, afirmações matemáticas na “linguagem formal” do código de computação. Os LLMs já podem traduzir de um um idioma para outro, como do português para o inglês. Mas traduzir da matemática para o código de programação é um desafio mais difícil. Há bem menos traduções de exemplo para treinar um LLM, para começar, e as linguagens formais nem sempre contêm todo o vocabulário necessário.

“Quando você traduz a palavra ‘queijo’ do português para o inglês, existe uma palavra em inglês para queijo”, disse Rute. “O problema está na matemática, não existe nem mesmo o conceito certo na linguagem formal.”

É por isso que os sete autores do primeiro artigo, profissionais do mercado e da academia, escolheram autoformalizar afirmações matemáticas curtas em vez de provas inteiras. Os pesquisadores trabalharam principalmente com um LLM chamado Codex, que tem como base o GPT-3 (o primeiro “cérebro” do ChatGPT), mas com treinamento extra em material técnico de fontes como o GitHub. Para fazer o Codex entender matemática bem o suficiente para autoformalizar, os pesquisadores deram a ele apenas dois exemplos de problemas matemáticos em linguagem natural e as suas traduções formais em código.

Depois do breve tutorial, eles alimentaram o Codex com afirmações em linguagem natural de aproximadamente quatro mil problemas matemáticos de competições do ensino médio. A princípio, o desempenho dele pode parecer decepcionante: o Codex traduziu os problemas para a linguagem de um programa de matemática chamado Isabelle/HOL com uma taxa de precisão de pouco menos de 30%. Quando não conseguia fazer isso, inventava termos para preencher as lacunas com seu léxico de tradução.

“Às vezes, ele simplesmente não sabe a palavra que precisa saber – qual é o nome no Isabelle para ‘número primo’ ou o nome no Isabelle para “fatorial’ – e apenas inventa o termo, o que é o maior problema com esses modelos”, disse Rute. “Eles fazem suposições demais.”

Mas para os pesquisadores, o importante não era que o Codex havia falhado 70% das vezes, mas que tinha tido sucesso em 30% das vezes depois de ter acesso a um número tão limitado de exemplos.

“Eles conseguiram fazer todas essas tarefas diferentes com apenas algumas demonstrações”, disse Wenda Li, cientista da computação da Universidade de Cambridge e coautor do artigo.

Cientistas tentam ensinar matemática para sistemas de IA Foto: Valentin Tkach/Quanta Magazine

Li e os demais coautores do artigo veem o resultado como característico do tipo de habilidade latente que os LLMs podem adquirir com dados gerais de treinamento suficientes. Antes dessa pesquisa, o Codex nunca tinha tentado traduzir da linguagem natural para o código matemático formal. Mas o Codex estava familiarizado com o código devido ao seu treinamento com o material do GitHub e com a matemática em linguagem natural da internet. Para aproveitar essa base, os pesquisadores apenas tiveram que mostrar a ele alguns exemplos do que queriam e o Codex poderia começar a ligar os pontos.

“Em muitos aspectos, o que é surpreendente nesse artigo é que [os autores] não fizeram muito”, disse Rute. “Esses modelos tinham essa capacidade natural de fazer isso.”

Os pesquisadores observaram o mesmo acontecer quando tentaram ensinar os LLMs não apenas a como traduzir problemas de matemática, mas também resolvê-los.

A matemática do Minerva

O segundo artigo, apesar de independente do trabalho anterior com autoformalização, chegou a uma conclusão semelhante. A equipe de pesquisadores do Google treinou um LLM para responder, em detalhes, questões de matemática de uma competição para estudantes do ensino médio, como “uma reta paralela a y = 4x + 6 passa pelo ponto (5, 10). Qual é a coordenada y do ponto onde esta reta passa pelo eixo y?”.

Os autores começaram com um LLM chamado PaLM, que tinha sido treinado com conteúdo geral em linguagem natural, semelhante ao GPT-3. Então eles treinaram o LLM com material matemático de sites como o arxiv.org e outros materiais técnicos, simulando as origens do Codex. Eles chamaram esse modelo ampliado de Minerva.

Os pesquisadores mostraram ao Minerva quatro exemplos do que queriam. Neste caso, isso significou soluções passo a passo para problemas de matemática em linguagem natural.

Em seguida, eles testaram o modelo com várias questões de raciocínio quantitativo. O desempenho do Minerva variava de acordo com o assunto: ele respondia corretamente às perguntas um pouco mais que a metade das vezes para alguns assuntos (como álgebra) e um pouco menos que a metade das vezes para outros (como geometria).

Uma das preocupações dos autores – comum em muitas áreas da pesquisa em IA – era que o Minerva respondesse às questões corretamente apenas porque já tinha visto elas, ou outras semelhantes a elas, em seus dados de treinamento. Esse problema é chamado de “poluição” e dificulta saber se um modelo está mesmo resolvendo os problemas ou apenas copiando o trabalho de outra pessoa.

“Há tantos dados nesses modelos que, a não ser que você esteja tentando evitar colocar alguns dados no conjunto de treinamento, se for um problema padrão, é muito provável que já tenha sido visto”, disse Rute.

Jason Rute, cientista da computação da IBM Research, vê potencial em modelos de linguagem grandes, mas também conhece seus pontos fracos. "Eles fazem muitas suposições", disse ele Foto: IBM

Para se protegerem dessa possibilidade, os pesquisadores submeteram o Minerva ao Exame Nacional de Matemática de 2022 da Polônia, realizado depois dos dados de treinamento do Minerva terem sido definidos. O sistema acertou 65% das questões, uma pontuação aceitável para um estudante de carne e osso e particularmente boa para um LLM, disse Rute. Mais uma vez, os resultados positivos depois de tão poucos exemplos sugeriram uma habilidade inerente para modelos bem treinados na execução dessas tarefas.

“Esta é uma lição que continuamos aprendendo no aprendizado profundo, que o volume ajuda surpreendentemente bastante em muitas tarefas”, disse Guy Gur-Ari, pesquisador que trabalhava no Google e é um dos coautores do artigo.

Os pesquisadores também descobriram maneiras de melhorar o desempenho do Minerva. Por exemplo, em uma técnica chamada “majority voting” (maioria absoluta), o Minerva resolveu o mesmo problema várias vezes, contabilizou os diferentes resultados e determinou como sua resposta final aquele que havia ocorrido na maioria das vezes (já que existe apenas uma resposta certa, mas inúmeras possíveis respostas erradas). Fazer isso aumentou sua pontuação em certos problemas de 33% para 50%.

Também foi importante ensinar o Minerva a explicar como chegou à solução dos problemas em etapas, um método conhecido como sugestão de cadeia de pensamento. Isso teve os mesmos benefícios para o Minerva que tem para os alunos: obrigou o modelo a desacelerar antes de dar uma resposta e permitiu que ele dedicasse mais tempo computacional a cada parte da tarefa.

“Se você pedir a um modelo de linguagem para explicar passo a passo, a precisão aumenta imensamente”, disse Gadgil.

Uma ponte necessária

Embora impressionante, o trabalho do Minerva chega com uma ressalva fundamental, que também foi reconhecida pelos autores: o Minerva não tem como verificar automaticamente se respondeu de forma correta a uma pergunta. E mesmo que tenha respondido a uma pergunta corretamente, não consegue verificar se os passos seguidos para chegar até ela são válidos.

“Ele às vezes apresenta falsos positivos, dando razões capciosas para respostas corretas”, disse Gadgil.

Em outras palavras, o Minerva pode mostrar seu trabalho, mas não pode verificá-lo, o que significa que depende do feedback humano para melhorar – um processo lento que talvez limite o quanto ele possa ser aprimorado.

“Realmente duvido que essa metodologia possa ser ampliada para problemas complexos”, disse Christian Szegedy, pesquisador de IA do Google e coautor do artigo anterior.

Em vez disso, os pesquisadores por trás de ambos os artigos esperam começar a ensinar matemática às máquinas usando as mesmas técnicas que permitiram a elas serem boas em jogos. O mundo está repleto de problemas de matemática, que poderiam funcionar como material de treinamento para sistemas como o Minerva, mas o Minerva não consegue reconhecer uma “boa” jogada em matemática do jeito que o AlphaGo faz quando está jogando bem Go.

“Por um lado, se você trabalha com linguagem natural ou com o tipo de raciocínio do Minerva, há muitos dados disponíveis por aí, toda a internet da matemática, mas, resumindo, você não consegue fazer o aprendizado por reforço com isso”, disse Wu. Por outro lado, “os assistentes de prova oferecem um ambiente fundamentado, porém têm poucos dados para serem treinados. Precisamos de uma espécie de ponte para ir de um lado ao outro.”

A autoformalização é essa ponte. As melhorias na autoformalização poderiam ajudar os matemáticos a automatizar aspectos da forma como eles escrevem provas e verificam se o trabalho deles está correto.

Ao combinar os avanços dos dois artigos, sistemas como o Minerva poderiam primeiro autoformalizar os problemas de matemática em linguagem natural, depois resolvê-los e verificar seu trabalho usando um assistente de prova como o Isabelle/HOL. Essa verificação instantânea ofereceria o feedback necessário para o aprendizado por reforço, permitindo a esses programas aprender com seus erros. Por fim, eles chegariam a uma resposta comprovadamente correta, com uma lista de etapas lógicas – combinando na prática o poder dos LLMs e do aprendizado por reforço.

Os pesquisadores de IA têm objetivos ainda maiores em mente. Eles veem a matemática como o campo de provas perfeito para desenvolver as habilidades de raciocínio da IA, porque ela é possivelmente a tarefa de raciocínio mais difícil de todas. Se uma máquina pode raciocinar de forma eficaz sobre matemática, segundo essa visão, ela deve naturalmente adquirir outras habilidades, como a capacidade de escrever código de computação ou dar diagnósticos médicos – e talvez até mesmo acabar com aquelas informações inconsistentes em uma história de unicórnios. /TRADUÇÃO ROMINA CÁCIA

História original republicada com permissão da Quanta Magazine, uma publicação editorialmente independente apoiada pela Simons Foundation. Leia o conteúdo original em To Teach Computers Math, Researchers Merge AI Approaches.

QUANTA MAGAZINE - O mundo aprendeu duas coisas nos últimos meses sobre os modelos de linguagem ampla (LLMs) – os mecanismos de inteligência artificial (IA) por trás de programas como o ChatGPT e Dall-E. A primeira é que esses modelos parecem ter a inteligência e a criatividade de um ser humano. Eles dão respostas detalhadas e claras para as perguntas feitas ou criam imagens fascinantes com apenas algumas palavras.

A segunda é que eles não são confiáveis. Às vezes fazem afirmações ilógicas ou declaram sem titubear mentiras como se fossem fatos.

“Eles falam de unicórnios, mas depois esquecem que há apenas um único chifre, ou contam uma história e depois mudam as informações ao longo dela”, disse Jason Rute, da IBM Research.

Isso é mais do que apenas um bug – pois comprova como os LLMs têm dificuldade para reconhecer seus erros, o que limita seu desempenho. O problema não é inerente aos sistemas de inteligência artificial. Os modelos de aprendizado de máquina se baseiam em uma técnica chamada aprendizado por reforço que permite aos computadores aprender com seus erros para se tornarem prodígios em jogos como xadrez e GO. Embora esses modelos costumem ser mais limitados em suas habilidades, eles demonstram um tipo de aprendizado que o LLMs ainda não dominam.

“Não queremos criar um modelo de linguagem que apenas converse como um ser humano”, disse Yuhuai (Tony) Wu, da Google AI. “Queremos que ele entenda do que está falando.”

Wu é coautor de dois artigos recentes que sugerem um caminho para conseguir isso. À primeira vista, eles falam de um uso muito específico: treinar sistemas de IA em matemática. O primeiro artigo descreve o treinamento de um LLM para traduzir afirmações matemáticas simples em códigos que um computador pode executar e verificar. O segundo treinou um LLM não apenas para entender problemas de matemática escritos em linguagem natural, mas para resolvê-los de verdade, usando um sistema chamado Minerva.

A tecnologia está crescendo em muitas direções diferentes, e todas elas podem trabalhar juntas

Siddhartha Gadgil, matemático do Instituto Indiano de Ciência em Bangalore

Juntos, os artigos sugerem a forma do modelo de IA do futuro, no qual os LLMs podem aprender a raciocinar por meio do pensamento matemático.

“Temos coisas como aprendizado profundo, aprendizado por reforço, AlphaGo e agora os modelos de linguagem”, disse Siddhartha Gadgil, matemático do Instituto Indiano de Ciência em Bangalore, que trabalha com sistemas matemáticos de IA. “A tecnologia está crescendo em muitas direções diferentes, e todas elas podem trabalhar juntas.”

Traduções não tão simples

Há décadas, os matemáticos traduzem provas em código de computação, um processo chamado formalização. O recurso é simples: se você escrever uma prova como código e um computador executá-lo sem erros, ela está correta. Mas formalizar uma única prova pode levar centenas ou milhares de horas.

Recentemente, Yuhuai (Tony) Wu foi coautor de dois artigos que ensinaram grandes modelos de linguagem a traduzir e resolver problemas matemáticos escritos em linguagem natural Foto: Christophe Testi/CreativeShot

Nos últimos cinco anos, pesquisadores de IA começaram a ensinar os LLMs a formalizar automaticamente, ou “autoformalizar”, afirmações matemáticas na “linguagem formal” do código de computação. Os LLMs já podem traduzir de um um idioma para outro, como do português para o inglês. Mas traduzir da matemática para o código de programação é um desafio mais difícil. Há bem menos traduções de exemplo para treinar um LLM, para começar, e as linguagens formais nem sempre contêm todo o vocabulário necessário.

“Quando você traduz a palavra ‘queijo’ do português para o inglês, existe uma palavra em inglês para queijo”, disse Rute. “O problema está na matemática, não existe nem mesmo o conceito certo na linguagem formal.”

É por isso que os sete autores do primeiro artigo, profissionais do mercado e da academia, escolheram autoformalizar afirmações matemáticas curtas em vez de provas inteiras. Os pesquisadores trabalharam principalmente com um LLM chamado Codex, que tem como base o GPT-3 (o primeiro “cérebro” do ChatGPT), mas com treinamento extra em material técnico de fontes como o GitHub. Para fazer o Codex entender matemática bem o suficiente para autoformalizar, os pesquisadores deram a ele apenas dois exemplos de problemas matemáticos em linguagem natural e as suas traduções formais em código.

Depois do breve tutorial, eles alimentaram o Codex com afirmações em linguagem natural de aproximadamente quatro mil problemas matemáticos de competições do ensino médio. A princípio, o desempenho dele pode parecer decepcionante: o Codex traduziu os problemas para a linguagem de um programa de matemática chamado Isabelle/HOL com uma taxa de precisão de pouco menos de 30%. Quando não conseguia fazer isso, inventava termos para preencher as lacunas com seu léxico de tradução.

“Às vezes, ele simplesmente não sabe a palavra que precisa saber – qual é o nome no Isabelle para ‘número primo’ ou o nome no Isabelle para “fatorial’ – e apenas inventa o termo, o que é o maior problema com esses modelos”, disse Rute. “Eles fazem suposições demais.”

Mas para os pesquisadores, o importante não era que o Codex havia falhado 70% das vezes, mas que tinha tido sucesso em 30% das vezes depois de ter acesso a um número tão limitado de exemplos.

“Eles conseguiram fazer todas essas tarefas diferentes com apenas algumas demonstrações”, disse Wenda Li, cientista da computação da Universidade de Cambridge e coautor do artigo.

Cientistas tentam ensinar matemática para sistemas de IA Foto: Valentin Tkach/Quanta Magazine

Li e os demais coautores do artigo veem o resultado como característico do tipo de habilidade latente que os LLMs podem adquirir com dados gerais de treinamento suficientes. Antes dessa pesquisa, o Codex nunca tinha tentado traduzir da linguagem natural para o código matemático formal. Mas o Codex estava familiarizado com o código devido ao seu treinamento com o material do GitHub e com a matemática em linguagem natural da internet. Para aproveitar essa base, os pesquisadores apenas tiveram que mostrar a ele alguns exemplos do que queriam e o Codex poderia começar a ligar os pontos.

“Em muitos aspectos, o que é surpreendente nesse artigo é que [os autores] não fizeram muito”, disse Rute. “Esses modelos tinham essa capacidade natural de fazer isso.”

Os pesquisadores observaram o mesmo acontecer quando tentaram ensinar os LLMs não apenas a como traduzir problemas de matemática, mas também resolvê-los.

A matemática do Minerva

O segundo artigo, apesar de independente do trabalho anterior com autoformalização, chegou a uma conclusão semelhante. A equipe de pesquisadores do Google treinou um LLM para responder, em detalhes, questões de matemática de uma competição para estudantes do ensino médio, como “uma reta paralela a y = 4x + 6 passa pelo ponto (5, 10). Qual é a coordenada y do ponto onde esta reta passa pelo eixo y?”.

Os autores começaram com um LLM chamado PaLM, que tinha sido treinado com conteúdo geral em linguagem natural, semelhante ao GPT-3. Então eles treinaram o LLM com material matemático de sites como o arxiv.org e outros materiais técnicos, simulando as origens do Codex. Eles chamaram esse modelo ampliado de Minerva.

Os pesquisadores mostraram ao Minerva quatro exemplos do que queriam. Neste caso, isso significou soluções passo a passo para problemas de matemática em linguagem natural.

Em seguida, eles testaram o modelo com várias questões de raciocínio quantitativo. O desempenho do Minerva variava de acordo com o assunto: ele respondia corretamente às perguntas um pouco mais que a metade das vezes para alguns assuntos (como álgebra) e um pouco menos que a metade das vezes para outros (como geometria).

Uma das preocupações dos autores – comum em muitas áreas da pesquisa em IA – era que o Minerva respondesse às questões corretamente apenas porque já tinha visto elas, ou outras semelhantes a elas, em seus dados de treinamento. Esse problema é chamado de “poluição” e dificulta saber se um modelo está mesmo resolvendo os problemas ou apenas copiando o trabalho de outra pessoa.

“Há tantos dados nesses modelos que, a não ser que você esteja tentando evitar colocar alguns dados no conjunto de treinamento, se for um problema padrão, é muito provável que já tenha sido visto”, disse Rute.

Jason Rute, cientista da computação da IBM Research, vê potencial em modelos de linguagem grandes, mas também conhece seus pontos fracos. "Eles fazem muitas suposições", disse ele Foto: IBM

Para se protegerem dessa possibilidade, os pesquisadores submeteram o Minerva ao Exame Nacional de Matemática de 2022 da Polônia, realizado depois dos dados de treinamento do Minerva terem sido definidos. O sistema acertou 65% das questões, uma pontuação aceitável para um estudante de carne e osso e particularmente boa para um LLM, disse Rute. Mais uma vez, os resultados positivos depois de tão poucos exemplos sugeriram uma habilidade inerente para modelos bem treinados na execução dessas tarefas.

“Esta é uma lição que continuamos aprendendo no aprendizado profundo, que o volume ajuda surpreendentemente bastante em muitas tarefas”, disse Guy Gur-Ari, pesquisador que trabalhava no Google e é um dos coautores do artigo.

Os pesquisadores também descobriram maneiras de melhorar o desempenho do Minerva. Por exemplo, em uma técnica chamada “majority voting” (maioria absoluta), o Minerva resolveu o mesmo problema várias vezes, contabilizou os diferentes resultados e determinou como sua resposta final aquele que havia ocorrido na maioria das vezes (já que existe apenas uma resposta certa, mas inúmeras possíveis respostas erradas). Fazer isso aumentou sua pontuação em certos problemas de 33% para 50%.

Também foi importante ensinar o Minerva a explicar como chegou à solução dos problemas em etapas, um método conhecido como sugestão de cadeia de pensamento. Isso teve os mesmos benefícios para o Minerva que tem para os alunos: obrigou o modelo a desacelerar antes de dar uma resposta e permitiu que ele dedicasse mais tempo computacional a cada parte da tarefa.

“Se você pedir a um modelo de linguagem para explicar passo a passo, a precisão aumenta imensamente”, disse Gadgil.

Uma ponte necessária

Embora impressionante, o trabalho do Minerva chega com uma ressalva fundamental, que também foi reconhecida pelos autores: o Minerva não tem como verificar automaticamente se respondeu de forma correta a uma pergunta. E mesmo que tenha respondido a uma pergunta corretamente, não consegue verificar se os passos seguidos para chegar até ela são válidos.

“Ele às vezes apresenta falsos positivos, dando razões capciosas para respostas corretas”, disse Gadgil.

Em outras palavras, o Minerva pode mostrar seu trabalho, mas não pode verificá-lo, o que significa que depende do feedback humano para melhorar – um processo lento que talvez limite o quanto ele possa ser aprimorado.

“Realmente duvido que essa metodologia possa ser ampliada para problemas complexos”, disse Christian Szegedy, pesquisador de IA do Google e coautor do artigo anterior.

Em vez disso, os pesquisadores por trás de ambos os artigos esperam começar a ensinar matemática às máquinas usando as mesmas técnicas que permitiram a elas serem boas em jogos. O mundo está repleto de problemas de matemática, que poderiam funcionar como material de treinamento para sistemas como o Minerva, mas o Minerva não consegue reconhecer uma “boa” jogada em matemática do jeito que o AlphaGo faz quando está jogando bem Go.

“Por um lado, se você trabalha com linguagem natural ou com o tipo de raciocínio do Minerva, há muitos dados disponíveis por aí, toda a internet da matemática, mas, resumindo, você não consegue fazer o aprendizado por reforço com isso”, disse Wu. Por outro lado, “os assistentes de prova oferecem um ambiente fundamentado, porém têm poucos dados para serem treinados. Precisamos de uma espécie de ponte para ir de um lado ao outro.”

A autoformalização é essa ponte. As melhorias na autoformalização poderiam ajudar os matemáticos a automatizar aspectos da forma como eles escrevem provas e verificam se o trabalho deles está correto.

Ao combinar os avanços dos dois artigos, sistemas como o Minerva poderiam primeiro autoformalizar os problemas de matemática em linguagem natural, depois resolvê-los e verificar seu trabalho usando um assistente de prova como o Isabelle/HOL. Essa verificação instantânea ofereceria o feedback necessário para o aprendizado por reforço, permitindo a esses programas aprender com seus erros. Por fim, eles chegariam a uma resposta comprovadamente correta, com uma lista de etapas lógicas – combinando na prática o poder dos LLMs e do aprendizado por reforço.

Os pesquisadores de IA têm objetivos ainda maiores em mente. Eles veem a matemática como o campo de provas perfeito para desenvolver as habilidades de raciocínio da IA, porque ela é possivelmente a tarefa de raciocínio mais difícil de todas. Se uma máquina pode raciocinar de forma eficaz sobre matemática, segundo essa visão, ela deve naturalmente adquirir outras habilidades, como a capacidade de escrever código de computação ou dar diagnósticos médicos – e talvez até mesmo acabar com aquelas informações inconsistentes em uma história de unicórnios. /TRADUÇÃO ROMINA CÁCIA

História original republicada com permissão da Quanta Magazine, uma publicação editorialmente independente apoiada pela Simons Foundation. Leia o conteúdo original em To Teach Computers Math, Researchers Merge AI Approaches.

QUANTA MAGAZINE - O mundo aprendeu duas coisas nos últimos meses sobre os modelos de linguagem ampla (LLMs) – os mecanismos de inteligência artificial (IA) por trás de programas como o ChatGPT e Dall-E. A primeira é que esses modelos parecem ter a inteligência e a criatividade de um ser humano. Eles dão respostas detalhadas e claras para as perguntas feitas ou criam imagens fascinantes com apenas algumas palavras.

A segunda é que eles não são confiáveis. Às vezes fazem afirmações ilógicas ou declaram sem titubear mentiras como se fossem fatos.

“Eles falam de unicórnios, mas depois esquecem que há apenas um único chifre, ou contam uma história e depois mudam as informações ao longo dela”, disse Jason Rute, da IBM Research.

Isso é mais do que apenas um bug – pois comprova como os LLMs têm dificuldade para reconhecer seus erros, o que limita seu desempenho. O problema não é inerente aos sistemas de inteligência artificial. Os modelos de aprendizado de máquina se baseiam em uma técnica chamada aprendizado por reforço que permite aos computadores aprender com seus erros para se tornarem prodígios em jogos como xadrez e GO. Embora esses modelos costumem ser mais limitados em suas habilidades, eles demonstram um tipo de aprendizado que o LLMs ainda não dominam.

“Não queremos criar um modelo de linguagem que apenas converse como um ser humano”, disse Yuhuai (Tony) Wu, da Google AI. “Queremos que ele entenda do que está falando.”

Wu é coautor de dois artigos recentes que sugerem um caminho para conseguir isso. À primeira vista, eles falam de um uso muito específico: treinar sistemas de IA em matemática. O primeiro artigo descreve o treinamento de um LLM para traduzir afirmações matemáticas simples em códigos que um computador pode executar e verificar. O segundo treinou um LLM não apenas para entender problemas de matemática escritos em linguagem natural, mas para resolvê-los de verdade, usando um sistema chamado Minerva.

A tecnologia está crescendo em muitas direções diferentes, e todas elas podem trabalhar juntas

Siddhartha Gadgil, matemático do Instituto Indiano de Ciência em Bangalore

Juntos, os artigos sugerem a forma do modelo de IA do futuro, no qual os LLMs podem aprender a raciocinar por meio do pensamento matemático.

“Temos coisas como aprendizado profundo, aprendizado por reforço, AlphaGo e agora os modelos de linguagem”, disse Siddhartha Gadgil, matemático do Instituto Indiano de Ciência em Bangalore, que trabalha com sistemas matemáticos de IA. “A tecnologia está crescendo em muitas direções diferentes, e todas elas podem trabalhar juntas.”

Traduções não tão simples

Há décadas, os matemáticos traduzem provas em código de computação, um processo chamado formalização. O recurso é simples: se você escrever uma prova como código e um computador executá-lo sem erros, ela está correta. Mas formalizar uma única prova pode levar centenas ou milhares de horas.

Recentemente, Yuhuai (Tony) Wu foi coautor de dois artigos que ensinaram grandes modelos de linguagem a traduzir e resolver problemas matemáticos escritos em linguagem natural Foto: Christophe Testi/CreativeShot

Nos últimos cinco anos, pesquisadores de IA começaram a ensinar os LLMs a formalizar automaticamente, ou “autoformalizar”, afirmações matemáticas na “linguagem formal” do código de computação. Os LLMs já podem traduzir de um um idioma para outro, como do português para o inglês. Mas traduzir da matemática para o código de programação é um desafio mais difícil. Há bem menos traduções de exemplo para treinar um LLM, para começar, e as linguagens formais nem sempre contêm todo o vocabulário necessário.

“Quando você traduz a palavra ‘queijo’ do português para o inglês, existe uma palavra em inglês para queijo”, disse Rute. “O problema está na matemática, não existe nem mesmo o conceito certo na linguagem formal.”

É por isso que os sete autores do primeiro artigo, profissionais do mercado e da academia, escolheram autoformalizar afirmações matemáticas curtas em vez de provas inteiras. Os pesquisadores trabalharam principalmente com um LLM chamado Codex, que tem como base o GPT-3 (o primeiro “cérebro” do ChatGPT), mas com treinamento extra em material técnico de fontes como o GitHub. Para fazer o Codex entender matemática bem o suficiente para autoformalizar, os pesquisadores deram a ele apenas dois exemplos de problemas matemáticos em linguagem natural e as suas traduções formais em código.

Depois do breve tutorial, eles alimentaram o Codex com afirmações em linguagem natural de aproximadamente quatro mil problemas matemáticos de competições do ensino médio. A princípio, o desempenho dele pode parecer decepcionante: o Codex traduziu os problemas para a linguagem de um programa de matemática chamado Isabelle/HOL com uma taxa de precisão de pouco menos de 30%. Quando não conseguia fazer isso, inventava termos para preencher as lacunas com seu léxico de tradução.

“Às vezes, ele simplesmente não sabe a palavra que precisa saber – qual é o nome no Isabelle para ‘número primo’ ou o nome no Isabelle para “fatorial’ – e apenas inventa o termo, o que é o maior problema com esses modelos”, disse Rute. “Eles fazem suposições demais.”

Mas para os pesquisadores, o importante não era que o Codex havia falhado 70% das vezes, mas que tinha tido sucesso em 30% das vezes depois de ter acesso a um número tão limitado de exemplos.

“Eles conseguiram fazer todas essas tarefas diferentes com apenas algumas demonstrações”, disse Wenda Li, cientista da computação da Universidade de Cambridge e coautor do artigo.

Cientistas tentam ensinar matemática para sistemas de IA Foto: Valentin Tkach/Quanta Magazine

Li e os demais coautores do artigo veem o resultado como característico do tipo de habilidade latente que os LLMs podem adquirir com dados gerais de treinamento suficientes. Antes dessa pesquisa, o Codex nunca tinha tentado traduzir da linguagem natural para o código matemático formal. Mas o Codex estava familiarizado com o código devido ao seu treinamento com o material do GitHub e com a matemática em linguagem natural da internet. Para aproveitar essa base, os pesquisadores apenas tiveram que mostrar a ele alguns exemplos do que queriam e o Codex poderia começar a ligar os pontos.

“Em muitos aspectos, o que é surpreendente nesse artigo é que [os autores] não fizeram muito”, disse Rute. “Esses modelos tinham essa capacidade natural de fazer isso.”

Os pesquisadores observaram o mesmo acontecer quando tentaram ensinar os LLMs não apenas a como traduzir problemas de matemática, mas também resolvê-los.

A matemática do Minerva

O segundo artigo, apesar de independente do trabalho anterior com autoformalização, chegou a uma conclusão semelhante. A equipe de pesquisadores do Google treinou um LLM para responder, em detalhes, questões de matemática de uma competição para estudantes do ensino médio, como “uma reta paralela a y = 4x + 6 passa pelo ponto (5, 10). Qual é a coordenada y do ponto onde esta reta passa pelo eixo y?”.

Os autores começaram com um LLM chamado PaLM, que tinha sido treinado com conteúdo geral em linguagem natural, semelhante ao GPT-3. Então eles treinaram o LLM com material matemático de sites como o arxiv.org e outros materiais técnicos, simulando as origens do Codex. Eles chamaram esse modelo ampliado de Minerva.

Os pesquisadores mostraram ao Minerva quatro exemplos do que queriam. Neste caso, isso significou soluções passo a passo para problemas de matemática em linguagem natural.

Em seguida, eles testaram o modelo com várias questões de raciocínio quantitativo. O desempenho do Minerva variava de acordo com o assunto: ele respondia corretamente às perguntas um pouco mais que a metade das vezes para alguns assuntos (como álgebra) e um pouco menos que a metade das vezes para outros (como geometria).

Uma das preocupações dos autores – comum em muitas áreas da pesquisa em IA – era que o Minerva respondesse às questões corretamente apenas porque já tinha visto elas, ou outras semelhantes a elas, em seus dados de treinamento. Esse problema é chamado de “poluição” e dificulta saber se um modelo está mesmo resolvendo os problemas ou apenas copiando o trabalho de outra pessoa.

“Há tantos dados nesses modelos que, a não ser que você esteja tentando evitar colocar alguns dados no conjunto de treinamento, se for um problema padrão, é muito provável que já tenha sido visto”, disse Rute.

Jason Rute, cientista da computação da IBM Research, vê potencial em modelos de linguagem grandes, mas também conhece seus pontos fracos. "Eles fazem muitas suposições", disse ele Foto: IBM

Para se protegerem dessa possibilidade, os pesquisadores submeteram o Minerva ao Exame Nacional de Matemática de 2022 da Polônia, realizado depois dos dados de treinamento do Minerva terem sido definidos. O sistema acertou 65% das questões, uma pontuação aceitável para um estudante de carne e osso e particularmente boa para um LLM, disse Rute. Mais uma vez, os resultados positivos depois de tão poucos exemplos sugeriram uma habilidade inerente para modelos bem treinados na execução dessas tarefas.

“Esta é uma lição que continuamos aprendendo no aprendizado profundo, que o volume ajuda surpreendentemente bastante em muitas tarefas”, disse Guy Gur-Ari, pesquisador que trabalhava no Google e é um dos coautores do artigo.

Os pesquisadores também descobriram maneiras de melhorar o desempenho do Minerva. Por exemplo, em uma técnica chamada “majority voting” (maioria absoluta), o Minerva resolveu o mesmo problema várias vezes, contabilizou os diferentes resultados e determinou como sua resposta final aquele que havia ocorrido na maioria das vezes (já que existe apenas uma resposta certa, mas inúmeras possíveis respostas erradas). Fazer isso aumentou sua pontuação em certos problemas de 33% para 50%.

Também foi importante ensinar o Minerva a explicar como chegou à solução dos problemas em etapas, um método conhecido como sugestão de cadeia de pensamento. Isso teve os mesmos benefícios para o Minerva que tem para os alunos: obrigou o modelo a desacelerar antes de dar uma resposta e permitiu que ele dedicasse mais tempo computacional a cada parte da tarefa.

“Se você pedir a um modelo de linguagem para explicar passo a passo, a precisão aumenta imensamente”, disse Gadgil.

Uma ponte necessária

Embora impressionante, o trabalho do Minerva chega com uma ressalva fundamental, que também foi reconhecida pelos autores: o Minerva não tem como verificar automaticamente se respondeu de forma correta a uma pergunta. E mesmo que tenha respondido a uma pergunta corretamente, não consegue verificar se os passos seguidos para chegar até ela são válidos.

“Ele às vezes apresenta falsos positivos, dando razões capciosas para respostas corretas”, disse Gadgil.

Em outras palavras, o Minerva pode mostrar seu trabalho, mas não pode verificá-lo, o que significa que depende do feedback humano para melhorar – um processo lento que talvez limite o quanto ele possa ser aprimorado.

“Realmente duvido que essa metodologia possa ser ampliada para problemas complexos”, disse Christian Szegedy, pesquisador de IA do Google e coautor do artigo anterior.

Em vez disso, os pesquisadores por trás de ambos os artigos esperam começar a ensinar matemática às máquinas usando as mesmas técnicas que permitiram a elas serem boas em jogos. O mundo está repleto de problemas de matemática, que poderiam funcionar como material de treinamento para sistemas como o Minerva, mas o Minerva não consegue reconhecer uma “boa” jogada em matemática do jeito que o AlphaGo faz quando está jogando bem Go.

“Por um lado, se você trabalha com linguagem natural ou com o tipo de raciocínio do Minerva, há muitos dados disponíveis por aí, toda a internet da matemática, mas, resumindo, você não consegue fazer o aprendizado por reforço com isso”, disse Wu. Por outro lado, “os assistentes de prova oferecem um ambiente fundamentado, porém têm poucos dados para serem treinados. Precisamos de uma espécie de ponte para ir de um lado ao outro.”

A autoformalização é essa ponte. As melhorias na autoformalização poderiam ajudar os matemáticos a automatizar aspectos da forma como eles escrevem provas e verificam se o trabalho deles está correto.

Ao combinar os avanços dos dois artigos, sistemas como o Minerva poderiam primeiro autoformalizar os problemas de matemática em linguagem natural, depois resolvê-los e verificar seu trabalho usando um assistente de prova como o Isabelle/HOL. Essa verificação instantânea ofereceria o feedback necessário para o aprendizado por reforço, permitindo a esses programas aprender com seus erros. Por fim, eles chegariam a uma resposta comprovadamente correta, com uma lista de etapas lógicas – combinando na prática o poder dos LLMs e do aprendizado por reforço.

Os pesquisadores de IA têm objetivos ainda maiores em mente. Eles veem a matemática como o campo de provas perfeito para desenvolver as habilidades de raciocínio da IA, porque ela é possivelmente a tarefa de raciocínio mais difícil de todas. Se uma máquina pode raciocinar de forma eficaz sobre matemática, segundo essa visão, ela deve naturalmente adquirir outras habilidades, como a capacidade de escrever código de computação ou dar diagnósticos médicos – e talvez até mesmo acabar com aquelas informações inconsistentes em uma história de unicórnios. /TRADUÇÃO ROMINA CÁCIA

História original republicada com permissão da Quanta Magazine, uma publicação editorialmente independente apoiada pela Simons Foundation. Leia o conteúdo original em To Teach Computers Math, Researchers Merge AI Approaches.

Atualizamos nossa política de cookies

Ao utilizar nossos serviços, você aceita a política de monitoramento de cookies.