Link alla notizia: https://www.hwupgrade.it/news/web/un-ia-risolve-in-3-giorni-un-enigma-che-i-matematici-non-riuscivano-a-chiudere-da-18-anni_161720.html

Un sistema di ricerca basato sull'intelligenza artificiale ha permesso a PSI di dimostrare la congettura di Aaronson-Ambainis, un problema matematico aperto dal 2008 che riguarda i limiti dei vantaggi dei computer quantistici. La dimostrazione è stata verificata formalmente con Lean, un software capace di controllare ogni passaggio matematico.

Click sul link per visualizzare la notizia.

Vedrete che presto verrà fuori qualche matematico che rosica :D

Vedrete che presto verrà fuori qualche matematico che rosica :D

Allora, iniziamo col chiarire che nessun matematico che si definisca tale può contestare l'uso di strumenti informatici per la risoluzione di problemi avanzati. Strumenti adoperati a tale scopo sin dalla loro invenzione, e proprio dagli stessi matematici. Ora, la questione controversa è che le argomentazioni (o per meglio dire, associazioni d'idee) proposte da un'IA non sono subito chiare e comprensibili perché non necessariamente basate su di un principio già elaborato. Mi spiego meglio: è come avere una lista d'ingredienti conosciuti, essere in possesso delle conoscenze necessarie per utilizzare correttamente i fornelli, ma senza la ricetta giusta difficilmente si possono ottenere risultati gustosi. Quindi, rosicare non è il termine corretto. Si può parlare di dubbi e scetticismo, ma chi ha davvero amore per la scienza e il progresso difficilmente incappa in rosicate a causa di un'IA (e mi sembra sia lo stesso anche in altri campi non prettamente scientifici).
In ogni caso:
I ricercatori stanno preparando una presentazione più breve del risultato destinata alla comunità scientifica.
Ovvero, c'è sempre l'intermediazione umana, perché, nonostante chi vuole far credere il contrario, l'unica vera intelligenza che può verificare la validità di un contenuto destinato alla stessa è solo quella umana (altrimenti si cadrebbe in un paradosso semantico dove il termine intelligenza non potrebbe più significare nulla visto che sarebbe recepito come qualcosa di diverso a ciò che dovrebbe essere in grado d'interpretarlo).

Anche la dimostrazione del Teorema dei quattro colori (https://it.wikipedia.org/wiki/Teorema_dei_quattro_colori) è stata fornita grazie a un complesso algoritmo informatico nel lontano 1977, quindi non c'è niente di speciale nell'utilizzo dell'informatica in campo matematico.
Se mai mi stupirei del fatto che una IA riuscisse a dimostrare ad esempio l'Ipotesi di Riemann (https://it.wikipedia.org/wiki/Ipotesi_di_Riemann).

Allora, iniziamo col chiarire che nessun matematico che si definisca tale può contestare l'uso di strumenti informatici per la risoluzione di problemi avanzati. Strumenti adoperati a tale scopo sin dalla loro invenzione, e proprio dagli stessi matematici. Ora, la questione controversa è che le argomentazioni (o per meglio dire, associazioni d'idee) proposte da un'IA non sono subito chiare e comprensibili perché non necessariamente basate su di un principio già elaborato. Mi spiego meglio: è come avere una lista d'ingredienti conosciuti, essere in possesso delle conoscenze necessarie per utilizzare correttamente i fornelli, ma senza la ricetta giusta difficilmente si possono ottenere risultati gustosi. Quindi, rosicare non è il termine corretto. Si può parlare di dubbi e scetticismo, ma chi ha davvero amore per la scienza e il progresso difficilmente incappa in rosicate a causa di un'IA (e mi sembra sia lo stesso anche in altri campi non prettamente scientifici).
In ogni caso:


Ne parlavo giusto la scorsa settimana con un mio amico matematico. Anche se rosicare non e' un termine molto diplomatico e' pur vero che c'e' forte preoccupazione nel mondo dei matematici.

