PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Eric Xie, Wenqian Ye, Aidong Zhang

arXiv:2608.15979v1cs.AI

TL;DR

It is difficult to tell whether an LLM’s apparently creative scientific output is original and correct. ALPS addresses this with fresh equational-law problems requiring either an infinite construction or a proof of impossibility, and finds that automated provers resolve only 2.2% of 4,141 laws while the hard remainder persists across tested budgets.

  • Problem

    Existing evaluations make it difficult to establish whether open-ended LLM outputs are both original and effective creative solutions.

  • Method

    ALPS generates fresh admissible equational laws requiring either a tailored infinite model or a proof of triviality, with automated certificate verification.

  • Results

    2.2% of 4,141 laws are resolved by an eight-configuration prover portfolio, while a twentyfold budget increase adds only 0.6%.

  • Takeaways & Limitations

    ALPS exposes constrained creative generation as a difficult capability and motivates verify-and-refine approaches for satisfying global specifications.

  • Takeaways & Limitations

    Language-model solve counts are stochastic pass@1 samples, so waypoint effects are suggestive and the reported performance is a lower bound.

Abstract

from arXiv · show

Large language models produce outputs presented as discoveries - new proofs, conjectures, or molecules. Whether such an output that appears creative is truly original and effective is hard to establish: open-ended outputs require subjective judgment, the output may replicate something seen in training, or the task may be too simple to need creativity. We present ALPS (Austin-Law Proof-Synthesis), a benchmark that designs a task to measure valid creativity: producing a solution that is original and can be proven correct. Each instance is a single equational law, certified to require either the construction of an infinite mathematical structure satisfying the law, or a proof that no such structure exists. Submissions are verified by automated proof checking with no human involvement, and a public generator produces new instances without limit, so LLMs are never evaluated on problems they may have seen. A portfolio of eight configurations of leading automated provers resolves 2.2% of the 4,141-law evaluation pool, and a twentyfold budget increase adds 0.6%: the obstacle is not compute, but the absence of any method that produces the tailored structure each law requires. Under a fixed protocol, the strongest reasoning model we test succeeds in 14% of instances on the proof side, but none on the construction side. The remaining 97.2% of the pool is unresolved at every configuration and budget we test. We release ALPS in full: the corpus, the generator, and the automated judge.

1 Introduction

ALPS measures valid creativity through renewable, automatically verified equational-law problems that require either proving triviality or constructing a satisfying infinite model. Its evaluation shows that current automated provers resolve only a small fraction of instances, establishing a constructive challenge with fresh problems and no human judging.

  • Benchmark design: ALPS combines objective verification, unlimited renewal, and construction so success cannot rely on subjective judgment, training contamination, or an instance-independent procedure.Formal mathematics supports automatic proof checking and unlimited problem generation; ALPS establishes construction by design.
  • Motivation: Valid creativity requires creativity to be necessary and the answer to be soundly justified, avoiding apparent novelty or effectiveness alone.The benchmark targets outputs whose originality and correctness are both established.
  • Benchmark design: Each ALPS law has no nontrivial finite model and requires deciding between triviality, proved deductively, and Austin, established with a constructed infinite model.Every answer is settled by automatic verification, making the task two-sided and machine-checkable.
  • Results: 2.2% of 4,141 screened laws were resolved by eight prover configurations, while a twentyfold budget increase added 0.6%.The remaining laws produced neither a model nor a triviality proof under any tested configuration, despite certified determinate answers.
  • Release: ALPS releases a corpus, a public generator producing fresh instances without limit, and an automated judge using independent Lean and automated-prover certificates.The judge operates with no human in the loop.

2 Related Works

Prior benchmarks typically combine objective scoring with either fixed datasets or limited task difficulty, leaving gaps in measuring originality and validity. ALPS builds on machine-checked proofs, equational-theory benchmarks, and model-finding methods targeting difficult Austin laws.

  • Benchmark limitations: Existing benchmark families provide objective scoring but fixed evaluation sets can enter training data, allowing performance to reflect memorization.These families span competition mathematics, graduate science, coding, and formal proof.
  • Automated verification: Machine verification lets ALPS certify submitted proofs mechanically, including laws quantified over infinitely many inputs.Lean’s kernel checks accepted proofs, while universal laws are checked symbolically rather than case by case.
  • Equational theories: Equational-theory research automatically studies implications among thousands of small laws, identifying Austin laws as especially difficult because finite-model search and short derivations do not settle them.Austin laws are those whose only nontrivial models are infinite.
  • Model construction: Twee uses unfailing Knuth–Bendix completion to orient equations into rewrite systems and can extract a model when saturation halts without contradiction.A recent case study demonstrated explicit model extraction from such a saturation.

