Technische Samenvatting: Dezelfde Formules, Andere Semantiek

Probleemstelling

Het artikel adresseert een kritieke lacune in het evalueren van de redeneervaardigheden van Large Language Models (LLMs) met betrekking tot modale logica. Terwijl bestaande benchmarks (bijv. ProofWriter, FOLIO, LogicNLI) deductie evalueren onder een vaste, impliciete achtergrondlogica, falen ze in het testen of modellen hun redenering kunnen aanpassen aan expliciet vermelde semantische specificaties. In modale logica hangt de geldigheid van een inferentie vaak af van specifieke frame-eigenschappen (bijv. reflexiviteit, transitiviteit, symmetrie) of domeincondities (bijv. constant versus variërend domein). Een model kan goed presteren door een dominant inferentie-regime te leren (een "vertrouwde" logica zoals S5) in plaats van zich te houden aan de specifiek verstrekte beperkingen. Het kernprobleem is bepalen of LLM's hun standaard logische intuïties kunnen onderdrukken om de gestipuleerde, potentieel niet-standaard, semantische condities te volgen.

Methodologie

De auteurs construeren een diagnostische benchmark die ontworpen is om semantische controle te isoleren van formule-gebaseerd patroonherkenning.

1. Constructie van de Benchmark:

• Gepaarde Problemen: De kern van de dataset bestaat uit paren problemen waarbij de premissen ($P$) en de conjectuur ($C$) identiek zijn, maar de semantische specificatie ($S$) precies één conditie verschilt (bijv. het vervangen van een reflexief frame door een transitief frame, of een cumulatief domein door een afnemend domein).
• Oracle Verificatie: Een geautomatiseerd redeneer-oracle (gebruikmakend van Vampire en Leo-III via de LET-embedding toolchain) verifieert dat de twee specificaties leiden tot tegengestelde waarheidswaarden ($y_a \neq y_b$) voor dezelfde formule.
• Gebalanceerde Kern: Om te voorkomen dat modellen een "conditie-alleen" shortcut gebruiken (waarbij het antwoord uitsluitend wordt bepaald door de semantische label zonder de formule te lezen), hebben de auteurs een "gebalanceerde niet-geneste kern" van 160 paren gecreëerd. In deze subset verschijnt elke semantische conditie even vaak met zowel True als False labels. Succes hier vereist strikt het lezen van de formule om te bepalen welke conditie de formule valideert.
• Omvang: De dataset dekt vijf frame-eigenschap contrasten (K–D, K–T, T–B, T–S4, B–S5) en drie domein contrasten (variërend–cumulatief, variërend–afnemend, cumulatief–constant), wat resulteert in 800 geneste-systeem paren en 160 gebalanceerde-kern paren.
• Prompting: Prompts maken gebruik van gecontroleerd Engels om regels expliciet te vermelden (bijv. "De toegankelijkheidsrelatie is reflexief en symmetrisch") zonder conventionele systeemnamen (zoals "S4") te gebruiken, waardoor het model gedwongen wordt te vertrouwen op de verstrekte regels.

2. Experimenteel Protocol:

• Modellen: De studie evalueert vijf recente modellen: DeepSeek V4 (Flash en Pro), GPT-5.6 (Luna en Terra), en Claude Sonnet 5.
• Condities:
  • Directe Prompting: Standaard inferentie zonder redeneermodus.
  • Redeneermodus: Geactiveerd voor specifieke modellen (bijv. DeepSeek Flash "high effort") om te testen of verhoogde berekening tijdens de inferentietijd helpt bij semantische adherentie.
  • Representatiegevoeligheid: Een subset test prestaties over verschillende formaten: benoemde Engelse condities, relationele definities en formele TPTP-syntaxis.
  • Semantische Affiniteit: Experimenten laten de specificaties weg om te identificeren welke "standaard" logica modellen verkiezen wanneer ze onbeperkt zijn.

Belangrijkste Resultaten

1. Falen van Semantische Controle onder Directe Prompting:
Op de gebalanceerde kern presteerden vier van de vijf modellen significant onder de 50% "conditie-alleen" baseline (die ervan uitgaat dat het model de formule negeert en gokt op basis van de conditie-label).

