An in-depth human study of the mathematical reasoning abilities in Large Language Models (2025)

Abstract: We study the generalization capabilities of large language models (LLM) through the lens of mathematical reasoning, asking if these models can recognize that two structures are the same even when they do not share the same nomenclature. We propose a human study to evaluate if LLMs reproduce proofs that they have most likely seen during training, but when the symbols do not match the ones seen. To test this in a controlled scenario, we look at proofs in propositional calculus , foundational for other logic systems, semantically complete and widely discussed online. We replace the implication operator ( \rightarrow ) with an unrelated, arbitrary symbol ( \spadesuit ) and ask experts to evaluate how the output of a selection of LLMs changes in terms of compliance, correctness, extensiveness and coherence. Our results show that nearly all our tested models produce lower quality proofs in this test, in particular open-weights models, suggesting the abilities of these LLMs to reason in this context have important limitations.

## introduction mathematical reasoning is a key aspect of human intelligence that encompasses pattern recognition and logical entailment. the development of artificial intelligence systems capable of tasks such as solving applied and theoretical mathematical problems has been a long-standing focus of research in the fields of machine learning and natural language processing, dating back to the 1960s @xcite . our interest in this topic rises from recent attempts to use language models for theorem proving by means of itps' programming languages and databases of theorems with their proofs. deep learning models can be trained in one of these many programming languages, and then used to generate mathematical proofs. data sources for neural theorem proving in itps include interactive learning environments that interface with itps, and datasets derived from proofs in itp libraries. when it comes to mathematical reasoning, and in particular to the ability of models to understand logical statements, we note that despite the abundance of studies, previous works generally assume that only "variables" are the ones not constant throughout problems. however, we see that in mathematics different nomenclatures are used in different areas, as well as in different time periods, to express the same ideas. examples of this fact include the use of ⊃ @xmath0; leibniz's df dx , lagrange's f ′ , and newton's ḟ notation in differential calculus; the different notation for the inner product for physicists ⟨•|•⟩ and for mathematicians ⟨•,•⟩; prefix f (x) and postfix (x)f notations for functions; and different notations for the von neumann generated algebra, such as: w * (•,•) and • ∨ •, to name a few. as we attempt to use llms to tackle proof generation tasks, for example using the "informal theorem proving" approach (please see §2 for more details on this), we think researchers and practitioners need to take this fact into consideration. furthermore, and in contrast to all these models, current state-of-the-art models in nlp are trained on large datasets of text extracted from the web. in this case, we have limited or no control on the kinds of expressions and/or operators that the models are exposed to during training. we can, however, still assume the models have been exposed mostly to the standard nomenclature. given this scenario, we ask: can these models recognize that two structures are the same even if they do not share the same nomenclature? for example, can models reproduce proofs that they have most likely seen during training, but when the symbols do not match the ones seen? if so, to what extent are these proofs plausible and correct? in order to answer these questions, we perform an in-depth human evaluation to assess the quality of the output generated by llms when prompted to generate proofs similar to the ones seen during training but with expressions that use a different notation. more recently, work on "informal" theorem proving has presented an alternative medium for theorem proving, in which statements and proofs are written in a mixture of natural language and symbols used in "standard" mathematics (e.g., in l a t e x), and are checked for correctness by humans. here we find the work of @xcite who developed naturalproofs, a large-scale dataset of 32k informal mathematical theorems, definitions, and proofs, and provided a benchmark for premise selection via retrieval and generation tasks. most of the data is taken from websites like proofwiki.com, and though this enables more flexibility when proving, the task is approached in a way similar to itps. ## proposed approach to study the posed research questions under a controlled scenario, we look at proofs in propositional calculus, a branch of formal logic that deals with propositions, which can be true or false, and relations between propositions, including the construction of arguments based on them @xcite . propositional calculus, also known as zeroth-order logic, does not deal with quantifiers over nonlogical objects (unlike first-order or higher-order logic). there are several reasons that we think make this the ideal scenario for our study: (1) all the machinery of propositional logic is included in first-order logic, higher-order logic, and all mathematics. in this sense, propositional logic is the foundation of other logic systems; (2) propositional calculus is semantically complete, i.e. any tautology (true formulas) can be proved with the formal axioms and the rules of inference of the system; propositional calculus is typically studied with a formal system, which contains a formal language and a deductive system. the language is composed of a set of well-formed formulas, which are strings of symbols from an alphabet (composed of propositional variables and propositional connectives) formed by a formal grammar (formation rules). the deductive system, in turn, contains the rules of inference, a function which takes premises and returns conclusions. to assess how models generalize in this scenario, we compared proofs generated by these models using "usual" and "unusual" symbols for connectives. we use a standard proof system usually referred to as a hilbert system. this is a deductive system that generates theorems from axioms (tautologies taken as starting point for further reasoning) and modus ponens. modus ponens can be summarized as: if p implies q and p is known to be true, one can conclude that q must also be true. it is generally expressed as {@xmath1, p } ⊢ q, where the turnstile symbol (⊢) denotes derivability, i.e. there is a formal derivation of a theorem from the axioms. as for connectives, we limit it to the logical and (∧), logical or (∨), the negation operator (¬), and the implication operator (→). for the axioms, we use a common set of 14 axioms used in undergraduate courses, shown in figure 1 . for our study, we propose to replace the implication operator (→) with an unrelated, arbitrary symbol (♠). in order to produce a significant perturbation in the input token distribution, we specifically select the unicode representation of the symbol (u+2660) for the replacement. alternative replacements are left for future work. we select two common theorems from propositional calculus extracted from @xcite , as shown in figure 2 and test models in two different scenarios, as follows. full context (fc) our first evaluation scheme is intended to simulate a noisy retrieval step prior to the proof generation. concretely, we offer the model the complete set of axioms together with the selected rule of inference, modus ponens. thus, in this scenario, we can also test the model's ability to identify and retrieve only the axioms that are needed to prove the selected theorem. ## results for this study, we consider the following models: (1) api-based llms, including chatgpt (gpt-3.5-turbo-0125) @xcite , claude 3 opus (claude-3-opus-20240229) @xcite , (2) open-weights models, including llama 3 (meta-llama-3-8b-instruct) (grattafiori and the llama 3 team, 2024; ai@meta, 2024), llama 3.1 (llama-3.1-8b-instruct) (int) and gemma 2 (gemma-2-9b-it) @xcite . the latter models are obtained from huggingface, and quantized to 4-bits @xcite to fit our gpu memory. for each input, we obtain 3 outputs from each model using a different random seed. we computed the following metrics to summarize model behavior and measure performance. we also observe that not only compliance did not follow the decrease trend seen for other metrics, but also that most models showed an increase in this metric when prompted with the arbitrary symbol. in fact, this variation in compliance appears to strongly correlate with our ♠-based replacement scenario. overall, the average compliance with the original symbol (→) is 43.85%, which compares unfavorably against 71.89% for our replacement scenario (♠). we note that such a significant gap is not evident when looking at performance differences due to variations in context, where we observe an average compliance of 60.22% for sc and 63.39% for fc. since invoking facts outside of the givens in the prompt is a big factor in how we compute the compliance criteria, we believe this counterintuitive increase in value can be at least partially explained by the changes in the semantics induced by our symbol replacement. intuitively, the semantic similarity between these expressions and the examples seen during training should be lower, making it more unlikely for the model to retrieve relevant content seen during training, even if not useful for the proof. to delve further into the data, we split the clarity into intervals, as seen in to better understand the impact of the different scenarios on models, we compute the difference in model performance when the model is presented with the perturbed input versus the original symbol and when the model is presented with the selected context versus the full context. for this study, in addition to the metrics introduced before, we also compute: for chatgpt, we noticed that there is a bigger drop in extensiveness for "sc to fc" than "→ to ♠", but the drop in correctness and flow is smaller for "sc to fc" than "→ to ♠". this suggests that chatgpt struggles to retrieve the necessary axioms from the givens, but the change in context does not seem to significantly impact its correctness. for claude, both changes seem equally challenging, with the change in context having slightly bigger impact on extensiveness, correctness, and flow. claude 3 opus was the only model to have a decrease across all metrics for both differences. there are three different types of steps that could appear in our studied proof: hypotheses, axioms, and rules of inference. with that in mind, we split each of our metrics into these three cases and summarize the results on we also observed that gemma 2 never attempted to use an axiom (all values are 0%), and its best performance was on extensiveness for hypotheses. chatgpt had the biggest gap on extensiveness for axioms (sc vs fc), and on the full context scenario, it always made mistakes on substitution. claude 3 opus was slightly worse at applying rois than making substitutions on easiest scenario (sc @xmath2, but it did much worse at substitution than on rois on the hardest scenario (fc with ♠). its only use of unnecessary steps was on the hardest scenario and it used extra axioms. we also analyze the spans highlighted by the annotators, alongside the comments left by them on each location. we collected a total of 304 annotations derived from highlighted spans, out of which, 170 were unique. we note that more than 99% of these comments denote errors made my the model, often related to the questions that were presented to the annotators. based on this insight, we use this information to empirically estimate "when" models tend to make their first mistake as they generate the requested proof. concretely, we compute the position in terms of number of characters, normalized by answer length, of the start of the spans highlighted by the annotator. these relative positions are then averaged for all the answers for each model. as shown in finally, we analyze the content of the annotations for each of the highlighted spans. we think these may provide additional insights on the nature of the mistakes by the models. in order to perform this analysis, we encode the annotations with sentence-bert @xcite , via the all-minilm-l6-v2 model, using the sen-tencetransformers foot_0 package. we then perform clustering using k-means via its scikit-learn implementation @xcite . we compute clusters varying parameter k, the number of clusters, with @xmath3, . . . , 15, and select the top 3 results as based on silhouette scores @xcite . finally, we visually analyze these best results by performing pca on the embedded annotation comments, and plotting them on a 2d chart, coloring the examples by cluster. we find the that @xmath4, highlighting four distinct behaviors models often engage in the following cluster, which here we represent by the instance closest to the centroid: (cluster 0) "inability to recognize the unicode symbol used to replace the implication operator", (cluster 1) "does not follow from axiom", (cluster 3) "substitution issue", (cluster 5) "incorrect usage of modus ponens". discussion it is known that if we have a theorem in propositional calculus, then it has arbitrarily many proofs. one cannot even guarantee there is a unique "minimal length" proof. hence, one may question our comparison of model outputs against a fix proof. however, since we study changes, we need a baselines to compare against. this also makes it easier to evaluate the output systematically and consistently. we also note that if we ## conclusions this paper studies the generalization capabilities of llm through the lens of mathematical reasoning. we perform an in-depth human evaluation of the output of llms when they are prompted to produce basic proofs in propositional calculus, comparing their answers when we replace the implication operator (→) with an unrelated, arbitrary symbol (♠). our results show that nearly all our tested models produce lower quality proofs in this test, in particular open-weights models, suggesting the abilities of these llms to reason in this context have important limitations. for future work we would like to extend this study to incorporate more proofs, models, and multiple annotators. we would also like to analyze how models react to other input perturbations, for example using other replacement symbols, and/or alternative representations for them.