Technisches Resümee: Gleiche Formeln, unterschiedliche Semantik

Problemstellung

Die Arbeit adressiert eine kritische Lücke bei der Evaluierung der logischen Schlussfolgerungsfähigkeiten von Large Language Models (LLMs) im Bereich der Modallogik. Bestehende Benchmarks (z. B. ProofWriter, FOLIO, LogicNLI) bewerten zwar Deduktion unter einer festen, impliziten Hintergrundlogik, versäumen es jedoch zu testen, ob Modelle in der Lage sind, ihr Schließen an explizit angegebene semantische Spezifikationen anzupassen. In der Modallogik hängt die Gültigkeit einer Schlussfolgerung oft von spezifischen Frame-Eigenschaften (z. B. Reflexivität, Transitivität, Symmetrie) oder Domänenbedingungen (z. B. konstante vs. variierende Domänen) ab. Ein Modell kann gut abschneiden, indem es ein dominantes Inferenzregime lernt (eine „vertraute“ Logik wie S5), anstatt sich an die im Prompt angegebenen spezifischen Einschränkungen zu halten. Das Kernproblem besteht darin, zu bestimmen, ob LLMs in der Lage sind, ihre Standard-Logikintuitionen zu unterdrücken, um den festgelegten, potenziell nicht-standardmäßigen semantischen Bedingungen zu folgen.

Methodik

Die Autoren konstruieren ein diagnostisches Benchmark-System, das darauf ausgelegt ist, die semantische Kontrolle von der formalen Mustererkennung zu isolieren.

1. Konstruktion des Benchmarks:

• Paarweise Probleme: Der Kern des Datensatzes besteht aus Paaren von Problemen, bei denen die Prämissen ($P$) und die Konjektur ($C$) identisch sind, sich aber die semantische Spezifikation ($S$) um genau eine Bedingung unterscheidet (z. B. das Ersetzen eines reflexiven Frames durch einen transitiven oder einer kumulativen Domäne durch eine abnehmende).
• Oracle-Verifizierung: Ein automatisiertes Reasoning-Oracle (unter Verwendung von Vampire und Leo-III via des LET-Embedding-Toolchains) verifiziert, dass die beiden Spezifikationen unterschiedliche Wahrheitswerte für dieselbe Formel ergeben ($y_a \neq y_b$).
• Ausgewogener Kern (Balanced Core): Um zu verhindern, dass Modelle eine „Bedingungs-nur“-Abkürzung nutzen (bei der die Antwort allein durch die semantische Bezeichnung bestimmt wird, ohne die Formel zu lesen), haben die Autoren einen „ausgewogenen, nicht-verschachtelten Kern“ von 160 Paaren erstellt. In dieser Teilmenge tritt jede semantische Bedingung gleich häufig mit sowohl „True“ als auch „False“ Labels auf. Erfolg erfordert hier strikt das Lesen der Formel, um zu bestimmen, welche Bedingung sie validiert.
• Umfang: Der Datensatz deckt fünf Frame-Eigenschaft-Kontraste (K–D, K–T, T–B, T–S4, B–S5) und drei Domänen-Kontraste (variierend–kumulativ, variierend–abnehmend, kumulativ–konstant) ab, was insgesamt 800 verschachtelte Systempaare und 160 ausgewogene Kernpaare ergibt.
• Prompting: Die Prompts verwenden kontrolliertes Englisch, um Regeln explizit anzugeben (z. B. „Die Erreichbarkeitsrelation ist reflexiv und symmetrisch“), ohne konventionelle Systemnamen (wie „S4“) zu verwenden, was das Modell dazu zwingt, sich auf die bereitgestellten Regeln zu verlassen.

2. Experimentelles Protokoll:

• Modelle: Die Studie evaluiert fünf aktuelle Modelle: DeepSeek V4 (Flash und Pro), GPT-5.6 (Luna und Terra) sowie Claude Sonnet 5.
• Bedingungen:
  • Direktes Prompting: Standard-Inferenz ohne Reasoning-Modus.
  • Reasoning-Modus: Aktiviert für spezifische Modelle (z. B. DeepSeek Flash „high effort“), um zu testen, ob eine erhöhte Inferenzzeit-Berechnung die semantische Adhärenz fördert.
  • Repräsentations-Sensitivität: Eine Teilmenge testet die Leistung über benannte englische Bedingungen, relationale Definitionen und formale TPTP-Syntax hinweg.
  • Semantische Affinität: Experimente lassen Frame-Spezifikationen weg, um zu identifizieren, welche „Standard“-Logik Modelle bevorzugen, wenn sie unbeschränkt sind.

Kernergebnisse

1. Versagen der semantischen Kontrolle unter direktem Prompting:
Auf dem ausgewogenen Kern schnitten vier der fünf Modelle signifikant unter der 50%-„Bedingungs-nur“-Baseline ab (die davon ausgeht, dass das Modell die Formel ignoriert und basierend auf dem Label rät).

