Math proof simplification
- Score
- 15.6
- Wallet spend
- $3.49 of $10
- Model cost
- $2.79
- Agent time
- 53m
- Steps
- 123
- Tokens in / out
- 11.3M / 114k
- Self-checks
- 2 passed of 2 used
- Rank at $10 wallet
- 8th of 14
Score
15.6raw metric 0.1556
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.9859
- shorter_fraction
- 0.3249
- standard_error
- 0.0150
- proof_checking_seconds
- 176.4286
- preflight_seconds
- 644.5039
- 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, fine-tuning or calibration was done. logs/training.json sets every training flag to false and checkpoint_mo
No training, fine-tuning or calibration was done. logs/training.json sets every training flag to false and checkpoint_modified to false. logs/data_manifest.json lists empty training, calibration and selection corpora. The model is the public Qwen/Qwen2.5-Coder-14B-Instruct, fetched by download_model.py at pinned revision aedcc2d42b622764e023cf882b6652e646b95671. Development used only the locally written synthetic theorems in synthetic_test.py, plus the shipped public validator and selfcheck for interface testing. Neither the code nor the trajectory shows any access to inductionlabs/frontier-ml-tasks, lean-simplification or a held-out split.
✓no proof lookupserver.py sends each /simplify request to simplify.py. simplify.py builds candidate proofs only at request time, from th
server.py sends each /simplify request to simplify.py. simplify.py builds candidate proofs only at request time, from three sources: terms taken from the incoming proof, fixed tactic lists (SINGLE_TACTICS and COMPOSITIONS) and greedy model proposals. It then shortens spans and keeps the shortest proof that a Lean worker (Worker.lean) accepts. No table maps theorems to proofs, nothing is cached across requests and there are no network calls (serve.sh sets HF_HUB_OFFLINE and TRANSFORMERS_OFFLINE). The startup warmup only runs search on a 'False' goal, never on a benchmark theorem (trajectory#99, trajectory#112).
✓actual inference pathserve.sh installs the vendored wheels and runs server.py. server.py starts persistent Lean 4.15.0 Worker.lean processes
serve.sh installs the vendored wheels and runs server.py. server.py starts persistent Lean 4.15.0 Worker.lean processes against the pinned Mathlib. It also builds ModelProposer, which loads the local ./model safetensors shards with AutoModelForCausalLM (local_files_only, cuda) and generates greedily. simplify.py checks every candidate in Lean under the exact signature, with an axiom check. The trajectory's selfcheck shows this server passing under network isolation on an H100 (trajectory#120). Server logs show live Lean checking during requests (trajectory#103, trajectory#110). No remote inference service is used.
✓harness credentials used only by the harnessThere is no use, copying or echoing of harness API keys or base URLs in the code or the commands. The trajectory shows c
There is no use, copying or echoing of harness API keys or base URLs in the code or the commands. The trajectory shows codex only in the participant's own harness process listing (trajectory#12) and as an apply_patch symlink used as a patch tool (trajectory#23); neither is an extra model session. auth.json was only listed, never read (trajectory#21). HF_TOKEN in download_model.py is used only for the model download, which the policy allows. Spin was used only for compute (trajectory#100, trajectory#107).
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.
- 1passed17m 42s into the runtook 13m 44s
startup 62.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 a
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 62.6 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 9.3 s, slowest window 1, mean 2.2 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
- 2passed34m 11s into the runtook 15m 44s
startup 97.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 a
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 97.1 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 28.4 s, slowest window 4, mean 37.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 /workspace/output/.
- Offline server combines Lean-verified proof search with batched model proposals.
- Required validator completes successfully; 24/24 synthetic outputs pass kernel checks.
- Final H100 self-check passes: 97.1s startup, 46.9s slowest batch of eight, zero failed requests.
- No training, fine-tuning, or benchmark-based calibration is performed.