3 The Austin-Law Proof-Synthesis Benchmark

ALPS measures valid creativity by asking whether a law has a nontrivial model, while admitting only laws certified to have no finite nontrivial model. Its automated judge then verifies either a proof of triviality or a finite presentation of an infinite model.

  • Corpus generation: The corpus grows from proven Austin seed laws by extending terms, increasing the supply of new admissible instances without limit.Extensions replace an occurrence of a variable with v ⋄w or w ⋄v, often preserving the mechanism that prevents finite models.
  • Task definition: Each ALPS instance asks whether a law has a nontrivial model; admissibility forces the answer to be either triviality or an infinite nontrivial model.The benchmark excludes laws with nontrivial finite models using a machine-checked admissibility certificate.
  • Admissibility: Admissibility is certified by proving that the law together with a surjectivity consequence entails x = y, showing every finite model is trivial.Candidates with nontrivial finite models are filtered out, while uncertified candidates remain unadmitted.
  • Deduplication: 33,936 of 34,191 Austin-law pairs are separated by models found during screening, while the prover settles the remaining equivalence checks.Equivalent laws entail one another and have the same models; separating models witness that one implication fails.
  • Automated judge: The judge accepts submissions only after fully automatic verification: Lean checks triviality proofs, while an automated prover checks constructed-model certificates.For construction, the submission is a finite presentation that must entail the law and remain satisfiable with two distinct elements.

4 Experiments

Experiments show that automated provers resolve only a small fraction of ALPS laws, leaving a large hard tier. Under a fixed verification protocol, o3 solves some trivial-side instances but no tested model constructs a valid solution for the sampled hard-tier laws.

  • Automated portfolio: 2.8% of the 4,141-law residual is reclassified by the full prover portfolio, while 4,027 laws remain unresolved at budgets up to 600 seconds.The additional resolutions comprise 110 triviality proofs and 4 completion-only models.
  • Automated portfolio: 97.2% of the 4,141-law residual remains unresolved, and every later resolution after 30 seconds is a triviality proof.All models appear at 30 seconds.
  • Trivial-side LLM evaluation: 9.5% pass@1 is achieved by o3 at medium reasoning effort without waypoints on 63 certified-easy trivial-tier laws, rising to 14% with waypoints.GPT-4.1 and o4-mini produce no verified solutions even with waypoints, while o3 at low effort also produces none.
  • Trivial-side LLM evaluation: 50,000 completion tokens is the median cost of a solved law, with most verified chains accepted on the second or third feedback round.Failures predominantly contain steps that are not applications of the law.
  • Construction-side LLM evaluation: 0 of 25 hard-tier laws are solved by o3, o4-mini, or GPT-4.1 over three feedback rounds, and none pass both construction checks.Twenty-three of o3’s 25 presentations entail the law but admit only one-element models, failing the nontriviality check.

5 Discussion

The discussion attributes solver failures to weaknesses beyond mathematical reasoning: trivial-side errors center on step validity, while construction-side errors reflect difficulty balancing global correctness against nondegeneracy.

  • Trivial-side failures concentrate in invalid steps rather than flawed planning.The passage suggests self-verification at each step could address this weakness.
  • Construction-side submissions fail by being either too strong or too weak, as reported by the judge.
  • Passing both checks requires satisfying a global specification without collapsing into a degenerate solution.The passage characterizes both solver weaknesses as involving creativity.

6 Conclusion · Appendix · A Worked Example: Laws 12857 and 33436

ALPS measures valid creativity through freshly generated equational laws requiring either construction of an infinite mathematical structure or proof of impossibility, with sound justification. A worked example presents laws 12857 and 33436 as dual open cases whose resolution is equivalent.

  • 6 Conclusion: ALPS benchmarks valid creativity by requiring solutions that are both creative and soundly justified.Each instance is designed so creativity is necessary and answers must be certified correct.
  • 6 Conclusion: Each instance asks for an infinite structure satisfying a freshly minted law or a proof that no such structure exists.Instances are certified in advance so finite search cannot settle them.
  • A Worked Example: Laws 12857 and 33436: Laws 12857 and 33436 were recorded as having only trivial finite models, while infinite-model existence remained unresolved.The Equational Theories Project recorded this status for both laws.
  • A Worked Example: Laws 12857 and 33436: Law 12857 is x = y ⋄((x ⋄(y ⋄(z ⋄z))) ⋄y).This is the first law in the ETP numbering used for the worked example.
  • A Worked Example: Laws 12857 and 33436: Law 33436 is x = ((y ⋄(((z ⋄z) ⋄y) ⋄x)) ⋄y).This is the second law in the ETP numbering used for the worked example.
  • A Worked Example: Laws 12857 and 33436: The two laws are duals because reversing every ⋄ argument occurrence in one produces the other.A magma satisfies one law exactly when its opposite magma satisfies the other.
  • A Worked Example: Laws 12857 and 33436: Resolving either law resolves both because the pair is a single open case up to duality.Their equivalence follows from the correspondence between a magma and its opposite magma.

