AI può fare matematica?
Sono già stati aperti argomenti nel forum sull'intelligenza artificiale ma la questione che vorrei sollevare è abbastanza specifica. AI ha imparato a giocare a scacchi e a Go da solo in una questione di ore e gioca senza mai perdere (anzi vince un buon numero di volte) contro i programmi migliori esistenti (si veda Alpha go e Alpha zero).
La mia domanda è se un giorno AI sarà capace di fare matematica. Dopo tutto anche la matematica è un gioco, le regole sono gli assiomi di Zermelo-Fraenkel (per esempio). Non è così facile definire lo "scopo del gioco" ma io potrei benissimo dare una congettura in pasto a AI e quello in una questione di ore me la dimostra o mi trova un controesempio. La cosa è preoccupante.
La mia domanda è se un giorno AI sarà capace di fare matematica. Dopo tutto anche la matematica è un gioco, le regole sono gli assiomi di Zermelo-Fraenkel (per esempio). Non è così facile definire lo "scopo del gioco" ma io potrei benissimo dare una congettura in pasto a AI e quello in una questione di ore me la dimostra o mi trova un controesempio. La cosa è preoccupante.
Risposte
Hai ragione Vict ho preso l'argomento con troppa superficialità. Comunque per chi fosse interessato ad AlphaZero e come funzioni c'è un simpatico video su YouTube di Daviddol (chi gioca a scacchi probabilmente lo conoscerà), consiglio di andarlo a vedere per chi è appassionato del gioco
@Dan95 Non serve una conoscenza approfondita di AlphaZero per sapere che non hai capito come funziona, basta leggere la descrizione su wiki. AlphaZero non cerca di prevedere le prossime mosse (sue o dell'avversario), ma cerca di intuire la mossa che ha più probabilità di vittoria in base alla situazione attuale, dalla mosse precedenti e dalla sua esperienza.
Insomma all'inizio il suo modello decisionale era totalmente banale, verosimilmente giocava contro se stesso usando mosse totalmente a caso. Man mano che giocava però cominciava a capire che alcune mosse erano migliore di altre e migliorava il suo modello decisionale in base al risultato delle partite. La descrizione di algoritmo per gli scacchi a cui hai fatto riferimento tu è più simile al funzionamento di Stockfish. La vittoria di AlphaZero su Stockfish penso sia comunque dettata anche dalla maggiore potenza di calcolo di AlphaZero. Detto questo ha mostrato che il puro intuito può battere la logica e la strategia negli scacchi.
Quindi a rigore ritengo che AlphaZero possa riuscire a capire come risolvere il tuo problema in un tempo inferiore a quello che ti ci vuole per convincere un bambino a provare a risolverlo.
Insomma all'inizio il suo modello decisionale era totalmente banale, verosimilmente giocava contro se stesso usando mosse totalmente a caso. Man mano che giocava però cominciava a capire che alcune mosse erano migliore di altre e migliorava il suo modello decisionale in base al risultato delle partite. La descrizione di algoritmo per gli scacchi a cui hai fatto riferimento tu è più simile al funzionamento di Stockfish. La vittoria di AlphaZero su Stockfish penso sia comunque dettata anche dalla maggiore potenza di calcolo di AlphaZero. Detto questo ha mostrato che il puro intuito può battere la logica e la strategia negli scacchi.
Quindi a rigore ritengo che AlphaZero possa riuscire a capire come risolvere il tuo problema in un tempo inferiore a quello che ti ci vuole per convincere un bambino a provare a risolverlo.
Ripeto potrei peccare su molti punti di quello che dico non avendo una conoscenza approfondita di come funzioni AlphaZero, ma da quello che ho capito lui impara dagli errori quindi per lui sbagliare è necessario per pensare. Mentre un bambino, permettetemi di dire con un buon talento per gli scacchi, conoscendo l'opposizione tra i due re gli viene subito l'intuizione di come procedere per mandare il re avversario alle strette non va necessariamente a tentativi provando diverse combinazioni, cosa che probabilmente farà la maggior parte dei bambini "normali".
"dan95":
La macchina proverà varie mosse analizzandole e capendo quale di queste è più vantaggiosa. Il bambino, al contrario, potrebbe avere subito l'intuizione di mandare il re avversario ai lati della scacchiera
Secondo me, le intuizioni non sono qualcosa di innato. Parliamone

e poi domandarsi: come?
...e nel domandarsi come, "proverà" varie combinazioni...

@vict
Ad un "qualsiasi" bambino certamente no, intendo in linea di principio. Il fatto che un bambino possa (sempre in linea di principio) pensare alla soluzione senza andare a tentativi come fa il programma secondo me è ancora una grande differenza tra noi e le macchine.
Un esempio, supponiamo di voler far risolvere ad un bambino (molto sveglio) e ad una macchina il finale re+torre vs re. La macchina proverà varie mosse analizzandole e capendo quale di queste è più vantaggiosa. Il bambino, al contrario, potrebbe avere subito l'intuizione di mandare il re avversario ai lati della scacchiera e poi domandarsi: come? Pensanci un attimo e analizzando la geometria della scacchiera riesce a capire come, magari mettendoci più tempo della macchina ma senza usare il suo brutale metodo.
Ad un "qualsiasi" bambino certamente no, intendo in linea di principio. Il fatto che un bambino possa (sempre in linea di principio) pensare alla soluzione senza andare a tentativi come fa il programma secondo me è ancora una grande differenza tra noi e le macchine.
Un esempio, supponiamo di voler far risolvere ad un bambino (molto sveglio) e ad una macchina il finale re+torre vs re. La macchina proverà varie mosse analizzandole e capendo quale di queste è più vantaggiosa. Il bambino, al contrario, potrebbe avere subito l'intuizione di mandare il re avversario ai lati della scacchiera e poi domandarsi: come? Pensanci un attimo e analizzando la geometria della scacchiera riesce a capire come, magari mettendoci più tempo della macchina ma senza usare il suo brutale metodo.
Un computer è molto più logico di quanto un qualsiasi umano possa mai essere. I sotware di dimostrazione automatica forniscono sempre dimostrazioni corrette (supponendo che l'implementazione sia corretta e che abbia sufficiente tempo e memoria per finire il proprio calcolo), seppur non necessariamente belle o minimali; un umano no.
La specialità degli umani è trovare pattern, e semplificare problemi. Inoltre non sono specializzati in nessuna attività specifica. Tranne forse quelle legate alla vista e al coordinamento motorio. Volendo la si può chiamare intuizione. I metodi basati sul machine learning cercano di usare la logica e la statistica per sostituire l'intuizione, ovvero creano dei modelli che gli permettano di decidere rapidamente anche in presenza di informazioni limitate. La loro specialità è la categorizzazione (e, suppongo, i giochi da tavolo
). Questi metodi non sono adatti a dimostrare teoremi, ma riescono a prendere decisioni abbastanza in fretta e possono battere gli uomini in varie attività.
Va osservato che un solutore automatico di teoremi produce il risultato corretto per ogni input, un metodo basato sul machine learning può invece produrre risultati completamente sbagliati se "educato male".
Per fare un ulteriore esempio. Un solutore automatico di teoremi saprebbe dimostrarti che non è possibile vincere a tic tac toe a meno di un errore del tuo avversario, ma non ha la più pallida idea di come si giochi a tic tac toe. Ad un programma dedicato al gioco di tic tac toe, non interessa altro che vincere e sa come farlo; ma non sa fare altro. Un programma come AlphaZero potrebbe imparare a vincere a Tic tac Toe, e dopo abbastanza tempo potrebbe avere l' "impressione" che non esistono mosse necessariamente vincenti, ma continuerà comunque a cercare di migliorare il suo stile di gioco.
Detto questo penso che dovresti togliervi dalla mente che un computer abbia bisogno di essere intelligente per risolvere problemi o che l'AI abbia davvero a che fare con i robot dei film di fantascienza.
@dan95: non capisco il tuo commento sul tatticismo. Pensi che se tu dicessi le regole degli scacchi ad un bambino riuscirebbe a risolvere un qualsiasi problema di scacchi? Io direi di no.
La specialità degli umani è trovare pattern, e semplificare problemi. Inoltre non sono specializzati in nessuna attività specifica. Tranne forse quelle legate alla vista e al coordinamento motorio. Volendo la si può chiamare intuizione. I metodi basati sul machine learning cercano di usare la logica e la statistica per sostituire l'intuizione, ovvero creano dei modelli che gli permettano di decidere rapidamente anche in presenza di informazioni limitate. La loro specialità è la categorizzazione (e, suppongo, i giochi da tavolo

Va osservato che un solutore automatico di teoremi produce il risultato corretto per ogni input, un metodo basato sul machine learning può invece produrre risultati completamente sbagliati se "educato male".
Per fare un ulteriore esempio. Un solutore automatico di teoremi saprebbe dimostrarti che non è possibile vincere a tic tac toe a meno di un errore del tuo avversario, ma non ha la più pallida idea di come si giochi a tic tac toe. Ad un programma dedicato al gioco di tic tac toe, non interessa altro che vincere e sa come farlo; ma non sa fare altro. Un programma come AlphaZero potrebbe imparare a vincere a Tic tac Toe, e dopo abbastanza tempo potrebbe avere l' "impressione" che non esistono mosse necessariamente vincenti, ma continuerà comunque a cercare di migliorare il suo stile di gioco.
Detto questo penso che dovresti togliervi dalla mente che un computer abbia bisogno di essere intelligente per risolvere problemi o che l'AI abbia davvero a che fare con i robot dei film di fantascienza.
@dan95: non capisco il tuo commento sul tatticismo. Pensi che se tu dicessi le regole degli scacchi ad un bambino riuscirebbe a risolvere un qualsiasi problema di scacchi? Io direi di no.
Se ci pensiamo quello che ha fatto AlphaZero (perdonatemi se sbaglio) è fare partite autonome, analizzarle, memorizzare eventuali mosse vantaggiose e svantaggiose in certe posizioni. In tutto questo AZ non ha usato una componente fondamentale dell'intelligenza: l'intuito. Infatti se noi avessimo dato a AZ un tatticismo da risolvere ancor prime delle sue innumerevoli partite, egli non sarebbe riuscito a risolverlo con le sole regole che gli erano state date. Non penso che una macchina creata dall'uomo possa mai essere capace di un pensiero logico-intuitivo ma sarà sempre più stupida di chi l'ha creata, come noi siamo più stupidi di chi ci ha creato, ovvero un bambino alieno che doveva fare un progetto per scuola in cui ha preso 7.
Beh, nessun teorema nuovo (se escludiamo i teoremi dimostrati con i computer ovviamente). Ma i logici matematici studiano queste cose da 50 anni https://en.m.wikipedia.org/wiki/Automat ... em_proving
@vict
Hai scritto che i computer hanno già dimostrato in passato teoremi, puoi farmi un esempio?
Hai scritto che i computer hanno già dimostrato in passato teoremi, puoi farmi un esempio?
"Martino":[...] D'altro canto Alphazero cosa fa? Non lo sappiamo! L'unica cosa che è stata fornita ad Alphazero come informazione sono le regole del gioco! In altre parole Alphazero ha dedotto principi non formulati (quello che per Stockfish erano le "caratteristiche", ma non necessariamente sono le stesse) in poche ore, come? Giocando contro se stesso e imparando dai propri errori (un approccio "umano" al gioco). Risultato? Il nuovo programma è di gran lunga migliore di qualsiasi programma di scacchi esistente. Per questo l'idea che il "creatore" deve sapere almeno quanto il "creato" è superata: questi programmi prendono poche informazioni di base e costruiscono cose inimmaginabili. [/quote]
[quote="vict85"]Gli scacchi sono un problema relativamente semplice per un computer.
...e qui sta la mia obiezione.

Quello che non potrà fare il programmatore è prevedere cosa farà il programma nel medio-lungo termine, perchè l'algoritmo di apprendimento avrà creato una rete di conoscenze talmente complessa che risulterà impraticabile calcolarla "a mano" in un tempo ragionevole per un essere umano. Ma il fatto che il programmatore non conosca a che punto dello sviluppo è la rete neurale dopo un tempo t (per t sufficientemente lungo) è solo una questione di potenza di calcolo.
In ogni caso, il programmatore deve conoscere l'algoritmo che sta alla base dell''"apprendimento" e quindi essere in grado di costruire la rete esattamente come il programma che ha istruito (teoricamente, del resto non credo che un essere umano potrà mai mettersi ad analizzare 44 milioni di partite in tutta la sua vita

"vict85":Visto che sono aggiornato sulla faccenda provo a dire in due parole cosa è successo recentemente. C'è un programma, Stockfish, che ha vinto il campionato mondiale dei programmi di scacchi nel 2016, era considerato fino a pochi giorni fa di gran lunga il programma più forte in assoluto. Usando il paradigma dell'intelligenza artificiale il gruppo DeepMind (di proprietà di Google) ha creato un programma, Alphazero, che ha sconfitto Stockfish in un match di 100 partite senza mai perdere (!). C'è una differenza fondamentale tra Stockfish e Alphazero, Stockfish valuta le posizioni in base a un vettore di caratteristiche, ognuna con un peso, e la valutazione è la media pesata di tali caratteristiche (tali caratteristiche sono per esempio il materiale, lo spazio, la struttura pedonale, la sicurezza del re, la coppia degli alfieri). D'altro canto Alphazero cosa fa? Non lo sappiamo! L'unica cosa che è stata fornita ad Alphazero come informazione sono le regole del gioco! In altre parole Alphazero ha dedotto principi non formulati (quello che per Stockfish erano le "caratteristiche", ma non necessariamente sono le stesse) in poche ore, come? Giocando contro se stesso e imparando dai propri errori (un approccio "umano" al gioco). Risultato? Il nuovo programma è di gran lunga migliore di qualsiasi programma di scacchi esistente. Per questo l'idea che il "creatore" deve sapere almeno quanto il "creato" è superata: questi programmi prendono poche informazioni di base e costruiscono cose inimmaginabili. Per questo dico che non è impensabile che in questo processo di auto-miglioramento un giorno il paradigma dell'intelligenza artificiale potrà probabilmente fare cose molto più vicine a quello che noi chiameremmo "idee".
Gli scacchi sono un problema relativamente semplice per un computer.
Io penso che il concetto di AI sia quanto meno mal definito. I computer possono tranquillamente dimostrare cose, già lo fanno, in alcuni casi anche meglio di noi perché non possiedono pregiudizi. Per loro però una dimostrazione non è altro che una sequenza di simboli, che segue una dall'altra seguendo particolari regole. Insomma la dimostrazione la scrivono ma questo non significa che ne colgano in qualche modo un significato, per lo meno non nel senso che intendiamo noi. Gli scacchi sono un problema relativamente semplice per un computer.
La simulazione del cervello umano è molto lontana, e considerata non necessaria in molti casi. Di fatto i computer battono gli uomini usando semplicemente statistica/machine learning e "forza bruta". I metodi che cercano di simulare il cervello umano vengono usati in rari casi e la dimensione della rete è insignificante rispetto al numero di neuroni nell'uomo (o in un topo).
La simulazione del cervello umano è molto lontana, e considerata non necessaria in molti casi. Di fatto i computer battono gli uomini usando semplicemente statistica/machine learning e "forza bruta". I metodi che cercano di simulare il cervello umano vengono usati in rari casi e la dimensione della rete è insignificante rispetto al numero di neuroni nell'uomo (o in un topo).
Non lo so, ma vedo difficile far padroneggiare una dimostrazione matematica ad una macchina pensante. Per esempio: il gioco degli scacchi e' molto piu' difficile per un umano che dimostrare che l'insieme dei numeri primi e' infinito; nonostante questo nessuna macchina, oggi, puo' dimostrare, credo, che i primi sono in numero infinito. C'e' secondo me ancora molto da fare, non sono un esperto di AI ma la logica che c'e' dietro agli scacchi e' "banale", non e' invece la logica, vera, che c'e' dietro una dimostrazione come quella dell'infinita' dei primi.
Ho l'impressione che non esista un singolo lavoro nell'ambito dell'attività umana che non possa essere sostituito un giorno dall'intelligenza artificiale, perlomeno se si tratta di un lavoro che rientra più nell'ambito tecnico-scientifico che in quello artistico. Stiamo vivendo un periodo di continui giganteschi passi avanti e non mi sorprenderebbe l'idea di un sistema di auto-apprendimento che riesce ad avere "idee" come noi le chiameremmo. Si tratta di un concetto ben lontano dalle potenzialità attuali ma come sappiamo bene è pensando in grande che si raggiungono obiettivi. In questi giorni si stanno proponendo ad AI vari giochi (Scacchi, Go, Shogi tra gli altri, vedere qui), e una delle mie curiosità è come AI approccerebbe giochi più vicini al "punto", tipo Nomic, un gioco in cui lo scopo è vincere (sic.) e quello che i giocatori possono fare come azione è modificare il regolamento del gioco stesso. Se si danno ad AI più e più sfide di questo tipo (andando dal puramente scientifico al "filosofico") si va più vicini alla simulazione sempre più fedele del cervello umano.
Guardi troppi film di fantascienza
Con queste domande però mi iquieti fortemente, aldilà delle Medaglie Fields... Se la risposta fosse positiva, a noi come umanità cosa ci resta? Il lavoro manuale lo fanno loro. Ci strappano anche le attività intellettive e speculative, a noi cosa resta? Uno direbbe: «Programmare i computers, no?». Sinceramente è un po' deprimente... Sì, programmare computers che penseranno al posto nostro...
Adesso io non sono uno che se ne intende di AI, ma ho letto che la coerenza di ZF(C) non è stata ancora provata. Questo potrebbe influire? E poi ci sono teorie più potenti di quella di ZF(C). Non lo so, si potrebbe usare NBG, bho...
Parlo da ignorante: allo stato attuale ci sono computers in grado di "imparare"? Magari è una domanda scema, però per me è importante. Perché io penso che se un computer è in grado di fare quello e solo quello per cui è stato programmato una macchina di certo non potrà mai sostituire una mente umana - anche perché dietro a un computer ci sta un cervello umano - e tanto meno rimpiazzare i matematici umani.
Però ho letto tempo fa che c'era in ballo l'ipotesi di far fare le dimostrazioni di problemi famosi ad alcuni problemi, tipo la Congettura di Goldbach. Anche se è ovvio che basta un controesempio per vanificare $n-1$ risposte positive, con $n$ grande quanto si vuole. Invece di verificare caso per caso, si potrebbe dare in pasto il sistema di Hilbert per le dimostrazioni? Oppure è diventato obsoleto?
Adesso io non sono uno che se ne intende di AI, ma ho letto che la coerenza di ZF(C) non è stata ancora provata. Questo potrebbe influire? E poi ci sono teorie più potenti di quella di ZF(C). Non lo so, si potrebbe usare NBG, bho...
Parlo da ignorante: allo stato attuale ci sono computers in grado di "imparare"? Magari è una domanda scema, però per me è importante. Perché io penso che se un computer è in grado di fare quello e solo quello per cui è stato programmato una macchina di certo non potrà mai sostituire una mente umana - anche perché dietro a un computer ci sta un cervello umano - e tanto meno rimpiazzare i matematici umani.
Però ho letto tempo fa che c'era in ballo l'ipotesi di far fare le dimostrazioni di problemi famosi ad alcuni problemi, tipo la Congettura di Goldbach. Anche se è ovvio che basta un controesempio per vanificare $n-1$ risposte positive, con $n$ grande quanto si vuole. Invece di verificare caso per caso, si potrebbe dare in pasto il sistema di Hilbert per le dimostrazioni? Oppure è diventato obsoleto?
"Martino":
La mia domanda è se un giorno AI sarà capace di fare matematica. Dopo tutto anche la matematica è un gioco, le regole sono gli assiomi di Zermelo-Fraenkel (per esempio). Non è così facile definire lo "scopo del gioco" ma io potrei benissimo dare una congettura in pasto a AI e quello in una questione di ore me la dimostra o mi trova un controesempio. La cosa è preoccupante.
Parto da un semplice presupposto: per quanto complesso, si tratterà di un algoritmo costruito su logiche ben precise e, a meno di bachi, queste logiche devono essere in qualche modo installate appositamente nella AI da chi la crea.
Questo significa che, nel momento in cui esisterà una AI in grado di dimostrare o confutare congetture, chi l'ha istruita (si spera un essere umano

Peccato che AI con i problemi indecidibili andrebbe in loop: ho scritto male?
Che destino triste e meraviglioso, se fosse vero. Da una parte avremmo la possibilità di risolvere molte delle congetture ancora in piedi ma dall'altra non avremmo più medaglie Fields da dare.