Mathematical Reasoning › Types of Mathematical Reasoning

Mathematical problems span an enormous range of difficulty and type. The field has organized these problems into several categories, each with associated benchmarks, and understanding the categories helps practitioners choose the right evaluation for their use case.

Elementary arithmetic word problems were among the first mathematical tasks applied to LLMs. These involve translating natural language descriptions into arithmetic operations and executing them. The challenge is not the arithmetic itself but the mapping from language to mathematical structure.

Consider this problem: "Maria has 24 apples. She gives a third to her neighbor and eats 4 herself. How many does she have left?" Solving this requires understanding "a third" as division by 3, interpreting "gives" as subtraction, and executing the operations in the correct order. The arithmetic is trivial; the linguistic parsing is not. Early seq2seq models for this task outperformed many approaches not by reasoning better but by learning to identify which numbers appear in the problem and what operations connect them, a shallow heuristic that breaks on problems designed to thwart it.

The GSM8K dataset (Grade School Math 8000), introduced by Cobbe et al. in 2021, became the standard benchmark for this category. It contains 8,500 grade school math word problems requiring 2 to 8 steps of arithmetic reasoning. The problems are linguistically diverse and designed to resist simple pattern matching. Performance on GSM8K improved dramatically with scale and chain-of-thought prompting: early models scored in the 30 to 40 percent range, while GPT-4 achieves over 90 percent.

The progression on GSM8K traces a remarkable arc. GPT-3 with few-shot chain-of-thought reached approximately 35 percent. Code-trained models like Codex did better, around 60 percent, because code training appears to improve procedural reasoning. PaLM at 540 billion parameters with chain-of-thought reached 56 percent. Then a qualitative jump occurred as models were trained specifically on mathematical reasoning data: GPT-4 crossed 90 percent, and subsequent specialized models approached 95 percent. At that level, GSM8K is effectively saturated, which is why harder benchmarks have become the primary frontier.

Algebra problems require setting up and solving equations. The challenge escalates significantly when problems involve multiple variables, inequalities, or systems of equations. Performance drops sharply compared to arithmetic because algebraic manipulation requires more precise symbolic reasoning, not just parsing and arithmetic.

Symbolic mathematics extends this to calculus, differential equations, and abstract algebra. Tasks include computing derivatives and integrals, solving differential equations, and verifying algebraic identities. These are areas where traditional computer algebra systems like Mathematica or SymPy excel but LLMs struggle. The reason is structural: a CAS implements formal rewrite rules that are guaranteed correct. An LLM generates tokens that pattern-match to correct transformations when those transformations appear frequently in training data but has no fallback when they do not.

Mathematical olympiad problems represent the frontier of automated mathematical reasoning. Problems from competitions like the AMC (American Mathematics Competition), AIME (American Invitational Mathematics Examination), and IMO (International Mathematical Olympiad) require novel insight, multi-step reasoning, and often creative problem decomposition that goes well beyond applying standard techniques.

The MATH benchmark (Hendrycks et al., 2021) contains 12,500 problems from AMC, AIME, and other competitions across seven categories: pre-algebra, algebra, number theory, counting and probability, geometry, intermediate algebra, and precalculus. Initial LLM performance on MATH was poor, around 3 to 6 percent for GPT-3. Subsequent models with chain-of-thought reasoning and targeted training reached 50 to 80 percent. IMO-level performance remains elusive: the best current systems can solve only a small fraction of problems that top human competitors find straightforward.

What makes competition mathematics hard is not just difficulty. It is novelty. Competition problems are explicitly designed so that standard procedures do not directly apply. A student who mechanically applies every technique they know will eventually fail. Success requires seeing the problem from an unexpected angle. This creative element is precisely what pattern-matching systems lack by design.

At the most rigorous end lies formal mathematics: machine-verified proofs in systems like Lean, Coq, or Isabelle. These theorem provers require finding a correct argument and expressing it in a formal language with an explicit, checkable proof term. Every logical step must be justified by a specific tactic or lemma reference.

The MiniF2F benchmark tests whether LLMs can produce formal proofs for mathematical statements. Performance is substantially lower than on informal problem solving because every step must be formally valid, not just plausible. Current systems achieve roughly 50 percent on a curated subset of high school competition problems using best-of-N sampling, far below human experts.

The gap between informal and formal performance is instructive. In informal reasoning, a model can state "by symmetry" or "it is clear that" and receive credit for the final answer even if the intermediate argument is incomplete. In formal systems, every logical step must be justified with a specific tactic or lemma reference. This forces the model to make its reasoning fully explicit, exposing gaps that informal evaluation hides. Researchers increasingly view formal verification as a gold standard for measuring true mathematical understanding rather than sophisticated pattern matching. When a model produces a formally verified proof, you know with certainty that the reasoning is sound. When it produces an informal solution, you can only assess whether the reasoning looks convincing.