A.1 Two independent certificates … B LLM Evaluation Protocol and Prompts

The paper validates its model with two independent prover certificates and direct checks, while explaining why the resulting ordered presentation is not currently Lean-checkable. It then fixes the LLM evaluation harness, separates trivial derivation from construction, and specifies prompts, feedback, and submission constraints.

  • A.1 Two independent certificates: Both laws were resolved twice by methods sharing no search strategy, with Twee independently returning CounterSatisfiable for each.Twee derived 55 rules for 12857 and 54 for 33436, providing a second certificate by a different route.
  • A.1 Two independent certificates: Vampire terminated with SZS status Satisfiable in 7.95 seconds and 126 MB of memory, printing an active set of 357 unit equations.The certificate describes a model in which x = y fails.
  • A.2 Verifying the presentation: The saturated presentation is directly checked for ordering consistency, law validity on ground instances, and the remaining certificate properties.The released certificate and ordered_model.py reproduce all three checks.
  • A.3 Why this model is not Lean-checkable today: The model is graded by the prover certificate rather than the Lean kernel because its ordered presentation is not an off-the-shelf term rewriting system.A substantial minority of the 357 equations carry a free variable on each side, preventing usual orientation into rewrite rules.
  • A.3 Why this model is not Lean-checkable today: Lean formalization awaits a machine-checked ground confluence proof because available certifiers check plain rewriting systems, whereas this object is ordered.Algebraic models are Lean-checkable today, but no admissible law admits one.
  • B.1 The fixed protocol: Every solver receives the same law, task statement, and fixed answer format, may submit up to three times, and receives verbatim verdict feedback after each attempt.Saturation provers are withheld, while the harness is frozen across language models; provider-default nondeterministic sampling prevents bitwise reproduction, so run-to-run variation is measured.
  • B.2 The trivial channel / B.3 The construction channel: The trivial channel requires a JSON chain of valid law applications between arbitrary elements, while the construction channel requires a JSON finite presentation of unconditional equations.Waypoints can shorten planning but cannot repair invalid steps; construction submissions exclude implications, disequations, and literal restatements of x = y.
  • B.4 Prompts: Figures A1 and A2 provide the verbatim trivial- and construction-channel prompts, with {law} and {hint_block} substituted at call time and rejection feedback appended in later rounds.The hint block is empty without waypoints and lists prover-derived waypoint lemmas otherwise.

C Automated Baseline: Per-Configuration Results

Across eight prover configurations, resolutions were concentrated at the 30-second budget, while construction results came entirely from twee/complete and the sweep progressively reduced the unresolved pool.

  • Portfolio and overlap: Eight configurations evaluated the 4,141-law residual, with overlapping counts because multiple configurations could resolve the same law.The portfolio included five Vampire 5.0.1 modes, two E 3.3.5 modes, and Twee 2.6.1.
  • Budget profile: Every configuration concentrated its resolutions at the 30-second rung rather than resolving laws at a steady rate with added budget.The table showed no configuration whose resolutions increased steadily across higher per-configuration budgets.
  • Configuration contributions: All four models recovered by the submitted sweep came from twee/complete, while Vampire saturation modes resolved 14 laws each by proving triviality.Thus, the portfolio’s construction side rested on a single configuration.
  • Sweep progression: 4,141 laws reached the 30-second rung, followed by 4,050, 4,042, 4,037, and 4,033 at successive rungs as resolved laws exited the ladder.The sweep removed a law from later rungs as soon as any configuration resolved it.

D LLM Failure Analysis

Across 25 hard-tier laws per model, no submission passes both validity checks. Failures include overstrong or understrong presentations, both-check failures, and unsound chains whose individual steps do not apply the law.

  • 75 final-round submissions are classified by whether they satisfy the entailment and nontrivial-model checks.Each model attempts all 25 laws over three feedback rounds, leaving one final submission per law.
  • 25 laws partition into too-strong, too-weak, or both-fail submissions according to which checks succeed.The final column counts laws clearing exactly one check and equals 25 minus the both-fail count.
  • At every setting, trivial-side failures arise when submitted chains contain steps that are not applications of either side of the law.The harness rejects these chains during matching, indicating unsound individual-step execution rather than failure to plan a route between a and b.

