⚛️ quantum physics

Building Shor's Algorithm in Lean: An Agentic Formalization of Quantum Attacks on RSA-2048 and P-256

Questo articolo presenta una formalizzazione agentica dell'algoritmo di Shor in Lean, in cui agenti IA assistiti da revisione umana hanno verificato con successo le fondamenta matematiche e le stime delle risorse logiche per gli attacchi quantistici a RSA-2048 e P-256, aprendo la strada alla progettazione e alla verifica assistita da IA di algoritmi quantistici.

Autori originali: Lei Zhang, Yusheng Zhao, Hongshun Yao, Xin Wang

Pubblicato 2026-07-16

📖 4 min di lettura🧠 Approfondimento

CC BY 4.0

Autori originali: Lei Zhang, Yusheng Zhao, Hongshun Yao, Xin Wang

Articolo originale sotto licenza CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Questa è una spiegazione generata dall'IA dell'articolo qui sotto. Non è stata scritta né approvata dagli autori. Per precisione tecnica, consulta l'articolo originale. Leggi il disclaimer completo

Immaginate il mondo digitale come una gigantesca, invisibile fortezza che protegge tutto, dai vostri conti bancari ai messaggi segreti del governo. Le serrature di questa fortezza sono enigmi matematici così complessi che, con gli odierni supercomputer, risolverli richiederebbe un tempo superiore all'età dell'universo. Questi enigmi sono l'ossatura della sicurezza moderna, nello specifico due tipi famosi: RSA, che si basa sulla difficoltà di moltiplicare insieme due enormi numeri primi, ed Elliptic Curve (crittografia a curve ellittiche), che utilizza la complessa geometria di curve disegnate su una griglia di numeri. Per decenni, abbiamo creduto che queste serrature fossero indistruttibili. Ma esiste una "chiave maestra" teorica nel mondo della fisica quantistica chiamata Algoritmo di Shor. È come uno strumento magico che, se venisse costruito, potrebbe risolvere questi enigmi in pochi minuti invece che in ere geologiche. Il problema è che costruire un vero computer quantistico è incredibilmente difficile, e dimostrare che i nostri progetti matematici per questa "chiave maestra" siano effettivamente corretti è ancora più difficile. È qui che entra in gioco un nuovo tipo di lavoro investigativo: usare l'intelligenza artificiale per aiutare i matematici a scrivere prove "verificate dalla macchina". Pensatelo come ad avere un avvocato robot che legge ogni singolo passaggio di un argomento legale per garantire che non ci sia un singolo errore di battitura o un vuoto logico, garantendo che la matematica sia solida al 100% prima ancora di provare a costruire la macchina.

Questo articolo riguarda un team di ricercatori che ha utilizzato un team di agenti software (aiutanti IA) per costruire una versione rigorosa e verificata dalla macchina dell'Algoritmo di Shor, specificamente per scassinare due dei due tipi di serrature digitali più comuni al mondo: RSA-2048 e P-256. Non si sono limitati a indovinare come funzionasse; hanno usato l'IA per leggere articoli scientifici, scrivere codice in un linguaggio chiamato Lean e poi hanno fatto in modo che un computer verificasse ogni singolo passaggio logico per garantire che la matematica reggesse. Il loro obiettivo era creare un "progetto" che dimostrasse esattamente quante risorse avrebbe richiesto un computer quantistico per scassinare queste specifiche serrature.

Per la serratura RSA-2048, che protegge gran parte dell'attuale infrastruttura di Internet, il progetto formalizzato dal team mostra che un computer quantistico avrebbe bisogno di circa 6.190 qubit logici (la versione quantistica dei bit informatici) e dovrebbe eseguire un colossale numero di 8,1 miliardi di porte Toffoli (un tipo specifico di operazione logica quantistica). Se eseguiste questo processo tre volte di seguito per sicurezza, la profondità totale del circuito sarebbe di 6,42 miliardi di passaggi. La matematica dimostra che questo metodo troverebbe con successo la chiave segreta almeno 2 volte su 3.

