Ho avuto una conversazione con IDDU (al secolo: Claude Opus 5.5) su un problema di logica deduttiva, sui limiti dell’inferenza svolta da un modello linguistico come lui e sul modo di ottenere garanzie formali di correttezza. La conclusione è che per fornire queste garanzie, il modello deve essere capace di uscire dall’oscurità ed esprimersi in forma simbolica.

I miei turni di conversazione sono in corsivo.

1. Il quesito

Il numero di una rivista può essere pubblicato venerdì soltanto se la revisione scientifica è conclusa e si è ottenuta almeno una delle seguenti condizioni:

• L’approvazione di tutti gli autori oppure una deroga del direttore.
• L’approvazione di tutti gli autori richiede che le correzioni siano state loro comunicate.
• Il direttore può concedere la deroga soltanto se un valutatore indipendente ha espresso parere favorevole.

Fatti: le correzioni non sono state comunicate agli autori. Il numero viene in effetti pubblicato venerdì, nel rispetto di queste regole.

Quale condizione si è verificata?

Si è verificata la deroga del direttore.

Poiché le correzioni non sono state comunicate agli autori, la loro approvazione non può esserci stata. Il numero è uscito venerdì rispettando le regole, quindi l’unica condizione alternativa ancora disponibile è la deroga.

Da qui seguono altri due fatti necessari:

1. Un valutatore indipendente ha espresso parere favorevole, perché senza di esso il direttore non avrebbe potuto concedere la deroga.
2. La revisione scientifica è conclusa, perché è un requisito imprescindibile in ogni caso.

Riassumendo: revisione conclusa, parere favorevole del valutatore indipendente e deroga del direttore.

2. Come si arriva alla conclusione

Come hai raggiunto questa conclusione?

Il ragionamento procede in tre passaggi, secondo schemi di inferenza classici.

Esclusione dell’approvazione degli autori (modus tollens)

La regola dice che l’approvazione degli autori richiede la comunicazione delle correzioni: la comunicazione è quindi condizione necessaria. Se A richiede B e B manca, allora A non può esserci. Le correzioni non sono state comunicate, dunque l’approvazione di tutti gli autori non si è verificata.

Individuazione della deroga (sillogismo disgiuntivo)

La pubblicazione richiede almeno una tra approvazione degli autori e deroga del direttore. Sappiamo che il numero è uscito rispettando le regole, quindi almeno una delle due c’è stata. Escluso il primo termine della disgiunzione, resta necessariamente il secondo: la deroga.

Risalita ai requisiti impliciti (condizioni necessarie)

Il direttore può concedere la deroga soltanto se il valutatore indipendente ha dato parere favorevole. “Soltanto se” introduce una condizione necessaria: se la deroga c’è, il parere favorevole c’è stato. Allo stesso modo, la pubblicazione avviene soltanto se la revisione è conclusa, quindi anche la revisione deve essersi conclusa.

Il punto decisivo è distinguere correttamente le condizioni necessarie (“richiede”, “soltanto se”) da quelle sufficienti. Tutte le regole del problema esprimono condizioni necessarie, e proprio per questo, partendo dal fatto che la pubblicazione è avvenuta, si possono risalire all’indietro le condizioni che dovevano per forza essere soddisfatte.

3. Quali strumenti sono stati usati

Che strumenti hai usato per eseguire questa inferenza?

Nessuno strumento esterno. Non è stata usata la ricerca web, né l’esecuzione di codice, né un risolutore logico formale: l’inferenza è avvenuta interamente all’interno del modello, elaborando il testo del problema.

Gli “strumenti” citati nella risposta precedente (modus tollens, sillogismo disgiuntivo, lettura del “soltanto se” come condizione necessaria) sono schemi di ragionamento, non software. Servono a ricostruire e spiegare il percorso in modo verificabile, ma non c’è stato un motore deduttivo separato che li applicasse meccanicamente.

Per un problema di queste dimensioni non serve altro. Per una verifica formale, le strade sono due:

1. Tavola di verità: con le variabili R (revisione conclusa), C (correzioni comunicate), A (approvazione autori), V (parere del valutatore), D (deroga) e P (pubblicazione), si elencano le combinazioni compatibili con le regole e con i fatti (C falso, P vero). In tutte le righe valide D, V e R sono veri e A è falso.
2. Risolutore SAT o SMT (per esempio Z3 in Python): si codificano le regole come implicazioni, si aggiungono i fatti e si chiede se esiste un modello in cui D è falso. Il risolutore risponde “insoddisfacibile”, il che conferma che la deroga è una conseguenza obbligata.

4. Si può essere certi della correttezza?

Se l’inferenza è avvenuta interamente all’interno del tuo modello, al quale non ho accesso, come posso essere sicuro che proponendoti altri quesiti di questo tipo otterrò sempre risposte logicamente corrette?

