Lean proof validity
- Score
- 0.0
- Wallet spend
- $8.43 of $50
- Model cost
- $19.55
- Agent time
- 4h 17m
- Steps
- 1,206
- Tokens in / out
- 177.5M / 348k
- Self-checks
- 1 passed of 3 used
- Rank at $50 wallet
- 11th of 14
Score
0.0raw metric 0.4734
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 loads AutoModelForSequenceClassification from /submission/model. For each request it tokenizes the Lean text (
server.py loads AutoModelForSequenceClassification from /submission/model. For each request it tokenizes the Lean text (max_length 1024), runs the model, applies softmax to the 2-label logits and sets the prediction to p(valid) > 0.90. The verdict comes only from this forward pass; there are no rules or regexes.
✓no lean execution or reimplementationThe trusted no_lean audit passed with no violations or review leads, and the submission has 0 Lean source files. server.
The trusted no_lean audit passed with no violations or review leads, and the submission has 0 Lean source files. server.py has no subprocess calls, Lean toolchain or checker logic. The wheels are standard ML and serving packages.
✓stateless per requestserver.py's batch worker only groups queued requests (up to 32, 5 ms timeout) for one batched forward pass. Each item ge
server.py's batch worker only groups queued requests (up to 32, 5 ms timeout) for one batched forward pass. Each item gets its own probability and future. The server has no cache, no memo keyed on inputs and no state that changes between requests.
✓actual inference uses reviewed weightsserve.sh runs uvicorn server:app from /submission. server.py loads /submission/model, which holds model/config.json (Qwe
serve.sh runs uvicorn server:app from /submission. server.py loads /submission/model, which holds model/config.json (Qwen2ForSequenceClassification) and model/model.safetensors (3,087,473,376 bytes; standard Qwen2 tensors plus score.weight [2,1536]). The trajectory shows the merged weights being produced (trajectory#1134), uploaded (trajectory#1150) and copied into the output model directory (trajectory#1153), with a matching file size (trajectory#1152).
✓training data provenancearchitecture.json and prepare_data.py declare the training data: positives from public Goedel-LM/Lean-workbook-proofs (t
architecture.json and prepare_data.py declare the training data: positives from public Goedel-LM/Lean-workbook-proofs (train), negatives from Goedel-LM/RL_dataset_V2 (train shards, lean4_revision subset with error messages), plus the allowed task/public/validation.jsonl. Both datasets were downloaded with hf_hub_download, as recorded in the trajectory. prepare_data.py filters out minif2f-tagged rows. The miniF2F name-pattern counts seen during exploration (trajectory#146) are only a review lead; no statement-level match to miniF2F and no miniF2F source was established, and no miniF2F dataset was downloaded.
✓non specialist initializationtrain.py starts from the general base model Qwen/Qwen2.5-Coder-1.5B (pinned revision in architecture.json) and applies L
train.py starts from the general base model Qwen/Qwen2.5-Coder-1.5B (pinned revision in architecture.json) and applies LoRA. train.log shows score.weight was newly initialized. The merge in trajectory#1134 combines this base with the trained LoRA checkpoint. No proof-checker or verifier checkpoint was used for initialization.
✓harness credentials used only by the harnessSearching the trajectory for API_KEY, BASE_URL, printenv/env dumps, push_to_hub and LLM/agent calls found no misuse of h
Searching the trajectory for API_KEY, BASE_URL, printenv/env dumps, push_to_hub and LLM/agent calls found no misuse of harness credentials. trajectory#90 only runs spin openrouter --help, which policy allows. HF downloads with a token are allowed. The served model makes no external API calls.
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.
- 1failed4h 1m into the runtook 6m 26s
failed startup: Server did not become healthy in 300s (last /health probe: RuntimeError: Submission HTTP request failed: ConnectionRefusedError: [Errno 111] Connection refused); end of its log: andling of the above exception, another exception occurred: Traceback (most recent call last):
3 gates
- ✓review prerequisites
- ✓no-Lean scan
- ✗startup · Server did not become healthy in 300s (last /health probe: RuntimeError: Submission HTTP request failed: ConnectionRefusedError: [Errno 111] Connection refused); end of its log: andling of the above exception, another exception occurred: Traceback (most recent call last): File "/opt/venv/lib/python3.12/site-packages/starlette/routing.py", line 654, in lifespan async with self.lifespan_context(app) as maybe_state: File "/opt/venv/lib/python3.12/site-packages/fastapi/routing.py", line 272, in __aenter__ await self._router._startup() File "/opt/venv/lib/python3.12/site-packages/fastapi/routing.py", line 6455, in _startup await handler() File "/submission/server.py", line 35, in load_model tokenizer = AutoTokenizer.from_pretrained(MODEL_PATH) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ File "/opt/venv/lib/python3.12/site-packages/transformers/models/auto/tokenization_auto.py", line 1140, in from_pretrained return tokenizer_class.from_pretrained(pretrained_model_name_or_path, *inputs, **kwargs) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ File "/opt/venv/lib/python3.12/site-packages/transformers/tokenization_utils_base.py", line 2097, in from_pretrained return cls._from_pretrained( ^^^^^^^^^^^^^^^^^^^^^ File "/opt/venv/lib/python3.12/site-packages/transformers/tokenization_utils_base.py", line 2344, in _from_pretrained except import_protobuf_decode_error(): ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ File "/opt/venv/lib/python3.12/site-packages/transformers/tokenization_utils_base.py", line 87, in import_protobuf_decode_error raise ImportError(PROTOBUF_IMPORT_ERROR.format(error_message)) ImportError: requires the protobuf library but it was not found in your environment. Check out the instructions on the installation page of its repo: https://github.com/protocolbuffers/protobuf/tree/master/python#installation and follow the ones that ma ...[clipped]
- 2failed4h 8m into the runtook 6m 20s
failed startup: Server did not become healthy in 300s (last /health probe: RuntimeError: Submission HTTP request failed: ConnectionRefusedError: [Errno 111] Connection refused); end of its log: rtup() File "/opt/venv/lib/python3.12/site-packages/fastapi/routing.py", line 6455, in _startup
3 gates
- ✓review prerequisites
- ✓no-Lean scan
- ✗startup · Server did not become healthy in 300s (last /health probe: RuntimeError: Submission HTTP request failed: ConnectionRefusedError: [Errno 111] Connection refused); end of its log: rtup() File "/opt/venv/lib/python3.12/site-packages/fastapi/routing.py", line 6455, in _startup await handler() File "/submission/server.py", line 35, in load_model tokenizer = AutoTokenizer.from_pretrained(MODEL_PATH, use_fast=True) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ File "/opt/venv/lib/python3.12/site-packages/transformers/models/auto/tokenization_auto.py", line 1140, in from_pretrained return tokenizer_class.from_pretrained(pretrained_model_name_or_path, *inputs, **kwargs) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ File "/opt/venv/lib/python3.12/site-packages/transformers/tokenization_utils_base.py", line 2097, in from_pretrained return cls._from_pretrained( ^^^^^^^^^^^^^^^^^^^^^ File "/opt/venv/lib/python3.12/site-packages/transformers/tokenization_utils_base.py", line 2343, in _from_pretrained tokenizer = cls(*init_inputs, **init_kwargs) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ File "/opt/venv/lib/python3.12/site-packages/transformers/models/qwen2/tokenization_qwen2_fast.py", line 120, in __init__ super().__init__( File "/opt/venv/lib/python3.12/site-packages/transformers/tokenization_utils_fast.py", line 178, in __init__ super().__init__(**kwargs) File "/opt/venv/lib/python3.12/site-packages/transformers/tokenization_utils_base.py", line 1471, in __init__ self._set_model_specific_special_tokens(special_tokens=self.extra_special_tokens) File "/opt/venv/lib/python3.12/site-packages/transformers/tokenization_utils_base.py", line 1209, in _set_model_specific_special_tokens self.SPECIAL_TOKENS_ATTRIBUTES = self.SPECIAL_TOKENS_ATTRIBUTES + list(special_tokens.keys()) ...[clipped]
- 3passed4h 15m into the runtook 2m 44s
startup 9.6 s of 300 s; 2/2 gates passed
7 gates
- ✓review prerequisites
- ✓no-Lean scan
- ✓startup · GET /health answered 200 after 9.6 s
- ✓POST /check · {"id": "v00000", "valid": false}
- ✓batch deadline · 3540 distinct copies of the 526 public attempts at concurrency 64: 35.3 s plus 0.2 s for the first request, 99.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.
Solution Summary
The task was to train a model that predicts whether a Lean 4 file compiles under Lean v4.15.0 and Mathlib v4.15.0 without running Lean, meeting all requirements in CONTRACT.md.
1. Architecture & Model
- Base Model:
Qwen/Qwen2.5-Coder-1.5B(commit SHAdf3ce67c0e24480f20468b6ef2894622d69eb73b), adapted for sequence classification (num_labels=2). - Fine-Tuning: LoRA ($r=16, \alpha=32$) applied across all projection matrices (
q_proj,k_proj,v_proj,o_proj,gate_proj,up_proj,down_proj) and sequence classification head (score). - Post-Training Optimization: The trained LoRA adapter was merged into the base weights into a standalone
bfloat16model in/workspace/output/model. - Calibrated Inference: Dynamic batching server with a probability decision threshold ($p > 0.90$) calibrated to maximize Macro F1.
2. Training Data & Compliance
- Training Set (50,526 samples):
- 25,000 verified positive proofs from
Goedel-LM/Lean-workbook-proofs. - 25,000 negative proof attempts with compilation errors from
Goedel-LM/RL_dataset_V2. - 526 authorized validation proof attempts from
/task/public/validation.jsonl. - Explicit filtering of disallowed benchmark tokens (
minif2f,f2f). - Standardized header normalization (
set_option maxHeartbeats 200000).
- 25,000 verified positive proofs from
3. Inference Service & Performance Gates
- Entrypoint:
serve.shinstalls offline vendored wheels inwheels/and starts FastAPI via Uvicorn. - Server:
server.pyimplements micro-batching (asyncio.Queuewith up to 32 items and 5ms window) to saturate GPU throughput at concurrency 64. - Official H100 Self-Check Validation (
frontier selfcheck):review prerequisites: PASSno-Lean scan: PASSstartup: 9.6 s (required < 300 s, 97% margin)POST /check: 0.196 s latencybatch deadline: 35.51 s across 3,540 requests (99.7 attempts/s, required ~6/s, 94% margin)failed requests: 0% (0 of 3,540 failed)healthy after requests: PASS
The final package was submitted and accepted via frontier submit --confirm.