A análise de O1 por Terence Tao

Introdução ao mathstodon.xyz

• mathstodon.xyz é parte de uma rede social descentralizada baseada em Mastodon, sendo uma instância para usuários ligados à matemática.
• Suporta renderização de LaTeX na interface web.
• Administrador: Christian Lawson-Perfect (@christianp)
• Estatísticas do servidor: 3 mil usuários ativos

Experimentos de Terence Tao com o GPT-o1

• GPT-o1: nova versão do GPT da OpenAI que realiza uma etapa inicial de raciocínio antes da execução do LLM.
• Experimento 1: em respostas a uma pergunta matemática ambígua, identificou corretamente o teorema de Cramér e forneceu uma resposta satisfatória.
  • Em versões anteriores, conceitos relacionados eram mencionados, mas os detalhes estavam errados.
• Experimento 2: ao enfrentar um problema complexo de análise, chegou à solução correta com muitas dicas e condução, mas não conseguiu gerar sozinho a principal ideia conceitual e cometeu alguns erros.
  • Houve melhora em relação ao modelo anterior, mas ainda é insuficiente.
  • Com mais algumas melhorias no futuro, pode vir a ser útil para trabalho em nível de pesquisa.
• Experimento 3: na tarefa de formalizar resultados em Lean, compreendeu bem o problema e fez bem a decomposição inicial, mas havia vários erros no código devido à falta de informações atualizadas sobre Lean.
  • Pode ser muito útil em uma IDE integrada com modelos especializados em Lean e Mathlib.

Discussão adicional

• Avanço das ferramentas de IA: há expectativa pelo surgimento de um ecossistema de ferramentas de IA capaz de lidar com diversas tarefas de pesquisa.
  • Atualmente, os grandes LLMs de uso geral recebem mais atenção, mas espera-se que modelos leves e open source ajustados para aplicações específicas também tenham um papel importante.
• Comparação entre IA e estudantes de pós-graduação: discussão sobre se ferramentas de IA podem contribuir em nível de estudantes de pós-graduação.
  • No momento, ainda exigem mais esforço do que um pós-graduando, mas há possibilidade de que essa proporção caia para 1 ou menos nos próximos anos.

# Resumo do GN⁺

• Terence Tao testou o novo modelo GPT-o1 da OpenAI para avaliar sua capacidade de resolver problemas matemáticos.
• O GPT-o1 melhorou em relação às versões anteriores, mas ainda tem algumas limitações.
• Com mais algumas melhorias no futuro, pode vir a ser útil para trabalho em nível de pesquisa.
• Há expectativa pelo surgimento de um ecossistema de várias ferramentas de IA para apoiar tarefas de pesquisa.
• Atualmente, os grandes LLMs de uso geral recebem atenção, mas espera-se que modelos leves e open source ajustados para aplicações específicas também tenham um papel importante.

[GN⁺]

Comentários no Hacker News

• Há expectativa de que, se o GPT for ajustado no Lean (assistente de provas) como foi no Python, ele se torne mais útil para matemática em nível de pesquisa

  • Em áreas relacionadas a pesquisa operacional (OR), o ChatGPT 4o aprendeu literatura de OR o suficiente para fornecer formulações úteis de programação inteira mista (MIP)
  • Ao apresentar problemas lógicos, ele gera fórmulas matemáticas úteis, exigindo apenas pequenos ajustes
  • Ele avisa sobre formulações fracas em que a lógica pode falhar, ajudando a evitar problemas
  • O GPT resolve problemas que antes exigiam passar o fim de semana inteiro quebrando a cabeça, economizando muito tempo
  • Para quem entende otimização MIP e consegue dividir o problema em partes menores, a assinatura mensal de US$ 20 do ChatGPT vale muito a pena
  • Muitas pessoas não conseguem usar bem LLMs ou criam expectativas exageradas e por isso ficam insatisfeitas
  • Quem conhece os pontos fortes dos LLMs e consegue verificar erros recebe grande ajuda no trabalho

• Imagine voltar para 2019 e ler que a experiência de interagir com a Alexa era "parecida com orientar um pós-graduando mediano, mas não totalmente incompetente"

  • Em cinco anos, a diferença foi enorme

• O modelo o1 é muito impressionante

  • Em um projeto de otimização de código Rust, obteve um grande ganho de velocidade e verificou a correção
  • Concebeu e implementou uma nova medida de dependência estatística baseada na divergência de Jensen-Shannon
  • Implementou rapidamente informação mútua normalizada, algo difícil de encontrar em implementação rápida ao lidar com vetores grandes (por exemplo, acima de 15.000 dimensões)
  • No começo, não conseguiu fornecer código Rust perfeito, mas corrigiu todos os bugs em uma única tentativa
  • O GPT-4o precisou de várias tentativas para corrigir erros de tipo em Rust
  • O Claude3.5 Sonnet é muito incompetente com Rust
  • Ajuda muito em tarefas extremamente desafiadoras
  • Entende e realiza o objetivo ao combinar otimização de desempenho e código relativamente sem bugs com resolução criativa de problemas e amplo conhecimento matemático e algorítmico

• As experiências com o modelo O1 variam muito

  • Ele se confunde até com perguntas simples

• A novidade é que o LLM, em vários temas, é "parecido com orientar um pós-graduando mediano, mas não totalmente incompetente"

  • Ajuda bastante a lidar com pequenas tarefas em áreas nas quais se tem muita experiência
  • Se o problema for dividido em partes menores, ele faz um trabalho sólido
  • É preciso compreensão conceitual, e a habilidade de escrever prompts é importante
  • Usa-se o LLM para entender temas complexos e confirmar os conceitos com validação de especialistas

• Humanos também podem se beneficiar de um tipo de raciocínio de "cadeia de pensamento"

  • Se todos os estudantes de matemática precisassem lembrar definições e informações relacionadas, sua capacidade melhoraria muito
  • A IA pode raciocinar melhor por não ter barreiras emocionais

• Concorda com a opinião de Terence Tao

  • LLMs podem melhorar o desempenho por meio de correspondência de padrões, mas talvez não sejam eficazes para produzir verdadeira generalização
  • Em problemas novos ou complexos, ainda podem ocorrer alucinações e raciocínio incorreto

• Há expectativa em voltar a estudar matemática como hobby independente

  • Recebe grande ajuda dos LLMs para resolver questões complexas de análise
  • Impressiona a capacidade dos LLMs de encontrar rapidamente conexões conceituais
  • Ao perguntar se seria possível fazer análise complexa em variedades não orientáveis relaxando uma definição específica, o LLM percebeu imediatamente que as equações de Cauchy-Riemann não são globalmente consistentes
  • Sem o LLM, não teria sido possível responder a essa pergunta

• A opinião de Terence Tao é surpreendente

• Daniel Litt ficou impressionado com o o1-preview, mas ainda não teve sorte ao resolver problemas matemáticos interessantes

  • Em tarefas simples, ele é mais confiável e pode economizar tempo em trabalhos não matemáticos