I computer sono pronti per risolvere questo problema di matematica notoriamente ingombrante?

Signora Tech | SuperRembo tramite codingtrain

L'informatica Marijn Heule è sempre alla ricerca di una buona sfida matematica. Professore associato alla Carnegie Mellon University, Heule ha una reputazione impressionante per la risoluzione di problemi matematici intrattabili con strumenti computazionali. Il suo risultato del 2016 con il problema delle triple pitagoriche booleane è stata un'enorme prova da prima pagina: La prova matematica di duecento terabyte è la più grande di sempre . Ora sta implementando un approccio automatizzato per attaccare l'affascinante semplice congettura di Collatz.

Proposto per la prima volta (secondo alcuni resoconti) negli anni '30 dal matematico tedesco Lothar Collatz, questo problema di teoria dei numeri fornisce una ricetta, o algoritmo, per generare un sequenza : Inizia con un numero intero positivo. Se il numero è pari, dividi per due. Se il numero è dispari, moltiplica per tre e aggiungi uno. E poi fai lo stesso, ancora e ancora. La congettura afferma che la sequenza finirà sempre a 1 (e quindi scorrerà continuamente attraverso 4, 2, 1).

Il numero 5, ad esempio, genera solo sei termini:

5, 16, 8, 4, 2, 1

Il numero 27 scorre 111 termini, oscillando su e giù, alla sua altezza raggiungendo 9.232, prima di atterrare 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 iniziali 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 attirato moltitudini di matematici e non, ma nessuno ha prodotto una dimostrazione. All'inizio degli anni '80, il matematico ungherese Paul Erdős dichiarò: La matematica non è ancora pronta per tali problemi.

Quello che vogliamo sapere è se gli esseri umani oi computer sono più bravi a risolvere tali problemi.

Marijn Heule

E probabilmente ha ragione, dice Heule. Per Heule, il fascino di Collatz non è tanto la prospettiva di una svolta quanto il progresso di tecniche di ragionamento automatizzato. Dopo averci armeggiato per cinque anni, Heule e i suoi collaboratori, Scott Aaronson ed Emre Yolcu, hanno recentemente pubblicato un carta sul server di prestampa arXiv. Sebbene non riusciamo a dimostrare la congettura di Collatz, scrivono, crediamo che le idee qui presenti rappresentino un nuovo approccio interessante.

È un nobile fallimento, dice Aaronson, uno scienziato informatico dell'Università del Texas ad Austin. Un fallimento perché non hanno dimostrato la congettura. Nobili perché hanno fatto progressi in un altro senso: Heule lo vede come un punto di partenza per determinare se gli esseri umani oi computer sono più bravi a provare 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 di matematica accumulata nel corso della storia. Ma a volte i computer eccellono dove gli umani sono senza speranza. Dì a un computer che aspetto ha una soluzione, assegnagli un obiettivo e uno spazio di ricerca ben definito, e poi con la forza bruta il computer potrebbe trovarla. Anche se è una questione di discussione se i risultati computazionali equivalgono a aggiunte significative al canone matematico. La visione tradizionale è che solo la creatività e l'intuizione umane, attraverso concetti e idee, estendono la portata della matematica, mentre i progressi attraverso l'informatica sono spesso liquidati come ingegneria.

Storia correlata

Questo algoritmo può dire quali sequenze di numeri un essere umano troverà interessanti Il risultato suggerisce che le macchine potrebbero un giorno essere addestrate per individuare l'eleganza e la bellezza matematica.

In un certo senso, il computer e la congettura di Collatz sono una combinazione perfetta. 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 ad una regola deterministica. Allo stesso modo, mostrare che un processo termina è un problema comune nell'informatica. Gli informatici generalmente vogliono sapere che i loro algoritmi terminano, vale a dire che restituiscono sempre una risposta, dice Avigad. Heule ei suoi collaboratori stanno sfruttando quella tecnologia per affrontare la congettura di Collatz, che in realtà è solo un problema di terminazione.

Il bello di questo metodo automatizzato è che puoi accendere il computer e aspettare.

Jeffrey Lagarias

L'esperienza di Heule è con uno strumento computazionale chiamato risolutore 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. Anche se in modo cruciale, nel caso di una sfida matematica, un risolutore SAT necessita prima che il problema venga tradotto, o rappresentato, in termini che il computer comprenda. E come dice Yolcu, uno studente di dottorato con Heule: la rappresentazione conta, molto.

Un colpo lungo, ma vale la pena provare

Quando Heule ha menzionato per la prima volta di affrontare Collatz con un risolutore SAT, Aaronson ha pensato: Non c'è modo che funzioni. Ma si convinse facilmente che valeva la pena provare, dal momento che Heule vedeva modi sottili per trasformare questo vecchio problema che avrebbe potuto renderlo flessibile. Aveva notato che una comunità di scienziati informatici utilizzava solutori SAT per trovare con successo prove di terminazione per una rappresentazione astratta del calcolo chiamata sistema di riscrittura. Era un tentativo lungo, ma suggerì ad Aaronson che trasformare la congettura di Collatz in un sistema di riscrittura avrebbe potuto consentire di ottenere una prova di terminazione per Collatz (Aaronson aveva precedentemente contribuito a trasformare l'ipotesi di Riemann in un sistema computazionale, codificandola in un piccolo macchina). Quella sera Aaronson progettò il sistema. Era come un compito a casa, un esercizio divertente, dice.

'In un senso molto letterale stavo combattendo un Terminator, almeno un dimostratore di teoremi di terminazione.'

Scott Aaronson

Il sistema di Aaronson ha catturato il problema di Collatz con 11 regole. Se i ricercatori potessero ottenere una prova di terminazione per questo sistema analogo, applicando quelle 11 regole in qualsiasi ordine, ciò dimostrerebbe vera la congettura di Collatz.

