Perché i computer non dimostrano i teoremi?
Non gli si può insegnare a svolgere le derivazioni logiche con efficienza?
Risposte
Siamo sicuri che dimostrare un teorema non sia riconducibile ad procedimento algoritmico?
"gugo82":
Ti stai basando sul fatto che esista una intelligenza artificiale tanto potente da apprendere la creatività che serve a dimostrare un teorema\(^{1}\)... Ma questo assunto è falso.
Non si può dire che non esisterà in futuro. Sarà perché studio cose facili e non devo dimostrare cose nuove da me, ma quello che faccio quando devo risolvere un esercizio è comporre cose che già conosco. Ad esempio nei libri di testo il materiale è presentato in modo che il teorema successivo segua intuitivamente da quello precedente.
Il teorema che hai proposto può essere risolto da un matematico che non lo abbia conosciuto precedentemente, ma più difficilmente da una persona che non si sia mai spremuta le meningi in quel senso. Il matematico ha un vasto bagaglio dal quale attingere per cominciare a fare delle prove, mentre l'altro non sa da dove partire.
"giuscri":
Mhn; non dubito che la cosa sia fattibile, ma --a mio parere-- la stai ponendo male: e' stato gia' detto qualcosa di simile, ma ...che vuol dire `risolvere' un teorema? Nulla, temo. Portare a casa un risultato/dimostrare una qualche tesi e' un lavoro che non riguarda ne' il calcolo ne' la ricerca di informazioni.
Hai presente le regole di derivazione link? Inizialmente non avevo alcuna idea di come dimostrare tautologie come \((\varphi \rightarrow \psi)\leftrightarrow \neg (\varphi \wedge \neg\psi)\), non mi veniva per nulla intuitivo. Guardando gli esercizi svolti pero' si notano una serie di regole generalmente utili, come assumere le proposizioni a sinistra di \(\rightarrow\), le proposizioni negate, etc... poi si va per tentativi.
Raccogliendo le regole empiriche che si usano nel dimostrare le proposizioni ed implementandole su una macchina, cosa le impedisce di derivare autonomamente? Magari si possono creare algoritmi che le permettono ricavare regole empiriche da sé, secondo la loro utilità.
Questi sono gli stessi procedimenti che si usano quando bisogna risolvere un esercizio di topologia. Se un computer avesse una grossa banca dati della matematica con i teoremi scritti sotto forma simbolica, perché non dovrebbe essere capace di replicare i risultati di una persona?
"4mrkv":
Per esempio, si prende un teorema risolvibile in modo molto elementare e gli si chiede di dimostrarlo: deve giustificare tutti i passaggi.
Ad esempio, già la vedo difficile con i primi teoremi di Geometria... Ad esempio, allo stato attuale delle cose, non credo esistano computer capaci di "inventare" una semplice costruzione come quella del pons asinorum.
Insomma, il problema fondamentale è che il computer non riesce fare analisi degli enunciati, non riesce a discernere le complessità di ciò che ha davanti e perciò non riesce a scomporre un teorema complicato in pezzettini più piccoli di "facile" dimostrazione; di conseguenza non può inventare strade per dimostrare un teorema.
Cosa che invece gli uomini fanno da qualche millennio.
"4mrkv":
Poi si passa a qualcosa di più difficile. Se è quasi impossibile risolvere Riemann non mi aspetto che il computer riesca a risolverlo, però deve potere competere con un bravo matematico.
Ti stai basando sul fatto che esista una intelligenza artificiale tanto potente da apprendere la creatività che serve a dimostrare un teorema[nota]Perché il dimostrare non è un procedimento algoritmico, come dovresti ben sapere.[/nota]... Ma questo assunto è falso.
Allo stato attuale, nessuna macchina ha questo tipo di intelligenza; ciò che c'è, e già è tanto, è l'intelligenza artificiale che riesce ad apprendere e simulare alcuni movimenti di esseri biologici. Ma queste cose sono relativiamente "semplici": ti basta pensare a quando hai imparato a reggerti in piedi, o a quando i cani imparano a camminare... Tutto avviene nei primi giorni/mesi/anni di vita. Mentre l'essere umano impara a creare matematica solo molto più in là con gli anni.
"4mrkv":
Per esempio, si prende un teorema risolvibile in modo molto elementare e gli si chiede di dimostrarlo: deve giustificare tutti i passaggi.
Mhn; non dubito che la cosa sia fattibile, ma --a mio parere-- la stai ponendo male: e' stato gia' detto qualcosa di simile, ma ...che vuol dire `risolvere' un teorema? Nulla, temo. Portare a casa un risultato/dimostrare una qualche tesi e' un lavoro che non riguarda ne' il calcolo ne' la ricerca di informazioni.
Penso che non sia poi così difficile far dimostrare ad un computer un certo tipo di tesi. Ad esempio, quei problemi che ci davano in prima liceo che consistevano in piccole dimostrazioni di geometria euclidea. Alla fine ci si basava su pochi principi e i procedimenti, per quel che ricordo, si prestavano ad essere ricondotti ad un algoritmo.
Comunque dipende da cosa si intende per dimostrazione, perchè a mio avviso anche quei programmi che calcolano integrali potrebbero essere intesi come in grado di dimostrare.
Comunque dipende da cosa si intende per dimostrazione, perchè a mio avviso anche quei programmi che calcolano integrali potrebbero essere intesi come in grado di dimostrare.
Per esempio, si prende un teorema risolvibile in modo molto elementare e gli si chiede di dimostrarlo: deve giustificare tutti i passaggi. Poi si passa a qualcosa di più difficile. Se è quasi impossibile risolvere Riemann non mi aspetto che il computer riesca a risolverlo, però deve potere competere con un bravo matematico.
Dipende da cosa intendi con "risolvere teoremi".
Esiste qualche evidenza teorica che non permette di scrivere un programma che risolve i teoremi usando un personal computer?
la maggior parte dei linguaggi di programmazione può essere tradotto per qualsiasi macchina. Siamo lontanissimi dall'avere una IA-Mente matematica-computer. Potrebbe già esistere la potenza di calcolo necessaria a simulare un cervello se collegassimo tutti i computer del mondo. Il problema sarebbe che il cervello da solo non funziona. E' un organo che cresce a partire dal feto e riceve vari stimoli, poi ha bisogno di tempo (anni) per formarsi e crescere con gli stimoli giusti e solo allora (se riuscissimo a mandargli gli stimoli giusti.. ma quanta potenza di calcolo servirebber per simulare il mondo intorno a un cervello?) potrebbe diventare in grado di ragionare come noi. A questo punto ci sarebbero i problemi etici, perchè se quello che hai fatto è un essere senziente, non potresti più "spegnerlo". perchè sarebbe come uccidere un altro essere. E non si tratta solo di potenza di calcolo, perchè per simulare tutti i dati che attraversano le varie connessioni bisognerebbe trasportare enormi quantità di dati rapidamente ai lati del mondo e il bottleneck non sarebbe più la potenza di calcolo di per se, ma la larghezza di banda di tutto l'internet globale (per quanto ne sappiamo potrebbe già essersi formata un IA che sta crescendo come nel film "terminator" XD)
Quale linguaggio si usa per scrivere un programma che poi potrebbe essere tradotto per qualsiasi macchina? Non so se mi sono spiegato bene. Scrivere qualcosa in maniera standard senza che sia necessariamente C++, Matlab, etc...
"4mrkv":
Ho visto link. Qualcosa c'è quindi.
se ne è accennato qui
"gugo82":
Il problema è che i computer ragionano in maniera lineare.
oppure, meglio, in maniera sequenziale.
È un problema legato al fatto che se fosse così tutti gli studenti di Analisi Matematica passerebbero l'esame con 30 e Lode 
.
Scherzo, non siamo ancora ai livelli di una vera e propria AI che approssimi in modo soddisfacente la mente umana, perciò è proprio un problema dell'architettura dei calcolatori odierni (ovvero tutte e tre le componenti da te indicate). Se uno studente che potenzialmente è più "intelligente" di un computer non riesce a dimostrare un teorema senza l'adeguato "allenamento" oppure "genio" (ammesso che non abbia letto da qualche parte la relativa dimostrazione o che non gli sia stata insegnata; io ho già avuto problemi a capirle avendole lette dopo aver seguito tutte le lezioni...
), figuriamoci un computer che per ora è vincolato a procedere mediante una logica di tipo lineare.
.Scherzo, non siamo ancora ai livelli di una vera e propria AI che approssimi in modo soddisfacente la mente umana, perciò è proprio un problema dell'architettura dei calcolatori odierni (ovvero tutte e tre le componenti da te indicate). Se uno studente che potenzialmente è più "intelligente" di un computer non riesce a dimostrare un teorema senza l'adeguato "allenamento" oppure "genio" (ammesso che non abbia letto da qualche parte la relativa dimostrazione o che non gli sia stata insegnata; io ho già avuto problemi a capirle avendole lette dopo aver seguito tutte le lezioni...
), figuriamoci un computer che per ora è vincolato a procedere mediante una logica di tipo lineare.
Ma è un problema legato ad una cattiva programmazione, ad una bassa potenza della macchina o alla struttura della macchina in se?
Il problema è che i computer ragionano in maniera lineare.
Quindi, se una dimostrazione può essere svolta mediante un algoritmo, tutto OK... Ma appena si passa a cose più complicate, addio.
Quindi, se una dimostrazione può essere svolta mediante un algoritmo, tutto OK... Ma appena si passa a cose più complicate, addio.
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo