Automazione del ragionamento matematicoFormalizzazione della matematica assistita dal computer

Marco Maggesi

Dipartimento di Matematica “U. Dini”

PLS – Perugia 2008

Il computer come strumento di progettazione

Molte attivita di progettazione oggi vengono svolte al computer:

E possibile progettare la matematica al computer?

Schermata di Isabelle/Isar

Cos’e la formalizzazione della matematica

Aspetti fondamentali:

I Linguaggio: Esprimere gli enunciati dei teoremi usando unlinguaggio formale.

I Regole: Scrivere le dimostrazioni usando un insieme fissatodi regole d’inferenza che possono essere espresse in manieraalgoritmica.

La correttezza di una dimostrazione formale e un fatto obiettivo,verificabile in linea di principio in maniera meccanica.

Formalizzato o formalizzabile?

La grandezza delle dimostrazioni formali (es. numero di passi)rende impossibile in pratica la loro costruzione esplicita.

”Un testo matematico convenzionale e la descrizioneinformale di una dimostrazione formale.”

La descrizione convince il lettore dell’esistenza della dimostrazioneformale. La dimostrazione formale resta un oggetto virtuale.

Con l’avvento dei computer si rende possibile la costruzioneesplicita delle dimostrazioni formali.

Un esempio: Formalizzazione del teorema di Euclide

Enunciato: La successione dei numeri primi 2, 3, 5, 7, 11, 13, 17, . . .e infinita.

Dimostrazione: Supponiamo per assurdo che la successione deiprimi sia finita: 2, 3, 5, 7, 11, 13, 17, . . . , pn.

Poniamo q = 2 · 3 · 5 · 7 · 11 · 13 · 17 · · · pn + 1.

Il numero q e primo o composto?

q non e primo perche e piu grande di tutti i primi.

Supponiamo allora che q sia composto e sia pi | q.

Allora pi divide 1 perche divide sia q che q − 1 e quindi anche laloro differenza.

Assurdo.CVD

Dimostrazione del teorema di Euclide (Isar)

theorem euclide: “¬finite primi” proofassume fin: “finite primi” def q ≡ “prod primi + 1”hence “q > 1” using prod gt one zero non primo fin by autohence “q ∈ composti ∨ q ∈ primi” using primo o composto by autothus False proof

have le q: “∀p.p ∈ primi =⇒ p < q”unfolding q def using prod le zero non primo fin by forceassume “q ∈ primi” hence “q 6∈ primi” using le q by autothus False by contradiction

nextassume “q ∈ composti”then obtain p where “p ∈ primi” “p < q” “p dvd q”using composto dvd primo by autofrom ‘p ∈ primi‘ fin dvd prod have “p dvd prod primi” by autowith ‘p dvd q‘ q def dvd plus right have “p dvd 1” by blastthus False using ‘p ∈ primi‘ primi non invertibili by auto

qed

qed

Dimostrazione del teorema di Euclide (semplificata)

theorem euclide: “¬finite primi”proof

assume “finite primi” def q ≡ “prod primi + 1”hence “q > 1” hence “q ∈ composti ∨ q ∈ primi”thus Falseproof

assume “q ∈ primi”have “∀p.p ∈ primi =⇒ p < q” hence “q 6∈ primi”thus False

nextassume “q ∈ composti”then obtain p where “p ∈ primi” “p < q” “p dvd q”have “p dvd prod primi” have “p dvd 1”thus False

qedqed

Dimostrazione automatica e verifica automatica

Dimostrazione automatica: L’utente propone una congettura alsistema e il computer cerca di dimostrarla (o di confutarla).

Verifica automatica (o dimostrazione interattiva): Il sistemaverifica una dimostrazione dettagliata fornita dall’utente.

I sistemi piu recenti tendono a combinare questi due approcci.

Computer e creativita

”La questione se un computer puo pensare e analoga aquella se un sottomarino puo nuotare.”

— Edsgar Dijkstra

La mancanza di immaginazione di un computer e la sua ciecameccanica ci rassicura sulla affidabilita delle dimostrazioni formali.

La scelta del formalismo

Qual e il miglior fondamento per la matematica?

Tante scelte possibili:

I Matematica classica o matematica costruttiva?

I Teoria dei tipi o teoria degli insiemi?

I Logica del primo ordine o logica di ordine superiore?

Compatibilita tra i diversi sistemi

Esistono diversi sistemi di dimostrazione assistita di ampio utilizzo:

ACL2, Coq, HOL Light, HOL4, Isabelle, Mizar, NuprlProofPower, PVS

Far comunicare sistemi diversi comporta problemi sia teorici chepratici.

Sistemi diversi usano formalismi diversi.

Alcuni teoremi formalizzati al computer

Esempi di teoremi formalizzati al computer.

I Teorema dei numeri primi

I Teorema di Godel

I Teorema della curva chiusa di Jordan

I Teorema fondamentale dell’algebra costruttivo

I Teorema dei quattro colori

Espressivita e rapidita

1. Dimostrazione assistita (il piu espressivo)

2. Calcolo simbolico

3. Calcolo numerico (il piu veloce)

Esempio limite: una qualsiasi calcolatrice tascabile puo dimostrare”2+2=4”.

Perche formalizzare la matematica?

I Per mostrare che cio e possibile.

I Per aumentare in modo radicale il rigore e l’affidabilita nellapratica matematica.

Ci sono dimostrazioni in dubbio?

Le dimostrazioni matematiche sono soggette a ‘referaggio’ maqualche errore puo sfuggire al controllo.

Sono sempre piu diffusi archivi di articoli non referati: arXiv

Un libro di Maurice Lecat Erreurs de Mathematiciens des origenesa nos jours (1935) fornisce 130 pagine di errori non banalicommessi da matematici famosi fino al 1900.