Per la serratura P-256, utilizzata in molti siti web sicuri e firme digitali, i requisiti sono ancora più intensi. La loro prova formalizzata indica che scassinare questa serratura richiederebbe 2.330 qubit logici e un massiccio 126 miliardi di porte Toffoli, con una profondità di circuito di 116 miliardi di passaggi. Proprio come per RSA, l'algoritmo è dimostrato avere successo con una probabilità di almeno 2/3. Interessante notare che, una volta che il computer quantistico ha svolto il suo lavoro pesante, la parte umana (o del computer classico) è sorprendentemente piccola, richiedendo solo 7 semplici passaggi aritmetici per finire il lavoro.

Ciò che rende speciale questo lavoro non sono solo i numeri, ma il modo in cui sono stati ottenuti. Inveve di far scrivere a un essere umano un lungo articolo sperando che nessuno trovi errori, hanno utilizzato un sistema "agentico". Agenti software hanno agito come ricercatori junior: hanno cercato il materiale sorgente, hanno scomposto affermazioni complesse in piccoli pezzi, hanno scritto il codice Lean e hanno persino cercato di correggere gli errori nelle prove. Gli esseri umani hanno poi revisionato la logica scientifica, mentre il computer ha controllato il codice. Il risultato è una libreria di matematica che è "verificata dalla macchina", il che significa che un computer ha verificato ogni singolo anello della catena logica.

L'articolo nota con cura che questa è una vittoria teorica, non pratica. Non hanno ancora costruito il computer quantistico, né hanno effettivamente scassinato una vera chiave RSA-2048. Inveve, hanno costruito l'ultima "prova di concetto" che dice: "Se mai costruiremo un computer quantistico con queste specifiche risorse, ecco esattamente come scaccerà queste serrature, ed ecco la garanzia matematica che funzionerà". Chiariscono anche che i loro numeri si basano su risorse "logiche", che sono i requisiti idealizzati prima di aggiungere la realtà disordinata di correggere gli errori causati dal rumore nella macchina. Questo lavoro non significa che le vostre password siano sicure domani, ma significa che se mai avremo l'hardware quantistico, avremo una mappa perfettamente verificata che mostra esattamente come usarlo per scassinare le serrature digitali più comuni del mondo.

Sintesi Tecnica: Costruire l'Algoritmo di Shor in Lean

