Un tentativo di affrontare l’ostica congettura di Collatz è stato un “nobile fallimento” che dimostra i limiti delle tecniche di ragionamento automatizzato.
di Siobhan Roberts
L’informatico Marijn Heule è sempre alla ricerca di una buona sfida matematica. Professore associato alla Carnegie Mellon University, Heule ha un’impressionante reputazione per la risoluzione di problemi matematici intrattabili con strumenti di calcolo. Il suo risultato del 2016 con il “problema delle triple pitagoriche booleane” ha conquistato i titoli di testa: Two hundred terabyte maths proof is largest ever.
Ora sta implementando un approccio automatizzato per risolvere la “semplice” congettura di Collatz. Proposta per la prima volta (secondo alcuni resoconti) negli anni 1930 dal matematico tedesco Lothar Collatz, questo problema di teoria dei numeri fornisce una ricetta, o algoritmo, per generare una sequenza numerica: inizia con qualsiasi numero intero positivo. Se il numero è pari, dividi per due. Se il numero è dispari, moltiplica per tre e aggiungi uno. Continuando con lo stesso procedimento, afferma la congettura, la sequenza finirà sempre a 1 (e quindi scorrerà continuamente su 4, 2, 1).
Il numero 5, ad esempio, genera solo sei termini:
5, 16, 8, 4, 2, 1
Il numero 27 scorre attraverso 111 termini, oscillando su e giù, alla sua altezza raggiungendo 9.232, prima di arrivare a 1.
Il numero 40 genera un’altra breve sequenza:
40, 20, 10, 5, 16, 8, 4, 2, 1
Ad oggi, la congettura è stata verificata dal computer per tutti i valori di partenza fino a quasi 300 miliardi di miliardi e ogni numero alla fine raggiunge 1. La maggior parte dei ricercatori ritiene che la congettura sia vera. Ha allettato moltitudini di matematici e non, ma nessuno ha prodotto una prova. All’inizio degli anni 1980, il matematico ungherese Paul Erdos dichiarò: “La matematica non è ancora pronta per tali problemi”.
“E probabilmente ha ragione”, dice Heule, secondo il quale il fascino di Collatz non è tanto la prospettiva di una soluzione quanto il progresso delle tecniche di ragionamento automatizzato. Dopo averci armeggiato per cinque anni, Heule e i suoi collaboratori, Scott Aaronson ed Emre Yolcu, hanno recentemente pubblicato un articolo sul server di prestampa arXiv. “Anche se non riusciamo a dimostrare la congettura di Collatz”, scrivono, “crediamo che le idee esposte rappresentino un nuovo punto di vista interessante”.
“È un nobile fallimento”, afferma Aaronson, uno scienziato informatico dell’Università del Texas ad Austin. Un fallimento perché non hanno dimostrato la congettura. Nobile perché hanno fatto progressi in un altro senso: Heule lo vede come un punto di partenza per determinare chi è più capace tra gli esseri umani e i computer a dimostrare tali problemi.
Tradurre la matematica in calcolo
Per molti problemi di matematica, i computer sono senza speranza, dal momento che non hanno accesso alla vasta opera del pensiero matematico accumulato nel corso della storia. Ma a volte i computer eccellono dove gli umani sono senza speranza. Se si presenta al computer una possibile soluzione, gli si assegna un obiettivo e uno spazio di ricerca ben definito, il computer con la sua capacità di calcolo dovrebbe risolvere il problema. Rimane comunque argomento di discussione se i risultati computazionali equivalgano ad aggiunte significative al canone matematico.
La visione tradizionale è che solo la creatività e l’intuizione umana, attraverso concetti e idee, estendono la portata della matematica, mentre i progressi tramite l’informatica sono spesso liquidati come ingegneria. In un certo senso, il computer e la congettura di Collatz sono in perfetta corrispondenza. Innanzitutto, come osserva Jeremy Avigad, logico e professore di filosofia alla Carnegie Mellon, la nozione di algoritmo iterativo è alla base dell’informatica e le sequenze di Collatz sono un esempio di algoritmo iterativo, che procede passo dopo passo secondo una regola deterministica.
Allo stesso modo, mostrare che un processo termina è un problema comune in informatica. “Gli informatici in genere vogliono sapere che i loro algoritmi chiudono un ciclo, vale a dire che restituiscono sempre una risposta”, afferma Avigad. Heule e i suoi collaboratori stanno sfruttando questa tecnologia per affrontare la congettura di Collatz, che in realtà è solo un problema di terminazione.
L’esperienza di Heule è con uno strumento computazionale chiamato “Solutore SAT” o un risolutore di “soddisfacibilità”, un programma per computer che determina se esiste una soluzione per una formula o un problema data una serie di vincoli. Nel caso di una sfida matematica, un risolutore SAT ha prima bisogno che il problema sia tradotto, o rappresentato, in termini comprensibili al computer. E come dice Yolcu, uno studente di dottorato con Heule: “La rappresentazione conta, molto”.
A lungo termine, ma vale la pena provare
Quando Heule ha menzionato per la prima volta la volontà di affrontare Collatz con un risolutore SAT, Aaronson ha pensato: “Non c’è modo che funzioni”. Ma si è convinto facilmente che valesse la pena provare, dal momento che Heule aveva visto modi sottili per rendere flessibile questo vecchio problema. Aveva notato che una comunità di scienziati informatici stava usando risolutori SAT per trovare con successo prove di terminazione per una rappresentazione astratta del calcolo chiamata “sistema di riscrittura”.
Era un’impresa ardua, ma l’idea di Heule di trasformare la congettura di Collatz in un sistema di riscrittura avrebbe potuto rendere possibile ottenere una dimostrazione di terminazione (Aaronson aveva precedentemente contribuito a trasformare l’ipotesi di Riemann in un sistema computazionale, codificandola in una macchina di Turing in miniatura).
Il sistema di Aaronson ha inquadrato il problema di Collatz con 11 regole. Se i ricercatori fossero in grado di ottenere una prova di terminazione per questo sistema analogo, applicando quelle 11 regole in qualsiasi ordine, ciò dimostrerebbe che la congettura di Collatz è vera.
Heule ha provato con strumenti all’avanguardia per dimostrare la cessazione dei sistemi di riscrittura, che non hanno funzionato: è stato deludente, ma non di certo sorprendente. “Questi strumenti sono ottimizzati per problemi che possono essere risolti in un minuto, mentre qualsiasi approccio per risolvere Collatz richiede probabilmente giorni, se non anni di calcolo”, afferma Heule. Ciò ha fornito la motivazione per affinare il loro approccio e implementare i propri strumenti per trasformare il problema di riscrittura in un problema SAT. (Si veda figura 1)
Aaronson ha pensato che sarebbe stato molto più facile risolvere il sistema con una regola in meno delle 11, lasciando un sistema “simile a Collatz”, una cartina di tornasole per l’obiettivo più grande. Ha lanciato una sfida uomo contro computer: il primo a risolvere tutti i sottosistemi con 10 regole avrebbe vinto. Aaronson ha provato a mano, Heule invece col risolutore SAT: ha codificato il sistema come un problema di soddisfacibilità – con un altro livello di rappresentazione intelligente, traducendo il sistema nel gergo delle variabili del computer che possono essere 0 e 1 – e ha lasciato che il suo risolutore SAT funzionasse sui core, alla ricerca di prove di risoluzione. (Si veda figura 2)
Entrambi sono riusciti a dimostrare che il sistema termina con le serie di 10 regole. A momenti è stata un’impresa banale, sia per l’umano sia per il programma. L’approccio automatizzato di Heule ha richiesto al massimo 24 ore. L’approccio di Aaronson ha implicato un notevole sforzo intellettuale, impiegando un certo numero di ore e una serie di 10 regole che non è mai riuscito a dimostrare, anche se crede fermamente che avrebbe potuto farlo, con più applicazione.
Da allora Yolcu ha messo a punto il risolutore SAT, calibrando lo strumento per adattarsi meglio alla natura del problema di Collatz. Questi trucchi hanno fatto la differenza, velocizzando le prove di terminazione per i sottosistemi a 10 regole e riducendo i tempi di esecuzione a pochi secondi. “La domanda principale che rimane”, dice Aaronson, “è: che fare del set completo di 11? Se si prova a far funzionare il sistema sul set completo, funziona all’infinito, il che forse non dovrebbe scioccarci, perché questa è la congettura di Collatz.
Per come la vede Heule, la maggior parte delle ricerche sul ragionamento automatizzato chiude gli occhi sui problemi che richiedono molti calcoli. Ma sulla base delle sue scoperte precedenti, crede che questi problemi possano essere risolti. Altri hanno trasformato Collatz in un sistema di riscrittura, ma è la strategia di utilizzare un risolutore SAT ottimizzato su larga scala con una potenza di calcolo formidabile che potrebbe far guadagnare terreno verso una dimostrazione.
Come partecipante al programma Amazon Scholar, ha ricevuto un invito aperto da Amazon Web Services per accedere a risorse “praticamente illimitate”, fino a un milione di core. Ma è riluttante. “Voglio qualche indicazione che si tratta di un tentativo realistico”, dice Heule.
Chi risolve il problema per primo?
“La bellezza di questo metodo automatizzato è che puoi accendere il computer e aspettare”, afferma il matematico Jeffrey Lagarias, dell’Università del Michigan. Ha “giocato” con Collatz per circa cinquant’anni ed è diventato custode della conoscenza, compilando bibliografie annotate e curando un libro sull’argomento, The Ultimate Challenge. Per Lagarias, l’approccio automatizzato ha fatto venire in mente un articolo del 2013 del matematico di Princeton John Horton Conway, il quale rifletteva sul fatto che il problema di Collatz potrebbe essere tra una classe elusiva di problemi che sono veri e “indecidibili”, ma allo stesso tempo non dimostrabili indecidibili.
Come ha notato Conway: “… potrebbe anche essere che l’affermazione che non sono dimostrabili non sia essa stessa dimostrabile, e così via”. “Se Conway ha ragione”, dice Lagarias, “non ci saranno prove, automatizzate o meno, e non sapremo mai la risposta”.
L’essere umano che probabilmente si è avvicinato di più alla soluzione è il matematico Terence Tao, dell’Università della California, a Los Angeles. Nel 2019 Tao ha dimostrato che la congettura di Collatz è “quasi vera per ‘quasi’ tutti i numeri”.
Tao crede che una dimostrazione umana della congettura sarebbe più significativa dal punto di vista matematico, arrivando al perché,rispetto a una prova al computer. “Ma far cadere un grosso problema irrisolto su un prover automatizzato potrebbe potenziare una trasformazione rivoluzionaria nel modo in cui i matematici utilizzano l’assistenza informatica nel loro lavoro”, afferma. “Con un problema “intrattabile” come questo, si deve fare uso di qualsiasi risorsa”.
Ciò che Heule e i suoi collaboratori cercano davvero, tuttavia, è uno scenario tale che, utilizzando un simile approccio, con questo problema, il computer riesca dove fallisce l’essere umano, o viceversa. “A oggi, non sappiamo se queste tecniche siano molto più potenti di quanto l’uomo è in grado di fare, o viceversa”, dice Heule. “Quello che vogliamo sapere è chi per primo risolve la congettura di Collatz.
(rp)
Immagine: Ms Tech | Superrembo via Codingtrain
