1 comentários

 
GN⁺ 3 시간 전
Opiniões no Hacker News
  • Independentemente do resultado ou da prova em si, é interessante que, mesmo nos modelos mais recentes, uma parte considerável do prompt seja usada basicamente para dizer ao modelo para realmente resolver o problema
    Expressões como “relatar estado, rejeitar otimismo vago, rejeitar a alegação de que proposições não comprovadas de compatibilidade global são ‘rotineiras’” mostram isso, e também chama atenção a quantidade de estratégia embutida
    Esse tipo de estratégia acaba passando a sensação de que é algo que o modelo deveria raciocinar sozinho; não é para diminuir o resultado, mas me lembrou o estilo inicial de cadeia de pensamento de quando se fazia prompt no GPT-4 com “pense passo a passo”

    • Acho que isso tem muito a ver com o pós-treinamento que os modelos normalmente recebem
      Eles são projetados para dar respostas curtas, diretas e em formato de resumo para perguntas básicas, então, embora tenham capacidade de raciocinar profundamente, sem prompt não tendem nessa direção
      O grande modelo de linguagem de 2026 é muito competente, mas parece um truque de salão: não é consciente, é mais uma máquina que desce a ladeira quando você prepara o contexto
      Com a entrada certa, ele pode chegar a respostas realmente novas, mas, por não ter vontade própria e depender de orientação humana, é ao mesmo tempo impressionante e mecânico
    • Grandes modelos de linguagem têm raciocínio básico e uma enorme memória
      Se você combinar esse raciocínio básico com busca podada e poder computacional massivo, dá para provar muita coisa; mas a memória dos fracassos humanos anteriores corta possibilidades cedo demais
      Por isso é necessário um esforço para convencer o modelo a não podar cedo demais com base em fracassos humanos anteriores
    • Achei engraçado ver exatamente o mesmo fenômeno quando perguntei sobre P=NP
      Os modelos recusavam de forma bem explícita até mesmo tentar, dizendo que era difícil demais, e foi preciso brigar bastante para fazê-los ao menos sugerir uma abordagem promissora
    • Talvez também sejam necessários modelos ajustados especificamente para pesquisa matemática, algo como “gpt-5.3-codex”
      Fico na expectativa de um “gpt-5.6-mathx”
    • Também vi dessa forma, e o prompt está cheio de meta-heurísticas
      Isso me lembrou de alguns anos atrás, quando se dizia que engenharia de prompt era uma habilidade
      Meu palpite é que o motivo de o modelo não fazer isso por conta própria é que, na maioria dos problemas, boa parte desses conselhos é ruim
      Em otimização de busca, normalmente há uma troca entre tempo e qualidade: uma busca muito ampla tende a retornar resultados ruins por bastante tempo, enquanto uma busca orientada à profundidade com heurísticas costuma produzir resultados bem razoáveis rapidamente
      O modelo provavelmente tenta naturalmente encontrar o meio-termo que é melhor na maioria dos casos, mas, em problemas muito difíceis em que tentativas moderadas não bastam, é necessária uma busca muito mais ampla e sem restrição de tempo
      Grande parte do prompt também parecia voltada a ampliar a busca, evitar convergência precoce e remover pressão de tempo
  • Acho que os critérios para tarefas fáceis de automatizar com agentes de IA podem ser organizados de forma bem sólida assim: o grau em que a correção da resposta pode ser especificada e verificada com facilidade, o grau em que novos candidatos a resposta podem ser implementados em texto, e o grau em que existe pesquisa prévia online
    Isso corresponde basicamente a engenharia de software e matemática
    Acho que boa parte do exagero em torno da IA vem do fato de que o próprio trabalho dos projetistas de IA é uma das profissões mais fáceis de automatizar com IA
    Eles pensam “se meu trabalho melhora tanto assim com IA, então todos os trabalhos devem ser iguais”, mas, ironicamente, a realidade parece quase o oposto, e o mesmo vale para previsões amplas de desaparecimento do trabalho

    • É uma perspectiva interessante, mas acho que 2 desses pontos estão um pouco exagerados
      A maior parte do software não é como resolver um problema matemático ou um conjunto de problemas matemáticos
      Problemas algorítmicos podem ser mais próximos disso, por serem uma área estreita em que já existe um oráculo para verificar se a resposta está certa ou errada
      Na maior parte do software, a função de correção é o quanto os usuários querem usar e pagar por aquilo, e isso é um problema bem nebuloso
      Como o custo de replicação do software é praticamente 0, os sistemas tendem a se tornar únicos, em vez de exatamente iguais entre si, e a divergir, em vez de convergir para outros sistemas
      A parte sobre pesquisa prévia também é interessante
      Pelo menos olhando para aplicações completas, na maioria dos casos não existe pesquisa prévia para a maior parte dos problemas e trade-offs reais, em escala significativa e de forma não trivial, que um software carrega
      Se o projeto for criar um app de lista de tarefas ou uma rede social, talvez haja precedentes suficientes para um sistema de grande modelo de linguagem construir isso, mas é bem possível que a maior parte dos apps não seja assim
    • Vamos supor que a IA só seja boa em software e matemática
      Se com IA for possível criar muito software bom e barato, esse software pode automatizar muitos empregos
      Então a IA não precisa tomar os empregos diretamente; o software escrito por IA pode fazer isso
      Isso vale ainda mais se isso também se tornar possível no software para robôs
    • Você pode explicar o que quer dizer com “a realidade é quase o oposto, e o mesmo vale para previsões amplas de desaparecimento do trabalho”?
      Parece bastante claro que a IA vai ficar boa em um grande conjunto de tarefas verificáveis, como programação, matemática etc.
      E também não vejo por que outro grande conjunto, como direito, contabilidade e análise financeira, não possa se tornar sobre-humano, embora pareça exigir mais trabalho para incorporar a especialização de domínio aos harnesses e ao software
      Você acha que há aspectos do trabalho intelectual em que a IA não vai conseguir se sair bem no longo prazo?
    • Muitos cargos de colarinho branco são verificáveis
      Se construirmos robôs, tarefas do mundo real também se tornam subitamente verificáveis
    • Segundo Dwarkesh, a repetibilidade no treinamento também é importante
  • Diferentemente do problema da distância unitária, o impressionante aqui não é um contraexemplo, e sim uma prova
    Ainda assim, a prova é extremamente concisa, então parece usar algum truque engenhoso que todos os especialistas deixaram passar
    Não é para diminuir esse resultado surpreendente nem mudar a meta, mas agora parece que a única conquista que a IA ainda não alcançou na matemática é uma prova autônoma do tipo construção de teoria para uma conjectura em aberto
    Ou seja, uma prova que exija criar uma teoria nova e substancial, capaz de se estender por pelo menos 30 páginas para resolver um problema em aberto

    • É realmente muito concisa e, exatamente como foi dito, dá a impressão de usar propriedades já descobertas e combiná-las de uma nova maneira
      Gostei muito do estilo
      Lê-se como um artigo antigo, daqueles em que o teorema e a prova avançam exatamente como dizem, de forma direta
    • Grant Sanderson distinguiu recentemente, no podcast do Dwarkesh, entre matemáticos que criam gramáticas e matemáticos que as manipulam
      Em alguns contextos talvez se usasse a palavra ontologia, e gostei bastante dessa distinção
      Parece que agora estamos na fase de manipulação da gramática
      Criar ontologias úteis ainda parece algo um pouco distante
      Não estou reclamando desse resultado incrível, só pensando em onde a meta estará no futuro
    • Existe mesmo motivo para dizer “porém”?
      Na minha leitura, encontrou de fato uma solução nova, e ela é elegante e antes ignorada
      Isso parece exatamente o tipo de resultado que um matemático humano desejaria alcançar
    • Por brincadeira, perguntei ao ChatGPT 5.5 qual era a importância desse problema e qual a chance de o 5.6 resolvê-lo com uma solução de três páginas, e ele respondeu que era quase zero
      Também pedi que pesquisasse na internet, mas mesmo assim continuou extremamente cético
    • Fico curioso se eles executaram sessões paralelas toda vez
      Uma tentando a prova, outra procurando um contraexemplo
  • Anúncio: https://x.com/eknight/status/2075643450196971805
    Prompt: https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98...

    • “Gaste pelo menos 8 horas antes de pensar em retornar ou desistir”
      O harness atual do modelo tem alguma noção de tempo gasto?
      Às vezes já vi o modelo perceber que um subprocesso estava demorando demais ou travou e encerrá-lo, mas nunca vi ele cronometrar o próprio tempo
    • “Leva pouco menos de 1 hora”
      Mesmo assim, fico curioso sobre o tamanho do viés do sobrevivente
      Quantos outros problemas fracassaram?
      Já houve tentativa frustrada de resolver esse mesmo problema com outros prompts?
      Ainda assim, é muito impressionante
  • É muito legal que o prompt tenha sido divulgado
    Fico curioso sobre quantos problemas em aberto são tentados a cada novo modelo de fronteira
    Eles tentam todos os problemas a cada lançamento?
    Qual é a taxa de sucesso?
    Existe uma subcomunidade dentro da matemática coordenando esse esforço?
    Quantas oportunidades ainda restam para serem exploradas?

    • É um pouco interessante que a saída completa não tenha sido divulgada
      Uma crítica comum à escrita matemática é que os resultados parecem “tirados da cartola”
      Escreve-se apenas a prova final polida, e tudo o que entrou no desenvolvimento dela fica escondido
      É irônico que, quando um modelo de linguagem grande escreve uma prova, essa prática continue
    • O prompt foi divulgado, mas o custo para obter o resultado não foi
    • Já estou quase certo de que milhões de dólares em custo de inferência já foram gastos na hipótese de Riemann
      Quanto mais fortes os modelos ficarem, mais dinheiro será investido
      Imagine pagar “apenas 1 bilhão de dólares” e ficar para a história como a empresa que resolveu o problema em aberto mais difícil e famoso da matemática
      Dá até para imaginar as manchetes do mundo todo
      Como se costuma dizer, a hipótese de Riemann é a forma mais difícil de ganhar um milhão de dólares
  • Se toda a verificação passar, isso será um marco gigantesco
    A IA agora usou um modelo pronto para resolver, em 1 hora, um dos problemas em aberto mais famosos da teoria dos grafos
    Neste ponto, ela talvez já seja uma matemática melhor do que a maioria dos humanos
    É parecido com quando softwares de xadrez começaram a vencer todo mundo, exceto os grandes mestres
    O que resta agora?
    Propor e construir teorias e estruturas totalmente novas?
    Depois disso, superar qualquer humano?
    E depois, resultados matemáticos alienígenas que mal conseguimos entender?

    • É difícil não sentir um certo vazio
      Sou uma pessoa bem mediana em termos de inteligência, talvez até abaixo da média
      Se eu souber que qualquer coisa que eu possa fazer um modelo de linguagem grande consegue fazer melhor, qual é o meu valor ou propósito?
      Qual é o meu valor no mercado de trabalho e como ser humano?
    • Parece que o que vai restar será humanos propondo novas conjecturas e máquinas preenchendo as provas
      Só não sei se haverá conjecturas interessantes o suficiente para sustentar novas carreiras
    • Você fala dessas coisas como se fossem o próximo passo imediato, mas talvez na prática não seja assim
      Por exemplo, nos últimos anos a IA não fez nenhum progresso em superar especialistas em arte ou escrita
      Ela melhorou muito em seguir prompts e agora consegue desenhar mãos e letras, mas o senso artístico está totalmente estagnado
  • Esse tipo de anúncio me deixa dividido
    Por um lado, há um potencial infinito no que podemos descobrir quando um prompt de IA resolve um problema antigo
    Por outro, perde-se algo estético, já que não foi uma pessoa lutando com o problema ou chegando à solução por uma nova intuição
    Se um prompt de IA rodar por duas semanas num datacenter e depois imprimir p=np, acho que isso pareceria um pouco vazio

    • Toda geração sentiu alguma versão desse sentimento
      “O teclado não tem alma. A caligrafia é pessoal e única, como uma impressão digital.” — Joyce Carol Oates sobre a máquina de escrever
      “Essa tua descoberta produzirá esquecimento nas almas dos que a aprenderem, porque deixarão de exercitar a memória e passarão a confiar em caracteres externos, lembrando-se não por si mesmos, mas por meios alheios. O que descobriste não é um remédio para a memória, mas para a recordação; e ofereces aos teus discípulos não a verdade, mas a aparência da verdade.” — Sócrates sobre a escrita
    • Entendo esse sentimento, mas, por outro lado, os humanos que lerem essa saída provavelmente receberão um grande boost de inspiração
      Novas respostas normalmente geram novas perguntas
  • O ChatGPT 5.6 Sol Pro considera que essa prova é válida
    Normalmente ele é muito bom em julgar se uma prova está correta e onde ela está errada, e um amigo meu que é pesquisador de matemática de ponta também conferiu: https://chatgpt.com/share/6a515ead-b464-83ed-b85c-c8674f56ea...
    Pessoalmente, fiquei ainda mais convencido de que isso é real

    • Claro que ele vai acreditar que a prova é válida, afinal foi ele que a escreveu
      Para verificar a saída de um grande modelo de linguagem, é preciso usar outro grande modelo de linguagem
  • “GPT-5.6 Sol Ultra gera prova da conjectura da cobertura dupla por ciclos”
    É um título de artigo extremamente enganoso
    O título deveria ser “Humanos sem nome usaram o GPT-5.6 para gerar uma prova não verificada da conjectura CDC”
    Mas, vindo da indústria de IA, imagino que seja texto publicitário

  • Gosto do fato de a prova ser tão concisa
    Já fiz algum progresso em alguns problemas em aberto de combinatória, e a prova que expandia a fronteira em um passo tinha 45 páginas

    • Fiz pesquisa em matemática no ensino médio, e a prova acabou se reduzindo a dezenas de casos de desigualdades polinomiais horrorosas
      Não consigo encontrar o PDF agora, mas o artigo final tinha cerca de 70 páginas, e algumas delas eram preenchidas por expressões polinomiais expandidas ocupando a página inteira
      A parte realmente em prosa provavelmente tinha umas 5 páginas
      Era claramente a prova menos elegante que já vi na vida
      Sou muito grato por ter tido a chance de fazer pesquisa cedo e colocar o pé na água, mas quando olho para aquele artigo hoje em dia fico constrangido