Стресс-тестирование компетентности LLM в рассуждениях с помощью доказательств в условиях минимального формализма

Аннотация

Мы представляем ProofGrid — набор тестов для оценки рассуждений LLM на основе машинно проверяемых доказательств, а не только финальных ответов. ProofGrid включает 15 задач, охватывающих написание доказательств, проверку доказательств, маскировку доказательств и заполнение пробелов в доказательствах. Задачи формулируются на минимальном формальном языке, в частности NDL — компактном языке естественного вывода, который помещается в короткие промпты и обеспечивает точную, аудитируемую верификацию. Это даёт механическую, воспроизводимую и детальную оценку, а не суждения людей или LLM. ProofGrid охватывает калиброванный спектр сложности — от фундаментальных тестов на рассуждение до структурно насыщенных задач, которые не решает ни одна современная модель, при этом минимизируя зависимость от предметных знаний, делегирования решателям и артефактов длинного контекста. Мы также разрабатываем сравнительную рамку для бенчмарков рассуждений и используем её для позиционирования ProofGrid относительно существующих работ по таким параметрам, как представление, гарантии верификации и глубина рассуждений. Методологически мы вводим инструментированный конвейер проверки доказательств, который допускает незначительные поверхностные отклонения, но локализует первую содержательную ошибку в рассуждении, повышая разрешение измерения и отделяя планирование доказательства от низкоуровневого шума исполнения. С помощью этого конвейера мы оцениваем широкий спектр открытых и проприетарных моделей. Результаты показывают быстрый прогресс, но и значительные сохраняющиеся ограничения: передовые модели хорошо справляются с рядом фундаментальных задач, однако сложные задачи, особенно требующие глобального комбинаторного рассуждения или низкоуровневого синтеза доказательств, остаются далеки от решения. Мы также выявляем эпистемическую нестабильность, когда модели генерируют ошибочные доказательства, но при этом корректно отвергают те же самые локальные умозаключения в изоляции, и формализуем это с помощью Индекса эпистемической стабильности. Наконец, мы дополняем точность анализом 2PL IRT, картами Райта и нормализованной мерой дискриминации задач на основе информации Фишера.

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.