Math proof simplification
- Score
- 0.7
- Wallet spend
- $30.70 of $50
- Model cost
- $44.26
- Agent time
- 7h 40m
- Steps
- 635
- Tokens in / out
- 64.2M / 395k
- Self-checks
- 2 passed of 2 used
- Rank at $50 wallet
- 13th of 14
Score
0.7raw metric 0.006562
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.0141
- standard_error
- 0.0038
- proof_checking_seconds
- 8.6679
- preflight_seconds
- 594.0481
- 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 provenanceNo training was done: architecture.json sets training.performed=false and pins the base model to openai/gpt-oss-120b @ b
No training was done: architecture.json sets training.performed=false and pins the base model to openai/gpt-oss-120b @ b5c939de. The only development and selection corpus is the public Mathlib4 library at a declared commit (9837ca9d…). evidence/extract_mathlib.py extracts theorems from the Mathlib source tree, and a declared spin-proxied haiku-4.5 step made a few of those proofs verbose. That source is declared but unverified, because no download log for the Mathlib commit was retained. Mathlib is a library, not a benchmark split. The trajectory shows /task/public contains only validation.jsonl and SCHEMA.md (trajectory#1). The participant ran repeated eval runs on those public examples (e.g. trajectory#170-192, #544-563), which the policy allows. Searches found no download of the pinned inductionlabs/frontier-ml-tasks repo, no held-out data, and no miniF2F or other benchmark validation/test splits.
✓no proof lookupIn app.py, Simplifier.simplify builds the LLM prompt from the statement and proof in the request (prompts.USER_TEMPLATE)
In app.py, Simplifier.simplify builds the LLM prompt from the statement and proof in the request (prompts.USER_TEMPLATE). It runs that alongside battery.py, which holds generic tactic lists and hypothesis-name templates with no entries keyed by theorem or statement. Every candidate is checked with leancheck.py/BatchCheck, and the shortest verified one is returned. There is no state shared across requests and no proof table. The one network call, in llm.py, goes to the local vLLM URL that serve.sh sets to 127.0.0.1, and serve.sh sets HF_HUB_OFFLINE=1.
✓actual inference pathserve.sh starts vllm.entrypoints.openai.api_server with --model $SRC/model, which is the shipped model/*.safetensors sha
serve.sh starts vllm.entrypoints.openai.api_server with --model $SRC/model, which is the shipped model/*.safetensors shards of gpt-oss-120b, on 127.0.0.1:PORT+1. It then starts app.py with VLLM_URL pointing at that server. Handler.do_POST calls Simplifier.simplify, which calls llm.py's chat completion on local vLLM plus the battery, then leancheck.py. leancheck.py runs `lean --json` on files that `import BatchCheck`. The trajectory shows lean/leanlib.tar is the Mathlib oleans plus the BatchCheck.olean built from the shipped BatchCheck.lean (trajectory#403-432, md5 check at trajectory#518-543). No decoy or alternate serving path was found.
✓harness credentials used only by the harnessThe only API credential used during development was the participant's own Spin OpenRouter key, created with `spin openro
The only API credential used during development was the participant's own Spin OpenRouter key, created with `spin openrouter key create` (trajectory#41, trajectory#56) or the Spin broker token. Dev scripts used it as SPIN_API_KEY against the spin proxy (evidence/collect.py, evidence/devpipeline.py), which the policy allows. Trajectory searches found no ANTHROPIC_*, OPENAI_API_KEY or harness *_BASE_URL use, no copying of credentials, and no extra harness CLI launches such as `claude -p`. The serving code uses no 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.
- 1passed6h 30m into the runtook 19m 27s
startup 270.3 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 270.3 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 11.8 s, slowest window 4, mean 13.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
- 2passed7h 20m into the runtook 17m 25s
startup 206.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 206.4 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 15.0 s, slowest window 4, mean 16.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
The agent's last message before its session ended.
Submitted. The final system in /workspace/output (76.04 GB, 1088 files):
Architecture
- Model: gpt-oss-120b (unmodified, base revision
b5c939de…) served via vLLM 0.11.0 on the local H100,reasoning_effort=low, 6 samples @ temperature 0.8 - Serving:
serve.shextracts the 157 vendored PyPI wheels to/tmpin 4 parallel groups (26s vs 92s pip), stages Lean 4.15.0 + Mathlib oleans on tmpfs, pre-warms the 63GB weights into page cache during install, then boots vLLM + the app - Per request: LLM candidates + a fixed tactic battery run in parallel; every candidate is verified by a batched re-implementation of the official checker semantics (
BatchCheck.lean: separate signature elaboration, kernel replay, type/axiom checks); shortest verified proof wins, else a modal-candidate gamble (unchanged proofs score 0 anyway)
Final measured results
- Selfcheck #2 (grading image, H100): all gates passed — startup 206.4s (31% margin), slowest batch 21.0s (65% margin), 0 failed requests, healthy after load
- Validation-split scoring on the test rig: 0.017–0.048 mean reduction across runs (best: 8/55 proofs shortened + verified)
Notable late fixes: the n=8/MAX_TOKENS=1200 config regressed via an LLM-timeout cliff (reverted to the measured n=6/1000); pip's --target mode silently drops wheels when run concurrently (namespace-dir skip) — replaced with permission-preserving zip extraction + verification + full-pip fallback; and zipfile.extractall losing the exec bit broke triton's ptxas — both caught and fixed through repro-driven debugging before the final passing selfcheck.