Riepilogo Tecnico: FormInv: Un Protocollo di Misurazione per l'Invarianza Semantica nei Benchmark di Ragionamento Matematico

1. Enunciato del Problema

I benchmark attuali per il ragionamento matematico nei Modelli Linguistici di Grande Dimensione (LLM) si basano pesantemente su metriche di accuratezza aggregate calcolate su formulazioni canoniche dei problemi. Questo articolo sostiene che tali metriche siano insufficienti perché presuppongono che la performance del modello sia indipendente da come una domanda è formulata. Gli autori identificano un critico "divario di misurazione": i modelli spesso mostrano un'alta accuratezza sui benchmark standard, ma non riescono a mantenere l'invarianza semantica—la capacità di produrre risposte coerenti attraverso parafrasi logicamente equivalenti.

L'articolo evidenzia che i benchmark standard (ad esempio GSM8K, MATH, MathCheck) mancano di una verifica rigorosa dell'equivalenza semantica delle parafrasi. Di conseguenza, le classifiche dei benchmark potrebbero essere artefatti di formulazioni specifiche piuttosto che vere misure della capacità di ragionamento. Gli autori si basano sulla teoria psicometrica, in particolare sulla Funzionamento Differenziale degli Item (DIF) e sulla Teoria della Generalizzabilità, per formalizzare questa questione. Essi ipotizzano che se la risposta di un modello cambia in base a riformulazioni semanticamente equivalenti, ciò indica un fallimento nella comprensione matematica genuina, affidandosi invece al riconoscimento di pattern superficiali.

2. Metodologia

2.1 Il Protocollo FormInv

Gli autori propongono FormInv, un protocollo di misurazione progettato per auditare e quantificare l'invarianza semantica. Il protocollo è composto da tre componenti fondamentali:

1. Il Divario di Invarianza (IG) e il Tasso di Coerenza Semantica (SCR):

   • IG: Definito formalmente come la deviazione standard delle risposte binarie di un modello attraverso una classe di equivalenza di parafrasi. Matematicamente, $IG(f, [x]_\sim) = \sqrt{p(1-p)}$, dove $p$ è la probabilità di una risposta corretta all'interno della classe di equivalenza. Un IG di 0 implica un'invarianza perfetta.
   • SCR: La proporzione di teoremi per i quali il modello risponde correttamente attraverso tutte le forme di parafrasi. A differenza dell'IG, che misura la varianza, l'SCR misura l'intersezione tra correttezza e invarianza.
   • Test Q di Cochran: Utilizzato come test statistico per l'omogeneità marginale attraverso $k > 2$ famiglie di parafrasi per determinare se il tasso di fallimento di un modello varia significativamente per famiglia.

2. La Tassonomia delle Parafrasi a 8 Famiglie:
   Il benchmark valuta i modelli attraverso otto distinte famiglie di trasformazione, categorizzate in base al loro rigore di verifica:

   • T1 (Formalmente Certificabile): Famiglie F4 (notazione), F6 (ordine), F7 (unpack) e F8 (equivalenza). Queste si basano su regole Lean4/FOL o sulla verifica tramite Sistemi di Algebra Computazionale (CAS) (ad esempio SymPy).
   • T2 (Condizionalmente Valida): Famiglie F1 (sintattica), F2 (quantificatore) e F3 (passiva). Queste dipendono dal contesto dei tipi e sono verificate tramite template o CAS quando applicabile.
   • T3 (Euristica): Famiglia F5 (variazione dei connettivi). Queste si basano su euristiche del linguaggio naturale e richiedono una revisione da parte di esperti di dominio.

3. Audit di Unanimità Cross-Modello:
   Un nuovo meccanismo di controllo qualità in cui una parafrasi viene segnalata come semanticamente errata se una supermaggioranza di modelli (ad esempio $\ge 6/9$) fallisce la parafrasi pur superando la versione canonica. Questo sfrutta l'assunzione che errori sistematici nella parafrasi stessa, piuttosto che nel ragionamento del modello, causino un fallimento universale.

2.2 Costruzione del Benchmark

• Substrato: La valutazione utilizza 103 teoremi curati da Mathlib4 (verificati in Lean4), che coprono domini come teoria dei numeri, algebra e analisi reale.
• Dataset: Il dataset principale (FormInv v1) contiene 760 elementi (103 teoremi $\times$ ~7,4 parafrasi). Una valutazione estesa "Track B" utilizza 100 teoremi più difficili da ntp-mathlib (811 elementi).
• Verifica: Le parafrasi sono generate tramite GPT-4o e verificate tramite un protocollo multistadio: CAS per le famiglie algebriche, garanzie di template per le famiglie superficiali e revisione umana al 100% da parte di esperti per le famiglie definitorie (F7/F8).

2.3 Configurazione Sperimentale

Lo studio valuta 9 modelli all'avanguardia (inclusi GPT-4o, Claude Sonnet/Haiku, DeepSeek V3/R1, Gemini 2.5 Flash e Llama 3.3 70B) su un range di 366–811 elementi. I modelli sono valutati in modalità zero-shot con vincoli rigorosi VERO/FALSO.

3. Risultati Chiave

3.1 Il Divario di Invarianza vs. Accuratezza

La scoperta più significativa è la disconnessione tra accuratezza aggregata e coerenza semantica.

