Main idea
CoEvoBench is a working name for a co-evolving Rasch benchmark for Lean proof solvers. Learn solver strength and node difficulty from verified attempts, report comparable solver scores, and assign each candidate solver–node pair a running priority. Solver improvements and observed weaknesses then guide development of the next benchmark release.
A node is a proof obligation, such as a lemma or theorem. A solver is a model together with its strategy and implementation. Compare results within a recorded protocol: fixed inputs, environment, retry limits, tools and budgets. Start with overlapping nodes so the solvers can be compared on a common scale.
Within a release: score eligible (solver, node) pairs → choose a pair → verify its attempt with Lean → record outcome, cost and time → update both solver and node estimates → refresh the leaderboard and priorities.
Across releases: analyze failures and coverage → improve or add versioned solvers → propose and validate new nodes → calibrate them against shared anchors → refresh the active bank → evaluate again. New nodes may be harder, cover missing mathematics, or reveal a different weakness.
Here, co-evolution describes the proposed feedback between solver development and benchmark development. Updating a strength estimate measures a solver; it does not improve the solver itself. The prototype does not train or rewrite agents. Human-led solver improvements can participate in the same versioned loop.
Current status: fitting, online updates and solver recommendations for a given node exist in a local prototype. The reference-panel leaderboard, joint pair priority with a time penalty, and evolving-bank workflow below are proposed extensions. Production routing and the public leaderboard have not been replaced. Numerical examples are illustrative.
Detailed math
Record an event (i, j, y, C, T): a versioned solver, an immutable node/context, a verified outcome, dollars spent and elapsed seconds. The outcome y is 1 for a valid proof and 0 for a graded unsuccessful invocation under the declared budget. An ungradeable run has no success label. Repeated invocations supply repeated observations; internal retries share one final invocation grade.
Task 1 · Strength, cost, speed and node difficulty
Solver i has parameters θi = (si, ci, vi): strength, cost and speed. Node j has parameters φj = (dj, aj, bj): proof difficulty, cost effect and time effect. All are learned estimates that can change as observations arrive. Superscript (t) denotes the current calibration state; it is omitted in some formulas for readability.
σ(x) = 1 / (1 + exp(−x))
μijC = E[cost | i, j] = $0.10 × exp(ci + aj)
μijT = E[time | i, j] = 30 seconds × exp(−vi + bj)
The gap si − dj is the log-odds of success. A zero gap gives 50%; a gap of 1 gives 73.1%. Raising both strength and difficulty by the same amount leaves the prediction unchanged. This formalizes “stronger solver on a harder node ≈ weaker solver on an easier node.” Difficulty is estimated relative to the solver population and evaluation protocol.
Higher strength and speed are better; lower cost is better. Separate node effects allow a problem to be expensive without assuming it is equally difficult or slow. The $0.10 and 30-second scales define the current zero-score starting estimates; they are tunable priors, not measured averages.
These cost and time expectations include failures. Under this additive model, the same-node cost ratio for A versus B is exp(cA − cB), and the duration ratio is exp(vB − vA). These invariances are assumptions to validate, just like the success model.
The success model has the requested problem-independent odds multiplier:
oddsAj / oddsBj = exp(sA − sB)
This compares odds, not probabilities. The property comes from keeping the success model one-dimensional with unit discrimination. Giving every node its own discrimination would generally make this ratio depend on the node.
Full recalibration
Fit all eligible observations to date within a dataset/protocol scope. Success uses Bernoulli negative log likelihood. Cost and time use a quasi-Poisson loss to estimate expected arithmetic cost and duration, using both successful and unsuccessful attempts. This does not assume dollars or seconds are Poisson counts.
fitted scores = argmin [Lsuccess + Lcost + Ltime + prior penalty]
A fit rewards predictions that assign high probability to the observed outcomes. Overlapping trials distinguish a strong solver from an easy workload. The conditional likelihood treats invocation outcomes as independent given the parameters; correlated repeats, shared context and solver specialization require validation. A finite prior-regularized score does not establish a well-measured ranking.
Objective and optimization
+ Σcost observed [exp(ci + aj) − (C / 0.10)(ci + aj)]
+ Σtime observed [exp(−vi + bj) − (T / 30)(−vi + bj)]
+ ½ Σall coordinates θ θ²
Here y is 1 for a verified proof and 0 for a valid unsuccessful attempt; C is dollars and T is seconds. Independent zero-centered Gaussian priors with precision 1 anchor the additive scales and keep sparse or all-success estimates finite. The prototype uses damped Newton steps, sparse conjugate-gradient solves and line search. Nonconvergent fits do not replace the current state.
Online updates
After each eligible invocation, update the relevant solver and node coordinates. The success likelihood contributes p − y to the strength gradient and y − p to the difficulty gradient. Unexpected success raises strength and lowers difficulty; other observations help distinguish the two explanations.
si(t+1) = si(t) + αs e
dj(t+1) = dj(t) − αd e
These are the likelihood-only updates, using the same pre-update prediction on both sides. Success raises strength and lowers difficulty; failure reverses those directions. More surprising outcomes produce larger steps. The prototype uses αs = αd = 0.1, plus prior shrinkage and clipping as shown below. Updating an estimate measures a fixed solver version; changing its model, tools or strategy creates a new version.
Exact update used in the prototype
gd = y − p + dj / nj
θ ← clip(θ − clip(0.1 × gθ, −0.25, 0.25), −20, 20)
Counts n include the new observation for that coordinate. For cost and time, use the residual exp(η) − measurement/unit, with the signs from their predictors and the same count-scaled prior shrinkage. Missing measurements leave that dimension untouched. Both sides use the pre-update prediction.
This is an order-dependent, regularized stochastic-gradient approximation. Periodic full recalibration reconciles the accumulated observations using the batch objective; a scheduling service for those recalibrations has not yet been added.
How the leaderboard is produced
Ability ranking: sort solvers by their current linked strength si(t), highest first. Under the scalar Rasch model, sA > sB implies pAj > pBj for every node. This is a model assumption: persistent domain-specific rank reversals would challenge a single global strength score.
For a percentage interpretation, use a common reference panel R with nonnegative weights summing to 1:
Σj ∈ R wj = 1
P is model-predicted success on the same reference workload for every solver. For common weights, its ordering matches strength under Rasch. It is not the raw success rate on each solver’s adaptively assigned tasks. Report the calibration revision, observation counts and validated uncertainty estimates; mark sparsely measured solvers provisional. Reliable ranking uncertainty is still to be implemented.
Should harder nodes get more weight?
The whiteboard proposes difficulty-based weights. One concrete option is:
β = 0 gives uniform weights; β > 0 emphasizes harder nodes. Freeze the reference difficulties used for weighting, β and panel membership for a reporting version. Current strength and difficulty estimates may still update, but weights should not silently change after every outcome. A continuously reweighted view can be shown separately as a live-workload metric.
Difficulty weighting changes the interpretation of the percentage, not the ability ordering under the scalar Rasch model. Large β can concentrate weight on a few uncertain hard items, so uniform weights are a useful baseline. Publish changes to the reference workload as a new version and retain linked strength comparisons.
When cost and time matter
Compute expected cost and duration over exactly the same panel and weights, including unsuccessful attempts:
TiR = Σj ∈ R wj μijT
UiR = PiR − γC CiR/Cref − γT TiR/Tref
Keep an ability leaderboard and optionally provide a utility leaderboard sorted by U. The coefficients γ express a declared application preference, not a universally correct tradeoff. Their values may differ from the experiment-selection weights below. Record pricing, timing conventions, scales and weights with the leaderboard version; expected duration does not represent tail latency.
Leaderboard utility evaluates a solver; running priority evaluates the value of an experiment. Information gain belongs in the running priority, not in the solver’s reported performance score. This reference-panel reporting design is proposed and has not replaced the public leaderboard.
Which solver–node pair should run next?
Give each eligible pair a running priority Rij(t). Higher values mean the next attempt is more valuable under the declared objectives. This proposed extension jointly chooses the node and solver; the existing backend only recommends a solver for a supplied node.
Information from an attempt
∂ℓ / ∂z = p − y; ∂²ℓ / ∂z² = p(1 − p) ≤ 1/4
Vij(t) = Vart(si − dj)
= Vart(si) + Vart(dj) − 2 Covt(si, dj)
Iij(t) ≈ ½ log(1 + pij(t)(1 − pij(t)) Vij(t))
Bernoulli Fisher information for the gap is largest at p = 0.5. The uncertainty term favors pairs whose parameters are still poorly measured. I is a local Gaussian/curvature information proxy about the joint parameters, not exact expected information gain or a direct guarantee of improved ranking accuracy. If the goal is specifically ranking solvers, information about strength contrasts may be a better future target.
How the H values are calculated
Hsᵢ and Hdⱼ measure curvature of the regularized Bernoulli negative log-likelihood with respect to solver strength and node difficulty. At a batch fit, they are diagonal entries of its Hessian:
Hdⱼ = ∂²Lreg/∂dj² = λ + Σn : jₙ = j pn(1 − pn)
Here n indexes eligible graded invocation events, pn = σ(siₙ − djₙ), and λ is the precision of the independent zero-centered Gaussian priors (currently λ = 1). The first sum includes every eligible attempt by solver i; the second includes every eligible attempt on node j. Repeated invocations count as separate observations, not separate internal retries. At fixed parameters, each event contributes pn(1 − pn), irrespective of whether it succeeded; the outcomes affect the fitted probabilities.
Online calculation: initialize each stored H to λ. For a new eligible event on (i, j), calculate p from the scores before their update, then accumulate:
Hsᵢ ← Hsᵢ + p(1 − p)
Hdⱼ ← Hdⱼ + p(1 − p)
Other H values stay unchanged. This is a running curvature approximation: old contributions retain the predictions used when they arrived. A full refit recomputes and replaces the H values using all eligible events and the newly fitted scores; it does not add the same history a second time.
Simple example: starting from λ = 1, four eligible attempts involving a solver, each with p = 0.5, give Hsᵢ = 1 + 4 × 0.25 = 2. Its reciprocal is 0.5, compared with the initial value 1. More accumulated curvature means a smaller uncertainty proxy.
The sampler uses the stored H values to approximate uncertainty in the score difference:
This is a diagonal-curvature heuristic, not a calibrated variance estimate. It replaces the joint precision matrix by its diagonal before inversion. In general, 1/Hsᵢ is not the marginal variance of si: taking reciprocals of Hessian diagonal entries is different from taking diagonal entries of the inverse Hessian.
Full covariance and limitations
Let ψ contain all solver strengths and node difficulties. At a converged batch fit ψ̂, define H = ∇²Lreg, where Lreg = Lsuccess + (λ/2)‖ψ‖². Each event contributes −pn(1 − pn) to its strength–difficulty off-diagonal entries. Those couplings matter because an outcome informs both the solver and the node.
A full Laplace approximation uses the inverse of the entire Hessian of the negative log posterior:
Var(si − dj) ≈ Σsᵢ,sᵢ + Σdⱼ,dⱼ − 2Σsᵢ,dⱼ
This is H of the negative log posterior, so the inverse has a positive sign. Keeping the full matrix accounts for parameter correlations and changes the marginal variance estimates as well as the covariance term. It is still a local Gaussian approximation; it is not an exact posterior or a guarantee of interval coverage.
- Online curvature is approximate too. Between batch fits, the implementation accumulates p(1 − p) using each event’s pre-update prediction. It does not reevaluate all previous observations at the latest parameters. The resulting diagonal values need not equal the current batch Hessian diagonal.
- Sparse data and weak overlap matter. Priors make the regularized Hessian invertible, but cannot create empirical comparisons between disconnected solver–node groups. Sparse or nearly all-success/all-failure data can make a local Gaussian approximation unreliable or prior-sensitive.
- Calibration must be checked. Correlated repeats or an inadequate scalar Rasch model can invalidate uncertainty estimates even with the full Hessian. The current proxy can distort information priorities and should not be presented as a confidence interval or proof of ranking certainty.
Proposed next step: evaluate full-Hessian contrast variances after converged batch fits, then check uncertainty coverage on controlled simulations and predictive calibration on held-out runs. For a contrast vector x with +1 at si and −1 at dj, solve Hz = x and compute xᵀz; this avoids explicitly storing a dense inverse. The current sampler still uses the diagonal heuristic; this page update does not implement the full-covariance method.
Running priority
− λC μijC,(t)/Cref − λT μijT,(t)/Tref
The terms reward learning and closing nodes, then penalize expected spending and time. Set oj = 1 when a successful attempt would close an open node, and 0 for a pure calibration rerun. Cost and time include failed attempts. Use fixed reference scales across all candidates so priorities can be compared between nodes.
One starting configuration to test is (λI, λS, λC, λT) = (0.40, 0.40, 0.15, 0.05), Iref = ½ log(1.25) ≈ 0.1116, Cref = $0.10, and Tref = 30 seconds. Iref corresponds to p = 0.5 and V = 1. These are proposed preferences to validate, not optimized weights or percentages of a testing budget. Displaying 100R is convenient; it is not a percentage and need not lie between 0 and 100.
“Not yet tried” and “not yet solved” are different
The whiteboard’s “not yet tried” annotation can define a separate coverage objective. Let fij = 1 if that solver version has no prior eligible invocation on that node, and 0 otherwise. Replacing oj with fij rewards a successful first trial of that pair, rather than closing an unresolved node. Record which objective is being used.
For the node-closing objective above, a failed first attempt leaves oj = 1, while fij becomes 0. A fresh pair on an already closed anchor can have oj = 0 and fij = 1. Coverage can also be enforced through a pilot allocation or eligibility rule. Do not forbid all repeat attempts: repeats can be useful for calibration, although every counted attempt must be fresh and its dependence on prior context must be recorded.
Select the node and solver together
(i*, j*) = argmax(i,j) ∈ Et Rij(t)
Et contains valid nodes and available solvers satisfying the protocol and execution limits. A node’s best available experiment determines Gj. Recompute priorities after each result. New nodes need controlled pilot coverage; a prior prediction of 50% is not evidence that the node is truly of medium difficulty.
To retain exploration, an optional joint sampling policy is:
/ Σ(k,ℓ) ∈ Et exp(Rkℓ(t)/τ)
Use the unscaled R in this expression; using the displayed 100R requires scaling τ too. Log the actual pair-selection probability. Enforce domain and anchor coverage, availability and hard spending limits through the scheduler. A negative priority does not by itself define a stopping rule; an explicit value for stopping, budgets and calibration requirements must be specified.
Existing sampler versus this proposed extension
The current local sampler accepts one node, normalizes information by the maximum over its eligible solvers, uses weights 0.4 / 0.4 / 0.2 for information / success / cost, and applies softmax with τ = 0.2 and ε = 0.1. It has no time penalty or joint node selection and does not dispatch jobs.
The proposal uses fixed information scaling across nodes, a separate time penalty and explicit node-closing or first-trial semantics. It requires new implementation and comparison with uniform sampling and success-per-dollar baselines under the same budget. Adaptive sampling probabilities aid auditing but do not by themselves correct model misspecification or make raw solve rates comparable.
Simple example
Consider two fictional solvers: A has strength 1.5, B has strength 0.5. An easy node has difficulty −0.5 and a hard node has difficulty 0.5.
| Solver | Easy node | Hard node | Cost / attempt | Time / attempt |
|---|---|---|---|---|
| A | 88.1% | 73.1% | $0.20 | 20 s |
| B | 73.1% | 50.0% | $0.05 | 10 s |
For this example, both node cost/time effects are zero. Set cA = log 2, cB = log 0.5, vA = log 1.5, and vB = log 3 to obtain those costs and durations.
A on the hard node and B on the easy node both have a gap of 1, giving 73.1% success. On either node, A’s success odds are exp(1.5 − 0.5) ≈ 2.72 times B’s. This does not mean A’s probability is 2.72 times larger.
Leaderboard versus running priority
Use the two nodes as a fixed reference panel with uniform weights (β = 0). For the optional utility leaderboard, choose γC = 0.15 and γT = 0.05, with the reference cost/time scales above:
| Solver | Strength | Panel success P | Panel utility U |
|---|---|---|---|
| A | 1.5 | 80.6% | 0.4726 |
| B | 0.5 | 61.6% | 0.5239 |
A leads the ability ranking; B leads this particular cost/time utility ranking. Neither ranking contains an information-gain bonus.
Now choose the next experiment. Suppose both nodes remain open and all four pairs have V = 1. Using the proposed four-term priority weights:
| Pair | Success p | Information I | Priority 100R |
|---|---|---|---|
| A · easy | 88.1% | 0.0499 | 19.8 |
| A · hard | 73.1% | 0.0897 | 28.1 |
| B · easy | 73.1% | 0.0897 | 52.3 |
| B · hard | 50.0% | 0.1116 | 50.8 |
The greedy policy selects B on the easy node. Its extra chance of closing a node outweighs its lower information relative to B on the hard node. If the easy node is excluded from the candidate pool, B on the hard node has the highest remaining priority. If the easy node stays as a closed calibration item, set o = 0 and recompute its priority instead. This illustrates why neither “strongest solver” nor “closest to 50%” is sufficient on its own.
What happens after a result?
For an online-update example, suppose only the hard node is eligible, B is selected, and it succeeds. Before this event, let both B and the hard node have four scored observations. With p = 0.5, learning rate 0.1 and the implemented prior shrinkage, the new strength is 0.54 and the new difficulty is 0.44. Their new gap is 0.10, so the next predicted success probability is about 52.5%. Cost and time update from the actual measurements, even if the proof had failed.
A later full fit reconciles this result with all other observations. As new nodes are added, keep shared anchors and evaluate prediction accuracy on held-out data; do not stop merely because the displayed ranking has stopped changing.
What changes when the benchmark and solver evolve?
Return to the original strengths A = 1.5 and B = 0.5. Their expected rates on the two original nodes are 80.6% and 61.6%. Admit a new node with linked difficulty 1.5: A has 50.0% predicted success and B has 26.9%. If the active pool now consists of the former hard node and this new node, their expected rates become 61.6% and 38.4%, even though neither solver changed.
Next, suppose an improved, separately versioned solver A′ is calibrated at strength 2.0. It has 62.2% success on the new node, and exp(2.0 − 1.5) ≈ 1.65 times A’s odds on every node under the model. The benchmark can now seek new informative candidates while retaining anchors and coverage. These numbers illustrate the proposed loop; they are not measurements of an implemented co-evolution system.
Co-evolution and comparable scores
There are three distinct kinds of change. Updating a score is already possible; evolving the test bank while preserving a meaningful historical comparison requires additional machinery.
| Layer | Status |
|---|---|
| Online calibration | Implemented locally: update solver and node parameters after eligible invocations, and refit accumulated data within a scope. |
| Adaptive evaluation | Recommendations implemented: choose a solver for a given open node. Automatic dispatch and a policy for choosing the next node are not implemented. |
| Evolving node bank | Proposed: admit new nodes, monitor coverage and saturation, rotate active items, and link calibrated scores across releases. |
Solver development is a separate proposed part of the loop: failures can guide changes to prompts, tools or proof strategies, and each changed solver receives a new identity. Keep an audit panel out of this development feedback, and record exposure to public development nodes. Otherwise improvements may reflect memorization or tuning to the active pool.
How the node bank could evolve
- Validate incoming nodes. Extract candidate obligations from authorized new papers or submissions. Check the statement, assumptions and Lean environment; deduplicate and assign an immutable identity. A changed statement or proof context becomes a new item version.
- Calibrate before promotion. Start new nodes as provisional, with uncertain difficulty. Allocate a controlled pilot budget across several solver strengths and shared anchor nodes. Promote them only when grading is reliable and there is enough overlap to assess their difficulty and usefulness.
- Refresh the active pool. Use observed coverage, uncertainty and validated signs of saturation to add informative nodes. Include new mathematical areas as well as harder problems. Reduce repeated testing of saturated items while retaining useful anchors and an audit history; invalid or withdrawn items need explicit exclusion and affected-score recalculation.
- Release a versioned snapshot. Record the active inventory, anchor set, eligibility rules, evaluation protocol and calibration revision. Preserve earlier score snapshots, and label any retrospective recomputation instead of silently changing historical results.
A ⊆ Bt ∩ Bt+1
B is the active bank, R contains items rotated out, N contains admitted candidates, and A is the retained anchor set. This is a proposed release rule, not an implemented scheduler. Archive rotated items and observations. Candidate selection should balance informative difficulty, uncertainty and mathematical coverage; no single success-rate threshold establishes saturation.
The live proof pipeline can stop spending on a closed node. The evaluation system may still run a fresh attempt on a retained anchor to measure another solver; it must not count the previously cached proof as a new success.
How scores could remain comparable
The expected raw solve rate on a bank B is:
Even with unchanged strength, this average falls when the bank gets harder. Ability and workload therefore need separate estimates. There is also an arbitrary origin in the Rasch likelihood:
Zero-centered priors fix an origin within each fit, but independently fitted releases need not share an empirical reference. The unit-discrimination model fixes the log-odds unit; the common origin still needs to be linked.
Keep a shared reference scale. Select unchanged anchor nodes spanning relevant difficulties and domains, and evaluate overlapping, versioned solver configurations on both old and new nodes. The solver–node observation graph must connect the releases; overlap alone is not proof that the model remains valid.
A proposed first linking method is to calibrate new items and solvers while holding vetted anchor difficulties at their reference values. An alternative is a joint calibration of linked releases with an explicit reference constraint. This follows the idea of common-item anchoring. The current backend fits separate scopes with zero-centered priors; it does not yet perform this cross-version linking. Identical priors or separately re-centering each new bank would not establish comparability.
The mathematics of a shared origin
As an illustrative diagnostic for two separately calibrated Rasch releases with the same log-odds unit, choose positive anchor weights wj summing to 1 and estimate the offset:
si,linked = si,new + k
dj,linked = dj,new + k
Adding the same offset to both coordinates preserves every new-release prediction. For example, if stable anchors are all estimated 0.3 units above their reference values, k = −0.3; a new-release strength of 1.8 maps to 1.5. This is an origin correction, not evidence of a performance change.
Anchor residuals dj,new + k − dj,reference should be assessed against estimation uncertainty and by domain. A shift cannot repair item-specific drift, unequal shrinkage or a poor scalar model. For the prototype, constrained joint calibration is the preferred next implementation to test; uncertainty in reference anchors and the link must be propagated rather than treating them as known perfectly.
Check the anchors for drift. Rerun stable reference solver versions and examine whether anchor outcomes still fit the linked model. Changed dependencies, evaluation settings, contamination or solver specialization can undermine the link. Anchor drift is a known concern in IRT equating research; that work motivates a check here, not a guarantee for proof-solving data. Replace suspect anchors through an overlapping transition and report linking uncertainty. If the link cannot be supported, report separate scales.
Separate progress from a changing workload. Report linked ability scores with their calibration version and uncertainty, alongside fresh performance on a fixed reference panel and coverage of the evolving pool. A drop in raw success rate after adding harder nodes does not by itself mean a solver became weaker. Model, tool or budget changes create a new solver configuration or protocol comparison. For cost and speed, also record the pricing basis and execution environment; stable proof difficulty alone does not align dollars or seconds.
A version-to-version example
Suppose release v1 has 100 nodes. For v2, introduce 40 new candidates and retain 20 unchanged nodes as anchors. Run several unchanged solver versions on the anchors and candidates under the same protocol. After checking overlap and anchor stability, calibrate the candidates onto the reference scale and decide which enter the active pool. These counts are illustrative, not minimum sample-size requirements.
If a reference solver’s raw success rate falls because v2 is harder, compare its linked strength estimate and fixed-panel performance before concluding that its ability changed. If anchor behavior has drifted, investigate the cause and qualify or withhold the cross-version comparison. The goal is a changing benchmark with an auditable, empirically checked reference scale.
Next, evaluate joint pair selection on a fixed, overlapping node bank and compare its calibration, ranking accuracy, node closures and spending against baselines. Then add a versioned node registry and admission pilot, anchor-based linking and drift checks before enabling bank rotation. Solver development and benchmark updates should preserve a separate audit panel. Automatic dispatch and evidence-based stopping rules remain future work.
What is implemented
| Component | Current behavior |
|---|---|
| Score fitting | Jointly fits solver and node effects from the accumulated observations; reports convergence. |
| Online updates | Eligible completed runs feed a private event log and update scores. Duplicate event IDs do not count twice. |
| Persistent state | SQLite transactions keep events and score updates together. A revision check prevents a full fit from overwriting newer updates. |
| Sampling | Existing implementation: recommend a solver for a supplied node using information, success and cost. Joint pair priority, the time penalty and the new reference-panel leaderboard are proposed extensions. |
| Validation | 59 tests passed across the new Rasch and existing monitoring/rating suites. A six-record pilot—two strategies on three problems—ran through fitting successfully. |
One observation means one graded node invocation, including its internal retries and tool calls. A final grade is not copied onto every internal retry. Per-retry learning needs per-retry grades and accounting that are not yet available.
Freshness and attribution are checked before ingestion. Cached or partially cache-seeded work is excluded; ambiguous whole-file attribution and mixed review/tiered runs are skipped. An infrastructure error does not become a failed proof, but its attributable, known cost/time can still update those dimensions. Missing cost is never zero.
The six-record pilot is a workflow check, not a reliable ranking. Private project data and benchmark scopes remain separate. No raw project data or backend source is published here.
Still to validate: probability and cost/time calibration, prior sensitivity, uncertainty, and the benefit of adaptive sampling. Shared anchor nodes are important: disconnected solver–node groups are comparable only through the priors. Stable rankings and a nearly solved benchmark are different signals; a stopping rule is still to be designed.
Related papers
These papers inform different parts of the design. They do not establish that the current heuristic or cost model is optimal for Lean proof solving.
- Self-Modifying Lean Proof Agents with Verifier-Grounded Benchmark Coevolution
The closest setting: evolving Lean proof agents and an active benchmark drawn from a tiered candidate pool. Mastered tasks are replaced with same-tier or harder tasks. The paper recalibrates scores by rerunning a champion solver on the changed bank. Our proposed linking instead uses shared Rasch anchor items and overlapping solver versions; a single reference solver’s multiplicative normalization does not establish invariant comparisons for every solver.
- Benchmark Self-Evolving: A Multi-Agent Framework for Dynamic LLM Evaluation
Uses multiple agents and six reframing operations to extend benchmark instances. Relevant to generating candidate nodes and exposing new weaknesses. Our formal-mathematics setting additionally needs statement, context and verification checks before candidates enter the scored bank.
- Dynabench: Rethinking Benchmarking in NLP
A human-and-model feedback loop for collecting challenging examples. A precedent for using current solver failures to guide researcher-submitted nodes and benchmark development.
- tinyBenchmarks: evaluating LLMs with fewer examples
Uses representative examples and IRT-based estimation to reduce evaluation effort. Relevant to choosing shared anchor nodes and testing how well a small sample predicts broader performance. Its multidimensional IRT model is richer than the scalar Rasch success model used here.
- Fluid Language Model Benchmarking
Combines IRT ability scores with dynamic item selection, including Fisher-information-based selection. Especially relevant to adaptive evaluation and saturation. It uses a 2PL model with item discrimination; our unit-discrimination choice preserves the requested problem-independent odds ratio. Adaptive selection from a bank and changing the bank itself are distinct design components.
- Rasch Scale Stability in the Presence of Item Parameter and Trait Drift
Studies stability of Rasch scales under item and population drift. Motivates checking anchor stability and linking uncertainty when the node bank changes; its educational measurement setting does not itself validate comparability for Lean solvers.
- Computer adaptive practice of Maths ability using a new item response model for on the fly ability and difficulty estimation
Updates learner ability and item difficulty after individual responses using an Elo-related model. A useful precedent for online joint calibration. Its educational practice setting and combined accuracy/time scoring differ from our separate solver objectives.
- A Hierarchical Framework for Modeling Speed and Accuracy on Test Items
Separates ability and speed and models their relationships through a hierarchy. Relevant to keeping solver speed distinct from strength. Our current mean-duration model does not implement that paper’s hierarchical response-time distribution or correlations.
- Learning to Optimize via Information-Directed Sampling
Balances immediate regret against information about the optimal action. A principled direction for improving the exploration–exploitation tradeoff. Our weighted utility and diagonal information proxy are not an implementation of IDS.
- Bandits with Knapsacks
Studies online learning when actions consume limited resources. Relevant to a future policy that manages a total spending budget. The current expected-cost penalty does not provide those algorithms’ budget or regret guarantees.
For the basic Rasch formulation, see the Stan item-response model documentation. Start with the Lean coevolution paper for the feedback loop, Fluid Benchmarking for adaptive measurement, and the scale-stability paper for cross-release comparisons. This proposal combines those research directions; their guarantees do not automatically transfer to our prototype.