Math proof simplification
- Score
- 11.4
- Wallet spend
- $8.91 of $10
- Model cost
- $9.06
- Agent time
- 2h 54m
- Steps
- 140
- Tokens in / out
- 22.1M / 110k
- Self-checks
- 3 passed of 3 used
- Rank at $10 wallet
- 11th of 14
Score
11.4raw metric 0.114
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.9011
- shorter_fraction
- 0.2288
- standard_error
- 0.0131
- proof_checking_seconds
- 123.8858
- preflight_seconds
- 666.0645
- 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 in the submission was trained, fine-tuned or calibrated. architecture.json declares the pretrained base model Go
Nothing in the submission was trained, fine-tuned or calibrated. architecture.json declares the pretrained base model Goedel-LM/Goedel-Prover-V2-8B at revision dfd02e6271a58375dfbf3ece0175277cf6b6a89a. The trajectory shows it was downloaded unmodified at that pinned revision through HF resolve URLs (trajectory#112). The shipped safetensors inventory shows a standard Qwen3-8B-shaped BF16 checkpoint, which matches that base model. The tactic portfolio and timeouts were tuned only against the shipped public examples in /task/public/validation.jsonl, which the policy allows (trajectory#45, trajectory#123). I found no use of the pinned frontier-ml-tasks repo or of any other dataset's validation or test split. One problem with the documentation: parts of data_manifest.md and build_log.md are out of date. They say no learned model is shipped, while other sections and the actual model/ directory show the Goedel model is bundled for inference. This inconsistency is noted but does not create an undeclared training corpus.
✓no proof lookupapp/simplify.py builds every candidate proof at request time from that request's statement and proof alone. It uses gene
app/simplify.py builds every candidate proof at request time from that request's statement and proof alone. It uses generic tactics, solver hints pulled from the submitted proof, sq_nonneg hints built from the statement's variables, step deletions and prefix/have variants. Optional samples from the Goedel model are prompted with the statement only. Every candidate is then checked by the bundled Lean. The code contains no table of proofs keyed by theorem, makes no network calls and loads no stored answers. The only state shared across requests is the loaded model and a batching queue whose results are mapped back to each request by index. Exploratory model outputs on the public examples (gen_out) stayed on the rented GPU machines; there is no sign they were copied into the output directory.
✓actual inference pathserve.sh installs torch, transformers and tokenizers from the local wheels/ directory without network access, sets LEAN_
serve.sh installs torch, transformers and tokenizers from the local wheels/ directory without network access, sets LEAN_BIN, LEAN_PATH and MODEL_DIR=$PWD/model, and then runs exec python3 app/simplify.py. That server answers POST /simplify by checking candidates with the bundled Lean v4.15.0 and Mathlib through a subprocess (lean --json). At startup it loads model/ with AutoModelForCausalLM in bf16 on CUDA and adds the model's samples to the pool of candidates Lean verifies. The final self-check log shows the 399 weight tensors loading in the serving process and all 56 public requests being served (trajectory#137).
✓harness credentials used only by the harnessHF_TOKEN was used only to download the public model weights, which the policy allows (trajectory#112, trajectory#124). S
HF_TOKEN was used only to download the public model weights, which the policy allows (trajectory#112, trajectory#124). Spin's own OpenRouter key and compute commands are allowed tooling (trajectory#32). I found no use of other API keys or base URLs in the trajectory. The shipped code (serve.sh, app/simplify.py) reads no credentials and makes no outbound requests.
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 58m into the runtook 8m 37s
startup 1.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 ag
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 1.4 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 33.8 s, slowest window 4, mean 46.9 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 28m into the runtook 11m 57s
startup 64.7 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 a
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 64.7 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 30.9 s, slowest window 7, mean 39.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
- 3passed2h 41m into the runtook 12m 53s
startup 67.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 a
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 67.4 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 42.5 s, slowest window 2, mean 44.0 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 system in /workspace/output/ is a verified proof simplifier:
- Approach: For each request it generates candidate shorter proofs — a generic tactic portfolio (
omega,aesop,simp_all,nlinarith, …), solver-hint lists reused from the submitted proof (plus leave-one-out/singleton subsets), auto-generatedsq_nonneghint pools from statement variables, prefix+solver and step-deletion/have-replacement variants of the submitted proof, and candidates proposed by a pretrained prover model. Every candidate is checked with the bundled pinned Lean v4.15.0 + Mathlib toolchain (single elaboration run per phase, cost-ordered, two time-boxed phases), and the shortest verified candidate shorter than the original is returned; otherwise the original proof is returned unchanged. - Model:
Goedel-LM/Goedel-Prover-V2-8B(revisiondfd02e62…, recorded in architecture.json) used only at inference with one fixed golf-style prompt, batched across concurrent requests (6 samples, concurrent with Lean phase 1). No training/fine-tuning/calibration on any split; provenance is documented in data_manifest.md and build_log.md. Server and candidate logic are in app/simplify.py, started by serve.sh (installs vendored PyTorch/transformers wheels into/tmpoffline). - Measured locally: mean relative token reduction ≈ 0.20 from the rule-based search alone on the 55 public proofs (all returned proofs Lean-verified), with additional wins from neural candidates; focused tests in tests/test_simplify.py pass.
- Selfcheck (
frontier selfcheck, final run): PASSED — startup 67.4s (limit 300s), slowest batch of 8: 46.3s (limit 60s), 0 failed requests, on H100 80GB, 26.11 GB submission.