Reliable Reasoning with Large Language Models via Preference-Based Maximum Satisfiability

Riepilogo Tecnico: Ragionamento Affidabile con Modelli Linguistici di Grande Dimensione tramite Soddisfacibilità Massima Basata su Preferenze

Enunciato del Problema

I Modelli Linguistici di Grande Dimensione (LLM) dimostrano capacità solide nella comprensione del linguaggio naturale e nella generazione di codice, ma mostrano un'affidabilità significativa quando sono incaricati di problemi di ottimizzazione complessi che coinvolgono molteplici vincoli e preferenze definite dall'utente. In domini come la robotica e la logistica, dove la correttezza e l'ottimalità dimostrabile sono critiche, gli LLM spesso falliscono nel soddisfare vincoli rigidi o nel minimizzare funzioni obiettivo quando si affidano esclusivamente al ragionamento interno (ad esempio, Chain-of-Thought) o alla generazione diretta di risposte. Questi fallimenti derivano dalla natura combinatoria dell'ottimizzazione e dall'incapacità dell'LLM di eseguire un ragionamento esatto, portando a soluzioni non fattibili o sub-ottimali difficili da verificare. Inoltre, i metodi formali esistenti come la Soddisfacibilità Massima (MaxSAT) richiedono agli utenti di esprimere le preferenze in linguaggi specializzati e rigidi (ad esempio, PDDL), creando una barriera all'ingresso per i non esperti.

Metodologia

Il documento propone un approccio neuro-simbolico ibrido che esternalizza il ragionamento dall'LLM a un solver formale. Il paradigma centrale, definito "vibe coding", consiste nell'LLM che traduce descrizioni del problema in linguaggio naturale in codice Python eseguibile, che viene poi risolto da un solver MaxSAT esatto.

La pipeline proposta consiste nelle seguenti fasi:

1. Pianificazione Intermedia: Prima di generare il codice, all'LLM viene richiesto di produrre una descrizione simbolica strutturata delle variabili decisionali, dei vincoli rigidi e delle preferenze soft. Questo passaggio mira a migliorare l'accuratezza della modellazione imponendo una scomposizione sistematica del problema.
2. Generazione del Codice: L'LLM genera codice Python utilizzando l'API PySAT per codificare il problema come un'istanza MaxSAT parziale ponderata. I vincoli rigidi sono codificati come clausole rigide, mentre le preferenze dell'utente sono codificate come clausole soft ponderate.
3. Risoluzione MaxSAT: Il codice generato viene eseguito per invocare un solver MaxSAT (nello specifico RC2 da PySAT). Il solver garantisce che l'assegnazione restituita sia fattibile (soddisfa tutte le clausole rigide) e ottimale (minimizza il peso totale delle clausole soft non soddisfatte) rispetto al problema codificato.
4. Verifica: Per valutare il sistema senza fare affidamento sul ragionamento interno dell'LLM, gli autori costruiscono una codifica MaxSAT "canonica" per ogni istanza del problema. Questa codifica canonica funge da verità fondamentale (ground truth) solo per la verifica. La soluzione prodotta dal codice generato dall'LLM viene verificata rispetto a questa codifica canonica per controllare:
   • Fattibilità: La soluzione soddisfa tutti i vincoli rigidi?
   • Ottimalità: La soluzione raggiunge lo stesso valore obiettivo della soluzione ottimale canonica?
   • Nota: Questa verifica consente codifiche alternative e soluzioni ottimali multiple, purché siano corrette secondo la semantica di riferimento.
5. Ciclo di Feedback: Se il codice non viene eseguito o produce un errore, il messaggio di errore viene restituito all'LLM per il raffinamento. Crucialmente, i risultati della verifica canonica (controlli di fattibilità/ottimalità) non vengono utilizzati come feedback al modello durante il processo di generazione per prevenire la perdita di dati o l'overfitting sul riferimento.

Contributi Chiave