Un libro simile oggi sarebbe costituito sicuramente da molti volumi.

Dimostrazioni ‘sospette’

Quali sono in pratica le dimostrazioni che suscitano maggiorepreoccupazione per la loro correttezza?

I Dimostrazioni molto lunghe e/o tortuose. Classificazione deigruppi semplici finiti.

I Dimostrazioni che fanno un uso intensivo del computer.Teorema dei quattro colori, dimostrazione di Hales dellacongettura di Keplero.

I Dimostrazioni di tipo tecnico. Verifica del software,dell’hardware, di protocolli/procedure di sicurezza.

Verifica formale del software e dell’hardware

In molti casi manca una dimostrazione informale di correttezza.

La correttezza viene abitualmente ‘stabilita’ attraverso testing.

Tuttavia, un testing esaustivo e impossibile e bug insidiosi possonosfuggire ai controllo.

Le conseguenze dei bug possono essere molto serie, anche mortali.

La verifica formale meccanizzata sarebbe la soluzione piusoddisfacente, ma sono necessarie enormi e ‘orrende’ dimostrazioni.

Il bug FDIV

Nel 1994 venne trovato un bug nella prima generazione deiprocessori Intel Pentium.

Il bug si verificava in condizioni estremamente improbabili. Fuscoperto da un matematico che si occupava di teoria dei numeri.

Intel dovette spendere 475 milioni di dollari per le sostituzioni.

Oggi nel centro di ricerche Intel lavorano informatici e matematicispecializzati nella formalizzazione delle dimostrazioni al computer.

Il futuro e inquietante. . .

Le statistiche sui processori di ultima generazione mostrano che

I la complessita dei processori aumenta di un fattore 4 ad ognigenerazione.

I il numero dei bug di progettazione cresce di un fattore 4 adogni generazione.

Fortunatamente le tecniche di riconoscimento dei bug pre-silicondanno un tasso di successo molto vicine al 100%.

In parte questo avviene grazie alle tecniche di verifica formale.

Il teorema dei quattro colori

Teorema dei quattro coloriUn esempio

Nella mappa a sinistra ci sono cinque colori ma possiamo cambiarela colorazione per usarne solo quattro.

Teorema dei quattro coloriRiduzione alla teoria dei grafi

Teorema dei quattro coloriStoria del problema

I 1852 Congettura

I 1879 Kempe annuncia una dimostrazione

I 1890 Heaywood trova un errore nella dimostrazione di 1979

I 1976 Appel e Haken danno una dimostrazione che fa un forteuso del computer

I 2004 Dimostrazione di Gonthier nel sistema Coq.

Congettura di Keplero o teorema di Hales?Impacchettamento delle sfere

ProblemaSistemare delle sfere nello spazio euclideo in modo che la densitamedia sia maggiore possibile.

Congettura di Keplero o teorema di Hales?Enunciato delle congettura

E facile vedere che le sfere possono essere impacchettate con unadensita media, pari a

π√18' 0.74048.

Congettura di Keplero

Nessun altro metodo di impacchettamento permette di ottenereuna densita media superiore.

Congettura di Keplero o teorema di Hales?Storia del problema

I 1611: Keplero formula la congettura.

I 1831: Gauss dimostra la congettura per “reticoli regolari”.

I 1900: Hilbert include la congettura nella sua famosa lista di23 problemi.

I 1998 Hales: dimostrazione della congettura con un forte usodel computer.

I 2003: La parte teorica della dimostrazione viene pubblicata suAnnals of Mathematics.

I 2003: Hales annuncia il progetto FlysPecK.

Chi controlla il controllore?

Perche dovremmo credere che una dimostrazione verificata alcomputer sia piu affidabile di una dimostrazione fatta a mano oprodotta da un programma ad-hoc?

I La logica del dimostratore potrebbe essere inconsistente.(Anche i logici piu famosi hanno proposto sistemi che si sonosuccessivamente rivelati essere inconsistente).

I Le regole d’inferenza potrebbero essere implementateincorrettamente.

I I software di dimostrazione assistita sono spesso programmimolto complessi.

Prima risposta: a chi importa?

E estremamente improbabile in pratica che un bug produca unadimostrazione ‘apparente’.

Anche il piu fragile dimostratore di teoremi si rivela piu affidabile diun essere umano nella maggior parte dei casi.

Problemi nella specifica e nella modellizzazione sono molto piufrequenti.

La certezza assoluta non esiste comunque.

Seconda risposta: forse ci importa

Ci sono stati alcuni esempi (anche se rari) di dimostrazioniapparenti.

Se richiediamo rigore matematico dobbiamo anche pretendererigore nello sviluppo dei dimostratori di teoremi.

Una dimostrazione formale serve proprio per accertare un fattomatematico al di la di ogni dubbio.

La perfezione e irraggiungibile ma vale comunque la pena diricercarla.

Architettura dei dimostratori di teoremi

Criterio di de Bruijn:

l’affidabilita di un verificatore di teoremi deve dipenderesolo dalla correttezza di un nucleo minimale.

Il nucleo che verifica una dimostrazione puo essere molto piupiccolo dell’intero dimostratore.

Esempio (HOL Light):

I 10 regole di inferenza

I 3 assiomi

I 430 linee di codice per l’implementazione del nucleo

Uso degli oracoli

Idea:

I usare un programma dedicato (es. CAS) per trovare ladimostrazione.

I usare un verificatore di teoremi per validare la dimostrazione.

Conclusioni

I La formalizzazione della matematica e possibile.

I Ha gia trovato importanti applicazioni in pratica.

I Potrebbe rivelarsi molto utile anche in matematica pura.

I Non e ancora emerso uno standard capace di affermarsi.