Technische Samenvatting: Verbeteren van Symbolische Vertaling van Taal Modellen voor Logisch Redeneren

Probleemstelling

De integratie van Large Language Models (LM's) met externe symbolische solvers (bijv. Z3, Prover9) biedt een verifieerbaar pad voor deductief logisch redeneren. Dit paradigma vereist het vertalen van Natuurlijke Taal (NL) naar Eerste-Orde Logica (FOL). Hoewel dit effectief is voor grote modellen, worstelen kleinere, meer toegankelijke LM's aanzienlijk met deze vertaaktaak. Ze produceren regelmatig incorrecte symbolische outputs door formatteringsfouten, syntaxisovertredingen en semantische inconsistenties. Bestaande benaderingen vertrouwen vaak op zelfcorrectie-loops gedreven door solver-feedback, maar deze methoden zijn sterk afhankelijk van het vermogen van het onderliggende model om foutmeldingen te interpreteren en accurate code te regenereren, een kracht die typisch is voorbehouden aan grotere, duurdere modellen. Bovendien is er een schaarste aan hoogwaardige symbolische data om kleinere modellen effectief te finetunen.

Methodologie

De auteurs stellen een drieledige aanpak voor om de prestaties van kleinere LM's (3B–4B parameters) te verbeteren bij NL-naar-FOL vertaling:

1. Data Synthese en Supervised Fine-Tuning (SFT)

Om het gebrek aan symbolische trainingsdata aan te pakken, synthetiseren de auteurs een dataset met behulp van een groot taalmodel (GPT-4o) op de ProofWriter dataset. Dit proces omvat:

• Generatie: Het creëren van NL-naar-FOL paren.
• Filtering: Een meerfasige pipeline inclusief correctie van de vorm, syntaxisvalidatie met behulp van Prover9, en semantische filtering om hoogwaardige vertalingen te garanderen.
• Training: De gesynthetiseerde data wordt gecombineerd met bestaande symbolische datasets (FOLIO) om Supervised Fine-Tuning (SFT) uit te voeren op vier kleine modellen: Gemma-3-4B, Phi-4-mini, Qwen2.5-3B, en Qwen3-4B. De trainingsinput concateneert de NL-bewering, de gegenereerde predicaatset en de FOL-representatie om gestructureerde generatiepatronen af te dwingen.

2. Incrementele Inferentie

Het artikel identificeert dat standaard "next-token" inferentie vaak leidt tot foutpropagatie, waarbij een enkele fout op token-niveau (bijv. een formatteringsfout) ervoor zorgt dat het model in repetitieve loops terechtkomt of malafide outputs genereert. Om dit te verzachten, introduceren de auteurs Incrementele Inferentie, een tweefasig proces:

• Fase 1 (Predicaat Generatie): Het model genereert eerst een consistente set predicaten ($\hat{P}$) die vereist zijn voor de gehele context van het probleem.
• Fase 2 (FOL Vertaling): Gebruikmakend van de uitgebreide input (NL-beweringen + $\hat{P}$), genereert het model de volledige FOL-beweringen.
  Deze decompositie dwingt predicaatconsistentie af over verschillende beweringen en maakt vroegtijdig stoppen mogelijk, wat het aantal formatteringsfouten aanzienlijk vermindert.

3. Verificatiemodule

Door gebruik te maken van de scheiding tussen predicaatgeneratie en volledige bewertingsgeneratie, integreren de auteurs een lichtgewicht Verifier. Deze module, geïmplementeerd als een klein LM met few-shot voorbeelden, controleert de gegenereerde predicaatset op arity-fouten (bijv. het gebruiken van een predicaat met een inconsistent aantal argumenten) voordat de FOL-vertalingsfase begint. Als er fouten worden gedetecteerd, geeft de verifieerder een gecorrigeerde predicaatset uit; zo niet, dan wordt de originele set doorgegeven.

Belangrijkste Bijdragen

• Fouttaxonomie: De auteurs categoriseren veelvoorkomende NL-naar-FOL vertaalfouten in vier types: Parsing (ontbrekende kwantoren, haakjesfouten), NoneType (kwantorlocatie, ontbrekende variabelen), Token (speciale tokens, onbekende operatoren), en Predicate (arity mismatch, onderwerp-predicaat conflicten).
• Data Synthese Pipeline: Een robuust framework voor het genereren van hoogwaardige, geverifieerde symbolische data om kleinere modellen te trainen, waardoor de kloof wordt overbrugd die wordt veroorzaakt door de schaarste van dergelijke data.
• Incrementele Inferentie Framework: Een nieuwe inferentiestrategie die predicaatgeneratie ontkoppelt van bewertingsvertaling, wat de outputstabiliteit en het naleven van formaten verbetert zonder extra instructies nodig te hebben tijdens de inferentie.
• Predicaat-niveau Metrieken: Introductie van Coverage (fractie van gebruikte predicaten aanwezig in de initiële set) en Usage (fractie van gegenereerde predicaten die daadwerkelijk gebruikt worden) om semantische consistentie te evalueren, naast standaard executieratio's.

Resultaten

De studie evalueert de voorgestelde methoden over vier logische redeneerdatasets: ProofWriter, FOLIO, ProntoQA, en ProverQA.

• Prestatiewinst: Supervised Fine-Tuning (SFT) verbetert zowel de executieratio's (het percentage geldige FOL-beweringen) als de redeneernauwkeurigheid aanzienlijk vergeleken met In-Context Learning (ICL) baselines over alle modelfamilies heen.
• Foutreductie: De combinatie van SFT en Incrementele Inferentie leidt tot substantiële reducties in formatterings- en syntaxisfouten. Zo liet het Qwen3-4B model op de FOLIO dataset bijvoorbeeld een daling van 57,4% in totale fouten zien.
• Predicaatgetrouwheid: Incrementele inferentie verbetert de predicaat-coverage aanzienlijk, met name op Out-of-Distribution (OOD) datasets zoals ProntoQA en ProverQA, door ervoor te zorgen dat het model expliciet de predicaatset definieert voordat de logica wordt gegenereerd.
• Impact van Verificatie: Het toevoegen van de arity-verificatiemodule verbetert de redeneernauwkeurigheid verder, vooral voor modellen die moeite hebben met abstracte concepten (bijv. ProntoQA), hoewel de winst bescheiden is vergeleken met de verbeteringen van SFT en incrementele inferentie.
• Modelgevoeligheid: De resultaten geven aan dat prestaties zeer gevoelig zijn voor de specifieke modelarchitectuur en de aard van de dataset. Bijvoorbeeld, Qwen3-4B vertoonde significante winsten op OOD-datasets, terwijl Phi-4-mini moeite had met contextretentie in lange premisse-sets onder standaard inferentie.

Betekenis en Claims

Het artikel claimt het veld dichter bij het ontwikkelen van betrouwbare en toegankelijke symbolische redeneersystemen te brengen. Door aan te tonen dat kleinere, kosteneffectieve modellen een hoge getrouwheid in logisch redeneren kunnen bereiken via gestructureerde data-synthese en inferentie-decompositie, betogen de auteurs dat de barrière voor het inzetten van neuro-symbolische systemen in omgevingen met beperkte middelen wordt verlaagd.

De auteurs hanteren een bescheiden toon met betrekking tot beperkingen:

• De gesynthetiseerde data, hoewel gecureerd, kan kleine inconsistenties bevatten.
• Het framework adresseert syntactische en formatteringsrobuustheid, maar garandeert niet volledig de semantische correctheid (d.w.z. de FOL kan syntactisch geldig zijn maar nog steeds de beoogde NL-betekenis verkeerd weergeven).
• De verificatiemodule introduceert extra inferentie-latentie, hoewel het incrementele inferentieproces zelf de latentie niet verhoogt buiten het aantal tokens om.
• Directe gedragsvergelijkingen tussen modellen zijn moeilijk vanwege de opaciteit van pre-training data.

Uiteindelijk suggereert het werk dat systematische foutcategorisering, gerichte fine-tuning en gestructureerde inferentie cruciaal zijn om kleinere LM's effectief te laten functioneren als componenten in verifieerbare logische redeneerpipelines.