• Framework Neuro-Simbolico: Gli autori presentano un metodo in cui gli LLM agiscono come interfacce in linguaggio naturale per solver MaxSAT parziali ponderati, traducendo l'intento dell'utente in formulazioni MaxSAT formali tramite generazione di codice.
• Verifica Indipendente: Lo studio introduce un protocollo di valutazione che verifica le soluzioni generate dall'LLM rispetto a una codifica canonica sia per la fattibilità che per l'ottimalità, disaccoppiando la validità della soluzione dalla correttezza del ragionamento interno dell'LLM.
• Analisi Empirica delle Preferenze: Il documento analizza come diverse configurazioni di preferenze definite dall'utente influenzino le prestazioni del ragionamento dell'LLM su vari problemi di ottimizzazione con vincoli.
• Valutazione della Pianificazione Intermedia: Il lavoro indaga l'efficacia di un passaggio di pianificazione intermedia, rilevando che migliora le prestazioni per modelli più forti ma può introdurre propagazione di errori per modelli più deboli.

Risultati Sperimentali

L'approccio è stato valutato su tre famiglie di compiti di ragionamento basati su preferenze: Massimo Insieme Indipendente (MIS), Programmazione e Copertura degli Insiemi. Il dataset comprendeva 300 istanze (25 per famiglia × 4 varianti di preferenza) testate su quattro LLM (GEMINI-3.1-PRO, GPT-5.5, LLAMA3.3 e QWEN3-CODER).

• Prestazioni di Base: Le basi di risposta diretta e Chain-of-Thought (CoT) hanno prestazioni scarse, raggiungendo spesso tassi di accettazione dello 0% sui compiti MIS e di Programmazione. Le basi Program-of-Thought (PoT) hanno mostrato lievi miglioramenti ma sono rimaste significativamente inferiori all'approccio basato su MaxSAT.
• Prestazioni della Pipeline MaxSAT: La pipeline proposta basata su MaxSAT ha raggiunto tassi di accettazione sostanzialmente più elevati. Per modelli forti come GEMINI-3.1-PRO e GPT-5.5, i tassi di accettazione hanno superato l'80% sui compiti di Copertura degli Insiemi e hanno raggiunto circa il 56–59% sui compiti di Programmazione e MIS quando è stata utilizzata la pianificazione intermedia.
• Impatto della Pianificazione: La pianificazione intermedia ha migliorato costantemente le prestazioni per i modelli più forti (ad esempio, GEMINI-3.1-PRO è passato dal 36% al 56% su MIS). Tuttavia, per i modelli più deboli (LLAMA3.3, QWEN3-CODER), la pianificazione ha talvolta peggiorato le prestazioni, suggerendo che può verificarsi una propagazione di errori se il modello non riesce a tradurre fedelmente il piano in codice eseguibile.
• Sensibilità alle Preferenze: Sebbene le preferenze dell'utente abbiano generalmente ridotto i tassi di accettazione rispetto all'impostazione "nessuna preferenza", l'approccio basato su MaxSAT è rimasto più robusto rispetto alle basi su tutte le varianti di preferenza.

Significato e Affermazioni

Il documento afferma che il suo contributo principale non è una nuova architettura di solver, ma una dimostrazione empirica e metodologica dell'uso degli LLM come interfacce per solver formali per l'ottimizzazione consapevole delle preferenze. Gli autori affermano che:

1. L'Esternalizzazione è Fondamentale: Non ci si dovrebbe fidare che gli LLM eseguano ragionamenti di ottimizzazione internamente; al contrario, sono altamente efficaci nel tradurre vincoli in linguaggio naturale in codice eseguibile.
2. Affidabilità tramite Solver: Delegando l'ottimizzazione e la verifica a solver MaxSAT corretti e completi, il sistema ottiene garanzie formali di fattibilità e ottimalità che il puro ragionamento LLM non può fornire.
3. Robustezza: La combinazione dell'interpretazione semantica guidata dall'LLM e della risoluzione MaxSAT consente un processo decisionale robusto e verificabile che accoglie le preferenze dell'utente senza richiedere linguaggi di dominio specializzati.

Gli autori concludono che separare l'interpretazione semantica (LLM) dall'ottimizzazione formale (solver MaxSAT) è una direzione promettente per costruire sistemi decisionali affidabili e rivolti all'utente, in particolare in campi dove la correttezza è fondamentale. Osservano che il lavoro futuro esplorerà impostazioni interattive in cui gli utenti possono affinare iterativamente le preferenze con il supporto di questo ciclo neuro-simbolico.