Va bene "l'amore per la scienza" ma a molti non piace l'idea di diventare meri revisori del lavoro di AI. Fare matematica e' principalmente lavoro creativo e una sfida intellettuale per chi arriva a certi livelli. Riprendendo il tuo esempio e' come se invece venisse assunto un nuovo chef bravissimo che e' capace di inventare ricette migliori di qualsiasi altra cosa fatta prima. Agli chef precedenti non resta che diventare meri esecutori e "provare" che le ricette del nuovo chef siano effettivamente di qualita'. E' chiaro che non e' una prospettiva particolarmente attrattiva per chi ha investito tutta la sua vita nel settore.


Ovvero, c'è sempre l'intermediazione umana, perché, nonostante chi vuole far credere il contrario, l'unica vera intelligenza che può verificare la validità di un contenuto destinato alla stessa è solo quella umana (altrimenti si cadrebbe in un paradosso semantico dove il termine intelligenza non potrebbe più significare nulla visto che sarebbe recepito come qualcosa di diverso a ciò che dovrebbe essere in grado d'interpretarlo).

Anche qui c'e' molta discussione nel mondo accademico. Gia' prima dell'AI alcune dimostrazioni erano conosciute da pochissime persone (letteralmente si possono contare sule dita di una singola mano). Questo perche' la lunghezza e la complessita' di tali dimostrazioni fa si che solo una manciata di persone abbia la capacita' di affrontarle.

Ma visto che ormai le macchine possono produrre dimostrazioni estremamente piu' lunghe e complesse di quelle attuali, ci si chiede cosa vuol dire effettivamente dimostrare un teorema.

Per parlare in termini che pochi anni fa sembravano fantascienza: e' possibile che si arrivi a un punto in cui una o piu' persone debbano verificare una singola dimostrazione prodotta da IA per tutta la vita. A quel punto quando consideri un teorema "dimostrato"?

Peccato che per l'utonto medio l'IA serve solo per fare gli edit di immagini per mettere tutti in bikini o altre robe del genere... vallo a spiegare a loro che ci sono anche utilizzi "Seri" dell'IA

Ovvero, c'è sempre l'intermediazione umana, perché, nonostante chi vuole far credere il contrario, l'unica vera intelligenza che può verificare la validità di un contenuto destinato alla stessa è solo quella umana (altrimenti si cadrebbe in un paradosso semantico dove il termine intelligenza non potrebbe più significare nulla visto che sarebbe recepito come qualcosa di diverso a ciò che dovrebbe essere in grado d'interpretarlo).

Non è quella la ragione, a nessuno frega del paradosso semantico, la questione in ballo è la fiducia, degli umani ci fidiamo, dell'AI no, per cui se l'AI dice che la dimostrazione è valida non ci basta. Lo stesso vale per tutti gli ambiti in cui oggi opera l'AI, la verifica umana è necessaria per la fiducia. Io mi occupo di coding e questa preoccupazione è tutt'altro che eccessiva, visto che l'AI un progetto completo senza fare cazzate di cui non si rende conto non me lo porta a termine, io sì.

Se un giorno, col tempo che serve, le AI sapranno guadagnarsi questa fiducia allora potremo anche accettare dimostrazioni matematiche senza la verifica umana, come del resto già fanno oggi tanti ingegneri che applicano teoremi senza avere la minima idea di come si dimostrano, si fidano semplicemente del fatto che qualche umano più intelligente di loro li ha verificati. Domani potrei fidarmi che qualche AI più intelligente di me li ha verificati, non cambia nulla.

[...]Anche qui c'e' molta discussione nel mondo accademico. Gia' prima dell'AI alcune dimostrazioni erano conosciute da pochissime persone (letteralmente si possono contare sule dita di una singola mano). Questo perche' la lunghezza e la complessita' di tali dimostrazioni fa si che solo una manciata di persone abbia la capacita' di affrontarle.[...]

Ah, la teoria inter-universale di Teichmüller... quanti bei ricordi...
Chissà se è stata già data in pasto a qualche IA. :rolleyes:
Controllerò quando avrò meno sonno.

Il motivo dell' avversità di alcuni matematici a queste soluzioni è nota ...

I problemi posti nella storia della matematica hanno spesso la funzione di "far crescere" gli strumenti a disposizione del pensiero matematico, una soluzione trovata con la IA è come il record (umano) dei 100mt battuto da un robot, che certo non stimola i giovani sportivi ad impegnarsi negli allenamenti come quando a battere il record è un essere umano ...

Il motivo dell' avversità di alcuni matematici a queste soluzioni è nota ...

I problemi posti nella storia della matematica hanno spesso la funzione di "far crescere" gli strumenti a disposizione del pensiero matematico, una soluzione trovata con la IA è come il record (umano) dei 100mt battuto da un robot, che certo non stimola i giovani sportivi ad impegnarsi negli allenamenti come quando a battere il record è un essere umano ...

Con l'unica differenza che il record dei 100mt battuto da un uomo o da un robot non ha nessun utilizzo per la gente comune, una soluzione ad un problema matematico invece potrebbe.

Per quanto riguarda i giovani sportivi devono mettersi in testa che la competizione è tra umani ed altri umani, non tra umani e macchine, sai che una gru può sollevare pesi di decine di tonnellate? Non vedo giovani palestrati che si scoraggiano perché non possono sollevare neanche una "Misera" tonnellata.

Fare matematica e' principalmente lavoro creativo e una sfida intellettuale per chi arriva a certi livelli. Riprendendo il tuo esempio e' come se invece venisse assunto un nuovo chef bravissimo che e' capace di inventare ricette migliori di qualsiasi altra cosa fatta prima. ...

Uhm, bisogna sempre capire se un LLM può avere creatività e capacità di inventare,
non vorrei che fosse il solito brute force.


"un software capace di controllare ogni passaggio matematico"
mi sembra la seconda eh

una soluzione trovata con la IA è come il record (umano) dei 100mt battuto da un robot, che certo non stimola i giovani sportivi ad impegnarsi negli allenamenti come quando a battere il record è un essere umano ...

La scienza non è uno sport, la competizione può essere un mezzo, non certo il fine.

BTW, il tuo discorso si applica agli scacchi, non esistono competizioni umano contro computer perché i computer oggi sono imbattibili, ma sai cosa è accaduto nel momento in cui i computer sono diventati imbattibili? Che le prestazioni dei giocatori umani sono aumentate.

Questo si misura in due modi, il primo è il punteggio ELO, i computer arrivano a 3500 punti ELO, gli umani si fermano attorno a 2800, ma rispetto agli anni 80 sono molti di più i giocatori che lo raggiungono, è la ragione è ovvia: usano i computer per allenarsi.

Il secondo metro di misura è la qualità delle mosse, nelle partite umane ogni mossa viene valutata con un punteggio prendendo come riferimento quella che avrebbe fatto il software, e il punteggio umano è cresciuto costantemente man mano che i motori scacchistici diventavano accessibili al pubblico.

Uhm, bisogna sempre capire se un LLM può avere creatività e capacità di inventare,
non vorrei che fosse il solito brute force.


Un LLM non sa neppure cosa sia il brute force. Se non serve capacità di inventare per risolvere un teorema mai risolto prima, allora cosa? E' evidente che un teorema mai risolto non può essere nei suoi dati d'addestramento.

"un software capace di controllare ogni passaggio matematico"
mi sembra la seconda eh

Ci si riferisce a Lean, un linguaggio formale per controllare le dimostrazioni. Non ha niente a che vedere né con il calcolo né tantomeno con il bruteforce, semplicemente è in grado di garantirti che tutti i passaggi logici sono corretti dal punto di vista formale, il ché non basta a validare la dimostrazione, ma almeno elimina gli errori palesi.

L'AI scrive la dimostrazione in Lean proprio perché ha bisogno di un risultato verificabile per dichiarare concluso il task.

Non è quella la ragione, a nessuno frega del paradosso semantico, la questione in ballo è la fiducia, degli umani ci fidiamo, dell'AI no, per cui se l'AI dice che la dimostrazione è valida non ci basta. Lo stesso vale per tutti gli ambiti in cui oggi opera l'AI, la verifica umana è necessaria per la fiducia. Io mi occupo di coding e questa preoccupazione è tutt'altro che eccessiva, visto che l'AI un progetto completo senza fare cazzate di cui non si rende conto non me lo porta a termine, io sì.

