Neue Benchmark enthüllt Schwächen von KI-Logikern

In der KI-Forschung dient Logik als kontrolliertes Testfeld, doch herkömmliche SAT-Benchmarks vermischen oft Oberflächenmerkmale wie Länge oder Wortwahl mit den eigentlichen strukturellen Faktoren, die die Erfüllbarkeit bestimmen. Ein neues Diagnose-Benchmark für 2‑SAT, basierend auf parametrisierten Familien strukturierter 2‑CNF‑Formeln, löst dieses Problem. Die Erfüllbarkeit lässt sich dabei eindeutig durch das Implikationsgraphen‑Modell beschreiben und entlang verständlicher Achsen anpassen.

Die Generatoren des Benchmarks isolieren gezielt verschiedene Kompetenzen und Fehlermodi: (i) widersprüchliche Zyklus‑UNSAT‑Kerne mit einstellbarer Größe und Ungleichgewicht, (ii) SAT‑Instanzen mit einer vorgegebenen Quote freier Variablen zur Steuerung der Lösungsvielfalt, (iii) eingebettete Backbones, die die Ausbreitung von Wahrheitswerten modulieren, (iv) späte Brücken‑Klauseln, die sonst monotone Regionen verbinden, und (v) Symmetrie‑ bzw. Duplikationsvarianten, die die Abstraktion unter Umbenennung und redundanter Struktur testen.

Mit diesem Benchmark wurden LLM‑basierte Reasoner hinsichtlich Entscheidungsgenauigkeit und Zuverlässigkeit der Zuordnungen bewertet. Zusätzlich wurde die Robustheit gegenüber semantisch unveränderlichen Störungen wie Klauselreihenfolge, Füllklauseln und Variablenumbenennung gemessen.

Die Ergebnisse zeigen, dass die Modelle bei gezielten strukturellen Interventionen deutliche Leistungsabfälle aufweisen, selbst wenn die Oberflächenstatistiken konstant bleiben. Diese „Brittlichkeitsregime“ bleiben bei herkömmlichen SAT‑Genauigkeitsmetriken verborgen, was die Notwendigkeit eines strukturell fokussierten Testens unterstreicht.