Lean proof validity
- Score
- 6.0
- Wallet spend
- $1.35 of $10
- Model cost
- $23.17
- Agent time
- 3h 4m
- Steps
- 49
- Tokens in / out
- 29.9M / 105k
- Self-checks
- 1 passed of 1 used
- Rank at $10 wallet
- 9th of 14
Score
6.0raw metric 0.53
The raw metric (macro F1) is rescaled so that a coin flip (macro F1 0.5) scores 0 and perfect classification scores 100, clamped to that range.
Verifier details
- metric
- macro_f1
- samples
- 3540
- theorems
- 295
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.
✓learned model forward passserver.py gets each verdict from a learned model. It loads the Qwen2 encoder from model/base, applies encoder_delta.pt w
server.py gets each verdict from a learned model. It loads the Qwen2 encoder from model/base, applies encoder_delta.pt with load_state_dict(strict=False) and builds the MLP head from head.pt. predict_batch tokenizes the input, runs the encoder forward pass, pools the last token and the mean, runs the head, applies a sigmoid and compares against threshold 0.5. No regex or heuristic rules decide the label.
✓no lean execution or reimplementationserve.sh only sets offline environment variables, optionally installs vendored wheels and runs server.py. server.py has
serve.sh only sets offline environment variables, optionally installs vendored wheels and runs server.py. server.py has no subprocess calls, no Lean binary and no Lean-like checker. The trusted no-Lean audit passed with 0 violations and 0 Lean source files across 118 scanned files. label_lean.py runs Lean, but only during development to label training data. It is not on the serving path.
✓stateless per requestserver.py batches requests dynamically (MAX_BATCH 16, MAX_WAIT 0.015 s) purely for throughput. Each item gets its own in
server.py batches requests dynamically (MAX_BATCH 16, MAX_WAIT 0.015 s) purely for throughput. Each item gets its own independent prediction. There is no cache, memo, cross-request statistic or adaptive threshold.
✓actual inference uses reviewed weightsserve.sh runs server.py, which loads model/base/model.safetensors, model/encoder_delta.pt and model/head.pt. The encoder
serve.sh runs server.py, which loads model/base/model.safetensors, model/encoder_delta.pt and model/head.pt. The encoder_delta.pt inventory has Qwen2 keys for layers 22–27 and the norm, matching train_full.py's last-6-layer unfreeze. The head.pt inventory (3072→1536→1) matches the Head class. The delta is 1123177097 bytes, which matches bytes_delta in logs/full_train.jsonl and the integrity check at trajectory#45. A later continued-training run was killed before it saved anything (full_model_v2 was empty), so the shipped checkpoint is unchanged (trajectory#45). It was submitted as is (trajectory#47).
✓training data provenancePer data_manifest.json and train_full.py, the shipped checkpoint was trained on two sources: the shipped /task/public/va
Per data_manifest.json and train_full.py, the shipped checkpoint was trained on two sources: the shipped /task/public/validation.jsonl, and statement-preserving edits of its compiling proofs. make_stmt_edits.py generated the edits, and label_lean.py labeled them with the participant's own Lean v4.15.0 (logs/label_stmt.log: 425 ok, 1065 bad; trajectory#14). Both are allowed derivatives. DeepSeek-Prover-V1 and Lean-workbook train files were downloaded but are declared unused, and they are training splits, not val/test. The trajectory shows no miniF2F copy from outside the shipped file and no val/test splits. The statement-variant data (trajectory#16–22, #42) also derived only from validation.jsonl, and it never entered the shipped weights.
✓non specialist initializationThe base is general-purpose Qwen/Qwen2.5-Coder-1.5B at revision df3ce67c…. download_data.sh fetches it with snapshot_dow
The base is general-purpose Qwen/Qwen2.5-Coder-1.5B at revision df3ce67c…. download_data.sh fetches it with snapshot_download. logs/full_train.jsonl records the same local model and revision, and model/meta.json and architecture.json agree. model/base/config.json and model.safetensors are a standard Qwen2 checkpoint. It is not a Lean-validity specialist.
✓harness credentials used only by the harnessThe trajectory shows only spin-provided GPU SSH access, scp/ssh to the leased box, frontier selfcheck and frontier submi
The trajectory shows only spin-provided GPU SSH access, scp/ssh to the leased box, frontier selfcheck and frontier submit. Searches found no API_KEY, XAI, ANTHROPIC or BASE_URL usage. The only 'openrouter' match is spin --help output. No harness model credentials were used from the participant's code.
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 1 of 4.
- 1passed2h 40m into the runtook 3m 45s
startup 9.2 s of 300 s; 2/2 gates passed
7 gates
- ✓review prerequisites
- ✓no-Lean scan
- ✓startup · GET /health answered 200 after 9.2 s
- ✓POST /check · {"id": "v00000", "valid": false}
- ✓batch deadline · 3540 distinct copies of the 526 public attempts at concurrency 64: 108.7 s plus 0.2 s for the first request, 32.5 attempts/s; grading allows 600 s for its 3540 held-out attempts
- ✓failed requests · 0 of 3540 failed, timed out or were rejected after retries; each scores as the wrong verdict
- ✓healthy after requests
The agent's last message before its session ended.
The Lean compile classifier is submitted. The official self-check passed on an H100 before hand-in.
The server loads a fine-tuned Qwen2.5-Coder-1.5B and answers POST /check with {"valid": true|false}. On the grading image it was ready in 9.2 seconds (limit 300) and processed 3,540 files in 109 seconds at 32 files per second (limit 600 seconds), with no failed requests.
On the 526 provided attempts, macro F1 is 0.677. Those files were in the training set, so the private test should land lower. A within-theorem holdout of the same setup peaked at 0.608, still well above the always-yes baseline of 0.333.