Riepilogo Tecnico: Formalizzare, non Ottimizzare: La Trappola Euristica nei Risolutori Combinatori Generati da LLM

Enunciato del Problema

I Large Language Models (LLM) faticano a risolvere problemi combinatori complessi attraverso un ragionamento autoregressivo diretto a causa del "collo di bottiglia del ragionamento" intrinseco nella navigazione di ampi spazi di ricerca e nel mantenimento della coerenza globale su vincoli a lungo orizzonte temporale. Sebbene recenti approcci neuro-simbolici tentino di mitigare questo problema chiedendo agli LLM di sintetizzare risolutori eseguibili, due domande critiche di progettazione rimangono irrisolte:

1. Rappresentazione: Come dovrebbe rappresentare l'LLM il risolutore? Un approccio algoritmico nativo (Python) è superiore alla modellazione dichiarativa (MiniZinc) o all'integrazione con API di risolutori (Python + OR-Tools)?
2. Ottimizzazione: L'LLM dovrebbe essere sollecitato a ottimizzare attivamente il processo di ricerca (ad esempio tramite euristiche, potature o limiti), oppure dovrebbe limitarsi a formalizzare rigorosamente il problema per un backend verificato?

I lavori precedenti valutano spesso queste impostazioni in isolamento o a livello aggregato di problema, fallendo nel decomporre gli esiti a livello di istanza in correttezza, validità dello schema e fedeltà. Inoltre, l'impatto della sollecitazione orientata all'efficienza sull'affidabilità dei risolutori generati non è stato sottoposto a un audit sistematico.

Metodologia

Gli autori introducono CP-SynC-XL, un benchmark che estende il dataset CP-SynC includendo 100 Problemi di Soddisfacimento di Vincoli (CSP) e Problemi di Ottimizzazione di Vincoli (COP) eterogenei, per un totale di 4.577 istanze parametriche. Lo studio valuta tre LLM all'avanguardia (GPT-5.3-CODEX, GEMINI 3.1 PRO, DEEPSEEK-V3.2) attraverso tre paradigmi di costruzione del risolutore:

1. Ricerca Algoritmica Nativa (Python): L'LLM genera un algoritmo Python autonomo utilizzando solo la libreria standard, progettando l'intera procedura di ricerca (ad esempio, branch-and-bound, programmazione dinamica).
2. Modellazione dei Vincoli tramite API Python (Python + OR-Tools): L'LLM codifica variabili, vincoli e obiettivi utilizzando l'API Python CP-SAT di OR-Tools, delegando la ricerca al risolutore.
3. Modellazione Dichiarativa dei Vincoli (MiniZinc + OR-Tools): L'LLM genera un modello MiniZinc, che viene poi compilato e risolto dallo stesso backend CP-SAT di OR-Tools.