• Claude Haiku 4.5 raggiunge un'accuratezza dell'86% ma solo un 50% di SCR, il che significa che metà delle sue risposte corrette sono inconsistenti attraverso le parafrasi.
• DeepSeek V3 raggiunge un'accuratezza del 96,4% e un 82% di SCR.
• Un divario di 10 punti in accuratezza nasconde un divario di 32 punti nell'SCR. L'articolo nota che l'accuratezza da sola è "costituzionalmente cieca" a questo fallimento strutturale.
• Esiste una forte correlazione negativa ($r = -0,965$) tra accuratezza e IG Medio, suggerendo che i modelli più accurati sono generalmente più invarianti, ma questa correlazione è guidata algebricamente dalla definizione di IG e non garantisce l'invarianza per famiglie specifiche.

3.2 Inversioni di Classifica e Complementarità

Le classifiche dei modelli non sono stabili; si invertono a seconda della famiglia di parafrasi:

• F6 (Ordine di Confronto): GPT-4o fallisce lo 0,0% degli elementi, mentre Claude Sonnet fallisce il 16,7%.
• F7 (Unpacking Definitorio): Claude Sonnet fallisce circa il 6%, mentre GPT-4o fallisce il 10,0%.
• Questo pattern di fallimento complementare implica che nessun singolo modello domina in senso di Pareto tutte le famiglie. Di conseguenza, i progettisti dei benchmark scelgono implicitamente una ponderazione delle famiglie che determina il vincitore. L'articolo formalizza questo come il corollario "No-Free-Benchmark": per qualsiasi classifica target, esiste una ponderazione $\lambda$ sulle famiglie di parafrasi che la realizza.

3.3 Risultati dell'Audit di Qualità

Il protocollo di unanimità cross-modello ha identificato con successo parafrasi semanticamente errate nei benchmark esistenti:

• Audit MathCheck: Applicato a 129 gruppi in MathCheck, il protocollo ha segnalato 4 parafrasi semanticamente errate (3,1%). Rimuovendo questi errori, GPT-4o è sceso dalla posizione 2 alla 4, elevando Claude Haiku e DeepSeek V3.
• Audit FormInv v1: Il protocollo ha identificato 11 errori negli elementi generati da GPT-4o, inclusi eccessi di bicondizionali, inversioni di voce passiva e rimozione del contesto dei tipi. Questi errori erano invisibili alla valutazione con un singolo modello ma sono stati esposti dall'unanimità.

3.4 Dipendenza dal Regime di Difficoltà

Nella valutazione "Track B" che utilizza teoremi più difficili:

• La correlazione tra accuratezza e invarianza si è indebolita ($r = -0,415$, non significativa).
• La difficoltà specifica di F5 (variazione dei connettivi) si è dissolta; tutte le famiglie si sono raggruppate a tassi di fallimento simili (28–35%).
• I modelli di ragionamento (DeepSeek R1, o4-mini) hanno mostrato l'IG più basso sui teoremi difficili, suggerendo che la deliberazione tramite Catena di Pensiero riduce la sensibilità superficiale solo quando i teoremi richiedono ragionamento di alto livello.

4. Contributi

1. Framework di Invarianza: Formalizza SCR e IG come metriche primarie per l'invarianza semantica, basate sul teorema dell'aspettativa condizionata di Doob e sulla teoria DIF. Classifica le famiglie di parafrasi in livelli T1, T2 e T3 in base al rigore di verifica.
2. Benchmark FormInv: Un dataset di oltre 760 elementi derivato da teoremi verificati in Lean4, valutato su 9 modelli con un rigoroso audit di unanimità cross-modello.
3. FormInvSelector: Un algoritmo che utilizza profili SCR per famiglia per raccomandare il modello con il tasso di fallimento atteso più basso per specifici regimi di attività (ad esempio, selezionare un modello per il ragionamento definitorio rispetto a compiti di confronto).
4. Audit della Qualità delle Parafrasi: Dimostra che l'unanimità cross-modello ($\ge 6/9$ modelli che falliscono una parafrasi) è un metodo automatizzato e a basso costo per rilevare elementi di benchmark semanticamente errati, separando efficacemente gli errori del benchmark dagli errori del modello.

5. Significato e Affermazioni

L'articolo afferma che FormInv è il primo protocollo ad applicare la teoria dell'invarianza di misurazione e metriche basate sulla DIF al ragionamento matematico formale. Il suo significato risiede in tre aree:

• Rivelazione di Difetti Nascosti: Espone che le metriche di accuratezza standard possono essere fuorvianti, nascondendo un "divario di 32 punti" tra la performance superficiale e la comprensione semantica genuina.
• Integrità del Benchmark: Fornisce uno strumento per i costruttori di benchmark per auditare i propri dataset prima della pubblicazione, impedendo che le classifiche siano artefatti di parafrasi difettose. Gli autori affermano che "se si generano parafrasi programmaticamente, non si sa quanti siano sbagliate".
• Valutazione Consapevole del Regime: Mette in discussione la nozione di un singolo "miglior" modello, dimostrando che le classifiche dipendono dal regime (variando per famiglia di parafrasi e difficoltà). L'articolo conclude che i progettisti dei benchmark scelgono implicitamente i vincitori selezionando quali famiglie includere, e FormInv rende questa scelta esplicita e auditabile.

Gli autori rimangono modesti riguardo ai limiti, notando che la certificazione su larga scala di tutte le parafrasi tramite Lean4 è un lavoro futuro, e che lo studio attuale si basa su un set curato di 103 teoremi (sebbene esteso a 100 più difficili in Track B). Sottolineano che FormInv è una metrica supplementare destinata ad affiancare, non a sostituire, le valutazioni esistenti basate sull'accuratezza.