Stress-Testing the Reasoning Competence of Language Models With Formal Proofs (2025)

Abstract: We present a broad empirical study of state-of-the-art LLMs and LRMs (Large Reasoning Models) on ProofGrid, a new battery of challenging but tractable logical inference tasks that form a domain-independent test of constraint-based reasoning. The tasks include proof writing and proof checking across propositional and equational logic. We also introduce two novel tasks: proof inpainting and proof gap-filling. Solving these problems requires tracking the global structure of a mathematical argument, writing hierarchical subproofs, maintaining coherence across nested assumptions, performing complex case analyses, applying inference rules, reasoning about identity and term rewriting, and reasoning about proofs themselves. Our experiments reveal impressive performance by top-tier models but also systematic failure modes. Along with the benchmarks, we release a new data resource comprising over 10K formal deduction problems and corresponding proofs.

## introduction large language models (llms) have rapidly advanced, finding applications in increasingly complex problems well beyond their original scope of narrow nlp tasks such as summarization, information extraction, and composition of short texts like emails. the recent development of the inferencecompute paradigm, commonly powered by reinforcement learning, has given rise to so-called large reasoning models (lrms). these models perform test-time search to identify promising completions that are more likely to yield correct answers, at the expense of higher inference costs. driven by this scaling of test-time compute, lrms have demonstrated dramatic improvements in logical and mathematical reasoning, enabling some models to even surpass human performance on some very challeng-* corresponding author ing benchmarks, such as frontiermath @xcite . however, most test batteries for logical reasoning are focused on the correctness of the final answer, typically determined by an exact-match comparison with the ground truth. this ignores the reasoning behind the answers and is likely to inflate performance, because models might arrive at the right answers for the wrong reasons, by latching on to superficial patterns. this evaluation paradigm is particularly unsuitable for mathematics, where proofs are not just a means to an end but the very foundation of the discipline. thus, to properly assess the mathematical reasoning abilities of llms and lrms, it is essential to evaluate whether they can construct and verify proofs. proofgrid addresses this gap by requiring models to write, check, and reason about formal logic proofs. an advantage of using pure logic to evaluate reasoning ability is that the problems are entirely abstract and thus require what psychologists call fluid intelligence, as opposed to crystallized intelligence @xcite . fluid intelligence refers to innate reasoning ability employed to solve novel problems, while crystallized intelligence reflects the declarative knowledge and problem-solving know-how that accumulates through explicit instruction. current benchmarks often allow models to leverage their vast stores of crystallized knowledge, acquired through their pretraining, enabling them to memorize their way to correct answers by employing shortcuts that are sometimes valid but are other times derived from spurious patterns. by focusing on form rather than content, symboliclogic problems gauge pure reasoning competence. in addition, most existing benchmarks no longer pose a serious challenge and are approaching saturation, as shown by near-ceiling performances from even general-purpose llms. proofgrid incorporates complex and structurally rich reasoning challenges that expose the limitations of even the most capable models. we hope that this will stimulate continued research and development in this field. the initial version of the proofgrid dataset contains about 10k problems and proofs for propositional logic and 1k problems and proofs pure equational logic. this is a data resource that we plan to expand continuously with new material. in addition to the data, we release a set of benchmarks based on task slices of the overall dataset. these are specific tasks based on fixed smaller subsets of the full dataset, each typically containing 200-500 instances. using this approach, we benchmarked 15 prominent lrms and llms across multiple tasks: proof checking, proof discovery, proof infilling, and recovery of proof gaps. proofs have formal syntax and semantics and are expressed in a natural-deduction style that mirrors human inferential practices the rest of this document is structured as follows. section 2 discusses related work; section 3 describes the datasets of proofgrid; section 4 presents the results of our evaluations; section 5 presents some findings from analyzing the results; and section 6 concludes. ## related work there are many datasets for evaluating a diverse array of reasoning skills, and while we cannot review all of them here, we can categorize them into 4 main groups depending on the type of reasoning on which they focus: (a) natural-language reasoning; (b) mathematical and scientific reasoning; (c) generalist/hybrid reasoning; and (d) formal reasoning. benchmarks in the first group probe the ability of models to reason in natural language. this includes classical nli benchmarks such as snli @xcite and mnli @xcite , which study entailment judgments of the form t |= h, where t is a context (or "theory") and h is a hypothesis. both t and h are naturallanguage texts found in the wild, and the task is to determine if h follows from t , is contradicted by it, or neither. these determinations are typically supported by informal or commonsense reasoning and general background knowledge, and require relatively shallow inferences. we include in this category datasets in which t and h are expressed in "controlled natural language" (cnl), namely, natural language that is not organic but rather synthesized from logic-formula templates, where the formulas come from a well-circumscribed logic such as datalog or a particular description logic. these datasets, which tend to emphasize multi-step inference chains and closedworld reasoning, include ruletaker @xcite , proofwriter @xcite , prontoqa @xcite , logicinference @xcite , logicasker @xcite , logic-nli @xcite , and fld @xcite . folio @xcite ) can arguably be placed in the same group. math benchmarks include gsm8k @xcite , math @xcite ), olympiadbench @xcite , omni-math @xcite , and the more recent (and much more demanding) frontiermath @xcite and olymmath @xcite . problems here are expressed in natural language and the expected answers are literals such as numbers or symbolic expressions like x 2 -5. these benchmarks do not test mathematical reasoning per se, since they follow an outcome-based evaluation paradigm that judges models only on their final answers. this allows models to exploit memorization, heuristics, and pattern matching. scientific-reasoning datasets, like arc @xcite , entailment bank @xcite , and theoremqa @xcite focus on natural science rather than mathematics, but they follow essentially the same pattern: questions are posed in natural language and probe problem-solving in knowledge-rich domains; only the answers are evaluated, not the reasoning. the third group comprises broad-coverage benchmarks like mmlu @xcite ) and its successor mmlu pro @xcite , hle (humanity's last exam) (scale ai and center for ai safety 2025), bbh @xcite and its successor bbeh ("big bench extra hard") (google research 2025), and supergpqa @xcite . these provide a coarse picture of general model ability but blur distinctions between domain knowledge, language understanding, and reasoning. they also remain outcome-focused. the last category includes formal-reasoning datasets that use symbolic inputs rather than natural language. a notable example here is minif2f @xcite , which contains 488 mathematics problems expressed symbolically in lean, metamath, isabelle, and hol light, and whose solutions require formal proofs in these systems. in principle, such benchmarks can verify not just the correctness of an answer but also the correctness of the reasoning behind the answer, since the reasoning is expressed as a formal proof that can be checked by machine. however, such benchmarks tend to be tied to specialized proof systems, restricting their accessibility. proofgrid falls into this last group, since its inputs are based on symbolic formulas and its outputs require structured formal proofs. it mitigates the issue of heavy dependence on esoteric details of complex formal systems by employing a minimalist natural-deduction formalism, which is both strikingly compact (the entire proof language is fully described in a short prompt) and aligned with ordinary reasoning practices. this should make proofgrid both rigorous and approachable. proofgrid can also be compared with the cnl members of the first group (benchmarks for "natural-language reasoning"), since they are also based on formal logics. relevant points of comparison include (i) the expressiveness of the underlying formalism; (ii) the range of reasoning mechanisms tested; (iii) the maximum depth of reasoning required; and (iv) the current degree of saturation. regarding expressiveness, some of the cnl datasets, such as ruletaker and proofwriter, are based on stratified datalog, which supports recursive horn clauses and limited negation but disallows full disjunction, unrestricted negation, quantifier alternation, and function symbols. likewise, prontoqa is based on positive horn logic, which is reducible to datalog over unary predicates. in theory, fld supports full first-order logic, albeit without equality or function symbols. in practice, the fragment it exercises is far more limited, essentially confined to monadic predicates without quantifier alternations. this reflects a broader trend among benchmarks in the cnl category. even though they are solidly framed in logic, most of them end up targeting very weak subsets of predicate logic, partly because of the sheer complexity of the infrastructure that is needed for a correct implementation of full-blown proofs in first-order logic. similar remarks apply to logicinference, logicasker, logicnli, and folio. consequently, these benchmarks end up testing mostly variants of simple forward chaining on conditional rules, which requires little more than universal specialization and modus ponens. by contrast, the current version of proofgrid is based on full propositional logic (with unrestricted negation and disjunction) and equational logic. the former allows us to encode a vast range of reasoning-intensive problems requiring proofs, many of which cannot be represented in datalog (e.g., problems involving parity and counting in general, graph connectivity, pigeonhole constraints, injectivity, mutual exclusion, and others). equational logic allows us to test the ability of ai models to reason about function applications and identity, which is beyond the scope of the cnl benchmarks. moreover, proofgrid supports a diverse range of reasoning idioms, including hypothetical reasoning (conditional proofs under provisional assumptions), which requires the tracking of nested assumption scopes, reasoning by contradiction and indirect proof, complex and highly nested case analyses, and so on. these are foundational tools in mathematical reasoning and crucial for evaluating whether a model understands how to structure and manage complex deductive arguments, not just chain together atomic rules. the maximum depth of reasoning required by cnl benchmarks is smaller than 10 (the most demanding is fld, with a maximum depth of 8). proofgrid problems feature reasoning chains with dozens of steps (in some cases over 100 steps). finally, the cnl benchmarks are largely saturated @xcite , with deepseek-r1 exceeding 80% overall accuracy on fld, folio, and prontoqa, and even gpt-4o scoring over 98% on prontoqa. by contrast, the mean accuracies of deepseek r1 and gpt-4o on proofgrid are 35% and 13%, respectively. in summary, proofgrid differs from prior reasoning benchmarks in four key ways: it enforces proof-based evaluation rather than outcome-only scoring; it minimizes content-knowledge advantages by using abstract symbolic inputs; it employs a minimalist natural-deduction framework that still supports a wide range of common reasoning mechanisms; and it introduces challenging tasks that even the best current models cannot solve reliably. ## datasets the inaugural version of proofgrid foot_0 has two parts, one for propositional logic and one for equational logic. the former has 2 datasets, pl 1 and pl 2 , and 4 tasks: proof checking; proof writing; proof infilling; and proof gap-filling. the equational-logic part has one dataset, eq 1 , and 3 similar tasks (proof checking, proof writing, and proof gap-filling). we describe all of them in detail below. all proofs in proofgrid are formal, and those in pl 1 and pl 2 are written in natural deduction style. natural deduction makes direct and intuitive use of techniques like conditional proof, reasoning by contradiction, case analysis, and application of inference rules that reflect the way human mathematicians and scientists construct and verify arguments. to evaluate and write these proofs, a reasoner must be able to recognize local and global logical relationships, track assumption and lemma scope, and compose multiple steps into coherent chains of inference. because natural deduction aligns closely with human inferential practice, both formally and cognitively, it offers an ideal testbed for probing the reasoning competence of ai models. another advantage of the particular naturaldeduction system used in proofgrid is its simplicity and autonomy. models do not need to have mastered the intricate syntax of complex interactive theorem-proving systems, either via pretraining or fine-tuning. instead, our pl 1 tasks rely solely on short but rigorous and self-contained prompts describing the formal syntax and operational semantics of an exceptionally simple and stripped-down natural-deduction language, ndl, along with a few well-chosen icl examples. our eq 1 proofs are even simpler (essentially sequences of term rewrites); their syntax and semantics are also fully described in short prompts and illustrated with examples. pl 1 data pl 1 is a relatively simple dataset comprising short and minimally structured problems and proofs. lrms do well both on proof-checking and on proof-writing in pl 1 , but we show that proof masking and gap-filling pose challenges even in this basic setting. pl 1 contains 1.4k problems, where each problem consists of a set of premises p 1 , . . . , p n and a conclusion p that is logically entailed by the premises. the p and p i are formulas constructed inductively from propositional atoms a, b, c, . . .. a complex formula is either a negation ( p); a conjunction (p 1 & p 2 ); a disjunction (p 1 | p 2 ); a conditional (p 1 ⇒ p 2 ); or a biconditional (p 1 ⇔ p 2 ). the negation operator binds most tightly, followed by conjunctions, disjunctions, conditionals, and biconditionals. all binary constructors are right-associative. premises and goals were randomly generated as tree structures; see appendix b for details. here is a sample proof-writing problem: derive @xmath0, p 2 = ( a ⇒ c); and p 3 = (c ⇒ d). appendix b contains additional examples and various statistics on the generated problems. proofs for all problems were generated automatically by a theorem prover written in athena (athena language team 2025), a natural-deduction system for proof engineering that can be viewed as a proper superset of ndl. all proofs generated by this theorem prover were confined to the ndl core. here is an example of a formal proof for the problem described above: as mentioned above, ndl is a minimal subset of athena that contains only introduction and elimination rules, conditional subproofs, and a few other convenient derived inference rules, such as de morgan and disjunctive syllogism. the theorem prover generated correct proofs by construction. to obtain a balanced dataset with roughly equal numbers of correct and incorrect proofs, we (a) randomly corrupted a number of these proofs so as to make them incorrect, and we (b) included proofs written by o3 and gemini-2.5-pro, which tended to have more organic errors than those produced by the noising procedures described in (a). pl 1 task 1: proof checking this task contains 300 instances. the objective is simple: given a proof for a given problem, determine if it is correct. an incorrect verdict must be accompanied by additional information: the line number containing the earliest error, the type of the error (syntax error, type error, or logic error); and a detailed description of the error. the full prompt can be found on the proofgrid repo. ground truth is determined by an instrumented version of the athena proof checker, designed to make the checker compatible with the ndl description given in the prompts. this instrumentation is necessary because some of these 300 proofs were written by models and contain syntax forms that are interesting generalizations of ndl's syntax forms, but are not, strictly speaking, allowed by ndl proper. for instance, in ndl an inference rule r is always applied to a number of plain formulas p 1 , . . . , p n . but models started taking the liberty of writing entire subproofs inline for various p i . athena actually allows this, but ndl does not, so instrumentation is needed to ensure alignment, so that when a model later is asked to check such a proof and complains that the proof violates ndl syntax, it receives full credit. as another example, case analyses are always binary in ndl: the ternary inference rule cases is applied to a binary disjunction (p 1 | p 2 ) and two conditionals of the form (p 1 ⇒ q) and (p 2 ⇒ q). but some models started applying cases to more complex disjunctions of the form with n conditionals (p i ⇒ q) for @xmath1, . . . , n, for a total of n + 1 arguments. this is also allowed by athena, but it is nowhere mentioned in the ndl definition in the proof-checking prompt, so if a model later checks such an lrm-generated proof and complains that cases is applied to too many arguments, it should be given credit, even if athena accepts such liberal applications of cases. our evaluation methodology for this task is lenient. if the proof is correct (according to this modified checker) and the model reports it as correct, we give the model a full point. we also give the model a full point if the proof is incorrect and the model reports it as such, although a manual review of error details reveals that in some cases models report spurious errors. pl 1 task 2: proof writing this task contains 400 instances. given a deduction problem ("derive p from p 1 , . . . , p n "), the model must write a proof for it, including english comments explaining the reasoning strategy. accuracy here is evaluated by checking the generated proofs with athena. we are lenient with respect to minor syntax errors: we wrote scripts that patch up a wide range of common syntax errors made by the models (such as failing to balance parentheses) before we send the result to athena for checking. we believe it is possible to likewise detect and repair a good deal of minor non-syntactic errors as well, in which case these accuracies would be expected to go up; this is left for future work. the data for this task was obtained by masking 400 proofs from the pl 1 dataset. given a proof, we randomly mask any number of the following four types of items: (a) conclusions (formulas immediately preceding the by keyword); (b) inference rules (immediately preceding on); (c) assumptions (immediately following assume); and (d) one or more arguments to an inference rule application (immediately following on). masks are unique identifiers: mask1, mask2, and so on. the objective is to determine if there is a way to unmask the proof completely so that it correctly derives the target conclusion from the given premises; and if so, to provide a detailed assignment of appropriate values to the masks. this is essentially a constraint satisfaction problem where the constraints are given by the syntax rules and operational semantics of proofs. the key question addressed by this task is whether a model can infer missing symbolic structure consistent with the rules that govern natural-deduction reasoning, and in particular whether it can jointly restore syntax and semantics. high accuracy in this task would strongly suggest that the model possesses a robust internal model of logical reasoning that goes beyond surface-level pattern recognition. model responses are evaluated by unmasking the proof according to the specified mask values and then checking that the resulting proof correctly derives the expected conclusion. if a model claims that the problem is unsolvable, we consider that response as incorrect when the original (unmasked) proof succeeds and correct when the original proof fails. this evaluation is deliberately lenient, because masking an erroneous proof might salvage it by occluding the error. thus, the accuracies reported in section 4 for this task are upper bounds on actual performance. by contrast, when we restrict evaluation to correct proofs that have been masked, then an unsolvability claim is always incorrect and we count it as such. accuracy restricted on the set of correct proofs is reported in section 4 as "strict" accuracy. as expected, a model's strict accuracy on proof infilling tends to be lower. pl 1 task 4: proof gap filling this dataset was obtained by randomly inserting holes (gaps) in a set of 200 correct proofs, written either by the athena theorem prover or by a model. unlike masks, which are locally focused on individual formulas and rules, gaps apply at the subproof level, i.e., a gap replaces a subproof, which could be either a single step (inference rule application), or a conditional subproof, or a proof chain: a sequence of consecutive subproofs. a proof usually receives several gaps, in different places. more information can be found in appendix b.1.2. we ask the models to map every gap to a subproof in such a way that the result becomes a correct proof of the goal from the premises. a solution is counted as correct iff it achieves that. we report accuracy based on this notion of correctness. since this task also involves the writing of proof fragments, we extend the same leniency toward minor syntax errors as in the proof-writing task. we provide more details in appendix b.2. the structure of all 300 problems is similar to that of pl 1 : each problem consists of a number of premises and a target conclusion. in all 300 cases, the conclusion does follow from the premises. in this paper we only study proof writing in pl 2 . the task involves ndl f , an even simpler version of ndl that replaces all inference rules with a single inference syntax form: p from p 1 , . . . , p n . the semantics of this form are simple: conclude p on the basis of p 1 , . . . , p n , where each p i is either a premise or an active assumption or a result deduced earlier in the proof, as long as (1) p indeed follows from p 1 , . . . , p n ; and (2) @xmath2. this specification is operationalized as follows. first, we check to make sure that @xmath3, or an active assumption or previously derived conclusion). if not, an error is reported. otherwise we make a call to a sat solver to see if p follows from p 1 , . . . , p n . if it does, the step is accepted, otherwise an error is reported. the restriction @xmath4. if no limit is placed, a model could avoid honest toil by generating an one-line proof: goal from premises. requiring @xmath5. 2 in this version of ndl, models are free to take much larger reasoning steps without bothering with tedious details. this ability to formulate helpful but straightforward lemmas without having to prove them in detail is crucial for pl 2 , because these problems are considerably more complex; demanding fully detailed ndl proofs for them would be neither fair nor realistic. it is also a more accurate reflection of how mathematicians actually work. while pl 2 problems are complex, they may be viewed as easy-hard problems. they are hard insofar as their general problem families are known to be challenging. but they are easy in that we make sure to only use problems whose size and difficulty are strictly bounded, in order to keep the tasks realistic and feasible. first, we ensure that the cnf encodings for the vast majority of problems (over 95% of them) contain no more than 100 clauses each (although we do not use cnf in the dataset, retaining full propositional-logic notation throughout). second, we ensure that every goal has a resolution proof with fewer than 150 steps. note that we generated most of these problems as unsatisfiability proofs for a list of formulas, but we then converted them to forward inference problems by taking the premises to be the tail of the list and the goal to be the negation of the head of the list. we solved each problem with vampire and analyzed the output resolution proofs to ensure that the overall number of inference steps was less than the maximum of 150 (we do not count cnf conversion steps). we then translated all resolution proofs produced by vampire into ndl f naturaldeduction proofs, which became the raw material for the proof-checking task: determine if the given ndl f proof is correct. all 300 ndl f proofs are correct by construction, so a model would attain perfect proof-checking accuracy if it deemed every proof to be correct. the proof-writing task was simply to write a proof in ndl f that derives the goal from the premises. ## results we use the following abbreviations: accuracies for proof checking and writing in pl 1 are given in tables 1 and 2 , respectively. proof unmasking and gap filling results for pl 1 are shown in these numbers reflect syntax repairs (such as parenthesis balancing) that we performed automatically on all generated pl 2 proofs. performance is considerably lower without these repairs (e.g., the raw accuracies of the top four models are as follows: 0.43 for grok-4, 0.37 for gpt-5, 0.33 for gemini-2.5-pro, and 0.21 for o3). finally, eq 1 results are shown in ## analysis models generally performed well on checking the simple proofs of pl 1 , and even on generating them, we asked all models to describe their proof strategies in natural language, and here is what o4-mini had to say about its proof for the pyramid of height 5: we build the desired disjunction (a 1 1 ∨ a 1 2 ) by lifting the given or-premises on the leaf atoms a 11 and a 15 up through each level of implications. at each stage we use nested case analyses (disjunction elimination) on the two orfacts for that level, together with the appropriate conditional premises, to derive the or-fact one level higher. repeating this from a 7 /a 8 /a 9 /a 10 up to a 2 /a 3 and finally a 1 yields (a 1 1 ∨ a 1 2 ). even when the models get the proof wrong, the high-level strategy is often correct. for instance, even in some cases where o3 tended to avoid hard work by "proving" the conjecture with a single-line application of from to dozens of premises, it would still articulate a proper strategy. this separation between strategic competence (e.g., outlining the overall proof structure and identifying relevant lemmas) and formal execution highlights the promise of an agentic approach to theorem proving. in such a framework, llm-based agents act as planners that explore and propose viable proof strategies, while classical proof assistants or symbolic solvers serve as executors that enforce rigor at the formal level. iterative interaction between these components mirrors human mathematical practice, where conceptual insights typically precede fully formalized arguments, and points toward a scalable neurosymbolic paradigm that combines the generative strengths of language models with the reliability of symbolic verification. ## conclusions this paper presented proofgrid, a novel benchmark designed to assess the logical reasoning abilities of llms and lrms through tasks that demand rigorous proof construction, checking, and infilling across propositional and equational logic. unlike prior benchmarks that focus solely on answer accuracy, proofgrid emphasizes the integrity of reasoning processes and offers a more accurate assessment of mathematical and logical competence. our results demonstrate that while state-of-the-art lrms exhibit very impressive capabilities on simpler inference problems, they continue to struggle with more challenging tasks, especially in reasoning over structurally rich problems. nonetheless, instances of high-quality reasoning, especially on problems requiring multi-step abstraction such as dag pebbling, suggest that these models are beginning to develop powerful inferential strategies. the results on the novel tasks of proof unmasking and gap-filling are particularly impressive. to solve these problems, models must reason about proofs themselves, identifying missing steps, determining the scope of relevant assumptions and lemmas, and reconstructing fully valid derivations. solving these tasks requires an awareness of proof structure that goes far beyond forward application of inference rules. while the masked proofs are relatively simple, it is nevertheless notable that leading lrms perform quite well, suggesting that these systems are beginning to exhibit competence in reasoning about reasoning itself. proofgrid should provide a robust platform for tracking and accelerating these developments, underscoring the importance of proof-based evaluation as models move toward deeper integration into scientific and mathematical workflows. the implications of progress on proof-based reasoning extend well beyond benchmarking. the formal methods community has long regarded fully verified proofs of program correctness as the gold standard for software reliability, but such proofs have been prohibitively difficult and resourceintensive, reserved mainly for mission-critical sys-tems. if ai models advance to the point of reliably generating formal proofs alongside code, this could radically transform software development: models could not only produce implementations, but also provide correctness guarantees that can be independently verified by trusted proof checkers. such a capability would represent a major step towards making llm-generated software genuinely robust and trustworthy.