Lo studio adotta un disegno fattoriale controllato confrontando un prompt di base (che chiede solo correttezza) con un prompt euristico (che richiede esplicitamente una progettazione orientata all'efficienza, come limiti più stretti, potature o annotazioni di ricerca).

La pipeline di valutazione include:

• Protocollo di Raffinamento: Un ciclo iterativo di raffinamento a quattro round in cui le esecuzioni fallite (crash, timeout, errori di formato) vengono reinviate all'LLM.
• Metriche:
  • Fornito: Frazione di istanze che restituiscono un output conforme allo schema.
  • Corretto: Frazione degli output forniti che superano il verificatore di riferimento.
  • Fedeltà: Il rapporto Corretto/Fornito (la quota di soluzioni restituite che sono effettivamente valide).
• Audit a Livello di Codice: Un'analisi accoppiata dei risolutori di base rispetto a quelli euristici per identificare specifici modi di fallimento e pattern di codice.

Contributi Chiave

1. Il Benchmark CP-SynC-XL

Gli autori introducono un benchmark su larga scala (4.577 istanze) progettato per valutare i risolutori sintetizzati dagli LLM a livello di istanza, separando gli output forniti dalla correttezza verificata per misurare la fedeltà condizionata.

2. Divergenza Rappresentazionale

Lo studio rivela una significativa divergenza nelle prestazioni del risolutore in base alla superficie di modellazione, anche quando il backend del risolutore sottostante (OR-Tools CP-SAT) è identico:

• Python + OR-Tools ottiene la correttezza assoluta più elevata tra tutti gli LLM.
• MiniZinc + OR-Tools mostra una copertura assoluta inferiore (più timeout di "nessuna soluzione") nonostante lo stesso backend, suggerendo un collo di bottiglia nella fluidità dell'LLM con la superficie dichiarativa piuttosto che nelle capacità del risolutore.
• Python Nativo presenta il tasso più alto di "fallimenti silenziosi"—restituendo soluzioni valide a livello di schema che falliscono la verifica—indicando che gli LLM faticano a progettare algoritmi di ricerca completi e corretti da zero.

3. La Trappola Euristica

Il documento identifica una "trappola euristica" in cui sollecitare gli LLM a ottimizzare la ricerca produce risultati inaffidabili:

• Guadagni Marginali, Alto Rischio: I prompt euristici producono solo piccoli guadagni mediani di velocità (1,03–1,12×) ma inducono un effetto fortemente bimodale. Mentre alcune istanze accelerano, molte altre rallentano, e la correttezza crolla bruscamente su una lunga coda di problemi.
• Sei Modi di Fallimento: Un audit a livello di codice identifica sei modi di fallimento specifici del paradigma attivati dai prompt euristici:
  • Limiti Non Verificati (Python + OR-Tools): Gli LLM inseriscono limiti "stretti" che non sono teoremi, causando inammissibilità.
  • Propagazione Indebolita (Python + OR-Tools): Riscritture semanticamente equivalenti (ad esempio, Big-M) che paralizzano il motore di propagazione del risolutore.
  • Innesco Rigido (Python + OR-Tools): Conversione di candidati euristici in vincoli rigidi, rimuovendo regioni ammissibili.
  • Perdita di Completezza (Python): Sostituzione della ricerca completa con ricerca locale incompleta o limiti di iterazione.
  • Collasso COP→SAT (MiniZinc): Assunzione errata di un valore ottimo e conversione dell'ottimizzazione in soddisfacimento.
  • Macchinario Ridondante (MiniZinc): Aggiunta di vincoli ausiliari eccessivi che sovraccaricano il processo di appiattimento del risolutore.

Risultati

• Classifica della Correttezza: Python + OR-Tools > Python ≳ MiniZinc + OR-Tools. Delegare la ricerca a un backend verificato (CP-SAT) supera significativamente la progettazione algoritmica nativa.
• Classifica della Fedeltà: MiniZinc + OR-Tools > Python + OR-Tools > Python. Quando viene fornita una soluzione, i modelli MiniZinc hanno la maggiore probabilità di essere corretti (massima fedeltà condizionata) perché il sistema di tipi del linguaggio e i controlli di benformatezza filtrano molti errori di codifica prima dell'esecuzione del risolutore. Python nativo è il meno fedele, spesso restituendo soluzioni confidenti ma errate.
• Impatto Euristico: Su LLM più potenti (GPT-5.3-CODEX, GEMINI 3.1 PRO), i prompt euristici producono guadagni marginali e inconsistenti (±3,6 punti percentuali). Su LLM più deboli (DEEPSEEK-V3.2), i prompt euristici causano un degrado significativo (ad esempio, -7,4 punti percentuali di correttezza su Python + OR-Tools).
• Analisi dei Fallimenti: Il modo di fallimento dominante della baseline è UNSAT (il risolutore restituisce una soluzione che il verificatore di riferimento rifiuta), causato principalmente da traduzioni errate dal linguaggio naturale al linguaggio formale (ad esempio, omissione di vincoli, interpretazione errata degli schemi di output). I prompt euristici esacerbano questo fenomeno introducendo limiti non verificati e sovrasollecitando il modello.

Significato e Principi di Progettazione

Il documento sostiene che il principale collo di bottiglia per i risolutori combinatori generati da LLM è la fluidità della superficie di modellazione, non la capacità del risolutore sottostante. I risultati supportano un principio di progettazione conservativo:

"Formalizzare, non Ottimizzare."

Gli LLM dovrebbero essere utilizzati principalmente per formalizzare variabili, vincoli e obiettivi per risolutori verificati. I tentativi di far generare agli LLM ottimizzazioni di ricerca (euristiche, limiti, strategie di potatura) dovrebbero essere trattati con scetticismo. Il documento conclude che qualsiasi ottimizzazione di ricerca autrice da un LLM deve essere validata indipendentemente prima dell'uso, poiché la "trappola euristica" introduce frequentemente limiti non verificati o sostituzioni algoritmiche che riducono sia la correttezza che la fedeltà. La strategia più affidabile è mantenere l'LLM vicino all'interfaccia di formalizzazione e affidarsi alla macchina nativa del risolutore per la ricerca.