🤖 AI

ALPS: Measuring Valid Creativity in Large Language Models with Mathematical Construction

The paper introduces ALPS, a novel benchmark that rigorously measures valid creativity in large language models by tasking them with generating original, verifiable mathematical proofs or constructions for randomly generated equational laws, revealing that current models struggle significantly with the construction side and that most instances remain unsolved even by advanced automated provers.

Original authors: Eric Xie, Wenqian Ye, Aidong Zhang

Published 2026-08-18

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Eric Xie, Wenqian Ye, Aidong Zhang

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

In the modern scientific landscape, artificial intelligence has begun to step out of the role of a data processor and into the role of a discoverer. We are seeing machines that can propose new chemical compounds, suggest novel materials, and even formulate mathematical conjectures that humans have not yet considered. This shift raises a profound question: when a machine produces an answer that looks like a breakthrough, how do we know it is truly creative and not just a clever repetition of something it memorized during its training? True creativity in science requires two things: the solution must be original, meaning it has not been seen before, and it must be effective, meaning it actually works and solves the problem at hand. The difficulty lies in verifying these qualities. In many fields, judging whether a new idea is valid requires human experts to look at the result and decide if it is good, a process that is slow and subjective. In mathematics, where answers can be checked with absolute certainty, the challenge is different: the problems are often so complex that a computer cannot simply search through every possibility to find the answer, and the problems themselves are often fixed sets that the machine might have already studied.

To solve this dilemma, researchers at the University of Virginia have developed a new way to test artificial intelligence, a benchmark they call ALPS. This system is designed to measure "valid creativity" by presenting the machine with a specific type of mathematical puzzle that cannot be solved by memory or by following a standard routine. The puzzles are based on rules for how a set of items can be combined. Imagine a collection of objects and a rule for mixing any two of them together. The researchers generate a specific rule, or law, that describes how these objects must behave. The machine's task is to decide one of two things: either the rule is so restrictive that it forces all the objects to be identical, or the rule allows for a complex, infinite structure of objects that satisfies the condition. If the machine claims the structure exists, it must build a description of it. If it claims the objects must be identical, it must prove that no other possibility exists. The brilliance of this setup is that the answers can be checked by a computer with perfect accuracy, without any human needing to look at the result. Furthermore, the system can generate an endless supply of these puzzles, ensuring that the machine is always facing a problem it has never seen before.

The researchers tested this system using a variety of powerful automated reasoning tools, which are specialized computer programs designed to solve logical problems. They ran these tools against a pool of over four thousand of these generated laws. The results were stark. Even with a massive increase in computing power, the automated tools could only solve a tiny fraction of the problems. Specifically, a portfolio of eight different configurations of the best available provers managed to resolve only about two percent of the laws. When the researchers increased the computing budget by twenty times, they found only a handful of additional solutions, and none of them were the complex structures they were looking for; they were only proofs that the objects had to be identical. This suggests that the barrier to solving these problems is not a lack of computing power, but a lack of a method to invent the specific, tailored structures that each unique law requires. The machine simply does not know how to build the right kind of infinite structure from scratch.

The researchers then turned to large language models, the type of artificial intelligence that powers many of the conversational tools used today. They tested the strongest reasoning models available, giving them the same puzzles and the same chance to prove their answers. On the side of the task where the machine had to prove that all objects were identical, the best model succeeded in about fourteen percent of the cases, but only on the simpler problems. On the side where the machine had to construct a new, infinite structure, the results were even more telling: none of the models succeeded. When the models did attempt to build a structure, they consistently failed in one of two ways. Either they proposed a structure that was too rigid, collapsing all the objects into a single point and thus failing to show a complex solution, or they proposed a structure that was too loose, failing to follow the rules of the law they were trying to satisfy. In every instance, the machine could not balance the need to follow the rules with the need to create something new and complex.

The study concludes that while these artificial intelligence systems are getting better at following instructions and checking their own work, they still struggle with the core act of scientific discovery: inventing a new structure that fits a set of constraints. The researchers released their entire system, including the generator that creates the puzzles and the automated judge that checks the answers, to the public. This allows other scientists to continue testing and improving these models without running out of fresh problems. The findings suggest that the path forward for AI in science may not be about giving the machines more data or more time, but about teaching them how to propose and refine their own ideas in a loop of creation and verification. Until machines can reliably construct these tailored solutions, their role in scientific discovery will remain limited, unable to cross the gap between processing information and generating truly valid, original knowledge.

Technical Summary: ALPS – Measuring Valid Creativity in Large Language Models with Mathematical Construction

1. Problem Statement

Current evaluations of Large Language Models (LLMs) in scientific domains (e.g., theorem proving, molecule design) struggle to distinguish between valid creativity and mere memorization or routine execution. A solution is considered "validly creative" only if it satisfies two joint criteria:

Originality: The solution is not a repetition of training data or a known general procedure.
Effectiveness: The solution is objectively correct and provides value for the specific task.

Existing benchmarks fail to measure this combination reliably because they lack at least one of three necessary properties:

Verifiability: Solutions must be objectively checkable (not subjectively judged).
Renewability: New problem instances must be generable without limit to prevent training data contamination.
Constructiveness: The task must require a solution tailored to the specific instance, preventing solutions via memory or standard algorithms.

Static corpora (e.g., MATH, miniF2F) fail renewability; synthetic puzzles (e.g., random SAT) often fail constructiveness as they can be solved by known procedures; and open discovery tasks (e.g., molecule design) often fail verifiability due to subjective human judgment.

2. Methodology: The ALPS Benchmark

