L'allineamento non basterà mai.

Nei modelli linguistici, l'allineamento è l'addestramento che segue il pre-addestramento: instruction tuning, poi apprendimento per rinforzo dal feedback umano o dell'IA (RLHF, DPO e loro varianti).^{1, 2} Il modello viene premiato per le risposte che i valutatori preferiscono: utili, cortesi e conformi alle regole ricevute. È ciò che ha trasformato semplici predittori di testo in assistenti utilizzabili, e continua a migliorare.

L'allineamento però agisce sulle tendenze e non sulle singole risposte. Rende più probabile una buona risposta senza dirvi se questa è corretta. E poiché i valutatori premiano le risposte che sembrano giuste, un modello può imparare a mostrarsi sicuro, o a dare ragione a chi chiede, quando non dovrebbe: è il problema noto come sycophancy, o compiacenza.³ Con un modello ben allineato si lavora meglio, ma resta incapace di dimostrare che un numero è corretto.

In nessun altro ambito la fiducia funziona così. Non ci fidiamo di un ufficio contabilità perché il personale è ben formato, ma grazie alle procedure: la revisione, la doppia firma, i conti che devono quadrare.

Su larga scala la fiducia si basa sulla possibilità di controllare, e non sulla qualità dell'addestramento di un sistema.

Il linguaggio naturale è il modo in cui pensiamo ad alta voce, ed è ambiguo per natura. Ogni volta che la posta in gioco è cresciuta, le persone hanno costruito qualcosa di più rigoroso al di sopra. I numeri e la contabilità, perché un debito significasse la stessa cosa per entrambe le parti. L'algebra, perché un risultato potesse essere ricavato di nuovo da chi non si fidava del suo autore. Il diritto scritto, la logica, la dimostrazione e infine i linguaggi di programmazione.

Nessuno di questi ha sostituito l'intuizione. Un matematico intuisce ancora il teorema prima di dimostrarlo. I sistemi formali ci hanno dato un modo per comunicare senza dover essere creduti: il ragionamento accompagna la conclusione, e un estraneo può controllarlo.

I modelli linguistici si trovano dove eravamo noi prima di quel passo. Sono fluenti, veloci, spesso nel giusto, e non hanno modo di consegnare il loro ragionamento in una forma che chiunque possa verificare.

I sistemi formali permettono alle persone di comunicare senza dover essere credute.

È ciò che intendiamo per IA neuro-simbolica. La parte neurale fa ciò in cui è brava: capire una domanda posta con parole comuni, nel contesto di un'azienda. La parte simbolica fa ciò che il linguaggio non può fare: formula la risposta come una regola che si può leggere, verificare, rieseguire e confrontare.

Il layer formale dà alla macchina lo strumento che le persone hanno costruito per sé. Un modello che scrive una regola in un linguaggio logico deve impegnarsi: su quali ordini contano, in quale periodo, su quale colonna. Quell'impegno può poi essere controllato da un verificatore, dai dati e dalla persona responsabile del numero.

Una regola inoltre dura nel tempo. Un paragrafo di spiegazione generata scompare con la conversazione. Una regola viene conservata, ha un nome e su di essa si costruisce, come i matematici conservano un lemma: un piccolo risultato tenuto da parte perché argomentazioni più ampie possano poggiarvi sopra. Conservata anche in git, così che la storia del ragionamento di un'azienda possa essere sottoposta ad audit come la storia del suo codice: chi ha deciso che cosa, e quando.

Il modello traduce. Il layer formale ragiona. È questo che rende il ragionamento verificabile.

Succederà, ed è l'argomento più forte a favore di un layer formale. A un modello più capace si affidano compiti più ampi e più autonomia, e produce più conclusioni di quante chiunque possa rivedere leggendole. Il divario tra ciò che un modello può produrre e ciò che una persona può controllare cresce a ogni generazione.

Leggere la spiegazione del modello è il primo controllo a smettere di funzionare. Quando un sistema ragiona meglio della persona che lo rivede, quella persona non sa più distinguere un argomento solido da uno convincente. Gli unici controlli che tengono il passo sono quelli che non dipendono dall'intelligenza di chi controlla: un verificatore che applica regole fisse, una query che gira sui dati, un controesempio che esiste oppure no.

La matematica ci è già passata. La dimostrazione del teorema dei quattro colori di Appel e Haken, nel 1976, si basava su calcoli al computer troppo lunghi per essere controllati a mano. Nel 2005 Georges Gonthier e Benjamin Werner l'hanno verificata formalmente nel dimostratore interattivo Coq, così che resta da considerare affidabile solo il piccolo nucleo di Coq.⁴ Samuel Ferguson e Thomas Hales hanno dimostrato la congettura di Keplero nel 1998, ma la dimostrazione completa è stata pubblicata solo nel 2006, perché i revisori non riuscivano a verificarne la parte informatica. Il progetto Flyspeck l'ha poi verificata formalmente nei dimostratori HOL Light e Isabelle, e i suoi controlli si sono conclusi nel 2014.⁵ Man mano che le dimostrazioni superavano ciò che le persone potevano leggere, la verifica formale è diventata più importante.

Controllare costa anche meno che trovare. Un verificatore non deve essere intelligente quanto il modello; deve solo confermare, passo dopo passo, ciò che il modello afferma. Un modello più intelligente quindi non è in concorrenza con il layer formale. Scrive regole migliori, più in fretta, e il layer trasforma ciascuna di esse in un risultato su cui chiunque può contare.

Più il modello è capace, più il suo lavoro ha bisogno di un controllo che non dipenda dalla fiducia nel modello.

Che un secondo modello possa fare da giudice al primo. È un'opinione in più, con gli stessi punti deboli. La verifica deve venire da qualcosa di natura diversa rispetto a ciò che viene verificato.

Che bastino delle protezioni aggiunte a posteriori. Filtrare ciò che un modello ha detto è diverso dal vincolare ciò che può affermare. Il controllo deve avvenire prima che la risposta venga data.

Ad aziende la cui conoscenza non è più dispersa tra persone, dashboard e documenti in disaccordo tra loro, ma scritta una volta come definizioni che si eseguono. Ad agenti che condividono una memoria fatta di regole verificate, e che possono essere sostituiti senza perdere ciò che è stato appreso. A un'IA che si adotta come qualsiasi strumento serio: perché si vede come arriva al suo risultato.

Stiamo costruendo in modo aperto i componenti di quel layer, e il prodotto che li mette al lavoro.