Math proof simplification
- Score
- 33.9
- Wallet spend
- $7.64 of $10
- Model cost
- $37.25
- Agent time
- 4h 19m
- Steps
- 275
- Tokens in / out
- 96.4M / 382k
- Self-checks
- 3 passed of 3 used
- Rank at $10 wallet
- 1st of 14
Score
33.9raw metric 0.3389
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.7712
- standard_error
- 0.0150
- proof_checking_seconds
- 406.2408
- preflight_seconds
- 660.7919
- 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 provenancearchitecture.json declares no training (training: none) and a base model pinned to revision a8d9e14432b2e8dd9df2a4d4e70f
architecture.json declares no training (training: none) and a base model pinned to revision a8d9e14432b2e8dd9df2a4d4e70f1ba9bc8d9b7b. It also declares the public train-split corpora, at pinned revisions, used to build the dev pool that tuned the search hyperparameters. dev/data/download.sh and its log record the downloads, and dev/build_devpool.py builds the pool from them. Nothing in the trajectory shows a validation or test split, or the forbidden inductionlabs/frontier-ml-tasks repo, being used for training or selection. validation.jsonl was used only for smoke tests (trajectory#202).
✓no proof lookupThe serving path is server.py -> simplify() -> Search, and it keeps state only within each request. Every candidate proo
The serving path is server.py -> simplify() -> Search, and it keeps state only within each request. Every candidate proof comes from a closer or minimization search, or from the local LLM, and is verified by Lean through leanpool/checkerd. The final check requires FRONTIER_PROOF_VALID. The replay dict in llm.enable_replay is used only by dev/exp3.py --replay, never by the server. No proof table or answer cache is shipped or loaded.
✓actual inference pathserve.sh execs app/server.py. main() starts the Lean checker pool and calls llm.start(), which launches vLLM offline on
serve.sh execs app/server.py. main() starts the Lean checker pool and calls llm.start(), which launches vLLM offline on ./model. Search calls llm.generate(), which POSTs to http://127.0.0.1:8001/v1/completions. The shipped safetensors shards match the DeepSeek-Prover-V2-7B config, downloaded at the pinned revision (trajectory#199). The checkerd daemon was compiled from Lean source written during the session (trajectory#24) and uses the same header as the official checker.
✓harness credentials used only by the harnessThe trajectory shows no use of harness credentials. Searches for ANTHROPIC, API_KEY, printenv and claude -p found nothin
The trajectory shows no use of harness credentials. Searches for ANTHROPIC, API_KEY, printenv and claude -p found nothing relevant. The only token use was the allowed HF_TOKEN download (trajectory#199), and the only model inference ran through the local vLLM server.
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 3 of 4.
- 1passed1h 24m into the runtook 9m 10s
startup 9.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 ag
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 9.1 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 36.0 s, slowest window 4, mean 36.5 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
- 2passed2h 48m into the runtook 10m 22s
startup 127.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 127.1 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 36.0 s, slowest window 4, mean 37.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
- 3passed4h 5m into the runtook 10m 47s
startup 128.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 128.6 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 30.4 s, slowest window 4, mean 36.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.
The contents match the selfchecked build (plus the added download log). Submitting: