Stresstest der Schlussfolgerungskompetenz von LLMs mit Beweisen unter minimalem Formalismus

Zusammenfassung

Wir stellen ProofGrid vor, eine Benchmark-Suite zur Bewertung des LLM-Schlussfolgerns mittels maschinell überprüfbarer Beweise, nicht nur anhand von Endantworten. ProofGrid enthält 15 Aufgaben, die sich über Beweisschreiben, Beweisprüfung, Beweismaskierung und Beweislückenschließen erstrecken. Die Aufgaben werden in minimaler formaler Notation ausgedrückt, insbesondere NDL, einer kompakten Sprache des natürlichen Schließens, die in kurze Prompts passt und eine präzise, prüfbare Verifikation unterstützt. Dies ergibt eine mechanische, reproduzierbare und feinkörnige Evaluierung anstelle von Beurteilungen durch Menschen oder LLMs. ProofGrid deckt ein kalibriertes Schwierigkeitsspektrum ab, von grundlegenden Schlussfolgerungstests bis hin zu strukturreichen Herausforderungsaufgaben, die kein aktuelles Modell löst, und minimiert dabei die Abhängigkeit von Domänenwissen, Löserdelegation und Langkontextartefakten. Wir entwickeln außerdem einen vergleichenden Rahmen für Schlussfolgerungs-Benchmarks und nutzen ihn, um ProofGrid im Verhältnis zu bestehenden Arbeiten hinsichtlich Repräsentation, Verifikationsgarantien und Schlussfolgerungstiefe zu verorten. Methodisch führen wir eine instrumentierte Beweisprüfungspipeline ein, die geringfügige Oberflächenabweichungen toleriert, während sie den ersten inhaltlichen Schlussfolgerungsfehler lokalisiert, die Messauflösung verbessert und die Beweisplanung von niedrigstufigem Ausführungsrauschen trennt. Mit dieser Pipeline evaluieren wir eine breite Palette offener und proprietärer Modelle. Die Ergebnisse zeigen schnelle Fortschritte, aber erhebliche verbleibende Grenzen: Spitzenmodelle schneiden bei mehreren grundlegenden Aufgaben gut ab, doch schwierige Aufgaben, insbesondere solche, die globales kombinatorisches Denken oder niedrigstufige Beweissynthese erfordern, sind noch lange nicht gelöst. Wir identifizieren zudem epistemische Instabilität, bei der Modelle fehlerhafte Beweise generieren, aber dieselben lokalen Schlussfolgerungen isoliert korrekt ablehnen, und formalisieren dies mit einem Epistemic Stability Index. Schließlich ergänzen wir die Genauigkeit durch 2PL-IRT-Analysen, Wright-Karten und ein normalisiertes Aufgabendiskriminierungsmaß basierend auf Fisher-Informationen.

English

We introduce ProofGrid, a benchmark suite for evaluating LLM reasoning through machine-checkable proofs rather than final answers alone. ProofGrid contains 15 tasks spanning proof writing, proof checking, proof masking, and proof gap-filling. Tasks are expressed in minimal formal notation, especially NDL, a compact natural-deduction language that fits in short prompts and supports precise, auditable verification. This yields mechanical, reproducible, and fine-grained evaluation rather than judgments by humans or LLMs. ProofGrid covers a calibrated difficulty spectrum, from foundational reasoning tests to structurally rich challenge tasks that no current model solves, while minimizing reliance on domain knowledge, solver delegation, and long-context artifacts. We also develop a comparative framework for reasoning benchmarks and use it to situate ProofGrid relative to existing work in terms of representation, verification guarantees, and reasoning depth. Methodologically, we introduce an instrumented proof-checking pipeline that tolerates minor surface deviations while locating the first substantive reasoning failure, improving measurement resolution and separating proof planning from low-level execution noise. Using this pipeline, we evaluate a broad range of open and proprietary models. Results show rapid progress but substantial remaining limits: frontier models perform well on several foundational tasks, yet difficult tasks, especially those requiring global combinatorial reasoning or low-level proof synthesis, remain far from solved. We also identify epistemic instability, where models generate flawed proofs yet correctly reject those local inferences in isolation, and formalize this with an Epistemic Stability Index. Finally, we complement accuracy with 2PL IRT analyses, Wright maps, and a normalized task-discrimination measure based on Fisher information.