Lean proof validity
- Score
- 26.6
- Wallet spend
- $8.49 of $10
- Model cost
- $5.32
- Agent time
- 2h 59m
- Steps
- 299
- Tokens in / out
- 88.1M / 331k
- Self-checks
- 1 passed of 1 used
- Rank at $10 wallet
- 6th of 14
Score
26.6raw metric 0.633
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 tokenizes each submission and runs a forward pass of the Qwen3 backbone (AutoModel, bf16) to get the last-toke
server.py tokenizes each submission and runs a forward pass of the Qwen3 backbone (AutoModel, bf16) to get the last-token hidden state. It applies the linear head from model/head.pt (weight [1,4096], bias [1]) to produce a logit. /check returns valid when logit > 0.25, the fixed threshold in model/threshold.json. The verdict is therefore the model's learned output, not a rule.
✓no lean execution or reimplementationThe trusted no_lean audit passed with no violations or leads. server.py has no subprocess call, no Lean or lake invocati
The trusted no_lean audit passed with no violations or leads. server.py has no subprocess call, no Lean or lake invocation and no rule-based validity logic, only tokenization, a model forward pass and a threshold comparison. serve.sh only sets offline flags and runs server.py. Lean was used offline to label training data (data/lean_label.py), which the policy allows.
✓stateless per requestThe worker thread in server.py collects requests into micro-batches (up to 32 within 10 ms) only for throughput. Each su
The worker thread in server.py collects requests into micro-batches (up to 32 within 10 ms) only for throughput. Each submission is encoded independently with the first/last-half truncation, and each gets its own logit. There is no cache, memo, persisted state or cross-request feature, so a request's verdict does not depend on other requests.
✓actual inference uses reviewed weightsserve.sh runs server.py --model-dir $HERE/model. server.py loads the model/ safetensors shards (Qwen3Model, 36 layers, h
serve.sh runs server.py --model-dir $HERE/model. server.py loads the model/ safetensors shards (Qwen3Model, 36 layers, hidden 4096, per model/config.json), model/head.pt and model/threshold.json. This structure matches the output of training/train_clf.py (merge_and_unload plus head.pt). training/logs/train_run2.log records the save to out_run2/merged. Trajectory steps 253–255 show the run2 results copied into /workspace/output/model, with threshold 0.25 and a full shard index.
✓training data provenanceAll sources are declared and pinned in data/download_data.sh, and data/logs/download_data.log confirms the downloads. Th
All sources are declared and pinned in data/download_data.sh, and data/logs/download_data.log confirms the downloads. They are Goedel-LM/Lean-workbook-proofs (train) and ricdomolm/numinamath-LEAN-trajs-850k (train shards 0–3), both at fixed revisions, plus the allowed shipped validation.jsonl. The 250 validation train rows were used, upweighted in training/make_run2.py, and 276 rows were held out as dev by theorem. Mutations are derived from these sources. Labels come from the participant's own local Lean compiles. miniF2F (cat-searcher/minif2f-lean4) was used only to remove overlapping signatures (data/minif2f_overlap.py, data/assemble.py); the manifest records 1 hit, which was not sampled. The LukeBailey181 miniF2F-solutions dataset appears only in a metadata listing (trajectory#31, trajectory#32) and was never downloaded or used.
✓non specialist initializationarchitecture.json and training/fetch_base.py pin Goedel-LM/Goedel-Prover-V2-8B at revision dfd02e62…. It is a proof-gene
architecture.json and training/fetch_base.py pin Goedel-LM/Goedel-Prover-V2-8B at revision dfd02e62…. It is a proof-generating Lean prover, which the policy allows as a base, not a validity classifier. training/train_clf.py applies a fresh LoRA adapter and a new 1-logit linear head, trains them on the participant's labeled data and then merges. The checkpoint structure (Qwen3Model shards plus a separate [1,4096] head) is consistent with that path.
✓harness credentials used only by the harnessA search of the trajectory found no use of the harness's model API credentials (no ANTHROPIC or other model-API key, and
A search of the trajectory found no use of the harness's model API credentials (no ANTHROPIC or other model-API key, and no BASE_URL calls to a model API). HF_TOKEN was used only for Hugging Face dataset and model listing and downloads (trajectory#31, trajectory#34, trajectory#36). The spin/s5cmd transfers moved the participant's own training artifacts (trajectory#253).
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 39m into the runtook 8m 23s
startup 10.5 s of 300 s; 2/2 gates passed
7 gates
- ✓review prerequisites
- ✓no-Lean scan
- ✓startup · GET /health answered 200 after 10.5 s
- ✓POST /check · {"id": "v00000", "valid": false}
- ✓batch deadline · 3540 distinct copies of the 526 public attempts at concurrency 64: 118.8 s plus 0.2 s for the first request, 29.7 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 submission is in (frontier submit --confirm, 08:35 UTC). The session is over.
What I submitted
A classifier built on Goedel-LM/Goedel-Prover-V2-8B (revision dfd02e6…, Apache-2.0). I fine-tuned it with LoRA plus a linear head on the last token, merged the LoRA, and shipped it with serve.sh and a stdlib HTTP server (POST /check, GET /health). Labels came from compiling each file with Lean 4.15.0 and Mathlib v4.15.0 during development. Lean is not in the submission. The shipped threshold is logit 0.25.
Results
- Held-out dev (25 theorems, 276 rows, not used in training or threshold choice): AUC 0.730, macro F1 about 0.666–0.669 across the flat part of the threshold curve.
validate.pyon all 526 provided rows: macro F1 0.770. This is optimistic because 250 of those rows were in training.- Frontier selfcheck: PASSED on an H100. Startup took 10.5 s, 3,540 attempts finished in 119 s (about 30/s against a 600 s limit), and there were no failed requests.
The model is a moderate signal, not a strong verifier. The dev score is limited by the small dev set and by how much of the failure modes (linarith, unsolved goals) a classifier can learn from about 10k examples.
Choices I made
- Training data: Goedel Lean Workbook proofs and NuminaMath trajectory attempts, rewritten to the task's file format and labeled by Lean. Also near-miss mutations of valid proofs. The provided validation was split by theorem: 25 for training, 25 held out. Label balance is about 50/50 to match the balanced test.
- Two runs: run 1 scored dev macro F1 0.639 at the shipped threshold. Run 2 added two extra copies of the validation training rows and scored 0.666, so I shipped run 2. Averaging both gave only a marginal gain, so I didn't ship both.
- MiniF2F: I used the miniF2F test/valid files only to drop training candidates that restate a miniF2F statement. One candidate matched and was not in the training file.
Caveats
- The CPU labeling boxes were released when their leases ended, so their console logs were not kept. The per-file verdicts are in
data/labels/. - The mutation part-2 labels are partial (691 of 2,147 rows). One row labeled before the axiom-parse fix still carries the old verdict.
- The architecture review has not run.
architecture.json, the data manifest, and the download script with its log are in place. - Budget: about $8.5 of the $10 was spent, mostly on the two H100 leases.