• DeepSeek V4 Flash: 4,4% strikte paar-accuratesse.
• DeepSeek V4 Pro: 2,5%.
• GPT-5.6 Luna: 21,2%.
• GPT-5.6 Terra: 25,0%.
• Claude Sonnet 5: 65,0% (het enige model dat de baseline overschreed).
  Dit geeft aan dat de meeste modellen falen in het volgen van de gestelde semantiek, en in plaats daarvan een vaste, vertrouwde logica toepassen, ongeacht de constraints in de prompt.

2. Redeneermodus als Herstellend Mechanisme:
Het activeren van de redeneermodus verbeterde de prestaties van DeepSeek V4 Flash drastisch, waarbij de accuratesse op de gebalanceerde kern steeg van 4,4% naar 88,1%. Vergelijkbare winsten werden waargenomen voor GPT-5.6 Luna op frame-problemen. Dit suggereert dat de fout niet noodzakelijkerwijs een gebrek aan logische kennis is, maar een falen om de juiste inferentie-modus te activeren om de specifieke beperkingen te verwerken.

3. Semantische Affiniteit en Standaardwaarden:
Wanneer specificaties werden weggelaten, vertoonden modellen coherente affiniteiten met vertrouwde logica's (bijv. DeepSeek Flash gaf de voorkeur aan K, terwijl Sonnet de voorkeur gaf aan K, en anderen de voorkeur gaven aan T). Deze standaardwaarden voorspelden echter niet betrouwbaar de fouten wanneer expliciete constraints aanwezig waren; modellen stemden vaak overeen bij ondergespecificeerde problemen, maar faalden in het aanpassen wanneer constraints werden toegevoegd.

4. Representatiegevoeligheid:
Het wijzigen van het inputformaat (van benoemde condities naar relationele definities of TPTP) veranderde de prestatierangschikking, maar herstelde de semantische controle niet consistent. Bijvoorbeeld, de accuratesse van GPT-5.6 Terra daalde van 38% (benoemd) naar 6% (relationele definities), wat aangeeft dat oppervlakte-formulering geen eenvoudige oplossing is voor het onderliggende probleem van semantische adherentie.

Belangrijkste Bijdragen

• Diagnostische Benchmark: Introductie van een gecontroleerd evaluatiekader dat het object-niveau probleem constant houdt terwijl de semantische specificatie varieert, specifiek ontworpen om "specificatiegevoeligheid" te testen.
• Gebalanceerde Kern: Een nieuw ontwerp voor datasets dat de mogelijkheid elimineert om problemen op te lossen door semantische condities aan antwoorden te koppelen zonder de logische formule te lezen.
• Empirisch Bewijs van Modus-afhankelijkheid: Demonstratie dat het vermogen om modale semantiek te volgen sterk afhankelijk is van de inferentie-modus (direct versus redeneren), wat het idee van statische logische redeneervaardigheden in LLM's uitdaagt.
• Resource Release: Openbare release van de formules, oracle-artefacten, tegenmodellen en modelresponsen.

Betekenis en Claims

Het artikel stelt dat benchmarks met vaste semantiek de robuustheid van LLM-redeneren kunnen overschatten. De primaire bevinding is dat modale kennis (het kennen van de logica) verschillend is van semantische controle (het toepassen van de specifieke gegeven logica). Een model kan over de noodzakelijke logische regels beschikken, maar kan er niet in slagen om een lokale specificatie de leidende factor te laten zijn voor het antwoord, en vervalt in plaats daarvan in een vertrouwde inferentie-regime.

De auteurs claimen bescheiden dat hun werk deze twee vermogens scheidt. Ze merken op dat hoewel de redeneermodus de gevoeligheid voor semantische interventies kan herstellen, dit de correctheid van tussenliggende afleidingsstappen niet garandeert (bijv. een model kan correct van logica wisselen, maar nog steeds een onjuiste conclusie afleiden door een redeneerfout). De studie concludeert dat toekomstige evaluaties expliciet moeten testen of modellen in staat zijn zich aan te passen aan gestelde beperkingen in plaats van te vertrouwen op vaste achtergrondveronderstellingen. Het artikel stelt geen nieuwe toepassingen of toekomstige architecturale wijzigingen voor, maar richt zich strikt op de diagnostische evaluatie van huidige modellen.