Heule ha provato con strumenti all'avanguardia per dimostrare la terminazione dei sistemi di riscrittura, che non ha funzionato: è stato deludente se non così 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 proprio approccio e implementare i propri strumenti per trasformare il problema della riscrittura in un problema SAT.

Una rappresentazione del sistema di riscrittura a 11 regole per la congettura di Collatz.

HEULE MARINA

Aaronson ha pensato che sarebbe stato molto più facile risolvere il sistema meno una delle 11 regole, lasciando un sistema simile a Collatz, una cartina di tornasole per l'obiettivo più grande. Ha lanciato una sfida uomo contro computer: vince il primo a risolvere tutti i sottosistemi con 10 regole. Aaronson provato a mano. Heule ha provato con il 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, quindi ha lasciato che il suo risolutore SAT funzionasse sui core , alla ricerca di prove di cessazione.

Il sistema qui segue la sequenza Collatz per il valore iniziale 27—27 è in alto a sinistra della cascata diagonale, 1 è in basso a destra. I passaggi sono 71, anziché 111, poiché i ricercatori hanno utilizzato una versione diversa ma equivalente dell'algoritmo di Collatz: se il numero è pari, allora dividi per 2; altrimenti moltiplica per 3, aggiungi 1 e poi dividi il risultato per 2.

HEULE MARINA

Entrambi sono riusciti a dimostrare che il sistema termina con i vari set di 10 regole. A volte era un'impresa banale, sia per l'umano che per il programma. L'approccio automatizzato di Heule ha richiesto al massimo 24 ore. L'approccio di Aaronson ha richiesto un notevole sforzo intellettuale, alcune ore o addirittura un giorno: una serie di 10 regole che non è mai riuscito a dimostrare, anche se crede fermamente di poterlo fare, con uno sforzo maggiore. In un senso molto letterale stavo combattendo un Terminator, dice Aaronson, almeno un dimostratore di teoremi di terminazione.

Da allora Yolcu ha messo a punto il risolutore SAT, calibrando lo strumento per adattarsi meglio alla natura del problema 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 dire del set completo di 11? Provi a eseguire il sistema sul set completo e funziona per sempre, il che forse non dovrebbe scioccarci, perché questo è il problema di Collatz.

Secondo Heule, la maggior parte della ricerca sul ragionamento automatizzato ha un occhio cieco per i problemi che richiedono molto calcolo. Ma sulla base delle sue precedenti scoperte, crede che questi problemi possano essere risolti. Altri hanno trasformato Collatz avere ha sistema di riscrittura , ma è la strategia di utilizzare un risolutore SAT ottimizzato su larga scala con una formidabile potenza di calcolo che potrebbe guadagnare terreno verso una dimostrazione.

Finora, Heule ha condotto l'indagine Collatz utilizzando circa 5.000 core (le unità di elaborazione che alimentano i computer; i computer consumer hanno quattro o otto core). In qualità di Amazon Scholar, ha ricevuto un invito aperto da Amazon Web Services ad accedere a risorse praticamente illimitate, fino a un milione di core. Ma è riluttante a usarne molto di più.

Voglio qualche indicazione che questo è un tentativo realistico, dice. Altrimenti, Heule sente che sprecherebbe risorse e fiducia. Non ho bisogno del 100% di fiducia, ma mi piacerebbe davvero avere alcune prove che ci sono ragionevoli possibilità che abbia successo.

Potenziare una trasformazione

Il bello di questo metodo automatizzato è che puoi accendere il computer e aspettare, dice il matematico Jeffrey Lagarias, dell'Università del Michigan. Ha giocato con Collatz per circa cinquant'anni ed è diventato custode della conoscenza, compilando bibliografie commentate e pubblicando un libro sull'argomento, L'ultima sfida. Per Lagarias, l'approccio automatizzato ha portato alla mente a carta del 2013 dal matematico di Princeton John Horton Conway, il quale pensava che il problema di Collatz potesse rientrare in una classe elusiva di problemi che sono veri e indecidibili, ma allo stesso tempo non dimostrabili indecidibili. Come ha osservato Conway: ... potrebbe anche essere che l'affermazione che non sono dimostrabili non sia di per sé dimostrabile, e così via.

Se Conway ha ragione, dice Lagarias, non ci saranno prove, automatizzate o meno, e non sapremo mai la risposta.

L'umano che si è probabilmente avvicinato di più è il matematico Terence Tao, dell'Università della California, a Los Angeles. Nel 2019 Tao ha dimostrato che la congettura di Collatz lo è quasi vero per quasi tutti i numeri (si basa quasi su due diverse definizioni tecniche, tuttavia secondo il semplice significato inglese).

Tao crede che una prova umana della congettura sarebbe matematicamente più significativa: arrivare al perché di esso - di una prova computerizzata. Ma la caduta di un grave problema irrisolto su un dimostratore automatizzato potrebbe potenziare una trasformazione rivoluzionaria nel modo in cui i matematici usano l'assistenza informatica nel loro lavoro, dice. Con un problema intrattabile come questo, prenderemo tutte le intuizioni che possiamo ottenere.

Ciò che Heule e i suoi collaboratori cercano davvero, tuttavia, è uno scenario tale che, usando questo approccio, con questo problema, il computer riesce dove fallisce l'umano, o viceversa. A questo punto, non sappiamo se queste tecniche siano molto più forti di ciò che gli esseri umani possono fare manualmente o meno, o se gli esseri umani possono fare cose che il computer non può fare, dice Heule. Quello che vogliamo sapere è se gli esseri umani oi computer sono più bravi a risolvere tali problemi.

A tal fine, vediamo chi risolve per primo la congettura di Collatz.

nascondere