Teste de Estresse da Competência de Raciocínio de LLMs com Provas sob Formalismo Mínimo

Resumo

Apresentamos o ProofGrid, um conjunto de benchmarks para avaliar o raciocínio de LLMs por meio de provas verificáveis por máquina, em vez de apenas respostas finais. O ProofGrid contém 15 tarefas que abrangem escrita de provas, verificação de provas, mascaramento de provas e preenchimento de lacunas em provas. As tarefas são expressas em notação formal mínima, especialmente NDL, uma linguagem compacta de dedução natural que cabe em prompts curtos e suporta verificação precisa e auditável. Isso proporciona uma avaliação mecânica, reproduzível e de granularidade fina, em vez de julgamentos feitos por humanos ou LLMs. O ProofGrid cobre um espectro de dificuldade calibrado, desde testes fundamentais de raciocínio até tarefas desafiadoras estruturalmente ricas que nenhum modelo atual resolve, ao mesmo tempo que minimiza a dependência de conhecimento de domínio, delegação a solucionadores e artefatos de contexto longo. Também desenvolvemos uma estrutura comparativa para benchmarks de raciocínio e a utilizamos para situar o ProofGrid em relação a trabalhos existentes em termos de representação, garantias de verificação e profundidade de raciocínio. Metodologicamente, introduzimos um pipeline instrumentado de verificação de provas que tolera pequenos desvios superficiais enquanto localiza a primeira falha substantiva de raciocínio, melhorando a resolução da medição e separando o planejamento da prova do ruído de execução de baixo nível. Usando esse pipeline, avaliamos uma ampla gama de modelos abertos e proprietários. Os resultados mostram progresso rápido, mas limites substanciais remanescentes: modelos de fronteira apresentam bom desempenho em várias tarefas fundamentais, mas tarefas difíceis, especialmente aquelas que exigem raciocínio combinatório global ou síntese de provas de baixo nível, permanecem longe de serem resolvidas. Também identificamos instabilidade epistêmica, na qual os modelos geram provas falhas, mas rejeitam corretamente essas inferências locais isoladamente, e formalizamos isso com um Índice de Estabilidade Epistêmica. Por fim, complementamos a acurácia com análises IRT 2PL, mapas de Wright e uma medida normalizada de discriminação de tarefas baseada na informação 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.