WordBench: A Benchmark for Learning and Search in Algebraic Word Problems

Mathematical discovery systems increasingly combine large language models (LLMs), reinforcement learning (RL), and formal verifiers, yet most mathematical benchmarks remain static collections of problems. We introduce WordBench, a benchmark for algebraic word problems that combines procedurally generated datasets with executable search environments and exact verification. A word problem asks whether finite symbolic expressions, or words, represent the same mathematical object under specified generators and relations. An open example is the Andrews–Curtis conjecture, where a successful certificate is a sequence of allowed presentation moves transforming a relator tuple to the trivial presentation. WordBench contains 24 families spanning rewrite and witness-construction problems, each with generative datasets, a deterministic symbolic search environment, and exact verification of submitted traces, action sequences, or algebraic objects in the Lean theorem prover. The released corpus, WordBench-Lit, contains $13,324$ instances, and the underlying data generators can produce fresh instances beyond this set. We benchmark classical breadth-first search, PPO agents, and LLMs under common verifier-defined success criteria. The results reveal strongly solver-dependent empirical difficulty: for example, PPO solves $99.1$% of instances on Thompson's group $F$ while some open-source LLMs remain below $10$%, whereas frontier LLMs achieve near-perfect performance on Artin–Tits and braid rewriting, where PPO remains below $1$%. More broadly, frontier LLMs solve a large fraction of WordBench-Lit, but performance remains nonuniform across families, with Andrews–Curtis being substantially less solved. Beyond benchmark performance, WordBench's environments enable controlled experiments on search behavior, learning dynamics, and empirical relationships across mathematical problems. As a case study, we find that cross-family PPO transfer learning can solve new dataset instances not discovered by target-only training, with different source families providing complementary coverage. Together, these results position WordBench as a common verifier-facing benchmark for studying learning and search across diverse mathematical word problems.