AlphaProof

[Joao Marcos]

Mathematicians put AI model AlphaProof to the test
https://www.nature.com/articles/d41586-025-03585-5
-- by Talia Ringer

Mathematicians use computational tools to prove theorems. An AI model
that is trained to use these tools might accelerate mathematical
discovery.

Nota: o AlphaProof produz demonstrações ---e refutações--- checáveis em Lean.

JM

[Márcio Palmares]

Apesar de resultados como esse (medalha de prata em olimpíada de matemática), alguns pesquisadores continuam defendendo a visão de que não se trata de inteligência (nem modelada, nem simulada, nem imitada...).

Nicolelis concedeu essa entrevista há poucos dias:

https://www.youtube.com/live/EqV6I5RZRiE?si=Uj3wfPiSzCrfCgbm

O que ele diz sobre máquinas de Turing me parece meio discutível (não sei se ele está bem assessorado por uma equipe de matemáticos e lógicos, às vezes parece que o que ele diz sobre computação é senso comum).

E apesar dessa reação que ele apresenta, as evidências empíricas vão se acumulando em favor da inteligência artificial (o fato de ser mal utilizada, causar danos colaterais, ser fonte de ganância e lucros para uns poucos, produzir danos ambientais, etc., poderia ser atribuído a qualquer tecnologia, mas não refuta o fato de que os modelos estão cada vez mais eficazes na execução de certas tarefas...).

De minha parte, fazendo experiências aqui, notei uma evolução espantosa do ChatGPT em comparação com o que ele "sabia" há um ano ou dois. Depois de resolver alguns problemas que propus a ele num plano teórico, ele me mostrou como construir o topos que deriva das ações de um monóide em conjuntos, como construir o classificador de subobjetos, como ver a lógica interna em ação, como interpretar os valores de verdade e os graus de verdade... Fez diagramas, discutiu todos esses conceitos com base num exemplo que eu inventei (artificial, claro, para me certificar de que ele sabia o que estava fazendo, e não apenas dando definições decoradas...). Em suma, talvez por eu ser apenas um estudante e estar estudando num nível básico, ele tenha conseguido me enganar perfeitamente e tenha parecido suficientemente inteligente (ao meu ver) para ser um interlocutor útil. Não sei como ele interagiria com um profissional trabalhando na fronteira de alguma pesquisa...

Seja como for, é muito difícil dizer que essas coisas não são (artificialmente) inteligentes.

Me parece que o Nicolelis perdeu o bonde da história, ficou para trás. Está criticando corretamente as corporações, o marketing, a exploração comercial da ferramenta, todos os efeitos colaterais, mas perdendo de vista o fato puramente teórico, o de que estamos diante de evidências empíricas cada vez mais sólidas apontando para o surgimento de uma nova realidade. Não é que a máquina seja capaz de substituir o ser humano, mas é bastante provável que surja uma nova modalidade de trabalho intelectual, de colaboração cada vez maior homem x máquina. 

M.

--
LOGICA-L
Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica <logi...@dimap.ufrn.br>
---
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+u...@dimap.ufrn.br.
Para ver esta conversa, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LiKFKjGM7b%2Bgs-OEnT0XetTuP9By5cQoy%2Bds6BPDRsPRw%40mail.gmail.com.