When Many Answers Are Valid, Voting Fails: Symbolic Verification for Best-of-K Causal Reasoning in LLMs

Sintesi Tecnica: Quando Molte Risposte Sono Valide, il Voto Fallisce

Problema
Le attuali metodologie di scaling all'inferenza per i Large Language Models (LLM), come la Self-Consistency, si basano sull'assunto che la risposta più frequente tra le tracce di ragionamento campionate sia la più affidabile. Questo approccio fallisce nei compiti di ragionamento causale in cui possono essere completamente corrette molteplici uscite distinte (ad esempio, diversi set di aggiustamento validi che soddisfano il criterio di backdoor di Pearl). In tali scenari di "molti soddisfatori", la massa di probabilità valida si frammenta tra più stringhe di risposta, mentre una singola risposta non valida può dominare il voto semplicemente essendo l'errore più comune. Di conseguenza, il voto a maggioranza esatto può selezionare una risposta non valida anche quando la maggioranza delle tracce campionate contiene un ragionamento valido, portando a selezioni inconsistenti e errate.

Metodologia: CALVER
Gli autori introducono CALVER (Causal Axiom-Level VERification), un verificatore simbolico training-free, progettato per selezionare il miglior candidato da un pool di $K$ tracce campionate senza consultare una risposta di riferimento.

• Contratto della Traccia (Trace Contract): CALVER richiede che i modelli producano il ragionamento in uno schema tipizzato a sei slot: (1) Grafo, (2) Query, (3) Strategia, (4) Record di Derivazione, (5) Risultato Computato, e (6) Risposta.
• Verifica Simbolica: Invece di aggregare le frequenze delle risposte, CALVER valuta ogni traccia deterministicamente rispetto a una specifica causale eseguibile. Il verificatore esegue sei controlli:
  1. Parsing del Grafo: Valida la struttura del grafo (DAG o ADMG).
  2. Binding della Query: Assicura che le variabili della query corrispondano al problema.
  3. Validità della Strategia: Verifica se l'insieme proposto soddisfa i criteri grafici (ad esempio, d-separation, m-separation, backdoor adjustment, raggiungibilità dell'intervento).
  4. Record di Derivazione: Verifica la sintassi e la provenienza dei passaggi di ragionamento.
  5. Risultato Computato: Ricalcola indipendentemente il funzionale (ad esempio, l'Average Treatment Effect) per garantire la coerenza numerica.
  6. Consistenza della Risposta: Conferma che la risposta finale sia allineata con il risultato computato.
• Regola di Selezione: Il selettore sceglie la traccia con il punteggio più alto (punteggio massimo implementato di 6). I pareggi vengono risolti selezionando la traccia più precoce.
• Modalità: CALVER opera in due modalità:
  • Supplied-Graph: Il grafo sorgente è fornito; le tracce sono valutate rispetto ad esso.
  • Constructed-Graph: Il modello deve estrarre un grafo dal testo; la traccia è valutata rispetto al proprio grafo ricostruito, mentre la valutazione finale utilizza il grafo sorgente nascosto.

Contributi Chiave

1. Formulazione: Il paper formula la selezione best-of-$K$ sotto la molteplicità delle risposte come aggregazione su una classe di validità decidibile. CALVER istanzia questo con un punteggio di traccia a sei componenti dipendente dal grafo per DAG e ADMG.
2. Teoria:
   • Soundness del Certificato ATE Stretto: Gli autori dimostrano che una traccia con punteggio massimo che soddisfa specifici guardiani (esclusione del trattamento e margine decisionale) garantisce una decisione di soglia corretta per le query di Average Treatment Effect (ATE).
   • Teorema della Frammentazione della Validità: Dimostrano che la maggioranza esatta può diventare inconsistente quando la massa di probabilità valida è divisa tra molte risposte valide, permettendo a una risposta non valida con una massa individuale leggermente superiore di vincere.
3. Esperimenti: Valutazione estensiva attraverso diverse famiglie di modelli (Qwen, Mistral), famiglie di grafi (CLEAR, bnlearn) e setting (grafi forniti, costruzione text-to-graph, puzzle logici).

Risultati

• Superiorità rispetto ai Baseline: Sul benchmark CLEAR clean-core (126 problemi con molteplici risposte valide), CALVER raggiunge il 42,1% di accuratezza, superando significativamente la maggioranza esatta (~30,9%), un medoido consapevole dell'insieme (set-aware medoid), la confidenza del modello, un modello di ricompensa appreso (Skywork Reward V2) e un giudice LLM (anche quando scalato a 72B di parametri).
• Scaling con $K$: Il divario di performance tra CALVER e la maggioranza si amplia all'aumentare del budget di campionamento ($K$). Mentre le performance della maggioranza si stabilizzano, CALVER continua a migliorare, raggiungendo il 57,9% con $K=32$.
• Robustezza alla Recupero del Grafo: Nei setting text-to-graph dove il recupero esatto del grafo è basso (ad esempio, 34% a livelli narrativi naturalistici), CALVER supera comunque la maggioranza di 17,6 punti percentuali. Ciò dimostra che la verifica per candidato può avere successo anche quando la struttura globale del grafo è ricostruita imperfettamente, purchi le relazioni locali della query siano preservate.
• Generalizzazione: Il metodo si trasferisce a benchmark indipendenti (bnlearn, CausalGraph2LLM), diverse famiglie di modelli e domini non causali (puzzle logici Knights and Knaves) quando il predicato di verifica viene adattato (ad esempio, consistenza della tabella di verità).
• Efficienza: La verifica simbolica aggiunge un overhead minimo (~7% rispetto al costo di generazione), valutando ogni traccia in 1–8 ms su un singolo thread CPU.

Significatività e Assertività
Il paper sostiene che CALVER fornisce un segnale di selezione più forte rispetto alla frequenza superficiale o ai modelli di preferenza appresi in regimi in cui esistono molteplici risposte valide. Stabilisce che:

• Il Voto Fallisce: La maggioranza esatta è fondamentalmente fallace per il ragionamento causale quando le risposte valide frammentano il voto.
• Validità Eseguibile: L'aggregazione basata sulla soddisfazione di una classe di validità definita dal compito (tramite verifica simbolica) è più affidabile dell'aggregazione basata sulla frequenza della stringa di risposta.
• Regime Limite: Il metodo è più efficace nel "regime intermedio" in cui molte risposte sono valide e nessuna estrazione singola è affidabile. Quando le risposte sono quasi uniche, il voto standard è sufficiente; quando l'estrazione text-to-graph è altamente affidabile, estrarre un singolo grafo e risolvere direttamente è superiore.
• Indipendenza: Il meccanismo di selezione si basa su predicati eseguibili (assiomi causali o regole logiche) piuttosto che su euristiche apprese, rendendolo robusto attraverso diverse architetture di modelli e obiettivi di addestramento.

Gli autori sottolineano che CALVER non pretende di determinare la verità scientifica su grafi causali del mondo reale, ma piuttosto di selezionare la traccia di ragionamento formalmente più valida dato la struttura o il testo fornito. Il vantaggio del metodo è strettamente legato alla capacità di eseguire un controllo di validità sul candidato.