Resource-Aware Neuro-Symbolic Reasoning for Local Small Language Models

Sintesi Tecnica: Ragionamento Neuro-Simbolico Consapevole delle Risorse per Small Language Models Locali

Definizione del Problema
Gli Small Language Models (SLM) offrono i vantaggi dell'esecuzione locale, inclusi la privacy, la disponibilità offline e la riduzione dei costi operativi. Tuttavia, la loro capacità limitata spesso richiede strategie come il campionamento ripetuto (self-consistency) per ottenere un ragionamento affidabile, il che moltiplica le chiamate al modello locale, la generazione di token e la latenza seriale. Sebbene esistano approcci neuro-simbolici, essi spesso presuppongono capacità di dimostrazione di teoremi generali o ignorano i vincoli specifici di risorse dell'hardware consumer. Il problema centrale affrontato è se una pipeline neuro-simbolica limitata e verificabile possa sostituire il campionamento neurale locale ripetuto per compiti di ragionamento strutturato senza sacrificare l'accuratezza, specificamente entro i vincoli degli SLM locali.

Metodologia: La Pipeline VFR-LLM
Gli autori propongono la pipeline Verifiable Formalization and Repair (VFR-LLM), un'architettura a cinque stadi progettata per delegare il ragionamento dal modello neurale a un risolutore deterministico:

1. Formalizzazione: L'SLM traduce un problema in linguaggio naturale in una rappresentazione di regole e vincoli a dominio finito tipizzata. Questo linguaggio intermedio include fatti radicati, regole di tipo Horn sicure e vincoli a dominio finito (ad esempio, ordinamento, posizioni assolute). Fondamentalmente, il modello deve fornire spazi sorgente (source spans) che colleghino ogni vincolo estratto al testo originale.
2. Controllo di Copertura: Uno strato di verifica ispeziona la formalizzazione per garantire che ogni vincolo sia radicato nel testo sorgente e che non esistano regole non supportate o entità sconosciute.
3. Esecuzione del Solver: Un risolutore deterministico (un risolutore enumerativo esatto per i compiti valutati) elabora il programma formalizzato per trovare un'assegnazione soddisfacente (ad esempio, un ordinamento totale di entità).
4. Riparazione (Repair): Se il solver fallisce o se le diagnostiche indicano errori di formalizzazione (ad esempio, argomenti invertiti o problemi di sintassi), un modulo di riparazione deterministico applica modifiche locali basandosi esclusivamente sugli spazi sorgente e sulle diagnostiche del solver. Non vengono utilizzate ulteriori chiamate al modello o risposte corrette (gold answers) durante questo passaggio.
5. Generazione della Risposta: La risposta finale viene derivata dall'output del solver, collegata ai vincoli verificati.

Il formalismo target è intenzionalmente modesto: un linguaggio simile a Datalog con domini finiti, escludendo simboli di funzione e quantificazione illimitata per garantire che il carico di traduzione rimanga gestibile per i modelli piccoli.

Contributi Chiave

1. Rappresentazione Tracciabile: Definizione di un formalismo di regole e vincoli a dominio finito tipizzato che richiede spazi sorgente per ogni fatto estratto, consentendo l'auditabilità del passaggio di traduzione.
2. Ciclo di Verifica e Riparazione: Implementazione di una pipeline che utilizza la validazione radicata sulla sorgente e la riparazione deterministica per identificare e correggere i fallimenti di formalizzazione prima dell'esecuzione del solver, anziché fare affidamento sul campionamento ripetuto.
3. Matrice di Valutazione Locale: Una valutazione completa utilizzando LM Studio su Apple Silicon (M3 Pro) con tre famiglie di modelli: Qwen3-4B, Microsoft Phi-4-mini-reasoning e Gemma-3n-E4B. I benchmark includono compiti di pura precedenza generati, compiti di precedenza tipizzati generati e due sottoinsiemi derivati da BIG-Bench Hard (Logical Deduction - pairwise ed esteso).
4. Confronto Consapevole delle Risorse: Un confronto rigoroso contro la self-consistency seriale ($k=5$) e una baseline di self-consistency adattiva consapevole dei costi, misurando accuratezza, chiamate al modello, token totali e latenza seriale.

