Mise à l'épreuve de la compétence de raisonnement des LLMs avec des preuves sous formalisme minimal

Résumé

Nous introduisons ProofGrid, une batterie de benchmarks pour évaluer le raisonnement des LLM à l’aide de preuves vérifiables par machine plutôt que par les seules réponses finales. ProofGrid contient 15 tâches couvrant l’écriture de preuves, la vérification de preuves, le masquage de preuves et le comblement de lacunes dans les preuves. Les tâches sont exprimées dans une notation formelle minimale, notamment NDL, un langage compact de déduction naturelle qui tient dans de courts prompts et permet une vérification précise et auditable. Cela permet une évaluation mécanique, reproductible et fine, plutôt que des jugements humains ou par LLM. ProofGrid couvre un spectre de difficulté calibré, allant de tests de raisonnement fondamentaux à des tâches de défi structurellement riches qu’aucun modèle actuel ne résout, tout en minimisant le recours aux connaissances du domaine, à la délégation à un solveur et aux artefacts de contexte long. Nous développons également un cadre comparatif pour les benchmarks de raisonnement et l’utilisons pour situer ProofGrid par rapport aux travaux existants en termes de représentation, de garanties de vérification et de profondeur de raisonnement. Sur le plan méthodologique, nous introduisons un pipeline instrumenté de vérification des preuves qui tolère des écarts superficiels mineurs tout en localisant le premier échec de raisonnement substantiel, améliorant ainsi la résolution de la mesure et séparant la planification de la preuve du bruit d’exécution de bas niveau. À l’aide de ce pipeline, nous évaluons un large éventail de modèles ouverts et propriétaires. Les résultats montrent des progrès rapides mais des limites substantielles persistantes : les modèles de pointe performent bien sur plusieurs tâches fondamentales, mais les tâches difficiles, notamment celles nécessitant un raisonnement combinatoire global ou une synthèse de preuves de bas niveau, restent loin d’être résolues. Nous identifions également une instabilité épistémique, où les modèles génèrent des preuves défectueuses tout en rejetant correctement ces inférences locales isolément, et nous formalisons ce phénomène par un indice de stabilité épistémique. Enfin, nous complétons la précision par des analyses IRT à 2 paramètres, des cartes de Wright et une mesure normalisée de discrimination des tâches basée sur l’information de Fisher.

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.