The authors introduce ALPS (Austin-Law Proof-Synthesis), a benchmark designed to fulfill all three properties simultaneously within the domain of equational theory.

Problem Formulation:

Domain: ALPS operates on magmas (sets with a single binary operation $\diamond$ ) and equational laws (universally quantified identities).
Task: Each instance is a law $L$ of the form $x = T[x, y, z, \dots]$ , where $T$ is a term of order five or more.
The Dichotomy: For any such law, exactly one of two conditions holds:
1. Trivial: The law entails $x = y$ , collapsing every model to a single element.
2. Austin: The law has a nontrivial model, which must necessarily be infinite (since all finite nontrivial models are ruled out by the benchmark's certification process).
The Challenge: The solver must either provide a deductive proof that $L \models x=y$ (Trivial side) or construct an infinite magma satisfying $L$ (Austin side).

Corpus Construction:

Generation: The corpus is grown via an extension engine. Starting from known Austin laws, variables in the term $T$ are recursively replaced with new operations (e.g., $v \to v \diamond w$ ). This ensures fresh, unseen problems can be generated indefinitely.
Screening & Admissibility: Candidates undergo a rigorous screening pipeline:
1. Finite-Model Filter: Discards laws with nontrivial finite models.
2. Admissibility Prover: Uses automated provers to certify that no nontrivial finite model exists. This relies on a logical consequence of finiteness: on a finite carrier, an injective map is surjective. The prover attempts to derive a contradiction from the law and the surjectivity of a subterm, certifying that any model must be infinite.
3. Deduplication: Equivalent laws (mutually entailing) are grouped into equivalence classes to ensure distinct problem counts.
Resulting Pool: From an initial generation of candidates, the authors produced a pool of 4,141 unresolved laws (the "hard tier") and a smaller set of "certified-easy" laws.

Answer Verification (The Automated Judge):
The judge verifies submissions through two distinct, fully automated channels with no human involvement:

Trivial Side: The LLM submits a chain of equalities. A harness auto-formalizes this into a Lean proof (checked by the Lean kernel) to verify that $L \implies \forall a, b: a=b$ .
Construction Side: The LLM submits a finite set of equations $E$ $E$ (a presentation). The judge verifies two claims using automated theorem provers (e.g., Vampire, E, Twee):
- Derivation: $E \vdash L$ (Every model of $E$ satisfies $L$ ).
- Satisfiability: $E \cup \{a \neq b\}$ is satisfiable (There exists a model of $E$ with at least two distinct elements).
- If both hold, the admissibility certificate of the instance guarantees the model is infinite.

3. Key Contributions

A Two-Sided Construction Task: A benchmark where every instance is certified to have a determinate answer (either trivial or infinite), isolating the need for creative construction.
Renewable Corpus & Generator: A public generator that mints fresh instances without limit, ensuring evaluation is never contaminated by training data.
Automated Judge: A system that certifies submissions via independent channels (Lean for triviality, automated prover certificates for construction) without human judges.
Strong Automated Baseline: A portfolio of eight configurations of leading provers (Vampire, E, Twee) that establishes the current "method-bound" limit of automation.

4. Experimental Results

Automated Prover Performance:

A portfolio of eight configurations resolved only 2.2% of the 4,141-law evaluation pool.
Increasing the compute budget by a factor of 20 added only 0.6% more resolved laws (all triviality proofs, no new models).
97.2% of the pool remains unresolved by any tested configuration, indicating the obstacle is the absence of methods to construct tailored infinite structures, not a lack of compute.
Side Finding: The authors resolved an order-5 law previously left open by the Equational Theories Project (ETP), confirming the existence of an infinite model via saturation.

LLM Performance:

Trivial Side: On a set of 63 "certified-easy" laws, the strongest model tested (o3) achieved a 14% pass rate (9 solutions) with waypoints (prover-derived lemmas) and 9.5% without. GPT-4.1 and o4-mini achieved 0%.
- Failure Mode: LLMs primarily failed by submitting chains containing invalid steps (steps not derivable from the law), which the harness rejected.
Construction Side: On a sample of 25 "hard-tier" laws (unresolved by automation), no LLM produced a verified solution.
- Failure Mode: Submissions were either too strong (entailed the law but collapsed to a single element, failing the distinctness check) or too weak (allowed distinct elements but failed to entail the law).
- o3 cleared exactly one of the two checks on all 25 laws. o4-mini and GPT-4.1 failed both checks on many laws.

5. Significance and Claims

The paper claims that ALPS successfully isolates valid creativity by removing confounds of memorization and routine execution.

Necessity of Creativity: The high failure rate of both automated provers and LLMs on the "hard tier" demonstrates that these problems cannot be solved by existing general procedures or brute-force search.
Nature of Failure: The specific failure profiles (invalid steps in trivial proofs; "too strong/too weak" presentations in construction) highlight that current models struggle with creative generation under constraints. They can often draft a structure but fail to balance global specifications without collapsing into degenerate solutions.
Scientific Parallel: The paper draws a parallel to the "specify–construct–verify" cycle in scientific discovery (e.g., molecule design), noting that ALPS makes every phase machine-checkable.
Future Direction: The authors suggest that the path forward lies in verify-and-refine loops (similar to Counterexample-Guided Inductive Synthesis, CEGIS), where solvers draft structures, receive automated feedback on validity, and revise.

The authors remain modest, noting that while the strongest LLMs show some capability on easy instances, they currently fail to construct valid infinite structures on hard instances, and the benchmark remains largely unsolved by current technology.