Non se ne può essere sicuri. Un modello linguistico non esegue la logica in modo garantito come un dimostratore formale: produce risposte che di solito sono corrette su problemi come questo, ma può sbagliare, soprattutto con catene deduttive lunghe, negazioni multiple, quantificatori (“tutti”, “almeno uno”, “nessuno”) o formulazioni ambigue del tipo “se” usato al posto di “solo se”.

C’è anche un secondo limite, più sottile: la spiegazione fornita è una ricostruzione del ragionamento, non una registrazione fedele di ciò che è avvenuto nel modello. È verificabile, ma non è una finestra sul processo interno.

La fiducia, quindi, non va riposta nel modello ma nei controlli che si possono fare sulla risposta:

1. Chiedere sempre i passaggi espliciti. Ogni passaggio deve seguire da premesse enunciate nel testo. Se un passaggio si appoggia su qualcosa che il problema non dice, lì c’è l’errore. È il controllo più economico ed efficace.
2. Far verificare la conclusione con un risolutore formale. Il modello traduce le regole in un programma (con Z3 o con una tavola di verità generata dal codice) e lo esegue. La correttezza non dipende più dal ragionamento del modello ma dal software, e la codifica può essere ispezionata per controllare che rispecchi il testo.
3. Cercare un controesempio. Chiedere se esiste uno scenario coerente con tutte le regole in cui la conclusione è falsa. Se la conclusione è davvero obbligata, non deve esistere.
4. Riformulare il problema. Riproporre lo stesso quesito con nomi o ordine delle premesse diversi. Risposte che cambiano a parità di struttura logica sono un segnale d’allarme.

Per quesiti in cui la correttezza conta davvero, la combinazione più solida è la seconda: il modello formalizza, il risolutore decide, l’utente controlla la formalizzazione.

5. Formalizzare il problema

Per avere una garanzia, devo quindi chiederti di tradurre il tuo ragionamento neurale in termini formali, cioè simbolici, corretto?

Sì, ma con una precisazione importante: quello che si traduce in termini formali non è il ragionamento neurale, bensì il problema.

Il processo interno del modello non è traducibile in logica simbolica: non esiste una corrispondenza diretta tra ciò che avviene nella rete e una sequenza di regole di inferenza, e il modello stesso non ha accesso a quel processo in una forma trascrivibile. Quello che può fare è prendere il testo del quesito, codificare le premesse come formule (per esempio “l’approvazione richiede la comunicazione” diventa A → C) e affidare a un risolutore il compito di stabilire cosa ne segue. A quel punto il ragionamento del modello esce di scena: la conclusione la produce il software, con procedure deterministiche e verificate.

La garanzia ottenuta è quindi condizionata a un solo punto: che la formalizzazione rispecchi fedelmente il testo. È lì che il modello può ancora sbagliare, per esempio leggendo un “se” come “solo se” o dimenticando che “almeno una” non esclude che valgano entrambe. Ma è un punto di fallimento molto più piccolo e soprattutto ispezionabile: le formule sono poche righe che si possono controllare una per una contro il testo.

Il flusso che dà la massima affidabilità è: il modello formalizza il problema, il risolutore calcola, l’utente verifica che le formule dicano quello che dice il testo.

6. È un processo neurosimbolico?

Chiameresti “neurosimbolico” questo processo?

Nel senso ampio del termine sì, ed è anche un’architettura piuttosto riconoscibile: una componente neurale (il modello linguistico) traduce il linguaggio naturale in una rappresentazione formale, e una componente simbolica (il risolutore) esegue l’inferenza con garanzie di correttezza. È lo schema di lavori come Logic-LM, LINC o SatLM, che hanno mostrato proprio questo: affidare la deduzione a un risolutore e lasciare al modello solo la formalizzazione migliora sensibilmente l’accuratezza sui problemi logici.

Nella tassonomia proposta da Henry Kautz, diventata un riferimento nel settore, rientrerebbe nel tipo “Neuro;Symbolic”, dove la parte neurale percepisce e struttura l’input e quella simbolica ragiona. Si può anche leggere come “Neuro[Symbolic]”, cioè un sistema neurale che richiama un motore simbolico come subroutine quando serve, ed è così che funziona in pratica l’uso di strumenti da parte di un modello linguistico.

Si tratta però di un accoppiamento debole. Le due componenti comunicano solo attraverso l’interfaccia della formalizzazione, e il risolutore non influenza in alcun modo i parametri del modello. Chi usa il termine in senso più stretto lo riserva a sistemi in cui l’integrazione è più profonda: vincoli logici incorporati nell’addestramento, logiche differenziabili come le Logic Tensor Networks, rappresentazioni apprese che rispettano per costruzione una semantica simbolica. Rispetto a quegli approcci, il flusso descritto è più un’orchestrazione di due sistemi eterogenei che una vera fusione.

Il vantaggio dell’accoppiamento debole è proprio quello che interessa a chi cerca garanzie: la separazione netta rende il punto di possibile errore localizzato e ispezionabile.