Os verificadores de prova e o copiloto matemático de IA na visão de Terence Tao
(scientificamerican.com)- À medida que as demonstrações matemáticas ficam mais rigorosamente formalizadas, ferramentas como o Lean estão mudando a forma de verificar provas humanas e a base de confiança para colaborações em larga escala
- Com o acúmulo de bibliotecas padrão como o mathlib, a barreira de entrada para formalizar desde teoremas de nível de graduação até áreas novas está diminuindo
- Na formalização da conjectura PFR, mais de 20 participantes dividiram entre si pequenos passos da prova, e Terence Tao se concentrou mais em orientar a direção geral do que em revisar linha por linha
- Em vez de “resolver” a matemática de imediato, a IA hoje está mais próxima de um copiloto de provas, ajudando na formalização, verificação e no trabalho repetitivo
- A pesquisa em matemática pode se transformar em um trabalho mais explícito e dividido, com separação entre definição de direção humana, formalização detalhada, treinamento de IA e interpretação de provas geradas por IA
A formalização está mudando a colaboração em matemática
- A pesquisa matemática tradicional se parecia mais com uma colaboração de poucas pessoas, e Tao vê em geral 5 pessoas como algo próximo do limite superior desse tipo de trabalho colaborativo
- Com um verificador automático de provas (
proof checker), é possível colaborar até com centenas de pessoas que não se conhecem- Os contribuidores enviam código, e o compilador Lean faz a verificação
- A confiança deixa de depender apenas de relações pessoais e pode ser confirmada por meio do resultado da verificação formal
- Na formalização de um resultado recente sobre a conjectura Polynomial Freiman-Ruzsa (PFR), participaram mais de 20 pessoas
- A demonstração foi dividida em muitos passos pequenos
- Cada participante ficou responsável por provar uma etapa
- Tao se concentrou em administrar a direção geral do progresso em vez de conferir cada contribuição linha por linha
Nem todo matemático precisa ser programador
- Em projetos de formalização, é possível dividir funções
- Algumas pessoas se concentram na direção matemática
- Outras se especializam em transformar pequenos fragmentos matemáticos em provas formais
- Mesmo matemáticos pouco familiarizados com computadores, como Peter Scholze, podem participar de projetos em Lean
- Se uma grande tarefa matemática for dividida em partes menores, é possível contribuir com subtarefas específicas sem compreender toda a teoria
Lean, mathlib e busca tornaram isso prático
- Um dos grandes motivos pelos quais a matemática formal se tornou prática foi o avanço das bibliotecas matemáticas padrão
- O Lean tem um grande projeto chamado mathlib
- Teoremas fundamentais da matemática de graduação, como cálculo e topologia, estão sendo incorporados um a um à biblioteca
- O objetivo é levar a biblioteca até o nível de pós-graduação
- Quando isso acontecer, ficará mais fácil formalizar áreas novas da matemática
- Como construir uma prova exige encontrar teoremas já verificados como verdadeiros, mecanismos de busca mais inteligentes também se tornam importantes
- Depois de formalizar todo o projeto PFR, a compilação para verificação leva apenas cerca de 30 minutos
- O gargalo não está no poder computacional, mas na usabilidade, na facilidade para o usuário e na adaptação das pessoas às ferramentas
- Hoje o Lean é visto como a linguagem formal com a comunidade mais ativa
- Para projetos de autor único, outras linguagens podem ser melhores
- O Lean é fácil de aprender e tem boa biblioteca e comunidade
- Pode vir a ser substituído por alternativas no futuro, mas hoje é a linguagem formal dominante
O custo da formalização ainda é alto
- Tao avalia que até consegue formalizar certos projetos, mas hoje isso pode lhe custar um mês do seu tempo
- Ainda não chegamos ao ponto de formalizar todos os resultados no dia a dia
- Isso pode fazer sentido quando aprender Lean ajuda
- Quando há grande interesse na correção do resultado
- É preciso escolher projetos em que a formalização realmente agregue valor
- Com a melhora da tecnologia, o custo da formalização pode cair
- Hoje isso pode levar 10 vezes mais tempo do que o método tradicional
- No futuro, isso pode cair para algo como 2 vezes, e talvez até menos de 1 vez
A IA pode se tornar o copiloto do matemático
- Tao imagina um futuro em que, em vez de digitar a prova diretamente, o matemático a explique a um sistema como o GPT, enquanto a IA tenta formalizá-la em Lean durante o processo
- Se a verificação passar, será possível fornecer juntos um artigo em LaTeX e uma prova em Lean
- Se o usuário quiser, isso pode até virar um assistente para submissão a periódicos
- No momento, o caminho mais rápido para formalizar ainda é o humano produzir primeiro a ideia e o rascunho da prova
- No longo prazo, também pode haver projetos em que humanos formalizem pequenos fragmentos sem conhecer a prova inteira, e IA e humanos conectem essas partes para provar um grande teorema
- Tao acredita que isso deve levar vários anos para se tornar viável
- A tecnologia atual ainda é insuficiente, e a formalização continua sendo um trabalho penoso
A distância até a ideia de que “a matemática será resolvida”
- Tony Wu e Christian Szegedy já disseram que, em 2 a 3 anos, a matemática será “resolvida” no sentido de que máquinas encontrarão provas melhor do que humanos
- Tao considera possível que, em até 3 anos, a IA se torne útil para matemáticos e traga avanços claros, mas não acha que isso signifique que a matemática estará resolvida
- A IA pode virar um copiloto útil quando parece que uma etapa da prova é verdadeira, mas o humano não consegue ver isso de imediato
- Mesmo que a IA passe a fazer matemática no nível atual dos humanos, matemáticos humanos ainda podem migrar para níveis mais altos de matemática
- Também pode se tornar possível provar de uma vez centenas ou milhares de teoremas com ajuda de IA
- O papel do matemático humano seria comandar o que a IA deve fazer
- Tao considera um pouco agressivo o cronograma de 2 a 3 anos para essa transformação
Entender provas e provas geradas por IA
- Uma demonstração matemática não é apenas um procedimento para confirmar que algo é verdadeiro, mas também um processo para entender por que é verdadeiro
- No futuro próximo, a IA tende a automatizar primeiro as tarefas tediosas e triviais, enquanto os humanos continuam definindo a direção
- Se a IA produzir uma prova difícil de entender e feia de ver, as pessoas ainda podem analisá-la de novo
- Por exemplo, em uma prova que chega à conclusão a partir de 10 hipóteses, pode-se verificar se ela continua válida mesmo removendo uma delas
- Pode surgir um novo tipo de matemático dedicado a extrair insights de provas geradas por IA
- As primeiras provas de IA podem parecer desprovidas de insight
- Pessoas poderão torná-las mais compreensíveis e encontrar sua estrutura
Problemas em aberto e os limites da IA
- Para provar conjecturas não resolvidas, primeiro é preciso quebrá-las em partes menores
- É muito mais fácil transformar um problema em um problema mais difícil do que em um problema mais fácil
- Tao avalia que a IA ainda não mostrou ser melhor do que humanos nessa tarefa de decomposição
- O uso de IA para sugerir possíveis conexões entre diferentes áreas é interessante
- Hoje a taxa de acerto é baixa
- De 10 sugestões, talvez apenas 1 seja interessante e 9 sejam inúteis
- Tao acredita que isso pode mudar no futuro
O problema dos dados no conhecimento matemático
- Um dos problemas no treinamento de IA para matemática é a falta de dados suficientes
- Artigos disponíveis online podem ser usados no treinamento, mas muita intuição matemática não aparece nos papers
- Conversas entre matemáticos
- Aulas
- Formas de orientar estudantes
- Tentativas fracassadas e o processo de correção
- As provas publicadas são resultados comprimidos, e as pessoas tendem a publicar apenas os casos de sucesso
- Os dados realmente valiosos são os processos em que alguém tentou algo, não funcionou, e depois ajustou o caminho
- No futuro, tentativas de pesquisa e fracassos podem ser registrados para treinar IA ou evitar que outros pesquisadores repitam erros
- Tao dá como exemplo uma situação em que alguém concorda em registrar seu processo de pesquisa para usar um sistema avançado de IA com Lean em 2040
A mudança para uma matemática mais explícita
- Muito do conhecimento matemático fica preso na cabeça de matemáticos individuais, e apenas uma pequena parte disso é deixada de forma explícita
- Quanto mais a formalização avança, mais conhecimento implícito se transforma em conhecimento explícito
- Livros-texto formalizados podem evoluir para livros-texto interativos
- Começando por explicações de alto nível da prova
- Etapas que não forem compreendidas podem ser abertas com mais detalhes
- Se a pessoa quiser, pode descer até o nível dos axiomas
- Isso pode facilitar que matemáticos de uma área contribuam para outra
- Subtarefas de um grande desafio podem ser especificadas com precisão
- É possível participar apenas da peça necessária, sem entender o todo
1 comentários
Opiniões do Hacker News
https://archive.is/Idouw
A expressão project manager mathematicians lembra a sátira “A letter to my old friend Jonathan”, escrita por Edsger Dijkstra em 1975 [1], e o texto posterior [2]
Era um texto crítico que mostrava o quão ridículo seria se a forma de criar software fosse aplicada à matemática, mas, em certo sentido, foi profético
O ponto central era criticar o absurdo de aplicar direitos de propriedade intelectual, especialmente à verdade matemática, e felizmente essa parte não parece ser uma grande preocupação na atual onda de mecanização
[1]: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD04xx/E...
[2]: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD05xx/E...
É um texto perspicaz, mas acho que o ponto que falta é que os LLMs estão cada vez mais abstraindo de maneiras super-humanas
Tao disse que “é fácil transformar um problema em algo mais difícil, mas é difícil transformá-lo em algo mais simples, e a IA nunca mostrou ser melhor que humanos nisso”, mas, pelo modo como LLMs funcionam, pode se tornar possível obter insights em um nível muito mais alto
Hoje eles estão mais próximos de assistentes, verificadores de fatos e executores de tarefas tediosas, mas em breve se tornarão entidades que sugerem insights. LLMs já comprimem embeddings e conhecimento, e têm insights que nós não enxergamos
Cena em que Hinton usa como exemplo a relação entre uma bomba nuclear e uma pilha de compostagem: https://www.youtube.com/watch?v=Gg-w_n9NJIE&t=4613s
São apenas máquinas treinadas para imitar o modo como humanos escrevem, e não há dados de treinamento necessários para imitar algo mais inteligente que humanos
Não tenho dúvida de que o aprendizado de máquina vai superar a inteligência humana, mas o gargalo é encontrar uma forma de fazê-lo aprender por conta própria com suas próprias saídas, sem intervenção humana, em vez de regredir sobre todo o texto do mundo
Ramanujan fez descobertas matemáticas brilhantes sem educação formal e tendo contato apenas com alguns livros de matemática, uma quantidade que, do ponto de vista dos dados de treinamento de um modelo de aprendizado de máquina, é praticamente nada
Levei uns 10 segundos para colocar em palavras, mas, se você conhece as informações necessárias, a resposta é óbvia
Hinton diz que isso mostra pensamento analógico, mas há muitos textos sobre jardinagem e sobre a física de pilhas de compostagem online, e é bem possível que o ChatGPT já os tenha visto durante o treinamento
Então esse exemplo parece um caso que não controla a possibilidade de o LLM já ter visto, na prática, a resposta nos textos de treinamento
Também é interessante a parte mais adiante no vídeo em que Ilya diz “existe uma prova de existência. O cérebro humano é uma rede neural” (https://youtu.be/Gg-w_n9NJIE?t=4966). Em geral concordo com a posição de que o cérebro humano também é uma rede neural, mas há muitas objeções de que neurônios reais não operam em 8 bits e de que tipos celulares, DNA, ambiente químico hormonal etc. são diferentes, então acho que há aí uma bifurcação filosófica
Isso pode ser feito em alguns minutos ou horas
Em contraste, para obter mais um especialista humano, é preciso que apareça alguém que goste de matemática como profissão, passe por décadas de educação e especialização avançada, e nem há garantia de que essa pessoa vá até o fim e alcance um nível capaz de empurrar a fronteira do conhecimento
Enquanto se espera por esse tempo, seria possível criar trilhões de especialistas de IA operando em paralelo
A largura de banda com que o cérebro humano absorve novas informações é baixa, mas máquinas podem copiar conhecimento de uma vida inteira em poucos segundos, manter milhares de conversas em paralelo e até serializar parte do cérebro para enviar a outra IA. Se chegarmos a matéria programável, também se torna possível criar computronium em escala exponencial e atingir uma espécie de ponto ômega em que milhares de anos de pesquisa são feitos em segundos
Não entendo nada de matemática, mas isso me fez lembrar da história do software. Antigamente, projetos incríveis como RollerCoaster Tycoon eram quase obras feitas por uma única pessoa
Depois, a engenharia de software se modularizou de um jeito parecido com o descrito na entrevista, e hoje virou uma enorme linha de montagem em que pessoas como eu produzem React como meio de vida; a produtividade por pessoa ou a habilidade exigida parecem ter chegado quase a 0
Fico com a impressão de que, quando uma área está no auge, um gênio guarda cem coisas na cabeça e faz o melhor trabalho; quando isso é substituído por uma linha de montagem, a área deixa de conseguir criar algo de valor de verdade
A engenharia de software não parou de fazer coisas incríveis; eu diria que é exatamente o contrário
Brincadeiras à parte, quando chegar o dia de corrigir um bug crítico, a competência aparece. O fato de um produto ou serviço ter ficado estável e lucrativo não significa que os desenvolvedores originais foram embora, nem que ninguém consiga realizar algo grande
Dizer que essa área não cria mais nada de valor de verdade está muito errado
É como comparar uma catedral feita por 100 pessoas ao longo de 100 anos com uma cabana feita por uma pessoa em um mês. A cabana fica de pé e serve de moradia, mas não é uma catedral
No desenvolvimento web, mesmo olhando só para Python, há tantos frameworks e tecnologias para cada pequena engrenagem da roda que é realmente difícil acompanhar
A habilidade em geral segue uma distribuição log-normal, então pessoas excepcionais são naturalmente raras; em áreas pequenas e iniciais, a falta de infraestrutura de apoio faz com que só pessoas de talento extremo sobrevivam, o que pode gerar uma densidade irrealisticamente alta de talentos de ponta
Produzir um app de lista de tarefas costurando à força 47 frameworks modernos é algo fundamentalmente diferente de gerar impacto significativo
Do ponto de vista de custo-benefício, existe um ótimo local forte em cuspir muito código barato, em vez de investir no longo prazo em coisas grandes; à medida que uma área amadurece, o piso de habilidade necessário para chegar a esse ponto diminui
Também não há muitas organizações focadas em treinar talentos de ponta. Por isso, é fácil explicar por que, à medida que a área cresce, a habilidade média cai quando deixada ao acaso; e, se a distribuição for mal administrada, corrigir isso depois pode sair caro
Provas verificadas por computador são uma área em que a IA pode se tornar útil em um prazo razoavelmente próximo. Mas talvez sejam mais parecidas com as redes neurais de motores de xadrez do que com um LLM completo
Provar tudo à mão é tedioso e demorado, então muitos solvers já são usados, mas táticas ou solvers sofrem quando se despejam teoremas e lemas demais sobre eles
Redes neurais funcionam bem como máquinas de busca que encontram lemas relacionados por correspondência de padrões
Indução e unificação de ordem superior também são, na prática, síntese de código, e enumerar cegamente todas as árvores sintáticas possíveis é muito ineficiente
Como os solvers fazem backtracking de qualquer forma, não há problema se a IA sugerir lemas inúteis em 95% dos casos, e isso pode ser dramaticamente melhor do que a busca manual
Ainda assim, não tenho certeza de que provas verificadas por computador sejam necessariamente boas para comunicação. Provas lidas por humanos são de alto nível e omitem detalhes por vários motivos, não apenas por questão de tamanho
O problema central é que eles precisam estar conectados às definições formais dos objetos matemáticos usados na prova
Mas humanos não pensam assim ao escrever ou ler provas. Em geral, temos uma noção informal de alto nível do que estamos “moralmente” fazendo e preenchemos os detalhes formais conforme necessário
Código de computador funciona até certo ponto porque a semântica formal da linguagem é muito mais próxima do modelo mental; já na matemática, o objetivo geralmente é diferente
A estratégia sledgehammer do Isabelle combina provadores automáticos de teoremas como E, Z3, SPASS e Vampire para tentar provar ou refutar um objetivo
Em teoria parece bom, mas na prática sai uma prova reconstruída que aplica uma dúzia de lemas aparentemente arbitrários, e esse tipo de prova é ilegível e muito frágil
Não parece que a IA vá resolver esse problema por mágica
As redes neurais atuais têm eficiência amostral extremamente baixa, e datasets de matemática formal são muito menores do que datasets como os de código Python
Terence Tao deu uma excelente palestra sobre esse tema há alguns meses e trata do uso do Lean em mais detalhes: https://www.youtube.com/watch?v=AayZuuDDKP0
Um matemático em atividade disse que, durante uma pesquisa, fez o GPT-4o provar o que talvez sejam novos lemas auxiliares
“Meu parceiro é matemático e, na semana passada, usou o ChatGPT pela primeira vez para tentar provar alguns lemas auxiliares para pesquisa. Ele já suspeitava que esses teoremas fossem verdadeiros e tinha mais ou menos uma abordagem, mas não era especialista nesse tipo de proposição. Foi a primeira vez que ele obteve do modelo uma prova correta e útil
O primeiro lema auxiliar foi algo que um colaborador descobriu em cálculos para valores pequenos de e. O ChatGPT não conseguiu encontrar uma prova até que lhe dissessem para tentar usar a função de Möbius
https://chatgpt.com/share/9ee33e31-7cec-4847-92e4-eebb48d4ff...
O segundo parece mais padrão, e acho que o Mathematica também conseguiria fazer. Mas o Mathematica não fornece uma derivação limpa, então ainda é útil
https://chatgpt.com/share/7335f11d-f7c0-4093-a761-1090a21579...”
Essas coisas estão ficando assustadoramente boas em raciocínio e em temas pesados
Se a área de machine learning continuar focada em adicionar capacidades de Sistema 2 para complementar o pensamento de Sistema 1 dos LLMs, a situação deve ficar intensa
É uma memória impressionante, não um raciocínio novo
Nós pensávamos nela não como uma soma sobre partições com coeficiente |τ|!, mas como uma soma sobre partições ordenadas; claro que as duas coisas são equivalentes
Se usamos partições com uma ordem cíclica, ou seja, coeficiente (|τ|-1)! em vez de |τ|!, o resultado é 0, não (-1)^e
A prova combinatória de Beren consiste em escolher um elemento especial e construir uma bijeção entre partições ciclicamente ordenadas de comprimento par e ímpar: se esse elemento estiver sozinho, ele é unido à parte seguinte; se não estiver, é separado em sua própria parte
No caso de ordem linear, aplica-se algo parecido começando pelo último elemento, mas as partições em que o último elemento está sozinho na última parte não são pareadas, então prossegue-se recursivamente para o elemento seguinte
No fim, tudo é pareado, e sobra apenas a partição em que todos os elementos estão separados e na ordem original. Dependendo da paridade do tamanho do conjunto original, a soma com sinais leva à proposição original
Também não sei quantos termos há na soma sobre “τ ≤ τ”, e não bate a conexão disso com estabelecer um dos lados esquerdo ou direito do item 3 e então concluir o outro
Na prática, o ChatGPT se lembrou da função de Möbius do reticulado de partições e a repetiu sem prova; depois disso, gerou bobagem que só parecia plausível
Construir essa função de Möbius é essencialmente o ponto central, e a pergunta é quase o mesmo que pedir uma prova de que essa função tem essa forma
Além disso, a fórmula geral apresentada pelo ChatGPT também está um pouco errada, e só funciona no caso |σ| = 1, que é o importante para a prova atual
Esse fato pode ser visto diretamente, sem escrever explicitamente todo o aparato da função de Möbius, fazendo uma indução elementar em que N(t,e) é o número de partições que dividem em t classes de equivalência, com a recorrência N(t,e+1)=N(t-1,e)+tN(t,e)
Três coisas se destacam nessa entrevista
Primeiro, Tao fala em project manager mathematicians, imaginando um futuro em que insights matemáticos sejam “produzidos” como outros resultados da sociedade. Ele atribui o fato de a matemática ainda não ter sido industrializada dessa forma à falta de ferramentas, e vê IA e assistentes de prova como potencialmente revolucionários nesse aspecto. Ainda assim, a interação e a orientação humanas continuam necessárias
Segundo, há muito conhecimento tácito que não aparece nos artigos. Coisas como intuição e conhecimento sobre fracassos são importantes; até os maiores matemáticos precisam conversar entre si para não repetir os mesmos erros
Terceiro, é fácil pensar que a matemática já é suficientemente formalizada, mas artigos pressupõem muito conhecimento comum. Formalizar provas de um jeito que assistentes de prova consigam entender ajuda mais pessoas a compreenderem o que realmente está acontecendo
Como Tao mostrou em sua palestra sobre o projeto Polymath, fica claro que ele é alguém sempre em busca de novos métodos de pesquisa matemática
Por enquanto, talvez esse tipo de projeto só seja viável quando medalhistas Fields como Tao ou Scholze têm a folga de gastar 10 vezes mais tempo em uma prova
Conversei recentemente com um pós-doutorando de um departamento de matemática de elite, e ele disse que ninguém ao redor dele usa lean4 em trabalho real
Para pesquisadores no início da carreira, provavelmente é melhor confiar na própria intuição e publicar o artigo
Para avaliar esse tema direito, impressões de algumas poucas pessoas não bastam
Por outro lado, em áreas de estilo mais intuitivo, como topologia de baixa dimensão, eu esperaria que menos gente use verificadores de prova
Aqui, intuitivo não quer dizer menos rigoroso. Uma prova por desenho de uma equivalência de homotopia é muito mais difícil de traduzir para algo que o Lean entenda do que uma lista de desigualdades
Para constar, estou na área de geometria/topologia e ainda não vi nem ouvi falar de alguém usando esse tipo de ferramenta
https://lean-lang.org/
https://github.com/leanprover/lean4
A parte que diz: “Se a IA fornecer uma prova incompreensível e feia, é possível analisá-la. Se essa prova usa 10 premissas para chegar a uma conclusão, ela ainda funciona se removermos uma das premissas? Esse tipo de ciência ainda não existe porque não há muitas provas geradas por IA, mas surgirá um novo tipo de matemático que receberá matemática gerada por IA e a tornará mais compreensível” corresponde exatamente ao que penso sobre o design de APIs públicas em código
Um papel que tradicionalmente era exercido apenas por desenvolvedores experientes agora pode ser bastante simplificado e se tornar acessível a todos