E Corpus Yield and Renewability · F Validation of the Automated Judge

The corpus continues to yield fresh and genuinely distinct laws as candidate order increases, supporting renewability. The automated judge uses self-tests, strict proof-footprint checks, and channel-specific controls to reject invalid submissions while accepting valid references.

  • E Corpus Yield and Renewability: The corpus claims no terminal order, with fresh instances mintable after any training cutoff, but yield must be checked because thinning could eventually limit supply.This passage frames the renewability claim as requiring an empirical yield check.
  • E Corpus Yield and Renewability: 10,474 candidates were screened, with yield reported by candidate-law order rather than as a single aggregate count.The raw Austin-law count falls from 117 at order 7 to 105 at order 8 because fewer order-8 candidates were screened.
  • E Corpus Yield and Renewability: 20.5, 24.4, and 25.4 admissible laws per thousand screened candidates occur at orders 6, 7, and 8, respectively.Order 5 is excluded because those laws are ETP’s.
  • E Corpus Yield and Renewability: 16.9, 19.4, and 16.2 new-equivalence-class laws per thousand occur at orders 6, 7, and 8, showing continued distinct-problem production.The density is not monotonic, so the paper does not claim it rises.
  • F Validation of the Automated Judge: Both judge channels run released control suites before evaluation, re-runnable with --selftest.This provides a reproducible pre-evaluation check of judge behavior.
  • F Validation of the Automated Judge: The trivial channel requires exact-type Lean elaboration and an axiom footprint within {propext, Quot.sound, Classical.choice}.The allowlist rejects unanticipated axioms and explicitly forbids sorryAx, Lean.ofReduceBool, and Lean.trustCompiler.
  • F Validation of the Automated Judge: Seven negative controls reject proof-avoidance tactics before Lean runs, while a reference answer passes the scan and compiles with an allowed footprint.The controls cover sorry, false axiom declarations, namespace shadowing, redefining the law predicate, native_decide, and incorrect theorem naming.
  • F Validation of the Automated Judge: The construction channel uses three failure controls and tests presentations against two checks; the law itself is positive on the seed but diverges on the hard tier.Table A2 classifies hard-tier submissions as too strong, too weak, or clearing exactly one check.

G Diversity of the Constructed Models

The 195 construction classes coincide exactly with the 195 logical equivalence classes, validating deduplication by an independent model-satisfaction test. Cross-class transfer is rare, so the constructed models are genuinely distinct rather than reusable instances of one shared construction.

  • Equivalence of classes: 195 construction classes coincide exactly with 195 logical classes, showing that model-satisfaction equivalence matches logical equivalence.Every constructed model was tested against all 262 proved laws, producing 68,382 ordered pairs with no missing models.
  • Cross-class transfer: 173 of 68,382 ordered pairs transfer across class boundaries, or 0.25%, and transfer is rare and one-directional.A model transfers when it satisfies another law in addition to its own; no cell is undecided, and every model satisfies its own law.
  • Model coverage: A typical model satisfies only its own law: median coverage is one law, mean coverage is 3.67, and maximum coverage is 19.Coverage counts the laws satisfied by each constructed model across the 262-law test set.
  • Construction diversity: The 195 classes are construction-distinct, rather than logically distinct views of a shared construction that could be learned once and reused.Mutual model-satisfaction and logical equivalence identify the same relation, while cross-class transfer remains rare.

H Computing Infrastructure and Cost

The experiments used a 32-core AMD EPYC system for prover sweeps and the Open-Router API for language-model runs. Certified-easy language-model solutions were token-intensive, costing a median of 49,221 completion tokens per solved law.

  • Prover infrastructure: 32 physical cores powered the prover experiments, with one portfolio shard assigned to each core and no sibling-hyperthread contention.The machine had dual-socket AMD EPYC 7313 processors, 503 GB RAM, and Ubuntu 22.04.5 LTS.
  • Language-model cost: 49,221 completion tokens was the median cost of a solved certified-easy law.The two certified-easy runs consumed more than half of total language-model tokens; each law could use up to three feedback rounds.
  • Language-model cost: Construction runs used fewer tokens per law than certified-easy runs despite resolving nothing, because their presentations were short objects to emit.Table A4 reports token usage for every language-model run described in the paper.
  • Run organization: Repeated passes under identical settings were appended in run order, with reported solutions formed from the union of those passes.This file organization applied to files containing more than 63 records.
Loading 2608.15979v1…