• DeepSeek V4 Flash: 4,4 % Genauigkeit bei Paaren.
• DeepSeek V4 Pro: 2,5 %.
• GPT-5.6 Luna: 21,2 %.
• GPT-5.6 Terra: 25,0 %.
• Claude Sonnet 5: 65,0 % (das einzige Modell, das die Baseline übersteigt).
  Dies zeigt, dass die meisten Modelle daran scheitern, die angegebene Semantik zu verfolgen, und stattdessen eine feste, vertraute Logik anwenden, unabhängig von den Prompt-Einschränkungen.

2. Reasoning-Modus als Restaurationsmechanismus:
Das Aktivieren des Reasoning-Modus verbesserte die Leistung von DeepSeek V4 Flash dramatisch und steigerte die Genauigkeit auf dem ausgewogenen Kern von 4,4 % auf 88,1 %. Ähnliche Gewinne wurden bei GPT-5.6 Luna bei Frame-Problemen beobachtet. Dies deutet darauf hin, dass das Problem nicht notwendigerweise ein Mangel an logischem Wissen ist, sondern ein Versagen bei der Aktivierung des korrekten Inferenzmodus, um die spezifischen Einschränkungen zu verarbeiten.

3. Semantische Affinität und Defaults:
Wenn die Spezifikationen weggelassen wurden, zeigten die Modelle kohärente Affinitäten zu bekannten Logiken (z. B. bevorzugte DeepSeek Flash K, Sonnet bevorzugte K und andere bevorzugten T). Diese Defaults sagten jedoch Fehler bei Vorhandensein expliziter Einschränkungen nicht zuverlässig voraus; Modelle stimmten oft bei unterbestimmten Problemen überein, scheiterten aber bei der Anpassung, sobald Einschränkungen hinzugefügt wurden.

4. Repräsentations-Sensitivität:
Die Änderung des Eingabeformats (von benannten Bedingungen zu relationalen Definitionen und TPTP) änderte die Leistungs-Rankings, stellte aber die semantische Kontrolle nicht konsistent wieder her. Beispielsweise sank die Genauigkeit von GPT-5.6 Terra von 38 % (benannt) auf 6 % (relationale Definitionen), was darauf hindeutet, dass die oberflächliche Formatierung keine einfache Lösung für das zugrunde liegende Problem der semantischen Adhärenz ist.

Zentrale Beiträge

• Diagnostisches Benchmark: Einführung eines kontrollierten Evaluierungsrahmens, der das Objekt-Level-Problem fix hält, während die semantische Spezifikation variiert wird, speziell entwickelt, um die „Spezifikations-Sensitivität“ zu testen.
• Ausgewogener Kern (Balanced Core): Ein neuartiges Design des Datensatzes, das die Möglichkeit eliminiert, Probleme durch die Abbildung semantischer Bedingungen auf Antworten zu lösen, ohne die logische Formel zu lesen.
• Empirischer Beleg für Modus-Abhängigkeit: Nachweis, dass die Fähigkeit, modale Semantik zu folgen, hochgradig vom Inferenzmodus (direkt vs. reasoning) abhängt, was die Vorstellung einer statischen logischen Denkfähigkeit von LLMs infrage stellt.
• Ressourcen-Freigabe: Veröffentlichung der Formeln, Oracle-Artefakte, Gegenmodelle und Modellantworten.

Bedeutung und Ansprüche

Die Arbeit argumentiert, dass Benchmarks mit fester Semantik die Robustheit des LLM-Reasonings überbewerten könnten. Die primäre Erkenntnis ist, dass modales Wissen (die Logik kennen) von semantischer Kontrolle (die spezifische gegebene Logik anwenden) unterscheidbar ist. Ein Modell kann über die notwendigen logischen Regeln verfügen, aber dennoch daran scheitern, eine lokale Spezifikation als Grundlage für seine Antwort zuzulassen, und statっtdessen auf ein vertrautes Inferenzregime zurückzugreifen.

Die Autoren behaupten bescheiden, dass ihre Arbeit diese beiden Fähigkeiten trennt. Sie merken an, dass der Reasoning-Modus zwar die Sensitivität gegenüber semantischen Interventionen wiederherstellen kann, dies aber keine Garantie für die Korrektheit der Zwischenschritte der Ableitung ist (ein Modell könnte zwar korrekt die Logik wechseln, aber dennoch aufgrund eines Fehlers im Reasoning zu einem falschen Schluss kommen). Die Studie kommt zu dem Schluss, dass zukünftige Evaluierungen explizit testen müssen, ob Modelle in der Lage sind, sich an angegebene Einschränkungen anzupassen, anstatt sich auf feste Hintergrundannahmen zu verlassen. Die Arbeit schlägt keine neuen Anwendungen oder zukünftigen Architekturänderungen vor, sondern konzentriert sich rein auf die diagnostische Evaluierung aktueller Modelle.