Risultati
I risultati empirici rivelano un'efficacia limitata e dipendente dal modello dell'approccio VFR-LLM:

• Performance di Qwen3-4B:

  • Pure Precedence (Pura Precedenza): Ha raggiunto un'accuratezza di 0.983 con una sola chiamata al modello, superando significativamente la self-consistency seriale (accuratezza 0.700, 5 chiamate) e riducendo i token totali del 34,4%.
  • BBH-Extended (Sorgente Pubblica): Ha raggiunto un'accuratezza di 0.933 rispetto allo 0.283 della self-consistency e allo 0.317 della risposta diretta. Sebbene i token totali siano aumentati leggermente a causa della lunghezza della formalizzazione, il metodo ha ridotto le chiamate al modello (1 vs 5) e la latenza seriale (11.32s vs 16.54s).
  • Typed Constraints (Vincoli Tipizzati): Le performance sono state "bloccate" dalla risposta diretta, che rimaneva più accurata ed economica in questi specifici strati.

• Performance di Gemma-3n-E4B:

  • Ha mostrato forti miglioramenti nei compiti di pure-precedence (0.683 vs 0.367 per la self-consistency).
  • I risultati sui compiti BBH-extended sono stati marginali (0.375 vs 0.350 per la risposta diretta), con un guadagno di accuratezza non statisticamente significativo.
  • I vincoli tipizzati hanno mostrato risultati misti, con una latenza spesso superiore alla risposta diretta.

• Phi-4-mini-reasoning:

  • Ha dimostrato gravi fallimenti di formalizzazione sui vincoli tipizzati, risultando in esiti negativi rispetto alla risposta diretta.

• Controlli di Robustezza:

  • Baseline Adattiva: Anche confrontato con una baseline di self-consistency adattiva consapevole dei costi (che riduce le chiamate da 5 a circa 4.2), VFR-LLM ha mantenuto un vantaggio significativo in termini di accuratezza su compiti di precedenza e BBH-extended per Qwen.
  • Tracciabilità: Un'alta accuratezza è stata fortemente correlata con alti tassi di "piena tracciabilità" (vincoli radicati nella sorgente). Qwen ha raggiunto un tasso di tracciabilità di 0.942 su BBH-extended, mentre Gemma ha raggiunto solo 0.292, spiegando il divario di performance.
  • Ablazioni Deterministiche: Il solver a dominio finito tipizzato ha risolto il 100% degli istanze BBH-extended, mentre un solver di sola precedenza ne ha risolte solo il 20.8%, confermando la necessità del formalismo esteso per questi compiti.

Significatività e Rivendicazioni
Il documento evita esplicitamente di affermare che il ragionamento simbolico migliori universalmente le performance dei modelli linguistici locali o riduca il calcolo per tutti i compiti. Invece, stabilisce una rivendicazione limitata:

1. Riduzione Condizionale delle Risorse: VFR-LLM è un'alternativa valida e consapevole delle risorse alla self-consistency seriale per compiti strutturati con vincoli espliciti (specificamente l'ordinamento e la logica a dominio finito) dove la risposta diretta è insufficientemente accurata.
2. Dipendenza dal Modello: Il successo della pipeline dipende fortemente dalla capacità dell'SLM di produrre formalizzazioni fedeli e radicate nella sorgente. Il metodo funziona bene per Qwen su specifici strati, ma fallisce o offre solo guadagni marginali per Phi e Gemma in scenari più complessi di tipi.
3. Auditabilità: Il contributo primario non è solo l'accuratezza, ma la capacità di fornire una traccia di ragionamento auditabile e diagnosticare i fallimenti (ad esempio, distinguere tra errori di traduzione e fallimenti del solver) senza l'overhead di ripetute generazioni neurali.
4. Nessuna Riduzione Generale del Calcolo: Il documento conclude che l'aggiunta di uno strato simbolico non riduce automaticamente i costi computazionali; in molti casi (ad esempio, compiti tipizzati con Qwen), la risposta diretta rimane l'opzione più efficiente e accurata. Il metodo è da vedersi come uno strumento diagnostico e un'alternativa specializzata al campionamento ripetuto per classi specifiche e limitate di problemi.