Se un giorno, col tempo che serve, le AI sapranno guadagnarsi questa fiducia allora potremo anche accettare dimostrazioni matematiche senza la verifica umana, come del resto già fanno oggi tanti ingegneri che applicano teoremi senza avere la minima idea di come si dimostrano, si fidano semplicemente del fatto che qualche umano più intelligente di loro li ha verificati. Domani potrei fidarmi che qualche AI più intelligente di me li ha verificati, non cambia nulla.

I risultati vanno validati e verificati a prescindere e la "fonte" conta (autorevolezza e pubblicaziooni scientifiche precedenti hanno un peso). Ricordo di un articolo dove c'era preoccupazione nel mondo scientifico, per interi test in ambito medico, elaborati con l'AI e pubblicati su riviste importanti, che contenevano errori grossolani, o con soggetti umani oggetto dello studio con tanto di nomi, età ecc... completamente inventati. Gli errori grossolani consentono di "svelare" rapidamente l'imbroglio, se c'è un controllo, ma andando avanti sarà sempre più difficile.

I risultati vanno validati e verificati a prescindere e la "fonte" conta (autorevolezza e pubblicaziooni scientifiche precedenti hanno un peso).

Certo, ma questa è la situazione di oggi, e nulla ci dice che non rimarrà tale in futuro, ma la confidenza si guadagna col tempo, e se nel tempo l'AI dovesse iniziare a dare risposte esatte 1000 volte su 1000, poi alla 1001 nemmeno controlli più, fai fare la peer review ad altre AI

Diversi futurologi prevedono che entro la prima metà degli anni '30 i test clinici dei medicinali verranno svolti su gemelli digitali, e qui il problema della fiducia diventa importante, perchè la scelta è tra fidarsi di una macchina che in una settimana può trovare la cura per una malattia rara o aspettare 2 anni per i test clinici, che potrebbero anche dare esito negativo, e nel frattempo la gente muore. All'inizio il digital twin servirà al massimo per passare più velocemente al test clinico, ma dopo un po' che il digital twin ci prende ogni volta, che si fa?

Certo, ma questa è la situazione di oggi, e nulla ci dice che non rimarrà tale in futuro, ma la confidenza si guadagna col tempo, e se nel tempo l'AI dovesse iniziare a dare risposte esatte 1000 volte su 1000, poi alla 1001 nemmeno controlli più, fai fare la peer review ad altre AI

Diversi futurologi prevedono che entro la prima metà degli anni '30 i test clinici dei medicinali verranno svolti su gemelli digitali, e qui il problema della fiducia diventa importante, perchè la scelta è tra fidarsi di una macchina che in una settimana può trovare la cura per una malattia rara o aspettare 2 anni per i test clinici, che potrebbero anche dare esito negativo, e nel frattempo la gente muore. All'inizio il digital twin servirà al massimo per passare più velocemente al test clinico, ma dopo un po' che il digital twin ci prende ogni volta, che si fa?

certo, l'affidabilità dei risultati e i controlli interni alla stessa AI, sono destinati ad aumentare. Ma tu dicevi che i risultati sono affidabili se provengono da un essere umano... anche no, come pure dall'AI, che può avere allucinazioni o essere usata falsificando i risultati. No, vanno verificati, magari da enti che usano AI certificate supervisionate da umani, come potrebbe accadere in futuro, ma un controllo ce lo devi mettere.

Ma tu dicevi che i risultati sono affidabili se provengono da un essere umano...

Dipende da quali dati stiamo validando, se sono le mie analisi del sangue il parere del mio medico è sufficiente, se è un esperimento scientifico importante andrà validato in peer review dalla comunità scientifica. In questi casi non si parla nemmeno di dimostrazione, ma di riduzione dell'incertezza. Alla fine comunque ci dovremo fidare, non è che ci mettiamo a rifare pure noi gli esperimenti a casa.