Bit-Exact AI Inference Verification Without Performance Tradeoffs

Sintesi Tecnica: Verifica dell'Inferenza AI Bit-Exact Senza Compromessi sulle Prestazioni

Definizione del Problema
Il documento affronta la sfida di verificare i calcoli dell'IA eseguiti da "avversari occulti" (covert adversaries)—entità che rispettano il monitoraggio solo quando la probabilità di rilevamento è elevata. Gli attuali metodi di verifica si scontrano con un ostacolo significativo: l'apparente non-determinismo dell'aritmetica in virgola mobile delle GPU. A causa della sommatoria non associativa nelle riduzioni parallele e delle approssimazioni specifiche dell'hardware, gli auditor sono spesso costretti ad accettare output corrispondenti solo in modo approssimativo. Questa ambiguità crea "gradi di libertà non verificabili" che gli avversari possono sfruttare per la steganografia, modifiche software non dichiarate o computazione occulta (ad esempio, elementi di batch nascosti). Sebbene le prove a conoscenza zero (ZKP) offrano una via d'uscita, esse richiedono tipicamente un rigoroso determinismo come precondizione, il che ha storicamente richiesto flag che degradano le prestazioni o librerie di kernel personalizzate.

Metodologia
Gli autori indagano sulle cause profonde della varianza dell'output nei moderni motori di inferenza (vLLM, HuggingFace Transformers) in esecuzione su GPU NVIDIA (L40, L40S, A100, H100) senza abilitare flag di determinismo che degradano le prestazioni. Il loro approccio prevede:

1. Analisi delle Cause Radice: Distinguere tra vero non-determinismo (causato da funzioni atomiche come atomicAdd, dove lo scheduling dei warp varia) e non-invarianza (deterministica ma con alberi di riduzione variabili a causa dello stack software, della dimensione del batch o della topologia dell'hardware).
2. Test Empirico: Eseguire l'inferenza attraverso varie SKU di hardware, versioni software, dimensioni di batch e formati di quantizzazione (BF16, FP8, INT8, INT4) per misurare le distanze L2 tra i vettori di segnale (log-probabilità, stati nascosti).
3. Emulazione Solo Software: Sviluppare un emulatore C/Python che giri interamente su CPU per prevedere l'output esatto a livello di bit dell'inferenza LLM accelerata da GPU. Questo emulatore modella:
   • Aritmetica dei Tensor Core: Replicare le specifiche finestre di allineamento a punto fisso, la troncatura e la logica di accumulo dei Tensor Core (ad esempio, la finestra a 26 bit dell'A100) e le istruzioni MMA.
   • Unità di Funzioni Speciali (SFU): Cache degli output hardware esatti per le funzioni trascendenti (esponenziale, radice quadrata inversa) che deviano dallo standard IEEE 754 ma sono deterministiche.
   • Riduzioni Specifiche dei Kernel: Mirroring degli esatti alberi di riduzione, dei confini dei tile e degli ordini di accumulo dettati da specifiche configurazioni di kernel (ad esempio, logica di dispatch di CUTLASS, FlashAttention-2, cuBLAS).
   • Confini dei Dati: Imporre confini di quantizzazione BF16 precisi tra le fasi della pipeline per corrispondere al comportamento dell'hardware.

Risultati Chiave

• Determinismo Senza Flag: Lo studio dimostra che i moderni motori di inferenza producono output bit-identici quando lo stack software, la SKU dell'hardware e le forme di input (inclusa la dimensione del batch) sono fissi. L'apparente non-determinismo è in gran parte una funzione del cambiamento degli ordini di riduzione basati su questi parametri, non di rumore casuale.
• Fonte di Varianza: L'unica vera fonte di non-determinismo identificata è stato l'uso di atomicAdd in specifici kernel di dequantizzazione INT (ad esempio, il kernel exllama predefinito per GPTQ in vLLM). Quando questi vengono evitati o sostituiti (ad esempio, usando il kernel marlin), gli output sono deterministici.
• Invarianza della Dimensione del Batch: Gli autori hanno osservato "classi di equivalenza" in cui il cambiamento delle dimensioni del batch non alterava l'output del primo elemento del batch, particolarmente a lunghezze di sequenza elevate (>4.000 token) dove la selezione del kernel si stabilizza.
• Accuratezza dell'Emulazione: L'emulatore software-only ha raggiunto 0 differenze di bit (accumulatori BF16 e FP32) rispetto alla ground truth delle esecuzioni su GPU per interi blocchi FFN e complessi blocchi FlashAttention-2 su molteplici architetture GPU. Ciò conferma che gli errori di arrotondamento accumulati possono essere previsti e auditati con precisione senza accesso all'hardware originale.

Contributi Chiave

1. Riformulazione degli Errori di Arrotondamento: Il documento sostiene che gli errori di arrotondamento non debbano essere visti come un vincolo sulla verificabilità, ma come una "firma auditabile" della specifica configurazione software e hardware utilizzata.
2. Protocollo di Verifica Bit-Exact: Stabilisce che la ricalcolazione bit-precisa è possibile senza un hardware identico, a patto che il verificatore conosca le chiavi fattori statici (SKU hardware, versioni software, pesi del modello, topologia del parallelismo) e la dimensione dinamica del batch.
3. Emulazione Solo Software: La dimostrazione di un emulatore basato su CPU capace di modellare l'aritmetica specifica delle GPU (inclusi gli alberi di riduzione dei Tensor Core e le approssimazioni SFU) per prevedere gli output dell'inferenza LLM bit per bit.
4. Preservazione delle Prestazioni: Il metodo di verifica non richiede i compromessi sulle prestazioni associati all'uso di flag di determinismo o di kernel invarianti personalizzati; si basa sulla natura deterministica esistente dei normali motori di inferenza quando le condizioni sono fisse.

Significato e Rivendicazioni
Il documento conclude che la "negabilità plausibile" negli output dell'inferenza IA può essere rimossa. Riportando la dimensione del batch concorrente e i dettagli della configurazione insieme all'output, un prover può ridurre la verifica a un semplice controllo pass/fail contro una ricalcolazione bit-exact. Gli autori affermano che la sensibilità numerica degli output funge da impronta digitale ad alta fedeltà dello stack hardware e software del prover. Ciò consente una governance credibile degli avversari occulti, garantendo che qualsiasi deviazione dal calcolo dichiarato (ad esempio, steganografia nascosta o modifiche software non autorizzate) risulterebbe in un mismatch di bit rilevabile, a condizione che la configurazione di verifica tenga conto dei fattori di configurazione specifici identificati. Il lavoro suggerisce che il "non-determinismo" spesso citato come barriera alla verifica dell'IA è in realtà un artefatto deterministico e riproducibile dell'ambiente computazionale.