Capability Frontiers › Code and Mathematical Reasoning

Two domains deserve special attention as capability frontiers because they offer rigorous external verification: code and mathematics. Unlike natural language tasks where quality is often subjective, code either runs correctly or it does not, and mathematical proofs are either valid or invalid. This objectivity makes these domains particularly valuable for studying capabilities that transfer as opposed to fluent-sounding but potentially incorrect outputs.

The ability to write functional code from natural language descriptions has improved dramatically with scale. Modern large language models can produce working solutions to competitive programming problems, implement algorithms from high-level descriptions, debug code from error messages, identify security vulnerabilities, and translate programs across programming languages. This capability has practical importance, with language models now used routinely in software development workflows.

What makes code generation particularly interesting as a capability domain is the feedback loop it enables. A model that writes code and then executes it can observe whether the code works and use that feedback to iterate. This grounded evaluation loop is qualitatively different from generating natural language, where correctness is much harder to assess automatically. A model editing code based on test failures has a reliable signal; a model editing an essay based on vague feedback is working with a noisier signal.

Code synthesis benchmarks like HumanEval and MBPP have shown substantial improvement as models scale, but perhaps more telling is performance on harder benchmarks like competitive programming datasets from platforms like Codeforces or LeetCode. These require syntactically correct code and algorithms that handle edge cases efficiently, a capability that requires understanding the problem structure rather than retrieving common patterns. Performance on these harder benchmarks remains substantially below top human competitors, even for the largest models, suggesting that algorithmic creativity and deep problem analysis remain challenging.

The ability to work with code also enables interesting forms of mathematical and logical reasoning that go beyond direct proof. A model that can write and execute programs to check mathematical conjectures on small cases, or to search for counterexamples, is using computation as a cognitive tool in a way that can substantially exceed pure language-based reasoning.

Mathematical reasoning represents a frontier where language models show impressive but inconsistent performance. Models can solve multi-step algebra problems, apply calculus, reason about probability, and work through geometry proofs. On olympiad-level mathematics, performance has improved substantially with scale and with specialized training, with some models reaching performance levels competitive with strong human competitors on subsets of olympiad problems.

The interesting cases for understanding capability are where models fail. They tend to fail on problems that require a non-standard approach that differs from anything in the training distribution, problems requiring careful tracking of many interleaved constraints (where a single tracking error invalidates the entire solution), and problems where a common-sense shortcut would produce the wrong answer. These failure modes suggest that mathematical problem-solving involves at least two distinct components: skill-based (knowing which techniques to apply, recognizing problem types) and reasoning-based (working through the implications step by step), with models currently excelling more at the former than the latter.

This distinction is important. A student who knows calculus techniques can solve most standard calculus problems by pattern matching to technique types. A research mathematician solving a novel problem must reason from first principles, which requires something more than technique recognition. Current models appear to be strong pattern matchers but weaker at the kind of creative first-principles reasoning that characterizes original mathematical insight.

Formal theorem proving offers the cleanest evaluation because proofs can be mechanically verified. Systems that interact with proof assistants like Lean or Coq get immediate, reliable feedback on whether each step is valid. This setup has enabled interesting research: models trained with feedback from proof assistants substantially outperform those trained on informal mathematical text alone. The reason appears to be that the proof assistant provides a ground-truth signal at each step of the proof, allowing the model to learn which reasoning steps are valid without having to rely on self-evaluation or human feedback. This finding suggests that grounded verification loops are important for developing reliable mathematical reasoning, just as code execution is important for code generation.

Some recent work has explored "neurosymbolic" approaches that combine language model generation with formal symbolic reasoning: the language model generates proof strategies and candidate steps, while the proof assistant verifies them and signals when to backtrack. This division of labor plays to the strengths of each component: the language model is good at generating plausible-looking next steps from a large distribution of possibilities, while the symbolic system is reliable at verification. Early results have been impressive on certain classes of formal mathematics, though scaling to graduate-level research mathematics remains an open challenge.