UFAL-CUNI at SemEval-2026 Task 11: An Efficient Modular Neuro-symbolic Method for Syllogistic Reasoning

Enunciato del Problema
I Large Language Models (LLM) hanno dimostrato competenza nel ragionamento sillogistico, ma soffrono di significativi bias di ragionamento, in particolare l'"effetto contenuto". Questo fenomeno si verifica quando il giudizio di un modello sulla validità di un argomento è influenzato dalla compatibilità dell'argomento con la conoscenza del mondo reale piuttosto che dalla sua struttura logica formale. SemEval-2026 Task 11 mira a disinnescare il contenuto dal ragionamento formale, sfidando i sistemi a valutare sillogismi aristotelici attraverso quattro sottocompiti: valutare la validità, selezionare le premesse rilevanti ed eseguire entrambi i compiti in contesti multilingue. L'obiettivo è costruire sistemi capaci di ragionamento indipendente dal contenuto, minimizzando al contempo l'effetto contenuto.

Metodologia
Gli autori propongono un approccio neuro-simbolico modulare ed efficiente che combina piccoli LLM per il ragionamento (nello specifico Qwen3 4B) con un dimostratore di teoremi simbolico (Prover9). L'architettura del sistema è composta da quattro componenti principali:

1. Traduzione Automatica (Opzionale): Per i sottocompiti multilingue (3 e 4), un LLM più grande (Gemma 3 27B) traduce gli input in inglese. Questo processo include un ciclo di auto-valutazione e correzione per garantire la fedeltà della traduzione prima dell'ulteriore elaborazione.
2. Parser FOL: Un piccolo LLM traduce le proposizioni in linguaggio naturale in Logica del Primo Ordine (FOL). Una chiave innovativa è l'uso di un formato LaTeX intermedio per questa traduzione. Gli autori ipotizzano che, poiché il LaTeX è ben rappresentato nei dati di addestramento degli LLM, esso produca formalizzazioni di qualità superiore rispetto alla traduzione diretta alla sintassi del dimostratore target. Il parser opera in modo multi-step, formalizzando le proposizioni una alla volta, mantenendo una mappatura coerente dei predicati tra le chiamate per garantire la coerenza logica.
3. Transpiler: Un componente basato su regole e guidato da espressioni regolari converte le formule FOL LaTeX intermedie nella sintassi specifica richiesta da Prover9.
4. Dimostratore Simbolico: Prover9 determina la validità logica del sillogismo formalizzato.
5. Recupero della Rilevanza (Sottocompiti 2 e 4): Invece di affidarsi all'LLM per identificare le premesse rilevanti, il sistema impiega un algoritmo simbolico greedy. Rimuove iterativamente le premesse e riesegue il dimostratore; se la prova fallisce dopo la rimozione, la premessa è considerata necessaria (rilevante).

Principali Contributi e Risultati

• Rappresentazione Intermedia: Il documento dimostra che istruire gli LLM a generare FOL in notazione LaTeX, seguito da una traslazione basata su regole, supera significativamente il parsing diretto alla sintassi nativa del dimostratore. Il parsing diretto ha comportato un calo di accuratezza di 10 punti e un aumento sostanziale dell'effetto contenuto a causa di frequenti errori di sintassi.
• Efficienza Neuro-Simbolica: Il sistema raggiunge un'accuratezza competitiva (circa il 95% sul sottocompito 1) utilizzando un modello da 4B di parametri, superando significativamente le baseline LLM zero-shot di dimensioni simili. Gli studi di ablazione confermano che la pipeline neuro-simbolica mitiga efficacemente l'effetto contenuto, mentre il ragionamento LLM end-to-end mostra un aumento netto del bias.
• Limiti dei Modelli Piccoli: Lo studio rivela che i piccoli LLM (4B) hanno capacità multilingue limitate. La pre-traduzione degli input con modelli più piccoli (ad esempio Gemma 3 4B o Qwen 3 4B) ha ottenuto risultati peggiori rispetto all'omissione totale della traduzione, suggerendo che sono necessari modelli più grandi per un pre-processing multilingue affidabile.
• Analisi delle Metriche: Gli autori forniscono un'analisi empirica e teorica critica della principale metrica di ranking del compito, il Combined Score (CS). Sostengono che il CS è eccessivamente sensibile al rumore statistico casuale in piccoli set di test. La loro analisi mostra che anche un modello non distorto può esibire effetti contenuti non nulli a causa della varianza, e la metrica penalizza in modo sproporzionato i sistemi ad alta accuratezza con errori minori, potenzialmente oscurando differenze reali di prestazioni.

Significato
Il documento afferma che, sebbene i piccoli LLM da soli siano insufficienti per un ragionamento sillogistico robusto e indipendente dal contenuto, diventano altamente efficaci quando integrati in una pipeline neuro-simbolica modulare. Il lavoro sottolinea l'importanza di sfruttare formati intermedi (LaTeX) che si allineano alle distribuzioni di addestramento del modello per migliorare l'affidabilità della formalizzazione. Inoltre, il documento contribuisce con una prospettiva critica sulle metriche di valutazione, suggerendo che i sistemi di ranking attuali potrebbero non distinguere in modo affidabile tra capacità di ragionamento genuine e artefatti statistici in compiti di ragionamento su piccola scala. Gli autori concludono che il loro approccio riduce con successo l'effetto contenuto per modelli di questa dimensione di parametri, offrendo una via praticabile per un ragionamento formale efficiente senza il costo computazionale di modelli massicci.