Enunciato del Problema
Il documento affronta la sfida della verifica formale delle fondamenta matematiche, dei comportamenti dei circuiti e delle stime delle risorse dell'algoritmo di Shor e delle sue varianti, mirando specificamente alla criptanalisi di RSA-2048 e della curva ellittica P-256. Sebbene gli sforzi esistenti di verifica formale abbiano coperto porzioni dell'algoritmo di Shor (come il calcolo dell'ordine o le operazioni unitarie astratte), vi è una mancanza di sviluppi verificati da macchina che integrino l'intera catena: dalla riduzione del problema crittografico e dall'analisi di probabilità, fino ai circuiti aritmetici reversibili e al conteggio concreto delle risorse logiche. Gli autori mirano a colmare questa lacuna fornendo un framework unificato, verificato da macchina, nel theorem prover Lean che connetta i claim crittografici di alto livello con il numero di gate e le probabilità di successo di basso livello.

Metodologia: Formalizzazione Agente-centrica
Il lavoro impiega un workflow di "formalizzazione agente-centrica". In questo processo, agenti software assistono nello sviluppo formale attraverso:

Analisi della Fonte: Recupero e analisi della letteratura scientifica pertinente (specificamente [Quantum 5, 433] e [ASIACRYPT 2017, 241–270]).
Decomposizione e Codifica: Scomposizione dei claim scientifici in obblighi matematici e computazionali, per poi generare codice Lean e prove.
Riparazione e Iterazione: Gli agenti propongono revisioni per correggere errori di prova.
Revisione Umana: Gli autori umani esaminano i claim scientifici, l'allineamento con le fonti e i risultati delle affermazioni formali.
Verifica da Macchina: Il kernel di Lean verifica tutte le prove accettate rispetto alle definizioni e alle assunzioni importate.

Questo workflow si basa sull'ecosistema Lean, inclusi Mathlib per la matematica generale, CSLib per le fondamenta dell'informatica e Lean-QIT per la teoria dell'informazione quantistica a dimensione finita. La libreria risultante utilizza nomi stabili e posizioni di moduli per consentire ad agenti e ricercatori di localizzare, ispezionare le dipendenze e riutilizzare i componenti verificati.

Contributi Chiave
Il documento presenta due formalizzazioni primarie a livello applicativo all'interno dell'ecosistema Lean:

Fattorizzazione RSA-2048:
- Formalizza la riduzione della fattorizzazione degli interi al calcolo dell'ordine.
- Sviluppa circuiti di aritmetica modulare reversibile (addizione, moltiplicazione, esponenziazione) basati sulla costruzione di Vedral–Barenco–Ekert.
- Implementa la via di Ekerå–Håstad per i logaritmi discreti brevi, che offre una specifica linea di base per i circuiti logici per RSA-2048.
- Combina questi elementi per produrre un'affermazione verificata da macchina riguardante il recupero dei fattori primi.
Recupero dello Scalare P-256:
- Formalizza il problema del logaritmo discreto su curve ellittiche (ECDLP) sul campo primo $\mathbb{F}_p$ .
- Costruisce l'aritmetica reversibile per il campo primo, inclusa l'inversione e la divisione di Montgomery–Kaliski.
- Implementa le operazioni di punti su curve ellittiche reversibili (addizione e raddoppio) e la moltiplicazione scalare tramite addizioni di punti controllate.
- Fornisce il primo sviluppo noto in Lean che fornisca un'affermazione di recupero dello scalare P-256 verificata da macchina con un limite di successo quantitativo e valori di risorse logiche.

Risultati Chiave
La formalizzazione produce due teoremi principali con profili di risorse espliciti e garanzie di successo:

Teorema 1 (RSA-2048): Un algoritmo quantistico esiste che restituisce un fattore $d \in \{p, q\}$ con una probabilità almeno di $2/3$ . Il profilo di risorse per tre tentativi sequenziali (per raggiungere la soglia di successo) include:
- $6.19 \times 10^3$ qubit logici.
- $8.1 \times 10^9$ gate Toffoli.
- $6.42 \times 10^9$ profondità massima del circuito.
- $3.69 \times 10^4$ operazioni aritmetiche classiche per il recupero.
Teorema 2 (P-256): Un algoritmo quantistico esiste che restituisce lo scalare privato $m$ con una probabilità almeno di $2/3$ . Il profilo di risorse per una singola esecuzione include:
- $2.33 \times 10^3$ qubit logici.
- $1.26 \times 10^{11}$ gate Toffoli.
- $1.16 \times 10^{11}$ profondità massima dei gate Toffoli.
- 7 operazioni classiche per il recupero diretto.

Il documento confronta questi risultati con precedenti analisi asintotiche ed stime a livello di gate, notando che la formalizzazione in Lean fornisce soglie di successo esplicite e conteggi di operazioni classiche che erano precedentemente assenti o meno rigorosi nei contesti verificati da macchina.

Significatività e Claim
Gli autori affermano che questo lavoro rappresenta un passo significativo verso il design e la verifica assistita da AI di algoritmi quantistici. Creando uno strato matematico riutilizzabile dove teoria dei numeri, limiti di probabilità, circuiti reversibili e formule di risorse condividono un unico linguaggio di prova, la libreria consente ai ricercatori di:

Recuperare teoremi intermedi e ispezionare le loro dipendenze.
Confrontare formulazioni correlate e assemblare componenti verificati in nuove analisi.
Mantenere una traccia dai claim finali fino alle premesse matematiche.

Il documento dichiara esplicitamente che questo è il primo sviluppo in Lean a fornire un'affermazione di recupero dello scalare P-256 verificata da macchina con limiti quantitativi di successo e valori di risorse logiche. Posiziona il lavoro come una fondazione per una più ampia criptanalisi quantistica verificata da macchina.

Limitazioni e Lavori Futuri
Il documento è modesto riguardo al proprio ambito. Nota che:

I profili di risorse sono logici e non tengono conto del rumore del circuito, della correzione degli errori quantistici, della produzione di stati magici o della pianificazione dei qubit fisici.
I teoremi finali a livello applicativo attualmente si basano su assunzioni esplicite importate dalla letteratura (ad esempio, conteggi di risorse specifici dai riferimenti [21] e [7]), piuttosto che derivare interamente da un'unica esecuzione di circuito formale partendo da input pubblici.
È necessario un lavoro futuro per costruire esecuzioni complete da input pubblici (modulo $N$ o punto pubblico $Q$ ) ed estendere l'analisi delle risorse ad architetture fault-tolerant e famiglie di circuiti ottimizzati.

Articoli simili