Stresstesten van de redeneercompetentie van LLM's met bewijzen onder minimaal formalisme

Samenvatting

Wij introduceren ProofGrid, een benchmark-suite voor het evalueren van redeneringen van LLM's via machinaal controleerbare bewijzen in plaats van alleen eindantwoorden. ProofGrid bevat 15 taken die betrekking hebben op bewijsschrijven, bewijscontrole, bewijsmaskering en het opvullen van gaten in bewijzen. Taken worden uitgedrukt in minimale formele notatie, met name NDL, een compacte natuurlijke-deductietaal die in korte prompts past en nauwkeurige, controleerbare verificatie ondersteunt. Dit levert een mechanische, reproduceerbare en gedetailleerde evaluatie op, in plaats van beoordelingen door mensen of LLM's. ProofGrid beslaat een gekalibreerd moeilijkheidsspectrum, van fundamentele redeneertests tot structureel rijke uitdagingstaken die door geen enkel huidig model worden opgelost, terwijl de afhankelijkheid van domeinkennis, solverdelegatie en lange-contextartefacten wordt geminimaliseerd. We ontwikkelen ook een vergelijkend kader voor redeneerbenchmarks en gebruiken dit om ProofGrid te positioneren ten opzichte van bestaand werk op het gebied van representatie, verificatiegaranties en redeneerdiepte. Methodologisch introduceren we een geïnstrumenteerde bewijscontrolepijplijn die kleine oppervlakkige afwijkingen tolereert terwijl de eerste substantiële redeneerfout wordt gelokaliseerd, wat de meetresolutie verbetert en bewijsplanning scheidt van ruis op laag niveau. Met behulp van deze pijplijn evalueren we een breed scala aan open en propriëtaire modellen. Resultaten tonen snelle vooruitgang, maar aanzienlijke resterende beperkingen: geavanceerde modellen presteren goed op verschillende fundamentele taken, maar moeilijke taken, vooral die welke wereldwijde combinatorische redenering of bewijssynthese op laag niveau vereisen, blijven verre van opgelost. We identificeren ook epistemische instabiliteit, waarbij modellen gebrekkige bewijzen genereren maar die lokale gevolgtrekkingen geïsoleerd correct verwerpen, en formaliseren dit met een Epistemische Stabiliteitsindex. Ten slotte vullen we nauwkeurigheid aan met 2PL-IRT-analyses, Wright-kaarten en een genormaliseerde taakdiscriminatiemaat op basis van Fisher-informatie.

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.