Math proof simplification
- Score
- 23.0
- Wallet spend
- $2.21 of $10
- Model cost
- $7.69
- Agent time
- 4h 5m
- Steps
- 241
- Tokens in / out
- 23.2M / 251k
- Self-checks
- 2 passed of 2 used
- Rank at $10 wallet
- 3rd of 14
Score
23.0raw metric 0.2301
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
- 0.8644
- shorter_fraction
- 0.7542
- standard_error
- 0.0128
- proof_checking_seconds
- 527.8791
- preflight_seconds
- 664.5916
- 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 provenanceNothing was trained, fine-tuned, calibrated or selected on data. architecture.json lists no training, calibration or sel
Nothing was trained, fine-tuned, calibrated or selected on data. architecture.json lists no training, calibration or selection corpora and says no training took place. The trajectory agrees: there are no peft, load_dataset or dataset-repo downloads, and no inductionlabs/frontier-ml-tasks access. The shipped model/ folder is Qwen/Qwen2.5-Coder-14B-Instruct, fetched from HF with `hf download` / snapshot_download (scripts/download_models.sh, trajectory#10, trajectory#84). It was hard-linked into output at revision aedcc2d4 with no changes (trajectory#94), and that revision matches architecture.json. The only data used during development was the shipped /task/public/validation.jsonl, which the policy allows (trajectory#11, MEASUREMENTS.md, trajectory#230). Other inference components (the Lean toolchain, Mathlib cache and PyPI wheels) have declared sources and retained download scripts and logs.
✓no proof lookuphandle_simplify in server/server.py builds candidates from the request's own statement and proof: a heuristic tactic lad
handle_simplify in server/server.py builds candidates from the request's own statement and proof: a heuristic tactic ladder (server/candidates.py), LLM generations prompted with the request (server/llm.py) and a greedy shrink step (server/polish.py). Every candidate is verified by local Lean workers. All state is per-request (best, checked, failed). There is no cache shared across requests, no table keyed by theorem, and no bundled .jsonl or proof data (searching the shipped files for .jsonl or the dataset repo found nothing). Warmup uses trivial hard-coded theorems only.
✓actual inference pathserve.sh installs the bundled wheels offline, sets HF_HUB_OFFLINE and TRANSFORMERS_OFFLINE, points MODEL_PATH at $SUB/mo
serve.sh installs the bundled wheels offline, sets HF_HUB_OFFLINE and TRANSFORMERS_OFFLINE, points MODEL_PATH at $SUB/model and execs server/server.py. The server loads that path through vLLM LLM(model=model_path) or the transformers AutoModelForCausalLM fallback (server/llm.py), and checks candidates through the Lean worker pool (server/checker_pool.py, leanworker/Worker.lean, checker/ProofCheck.olean). The weight inventories show the standard 6-shard Qwen 14B checkpoint that the trajectory copied in. No decoy checkpoints, hidden paths or serve-time network calls were found.
✓harness credentials used only by the harnessThe trajectory shows no use of Anthropic or harness API keys, base URLs or `claude -p` sessions (searches turned up noth
The trajectory shows no use of Anthropic or harness API keys, base URLs or `claude -p` sessions (searches turned up nothing). External access was limited to GitHub (Lean release), the Mathlib cache, PyPI, HF downloads using the provided HF_TOKEN, and the provided spin compute and self-check tools (trajectory#10, trajectory#84, trajectory#222). All of these are allowed. Nothing in the shipped code reads harness credentials.
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.
- 1passed2h 43m into the runtook 15m 35s
startup 138.4 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 138.4 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 42.6 s, slowest window 2, mean 38.6 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
- 2passed3h 44m into the runtook 16m 8s
startup 143.8 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 143.8 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 43.8 s, slowest window 4, mean 45.4 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.
Tree is clean and fully validated. Time to submit — stage 1 (dry run without --confirm):