Pruebas de estrés de la competencia de razonamiento de los LLMs con demostraciones bajo un formalismo mínimo

Resumen

Presentamos ProofGrid, un conjunto de pruebas de referencia para evaluar el razonamiento de modelos de lenguaje mediante pruebas verificables por máquina, y no únicamente a partir de respuestas finales. ProofGrid incluye 15 tareas que abarcan escritura de pruebas, verificación de pruebas, enmascaramiento de pruebas y relleno de huecos en pruebas. Las tareas se expresan en notación formal mínima, especialmente NDL, un lenguaje compacto de deducción natural que cabe en instrucciones breves y permite una verificación precisa y auditable. Esto proporciona una evaluación mecánica, reproducible y de grano fino, en lugar de juicios realizados por humanos o modelos de lenguaje. ProofGrid cubre un espectro de dificultad calibrado, desde pruebas de razonamiento fundamentales hasta tareas de desafío estructuralmente ricas que ningún modelo actual resuelve, minimizando al mismo tiempo la dependencia de conocimientos de dominio, delegación de solucionadores y artefactos de contexto largo. También desarrollamos un marco comparativo para puntos de referencia de razonamiento y lo utilizamos para situar ProofGrid en relación con trabajos existentes en términos de representación, garantías de verificación y profundidad de razonamiento. Metodológicamente, introducimos un flujo de verificación de pruebas instrumentado que tolera desviaciones superficiales menores mientras localiza el primer fallo sustancial de razonamiento, mejorando la resolución de la medición y separando la planificación de pruebas del ruido de ejecución de bajo nivel. Utilizando este flujo, evaluamos un amplio rango de modelos abiertos y propietarios. Los resultados muestran un progreso rápido pero limitaciones sustanciales remanentes: los modelos de frontera se desempeñan bien en varias tareas fundamentales, pero las tareas difíciles, especialmente aquellas que requieren razonamiento combinatorio global o síntesis de pruebas de bajo nivel, están lejos de estar resueltas. También identificamos inestabilidad epistémica, donde los modelos generan pruebas defectuosas pero rechazan correctamente esas inferencias locales de forma aislada, y formalizamos esto con un Índice de Estabilidad Epistémica. Finalmente, complementamos la precisión con análisis IRT 2PL, mapas de Wright y una medida de discriminación de tareas normalizada basada en la información 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.