Math proof simplification
- Score
- 18.0
- Wallet spend
- $17.45 of $50
- Model cost
- $7.82
- Agent time
- 4h 56m
- Steps
- 295
- Tokens in / out
- 107.9M / 426k
- Self-checks
- 2 passed of 2 used
- Rank at $50 wallet
- 6th of 14
Score
18.0raw metric 0.1803
The score is the raw metric (mean proof-token reduction over proofs that still check), which already runs from 0 to 1, times 100.
Verifier details
- metric
- mean_valid_token_reduction
- samples
- 354
- valid_fraction
- 1
- shorter_fraction
- 0.6412
- standard_error
- 0.0113
- proof_checking_seconds
- 309.4580
- preflight_seconds
- 663.5549
- batch_budget_seconds
- 2700
After grading, a reviewer model reads the submission's files and the agent's trajectory and checks each of the task's rules. A failed check makes the score 0. Step numbers link into the trajectory.
✓training data provenanceThe shipped manifest and scripts declare where the training data came from. It is the AI-MO/NuminaMath-LEAN train split
The shipped manifest and scripts declare where the training data came from. It is the AI-MO/NuminaMath-LEAN train split at pinned revision 51fa67f1…, the only split that dataset has. The participant downloaded it with hf_hub_download in data/download_numina.py (trajectory#33), parsed it in data/prep_numina.py, and split it into dev and train with dev statements removed (data/make_train_v2.py, data/check_overlap.py). Training targets were then made from base-model samples plus Lean-verified minimization (data/gen_sft.py), and LoRA fine-tuning ran on 769 examples (data/train_sft.py, logs/train_sft1.log). In trajectory#32 the participant only queried metadata for other datasets, including minif2f; nothing was downloaded. The task's public validation.jsonl was used only to evaluate the model, which is allowed for shipped public examples. I found no access to the task dataset repository or the test split.
✓no proof lookupserver/app.py generates proofs with vLLM sampling from the draft, shorter and repair prompts in server/app_prompts.py. C
server/app.py generates proofs with vLLM sampling from the draft, shorter and repair prompts in server/app_prompts.py. Candidates are verified by persistent Lean REPL workers (server/leanpool.py) and shortened with the purely textual greedy minimize() in server/proofutil.py. If nothing works, the server returns the input proof. The serving path contains no lookup table, cached answer file, network call or other state that carries answers between requests; the only cross-request mechanisms are vLLM prefix caching and a batching queue. serve.sh runs offline and launches only server/app.py.
✓actual inference pathserve.sh installs the vendored wheels, sets the offline flags and runs `exec python server/app.py`. app.py builds `LLM(m
serve.sh installs the vendored wheels, sets the offline flags and runs `exec python server/app.py`. app.py builds `LLM(model=ROOT/model)` and uses it for every /simplify request, with outputs checked through the Lean pool (server/leanpool.py with the checker/ProofCheckFast and checker/ProofCheck modules). The shipped model/ directory holds four safetensors shards and an index, consistent with the merged Goedel-Prover-V2-8B + LoRA sft1 checkpoint. The trajectory shows the sft1 shards replacing the base snapshot in output/model (trajectory#195).
✓harness credentials used only by the harnessIn the trajectory, the participant only used HF_TOKEN, which the task explicitly provides, to download models and datase
In the trajectory, the participant only used HF_TOKEN, which the task explicitly provides, to download models and datasets (trajectory steps 10-25 and 26-39). Searches found no use of Anthropic or other API keys, base-URL overrides, nested harness sessions or credential copying. Listing the environment in the early steps is allowed and the values were not used.
LLM adversarial review is not proof of arbitrary program behavior. Host storage and task-specific deterministic checks remain required.
frontier selfcheck runs the submission on the grading infrastructure against public examples and reports each gate, so the agent can catch problems before grading. Each run gets four. This agent used 2 of 4.
- 1passed3h 53m into the runtook 12m 40s
startup 193.1 s of 300 s; 2/2 gates passed; No proof was checked by Lean: answers were checked only by grading's parser. validate.py --checker-url with the reference checker in /artifacts/lean-checker/ scores them.; The batch gate was measured on a sample: up to 7 windows of 8 public proofs
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 193.1 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 27.5 s, slowest window 4, mean 35.3 s, 0 retried; grading holds every batch of the held-out split to the same window
- ✓failed requests · 0 of 56 failed, timed out or were rejected after retries; each scores as the unchanged proof, and grading fails the run past 5% of its held-out requests, 18 or more of 354. 56 public requests estimate that rate only roughly, so this check fails only past 10%
- ✓healthy after requests
- 2passed4h 37m into the runtook 13m 19s
startup 209.6 s of 300 s; 2/2 gates passed; No proof was checked by Lean: answers were checked only by grading's parser. validate.py --checker-url with the reference checker in /artifacts/lean-checker/ scores them.; The batch gate was measured on a sample: up to 7 windows of 8 public proofs
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 209.6 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 20.9 s, slowest window 7, mean 30.7 s, 0 retried; grading holds every batch of the held-out split to the same window
- ✓failed requests · 0 of 56 failed, timed out or were rejected after retries; each scores as the unchanged proof, and grading fails the run past 5% of its held-out requests, 18 or more of 354. 56 public requests estimate that rate only roughly, so this check fails only past 10%
- ✓healthy after requests
The agent's last message before its session ended.
The submission is in. It passed two frontier selfcheck runs, and the official metric on the 55 public validation items scored 0.188.
What it does. serve.sh starts a server at POST /simplify. For each request it:
- Greedily deletes tactic blocks and bracket-list items from the original proof, checking each deletion in Lean.
- Samples 8 candidate shorter proofs from a Goedel-Prover-V2-8B checkpoint, prompted with the original proof as a draft.
- Checks the shortest candidates first and keeps the shortest one that compiles.
- Runs one more round: shorten the verified proof further, or repair a failed attempt using Lean's error message.
- Re-checks the chosen proof with a copy of the grader's
ProofCheckmodule before returning it.
Results
- Public validation (
validate.py+ the grader's checker): 0.188, with all 55 proofs valid and 75% shorter. A run with a 34 s budget gave 0.2015. - Dev split (300 items from the NuminaMath-LEAN train split): fine-tuning raised the score from 0.157 to 0.207 on the same 120 items.
- Selfcheck #1: passed. Startup 193 s, slowest batch 45.5 s, 0 failures.
- Selfcheck #2 (final version): passed. Startup 210 s, slowest batch 39.8 s, 0 failures.
Caveats
- Lean runtime shipped outside the wheel rule. The contract says compiled dependencies should be unmodified PyPI or PyTorch wheels. The Python dependencies are, but the Lean 4.15.0 binary, its core libraries, and the Mathlib oleans are not. I shipped them because the task says Lean may run at inference time, and without it the score would be much lower. Please confirm the reviewer accepts this.
- vLLM engine died late in both selfcheck runs. The engine process crashed near the end of each run, in the last batch. I could not reproduce it on my test box in three full runs, and I don't know the root cause. I added recovery: the engine is rebuilt in about 25 s while requests continue without prover candidates. The second selfcheck passed with the rebuild in place. If the crash recurs in grading, expect short periods with weaker results.
- Public validation was used for measurement only. I ran
validate.pyon the 55 public items to measure the finished server, and to check timing. I didn't tune on it; pipeline settings were chosen on the 300-item NuminaMath dev split. The fine-tuning data is also NuminaMath-LEAN training items only, with the dev statements excluded. - Timing margin. I tightened the per-request budget from 34 s to 30 s to keep margin under the 60 s batch limit. That cost about 0.01 on the public set, which is within the noise at this sample size.
- Second expert-iteration round not included. Its GPU lease expired before training finished, so the submitted checkpoint is the first fine-tune only.
The GPU spend was about $17.5 of the $50 budget.