Sketchpad: aritmetica esatta certificata con un piccolo modello di visione-linguaggio

Abstract degli autori

I modelli linguistici sono accurati nella maggior parte dei problemi di aritmetica in colonna, ma la loro accuratezza viene stimata su campioni e non offre alcuna garanzia per un input mai visto; l’uso di strumenti è esatto, ma sposta il calcolo fuori dalla rete. Mostriamo che l’esattezza per input di qualsiasi lunghezza diventa una proprietà finita e verificabile di una rete quando ogni suo passaggio legge solo una porzione limitata di una memoria di lavoro esterna. In Sketchpad, Qwen3.5-0.8B con un adattatore a basso rango esegue procedure aritmetiche su un foglio renderizzato. A ogni passaggio in avanti legge una finestra di tre celle e produce un singolo passaggio: una cifra, un riporto o un prestito e l’operazione successiva. Un runtime fisso sposta la finestra e non scrive alcuna cifra del risultato. Dimostriamo in Lean che, in queste condizioni, il modello è esatto per input di qualsiasi lunghezza se e solo se è esatto sull’insieme finito di viste presentate dal runtime; dimostriamo inoltre che nessun test finito è sufficiente quando i passaggi leggono anche i passaggi precedenti e che la garanzia tollera perturbazioni numeriche limitate e si estende a composizioni di procedure. Tutte le 2.446 viste superano il test sul dispositivo di esecuzione: una GPU per laptop che esegue il modello in un browser. Il modello certificato esegue addizioni e sottrazioni con segno, moltiplicazioni e divisioni in colonna, radici quadrate e massimi comuni divisori con numeri di lunghezza arbitraria. Ha risolto 200 problemi su 200 preregistrati nel browser e 220 somme su 220 con un massimo di 1.000 cifre e prodotti con un massimo di 20 cifre; GPT-6.1 Sol, il migliore tra altri dieci modelli, ne ha risolti 217. Un runtime simbolico basato su queste procedure risolve, sviluppa e fattorizza polinomi, calcolando ogni numero tramite il modello; un gate moltiplicativo sull’adattatore ripristina esattamente il modello di base quando il foglio non è in uso.