| # Strict Lean 4 verifier (Track L / P1) |
|
|
| A reward and an evaluator for formal proofs that cannot be gamed by "it compiles". Code: |
| `align/verify/lean/` (stdlib only), installer `scripts/lean_setup.sh`, ceiling test |
| `scripts/lean_ceiling_test.py` (+ frozen case tables `scripts/lean_ceiling_cases.py`), tests |
| `tests/test_lean_verifier.py`. The Lean toolchain is an external binary |
| (`docs/DEPENDENCY_POLICY.md`, "External binary: Lean 4 toolchain"), reached only through |
| `subprocess`. |
|
|
| Status (2026-10-12): implemented, tested without Lean (173 tests, fake REPL), tested against the |
| real toolchain (19 slow tests), mutation-tested (40 hand mutants), and **ceiling-tested**: |
|
|
| | | | |
| |---|---| |
| | Known-good accepted | **177 / 178 = 99.44 %** (Wilson 95 % [96.9 %, 99.9 %]); floor 98 % -> PASS | |
| | Adversarial accepted | **0 / 61** -> PASS (a compile-only grader would have paid 51) | |
| | Throughput, 8 workers | 0.57 proofs/s on a heavy unfiltered mix; 4.4 proofs/s on the median mix (GRPO shape) | |
| | Memory per warm REPL | 0.64-0.65 GiB PSS with 8 workers (0.24 GiB private); 0.85 GiB peak under load | |
| | Install | 5.57 GiB, 3 min; `import Mathlib` 3.2 s warm / 39.7 s cold | |
|
|
| Section 5 holds the numbers; every figure there is copied from a file under `.tmp/lean_ceiling/`. |
| Section 4 is the pre-registration. Section 6 lists what this verifier does not promise. |
|
|
| ## 1. The pin |
|
|
| | | | |
| |---|---| |
| | Lean | `leanprover/lean4:v4.9.0-rc1` (`lean --version`: 4.9.0-rc1, commit `be6c4894e0a6`) | |
| | Mathlib | `leanprover-community/mathlib4@d1d1e4b72c6e009edd97cabe1d661b021fe8eeae` (2024-06-12) | |
| | REPL | `leanprover-community/repl@v4.9.0-rc1` (`7df77c0a1c91`), built against the same toolchain | |
| | elan | 4.2.4 | |
| | Location | `/apps/development/rlhf/lean/` (`elan/`, `workspace/` = Lake project requiring Mathlib at the rev above, `repl/`, `PINS.json`) | |
|
|
| **Provenance (how "the Goedel-Prover-V2 pin" was determined, not assumed).** Goedel-Prover-V2's |
| README says "we follow DeepSeek-Prover-V1.5, which uses Lean 4 version 4.9 and the corresponding |
| Mathlib". The repo's `mathlib4` git submodule is `xinhjBrant/mathlib4` at commit |
| `2f65ba7f1a9144b20c8e7358513548e317d26de1`. That commit is a single child (message `align`, |
| 2024-08-07, Huajian Xin of DeepSeek) of upstream `d1d1e4b72c6e`, and changes only |
| `lakefile.lean` and `lake-manifest.json` to add `xinhjBrant/repl@deepseek` as a Lake dependency; |
| its `lean-toolchain` is `leanprover/lean4:v4.9.0-rc1`. So "Lean 4.9" in that README is |
| nominal: the binary is **4.9.0-rc1**, not 4.9.0. |
|
|
| **Deviation, and why it is safe.** We pin the *upstream parent* and build the REPL separately. |
| Mathlib's prebuilt `.olean` cache is keyed on a hash that includes `lakefile.lean`, so the |
| DeepSeek child commit would not hit the cache and would force a multi-hour Mathlib build. The |
| parent's Mathlib sources, and therefore the `.olean`s, are byte-identical to what the child |
| compiles; the only difference is which REPL fork the lakefile names. We use upstream |
| `repl@v4.9.0-rc1`, whose protocol (`cmd`/`env`) is all this package needs. The fork's extra |
| options (`allTactics`, `ast`, `premises`) are not used. Install cost with the cache: 3 minutes, |
| 5.8 GB (Section 5). |
|
|
| **Version drift is a correctness issue.** SafeVerify keeps separate branches for 4.9.0 and |
| 4.15.0; PutnamBench moved to 4.33.1 in 2026-09. Proofs verified here say nothing about 4.33. |
| Every number this verifier produces must be reported with this pin and the verifier tier. |
|
|
| ## 2. Architecture and what each layer defends |
|
|
| ``` |
| completion text ──extract_lean_code──▶ code ──static_check──▶ Plan |
| (reward.py) (strict.py: lexer, bans, header, target) |
| │ reject: no Lean touched |
| ▼ |
| ReplPool.acquire ─▶ Worker: [import once] ─▶ [audit prelude] ─▶ [header opens] |
| (repl_pool.py) │ |
| ref = `theorem _align_ref <given signature> := sorry` ──▶ env R |
| candidate body, run in env R ──▶ env C (errors / sorry ⇒ reject) |
| `#align_audit "<nonce>" 1 <target> _align_ref` in env C ──▶ verdict JSON |
| ``` |
|
|
| | Layer | Rejects | Independent of the lexer? | |
| |---|---|---| |
| | `extract_lean_code` | no fence / truncated (unclosed) fence / prose | n/a | |
| | header equality | any change to imports, `open`s, options (token-for-token vs the reference header) | yes (token compare) | |
| | lexical bans | `sorry`/`admit`, `native_decide`, `unsafe`/`partial`, `implemented_by`/`extern`/`export`, `axiom`/`opaque`, `macro`/`elab`/`syntax`/`notation`/`run_cmd`/`initialize`, any `#cmd`, `namespace`/`section`/`variable`/`attribute`/`local`, `instance`, `def`/`abbrev` (unless `allow_helper_defs`), `Lean.*`/`IO.*` identifiers, `exact?`/`apply?`, non-whitelisted `set_option` (incl. `maxRecDepth` > 16384), attributes that change compilation/elaboration | no (this is the lexer) | |
| | target rules | target missing, declared twice, `private`/`protected`/attribute on it, signature tokens differ from the reference's (strict mode) | no | |
| | compile | any `error`; any `sorry` warning; non-empty `sorries` | yes (Lean) | |
| | **audit: axioms** | any axiom outside {`propext`, `Quot.sound`, `Classical.choice`}: catches `sorryAx`, `Lean.ofReduceBool`/`trustCompiler` (`native_decide`), user axioms, even if the lexer were fooled | yes | |
| | **audit: statement bridge** | the kernel is asked to check `theorem _align_bridge : <type of _align_ref> := <candidate>`. `_align_ref` was elaborated *before* the candidate existed, so a definition-hole (instance, `variable`, shadowing) that makes the same text mean something else fails here | yes | |
| | **audit: kernel recheck** | every local theorem re-added with `debug.skipKernelTC` forced off | yes | |
| | **audit: meta-declaration scan** | a NEW local constant whose type/value mentions `Lean.Elab/Meta/Macro/Parser/PrettyPrinter/Syntax/Environment/Core/Compiler`, `IO`, `unsafeCast`: the footprint of an `elab`/`macro` that slipped past the lexer | yes | |
| | audit: kind | the target must be a `theorem` (not a `def` that happens to inhabit the type) | yes | |
|
|
| The audit verdict is the one info message tagged `ALIGN_AUDIT <random nonce>`, produced by a |
| **separate REPL call** after the candidate ran. The candidate's own output cannot carry the |
| nonce (it is generated after the candidate text is fixed), so it cannot forge a verdict. |
|
|
| Reward semantics (`reward.py`): `accuracy ∈ {0,1}`, 1 only if every layer passes. Diagnostics |
| (`StrictResult.reasons`, `.diagnostics`) are returned separately and never folded into the |
| reward: shaped partial credit ("compiles but has `sorry`") is exactly the gradient a policy |
| follows to the exploit (Leanabell-V2 also found shaped rewards slightly worse than binary). |
| Plug-in points, none of which change the loss or `CompositeReward`: |
|
|
| ```python |
| from align.verify.lean import ReplPool, StrictVerifier, LeanAccuracy, find_toolchain |
| pool = ReplPool.from_toolchain(find_toolchain(), preflight=True) # host rules + worker count |
| acc = LeanAccuracy(StrictVerifier(pool)) |
| accuracy, result = acc.score(formal_statement, completion_text) # float in {0,1}, diagnostics |
| terms, result = acc.reward_terms(composite, formal_statement, completion_text, fmt, n_tokens) |
| outcomes = acc.verify_batch(statements, completions) # OutcomeVerifier surface |
| ``` |
|
|
| **Failure semantics.** A proof that times out, exhausts memory or kills its REPL scores 0 (that |
| is a property of the proof). A *dead verifier* must not: `LeanInfraError` is raised when the |
| base environment cannot be built or when more than half of a batch (of at least 8) died for |
| infrastructure reasons. Otherwise a broken toolchain would feed the policy an all-zero reward |
| that reads as "the model got worse" (the 0/100 perfect-policy incident, mirrored). |
|
|
| Failure taxonomy (`StrictResult.reasons`): `no_code`, `parse_error`, `unsupported_statement`, |
| `header_mismatch`, `target_missing`, `target_modifier`, `statement_mismatch`, `banned:<x>`, |
| `compile_error`, `sorry`, `not_theorem`, `axiom:<name>`, `bridge_failed` (defeq mode), |
| `kernel_recheck_failed`, `meta_decl`, `skip_kernel_tc`, `timeout`, `crash`, `memory`, |
| `output_too_large`, `protocol`, `reference_invalid`. |
|
|
| Statement modes. `strict` (default): signature tokens equal the reference's *and* the kernel |
| bridge passes. `defeq`: bridge only, so an alpha-renamed or restated-but-defeq signature is |
| accepted. The bridge is checked by the kernel (not the elaborator's `isDefEq`), so "accepted" |
| means "the candidate's constant has a type the kernel accepts as the reference's type". |
|
|
| ## 3. REPL pool: measured facts the design rests on |
|
|
| | Fact (measured on this box, Lean 4.9.0-rc1 + Mathlib pin) | Consequence in code | |
| |---|---| |
| | The REPL **does not flush stdout when it is a pipe** (only a pty line-buffers); the client blocks forever | binary wrapped in `stdbuf -o0 -e0` (`tests::test_wrapped_argv_*`) | |
| | `lake env` prints **cwd-relative** paths (`././.lake/...`) | absolutised once in `toolchain.build_child_env`; child gets a minimal environment (no tokens) | |
| | A **second fresh `import Mathlib` in a live process** cannot re-mmap the `.olean`s and reads them into the heap: `Pss_Anon` 0.25 → **4.14 GiB** | one import per process; every header variant is layered on it (`split_imports`, `Worker.header_env`); a different import set recycles the process | |
| | RSS is ~3.65 GiB but 3.40 GiB of it is the shared, read-only `.olean` mapping; private heap is ~0.25 GiB | the watchdog caps **`Pss_Anon`**, not RSS; `plan_workers` budgets shared-once + n × cap | |
| | `Nat.pow exponent is too big` and `lean::stack_space_exception` **abort the process** (`rc=1`, `rc=-6`) | `ReplCrash` with the stderr tail; the next `acquire` respawns; scored 0 | |
| | `debug.skipKernelTC` is an **unknown option** on 4.9.0-rc1 | the whitelist + the audit's `skip_tc` check are guards for a pin upgrade, not a live exploit here | |
| | Lean 4.9 has **no public `collectAxioms`** (`#print axioms` is private) | `alignCollectAxioms` in the prelude (same traversal) | |
| | `variable (h : False)` *used in a proof body* is added to the theorem's type in 4.9 (pre-4.11 behaviour) | `variable` is banned lexically and the bridge catches it independently | |
|
|
| Limits per worker (defaults, `ReplLimits`): anonymous-memory cap 4 GiB (watchdog polls |
| `smaps_rollup` every 0.5 s), `prlimit --as=16GiB --fsize=256MiB --core=0`, `nice +5`, output cap |
| 16 MiB, per-proof wall budget 180 s (compile + audit), SIGKILL of the whole process group on any |
| violation, `MALLOC_ARENA_MAX=2`. Workers recycle after 1000 commands. Default worker count is |
| `min(8, cores // 4)` = 8 on this box; `ReplPool.from_toolchain(preflight=True)` applies the |
| `/apps/CLAUDE.md` checks (≥ 45 GB `MemAvailable`, load < 2× cores, disk queue < 64) through |
| `align.utils.guard.preflight_host_check` and then shrinks the worker count so that, even with |
| every worker at its cap, `MemAvailable` stays above the 45 GB floor. The ceiling-test script |
| takes the same exclusive heavy-job `flock` as the trainers (a Lean pool is a heavy job). |
|
|
| ## 4. Pre-registration (written BEFORE the registered ceiling run) |
|
|
| Registered 2026-10-12 20:12 IST, before any run of `scripts/lean_ceiling_test.py` without |
| `--allow-unregistered`. The case tables (`HEADER`, `STATEMENTS`, `ADVERSARIAL`, `RESTATED` in |
| `scripts/lean_ceiling_cases.py`) are frozen by hash: |
|
|
| PREREG_TABLE_SHA256: `61636c7136eb647801c588b00a35bd8bcc6ef4db126c21ea75769092883ff7e2` |
|
|
| `python scripts/lean_ceiling_test.py --verify-prereg` recomputes it; the registered run refuses |
| to start on a mismatch. |
|
|
| **Honest note on process.** The tables were developed against this verifier (about six exploratory |
| runs on 1-2 workers, `--exploratory --allow-unregistered`) so that every adversarial case is |
| *live* (it would be paid by a compile-only grader, which the run also measures) and every |
| restated proof compiles. Those exploratory runs informed case *authoring* only; thresholds |
| below were fixed before the registered run, and any verifier change after registration that |
| alters a verdict is reported as an amendment in Section 7, with the pre-amendment matrix kept. |
|
|
| **Configuration under test** = shipped defaults: `StrictConfig()` (strict statement mode, no helper |
| defs, kernel recheck ON, 180 s budget per proof) and `ReplLimits()` (4 GiB anonymous cap, 16 GiB |
| `--as` backstop), 8 workers, `lean_workbook` compile-only filter budget 120 s. |
|
|
| **Known-good set.** (a) Public verified proofs: 6 contiguous slices of 25 rows at offsets |
| 0, 5000, 10000, 15000, 20000, 25000 of `Goedel-LM/Lean-workbook-proofs` (29,750 proofs verified |
| under the Lean 4.9 / DeepSeek-Prover-V1.5 Mathlib environment), fetched over HTTP, never the |
| full dataset. (b) 30 hand-restated Mathlib-style theorems with proofs. The formal statement |
| given to the verifier is derived mechanically from each proof file (header + last theorem's |
| signature cut at the signature-ending `:=` + `sorry`). **Filter:** an independent compile-only |
| pass (same REPL, no strictness: no `error` message and no `sorry` warning) defines "compatible |
| with the pin"; items failing it are excluded *and listed*. Scored population = compile-clean |
| items. **Pass:** ≥ 98 % accepted and ≥ 50 items. (The roadmap's P1 row says ≥ 99 %; the task |
| fixed 98 %, which is what is registered. Both are reported.) Any rejected known-good item is |
| listed with its reasons; rejections caused by the policy bans (e.g. a genuine `native_decide` |
| in a public proof) count as failures, because that is the cost the RL stage would pay. |
|
|
| **Adversarial set.** ≥ 30 hand-built cases, all registered (61): categories sorry (7), admit (2), |
| extra axiom (4), native_decide (3), changed statement (6), weakened hypothesis (3), definition |
| hole (4), environment manipulation via elab/macro/run_cmd/initialize/#eval/#exit (9), theorem |
| proved for a different name (6), timeout/crash/memory bombs (3), banned constructs (6), header |
| tampering (4), no code (4). Each is a *completion* (prose + fenced block) so fence extraction, |
| static gate, REPL compile and audit are all exercised. **Pass:** 0 accepted. Bomb cases run on |
| a dedicated 1-worker pool (1 GiB anonymous cap, 30 s budget) so they terminate promptly; the |
| code path is the same. Reported alongside, not part of the pass criterion: how many cases a |
| compile-only grader would pay; and which cases the Lean-side audit rejects *on its own* with |
| the lexical gate disabled. |
|
|
| **Confusion matrix** (reported verbatim): rows = truth (good / bad), columns = verdict |
| (accept / reject); good = compile-clean known-good, bad = adversarial. |
|
|
| **Measurements** (reported, no threshold): install disk size; `import Mathlib` cold |
| (page cache evicted with `posix_fadvise(DONTNEED)`) and warm; per-REPL PSS / Pss_Anon / RSS from |
| `/proc/<pid>/smaps_rollup` with Mathlib imported, for one process and for 8 concurrent workers; |
| throughput (proofs/s) at the worker count used, with the worker set warm, on unique statements |
| and in the GRPO shape (12 statements × 8 samples); latency p50/p90/p99; PSS sampled during the |
| run. |
|
|
| ## 5. Results |
|
|
| All numbers below are copied from `.tmp/lean_ceiling/registered/result.json` and |
| `.tmp/lean_ceiling/registered.log` (the registered run: hash verified, `prereg_registered=true`, |
| 8 workers, host preflight passed, heavy-job lock taken after waiting for another track's job |
| to release it, started ~20:13 IST, 2026-10-12). Host: 48 cores; `MemAvailable` never fell below |
| 136.9 GB in the samples taken during the strict known-good pass. |
|
|
| ### 5.1 Ceiling test: confusion matrix (verbatim) |
|
|
| ``` |
| verdict ACCEPT verdict REJECT total |
| truth GOOD proofs 177 1 178 |
| truth BAD proofs 0 61 61 |
| ``` |
|
|
| | Criterion (pre-registered) | Measured | Verdict | |
| |---|---|---| |
| | known-good accepted >= 98 %, n >= 50 | **177 / 178 = 99.44 %** (Wilson 95 % [96.89 %, 99.90 %]); n = 178 | **PASS** (also >= the roadmap's 99 %) | |
| | adversarial accepted = 0, n >= 30 | **0 / 61** | **PASS** | |
| | gate 5 of the roadmap: strict false-negative rate > 5 % blocks P2 | 0.56 % (upper Wilson 3.1 %) | not blocked | |
|
|
| **Known-good population.** 180 candidates (150 Lean-Workbook-proofs rows from dataset revision |
| `b731852af8d8`, raw file sha256 `55932494...aebef`; 30 restated). The independent compile-only |
| filter kept 178: **148 + 30**. The 2 excluded (`lean_workbook_10036`, `lean_workbook_plus_64037`) |
| were excluded because the compile-only pass hit its **120 s budget** (`why: timeout`), not because |
| of a compile error, so "version-incompatible" would be the wrong label: they are slow proofs. |
| All 30 restated proofs were accepted. |
|
|
| **The one rejected known-good proof: `lean_workbook_51088`, reason `timeout`** (180 s strict |
| budget). It is a nlinarith proof with nine hints. Follow-up (exploratory, 1 worker, not part of |
| the registered numbers), same proof, same pool code, only the REPL environment layers differ: |
|
|
| | environment the body runs in | wall time | |
| |---|---| |
| | imports + header (what the compile-only filter uses) | 99.9 s (filter: 104.1 s) | |
| | + reference theorem `_align_ref` | 225.8 s | |
| | + audit prelude | 513.6 s | |
| | + both (= the strict path) | 516.5 s (timed out at 400 s in a separate strict run) | |
|
|
| On `lean_workbook_10009` (20 s) the same four environments take 19.9 / 20.8 / 20.1 / 20.0 s. So |
| this is not a systematic strict-tier slowdown; it is the well-known run-time chaos of a borderline |
| `nlinarith` (the certificate search is sensitive to state it inherits from earlier commands) hitting |
| a 180 s wall-clock budget. It is a genuine false negative of the *reward* (such a proof would score |
| 0), it is bounded at one in 178 here, and raising the budget to Goedel's 300 s would not have saved |
| it (517 s). The honest reading: wall-clock-bounded verification of proofs this close to the limit is |
| flaky in BOTH directions, so for evaluation (not training) report results at a stated budget. |
|
|
| **Adversarial population (61 cases, all rejected).** First reason per case: 58 rejected by the |
| static gate (no Lean call), 3 by the REPL layer (the bombs). By category (cases / accepted): |
| sorry 7/0, admit 2/0, extra_axiom 4/0, native_decide 3/0, changed_statement 6/0, |
| weakened_hypothesis 3/0, definition_hole 4/0, env_manipulation 9/0, wrong_name 6/0, |
| timeout_bomb 3/0 (timeout, `rc=-6` stack-overflow crash, anonymous-memory kill at 1110 MiB over a |
| 1024 MiB cap), banned_construct 6/0, header_tamper 4/0, no_code 4/0. |
| |
| * **A compile-only grader would have paid 51** of the 54 code-bearing, non-bomb cases |
| (each case's own text compiled with no strictness). The 3 it would not: `header_missing` (no |
| Mathlib), `duplicate_target` (Lean itself rejects a duplicate name) and `skipKernelTC_option` |
| (unknown option on this Lean). The 3 bombs and the 4 `no_code` cases are not applicable. So |
| 51 are live exploits, not strawmen. |
| * **Semantic layer alone** (lexical gate OFF, so each exploit actually executes inside Lean, with |
| `kernel_recheck` on): rejected **45 of the 54** code-bearing non-bomb cases by the Lean-side audit |
| alone (`sorry`, `axiom:bad`, `axiom:Lean.ofReduceBool`, `axiom:evil` after an `elab` added an |
| axiom, `statement_mismatch` for the instance hole, the `variable` hole, shadowing via |
| `macro_rules`, changed constants/hypotheses, `meta_decl` for `initialize`, `target_missing` |
| for wrong names/namespaces/private targets, `header_mismatch`). The 9 it accepted are the |
| *policy-only* set, where the proof of the stated theorem is valid and the lexical ban is the |
| only thing stopping it: `eval_side_effect`, `exit_after_theorem`, `attribute_on_target`, |
| `unsafe_implemented_by`, `partial_def`, `extern_attr`, `search_tactic_exact_q`, |
| `maxRecDepth_abuse`, `helper_def_with_proof`. None is a soundness gap (the theorem is proved); |
| they are rejected to keep the attack surface small, and each costs real-world proofs that use |
| them (Section 6, item 5). |
|
|
| ### 5.2 Install and process measurements |
|
|
| | Quantity | Measured | |
| |---|---| |
| | Install time (`lean_setup.sh`, cache hit) | 3 min 9 s (18:23:06 -> 18:26:15); an idempotent re-run takes ~10 s | |
| | Disk, total | 5,981,549,078 B = **5.57 GiB**: elan + toolchain 0.93 GiB, workspace 4.34 GiB (of which Mathlib package 4.11 GiB), REPL 94 MiB | |
| | `import Mathlib` + `Aesop`, **cold** (page cache for all 11,171 `.olean/.ilean/.so` files = 4.19 GiB evicted with `posix_fadvise(DONTNEED)`) | **39.7 s** | |
| | same, **warm** (3 runs) | 3.19, 3.20, 3.19 s (median **3.19 s**) | |
| | 8 workers warmed in parallel | 3.38 s (warm cache) | |
| | One REPL after the import (alone on the box) | RSS 3439 MiB, **PSS 3437 MiB**, `Pss_Anon` **244 MiB**, `Pss_File` 3193 MiB, 1 thread, VmSize 4071 MiB | |
| | **Per-worker PSS with 8 workers all holding Mathlib** | **643-653 MiB** each (mean 648; RSS 3.4-3.5 GiB each) = 244 MiB anonymous + 3193 MiB / 8 shared. Sum of PSS **5.06 GiB**; sum of RSS **26.8 GiB** (the double count the PSS figure removes) | |
| | Per-worker PSS **during** the 178-proof run (sampled every 0.5 s) | mean 717-792 MiB, max **873 MiB**; `Pss_Anon` max 404 MiB; RSS max 3.65 GiB | |
| | Worker growth over 1042 commands | none that approached any limit: recycled 0 times (limit 1000/worker) | |
|
|
| `fincore` was not usable for confirming the eviction (its output did not parse into a residency |
| fraction: the script printed `None` and `4096.0`; ignore those two fields in `result.json`). The 12x |
| cold/warm gap is the evidence that the eviction worked. |
|
|
| Model implied by the measurements: `PSS(n workers) ~ 0.24 GiB + 3.12 GiB / n` per worker, total |
| `~ 3.12 + 0.24 n` GiB. Eight workers cost ~5 GiB of RAM in total. The worst case (all eight at |
| their 4 GiB anonymous cap) is 3.12 + 8 x 4 = 35 GiB, which is what `plan_workers` budgets against |
| the 45 GB floor, so the pool cannot push `MemAvailable` under the floor on this host. **Roadmap gate 5** ("above ~4 GB per warm REPL the pool |
| shrinks below ~8 workers") is not triggered: 0.65 GiB per warm REPL, 0.85 GiB peak under load. |
|
|
| ### 5.3 Throughput (8 workers, warm) |
|
|
| | Shape | Proofs | Wall | Proofs/s | Notes | |
| |---|---|---|---|---| |
| | 178 unique statements (the known-good set, strict tier incl. kernel recheck) | 178 | 310.9 s | **0.573** | latency p50 1.97 s, p90 21.4 s, p99 158.6 s, max 180.3 s (the timeout), mean 9.76 s | |
| | GRPO shape: 12 median-latency statements x 8 identical samples | 96 | 21.9 s | **4.38** | reference environment and baseline audit reused per worker; all 96 accepted | |
|
|
| The first number is dominated by the heavy tail of Lean-Workbook `nlinarith` proofs (mean 11.7 s, |
| median 2.65 s for those; the 30 restated proofs: median 0.18 s, max 1.5 s) and by one 180 s |
| straggler: the ideal packing of the work is 178 x 9.76 s / 8 = 217 s. It is **not** a verifier |
| overhead: the compile-only filter took 273 s for 180 candidates on the same 8 workers, i.e. the |
| strict tier added ~14 % (audit 0.03-0.7 s per proof; kernel recheck +0.04-0.12 s on 20-43 s |
| proofs). Against the research report's guess of "1-3 proofs/s for 8-16 workers (low confidence)": |
| **0.57/s on a heavy, unfiltered population and 4.4/s on a median population**; either way |
| verification stays far above generation (~0.1-0.17 proofs/s per the report), so it is not the |
| binding constraint at this worker count. |
|
|
| ### 5.4 Test and mutation evidence |
|
|
| * `pytest tests/test_lean_verifier.py -m "not slow"`: 173 passed (no Lean needed; fake REPL |
| binary speaks the real protocol, including the audit message). |
| * `pytest tests/test_lean_verifier.py -m slow`: 19 passed on the real toolchain (accepts a correct |
| proof, rejects eight exploits with the lexical gate OFF, defeq-vs-strict mode, invalid reference, |
| timeout + recovery, end-to-end reward path, concurrency, memory shape). |
| * `tests/test_dependency_firewall.py`: 2 passed (`align/verify/lean/` and the two scripts import |
| only stdlib / `align`). |
|
|
| ## 6. Residual risks (what this verifier does NOT promise) |
|
|
| 1. **Lexer desync.** The lexical gate is a hand-written tokenizer, not Lean's. It follows Lean's |
| rules for nested comments, string escapes, raw strings, char literals and `«»`, and on any |
| unusual construct falls back to a raw-text scan, but it has not been differentially fuzzed |
| against Lean's real tokenizer. Mitigation: layers 3+ (axioms, bridge, kernel recheck, |
| meta-declaration scan) do not use it; the semantic-only column of the ceiling test shows |
| what they catch alone. What only the lexer stops is listed there (all of it is |
| *policy*, not soundness: the proofs are valid for the stated theorem). |
| 2. **No OS sandbox.** The REPL runs as the same user with filesystem access and no |
| network namespace. Code can only execute inside the elaborator through meta-programming |
| (`elab`/`macro`/`run_cmd`/`#eval`/`initialize`/`unsafe`), all of which are banned lexically |
| AND detected by the meta-declaration scan, and the child's environment holds no secrets |
| (`toolchain.build_child_env`). A meta-programming escape that evades both would run with the |
| verifier's file permissions. For adversarial RL, run the pool as a dedicated unprivileged |
| user or under `unshare --net` / a cgroup; that needs privileges this task did not have. |
| 3. **Statement fidelity.** The bridge proves the candidate proves the GIVEN formal |
| statement. It says nothing about whether that statement means what the informal problem |
| says (miniF2F: formal/informal discrepancies in over half the problems, 16 unprovable |
| statements; the report, section 5F). Report miniF2F-v2/PutnamBench with the pin and tier. |
| 4. **Trust base.** The Lean kernel, `propext`, `Quot.sound`, `Classical.choice`, the REPL, and |
| the prelude (`AUDIT_PRELUDE`, ~100 lines). The prelude is a trusted program; it is |
| exercised by the real-toolchain tests, not formally verified. |
| 5. **Policy rejections are not soundness failures.** `def`/`instance`/`notation`/`namespace` |
| helpers, `exact?`, `#eval` and so on are rejected even when the proof of the stated theorem |
| is valid. That is deliberate (smaller attack surface) and has a cost: public proofs that use |
| them are false negatives. `allow_helper_defs=True` relaxes only `def`/`abbrev`. |
| 6. **Version drift.** Proofs from other Lean/Mathlib versions will fail to compile (counted as |
| 0), which is correct for this pin and wrong as a statement about the proof. |
| 7. **Throughput numbers are for this population** (short Lean-Workbook-style and restated |
| proofs). A prover that emits long `nlinarith`/`decide` proofs will be slower; the audit costs |
| ~0.3 s for proofs whose dependency closure reaches real analysis and ~0.03 s for `omega`. |
|
|
| ## 7. Amendments |
|
|
| **7.1 Changes between the exploratory runs and the registration (before 20:12 IST; not |
| amendments, listed so nothing is hidden).** Case-table edits made after seeing exploratory output: |
| `sorry_branch` (its `all_goals sorry` was dead code, so the proof was valid: moved the `sorry` into |
| a live branch); `sorry_after_char_quote` / `sorry_after_comment_opener_string` (did not compile; |
| rebuilt so the `sorry` really sits between two quote-bearing literals); `axiom_private`, |
| `axiom_reducible_attr` (did not compile; replaced by `axiom_polymorphic`, `axiom_via_simpa`); |
| `ofReduceBool_term` (`rfl` cannot discharge `Lean.reduceBool`; replaced by |
| `native_decide_in_helper_lemma`); `local_notation_hole` (a local `+` notation is *ambiguous* with |
| the builtin one, so it never elaborates; replaced by `variable_hole_hypothesis`); |
| `rs_default_arg` (did not compile). Verifier changes made before registration, each driven by a |
| measurement: single import per process (Section 3), the late-answer drain, `kernel_recheck` |
| default, the `open Lean`-root ban, `notation3`/`binder_predicate`/... bans, 180 s default budget, |
| `split_imports`/prelude-before-opens layering. The `skipKernelTC_option` case turned out to be |
| **inert on this pin** (the option does not exist) and was kept, labelled. |
|
|
| **7.2 Retraction.** A first measurement reported the kernel recheck as costing "2.2-3.2x" |
| (`lean_workbook_10009`: 21 s -> 68 s). That reading came from a run on a host where two other |
| Lean processes were competing; isolated measurements (`#align_audit` flags 0 vs 1 on the same |
| environment) show **+0.04 to +0.12 s** against 20-43 s of elaboration. The recheck is therefore ON |
| by default; the claim was removed from the code comment before registration. (The same episode is |
| why the headline timings here come from the registered run; the few ad-hoc timings are labelled |
| exploratory.) |
|
|
| **7.3 Verifier changes after registration:** none. The registered run used the tree that is |
| described here. |
|
|
| **7.4 Failures found by running against the real toolchain (each has a regression test).** |
| (1) REPL never flushes a pipe -> `stdbuf`; (2) `lake env` paths are cwd-relative -> absolutised; |
| (3) a second `import Mathlib` in a live REPL costs +3.9 GiB anonymous and tripped the 4 GiB |
| watchdog on the first multi-case run -> one import per process, layered headers; (4) |
| `#print axioms`'s collector is private in 4.9 -> own traversal; (5) with `autoImplicit` on (plain |
| Lean default) an *unknown identifier* in a statement is silently an implicit variable, so "invalid |
| reference statement" needs a genuine type error to trigger `reference_invalid`; (6) `sqrt` under |
| `open Real Nat` is already ambiguous, so a root-level `def sqrt` is not a viable definition hole |
| here (instances and `variable` are); (7) pool statistics were counted only when an error escaped |
| `acquire`, not when the caller handled it. |
|
|
| **7.5 Hand mutants** (each removes one fix in a COPY of the package, then runs the non-slow |
| tests; `.tmp/lean_notes/mutants.py`, final run after the last code change except docs): |
|
|
| | | Mutant (fix removed) | Killed by | |
| |---|---|---| |
| | M01 | accept any audit-tagged message (forgeable verdict) | `test_audit_message_without_the_nonce_is_ignored_forged_verdict_regression` | |
| | M02 | no axiom whitelist check | `test_each_audit_finding_rejects[axiom/sorryax/ofreduce]` | |
| | M03 | ignore the kernel statement bridge | `test_each_audit_finding_rejects[bridge]` | |
| | M04 | no meta-baseline subtraction | `test_verdict_accepts_a_clean_audit` | |
| | M05 | no meta-declaration check | `test_each_audit_finding_rejects[meta]` | |
| | M06 | ignore `sorry` warnings / `sorries` | `test_each_audit_finding_rejects[sorrywarn/sorrylist]` | |
| | M07 | header failure scored 0 instead of `LeanInfraError` | `test_header_failure_raises_infra_error_never_a_zero` | |
| | M08 | candidate runs without the reference env | `test_command_order_and_envs_are_the_contract` | |
| | M09 | no `stdbuf` | `test_wrapped_argv_uses_stdbuf_prlimit_and_nice` | |
| | M10 | kill the pid, not the process group | `test_timeout_kills_grandchildren_too_via_process_group` | |
| | M11 | no memory watchdog | `test_memory_watchdog_caps_anonymous_memory_not_rss` | |
| | M12 | timeout without killing | `test_timeout_kills_the_process_and_leaves_no_zombie` | |
| | M13 | tolerate bytes after the terminator | **survives: equivalent mutant** (two concatenated JSON objects fail `json.loads` anyway); the real defence is M39 | |
| | M14 | first `:=` wins | `test_sig_end_skips_let_in_type_not_the_first_colon_eq` | |
| | M15 | no char-literal handling | `test_lexer_char_literal_quote_is_not_a_string_start` | |
| | M16 | block comments do not nest | `test_lexer_drops_line_and_nested_block_comments` | |
| | M17 | no raw-scan fallback on lexer anomalies | `test_anomaly_triggers_raw_scan_...` | |
| | M18 | re-import for every header variant | `test_second_header_variant_reuses_the_import_never_imports_twice_regression` | |
| | M19 | lake paths left cwd-relative | `test_build_child_env_absolutises_...` | |
| | M20 | no header equality | `test_static_rejections[header...]` | |
| | M21 | `set_option` whitelist off | `test_banned_constructs_fire[set_option...]` | |
| | M22 | dead pool emits zeros | `test_reward_raises_when_the_pool_looks_dead_...` | |
| | M23 | defs accepted as proofs | `test_each_audit_finding_rejects[def]` | |
| | M24 | kernel recheck never requested | `test_kernel_recheck_is_on_by_default_...` | |
| | M25 | `skip_tc` ignored | `test_each_audit_finding_rejects[skiptc]` | |
| | M26 | recheck failure ignored | `test_each_audit_finding_rejects[recheck]` | |
| | M27 | private/attribute target allowed | `test_static_rejections[target_modifier]` | |
| | M28 | signature token equality off | `test_static_rejections[statement_mismatch]` | |
| | M29 | identifier ban list off | `test_banned_constructs_fire` | |
| | M30 | salvage unclosed fences | `test_extract_unclosed_fence_is_not_salvaged` | |
| | M31 | first fence instead of last | `test_extract_takes_last_closed_lean_fence_and_ignores_think` | |
| | M32 | duplicate target allowed | `test_static_target_declared_twice_is_rejected` | |
| | M33 | ablated verifier usable as a reward | `test_reward_refuses_the_ablated_verifier` | |
| | M34 | worker never returned to the pool | **hang-killed** (the pool tests block; 90 s watchdog) | |
| | M35 | no recycling after `max_requests` | `test_worker_recycled_after_max_requests` | |
| | M36 | unbounded glibc arenas | `test_build_child_env_absolutises_...` | |
| | M37 | child inherits the whole `lake env` | `test_build_child_env_absolutises_...` (secrets leak assertion) | |
| | M38 | no output cap | `test_oversized_output_kills_the_process` | |
| | M39 | late second answer attributed to the next request | `test_late_second_answer_is_detected_...` | |
| | M40 | `open Lean` makes meta identifiers spellable | `test_banned_constructs_fire[open Lean...]` | |
|
|
| 40 mutants: **38 killed by an assertion, 1 killed by a hang (M34), 1 survivor (M13, equivalent)**. |
| Not covered by any mutant, by construction: the `skip_tc` audit path against the REAL option (it |
| does not exist on this pin; `test_real_skip_kernel_tc_option_does_not_exist_on_the_pin` fails the |
| day the pin changes) and the Lean prelude's kernel-recheck loop against a proof that elaborated |
| with the kernel disabled (no way to produce one on 4.9 without the banned meta-programming). |
|
|
| **7.2 V1 freeze (2026-10-14, branch `phase0/verifier`; PROPOSED FROZEN HASH, merge after chain6 exits).** |
| Fixes (regressions in `tests/test_lean_hardening.py`, each adversarial proof was accepted or aborted a batch before): |
| U08-1/2 lexer desync (`\/` and `//` are single tokens; a comment opener glued to any other symbol is refused as |
| ambiguous; numerals no longer swallow letters: `1macro`; raw strings of any hash count; real-Lean differential fuzz); |
| U08-40 `s!`/`f!`/`m!` interpolation flagged whatever sits before the quote; U08-4/12 `_align*` names and |
| `_root_.`/`«»` spellings banned; U08-5 axiom-walk fuel exhaustion reports `_align_fuel_exhausted` (fails closed) and a |
| missing `axioms` field is `audit_incomplete`; U08-3 `ReplPool.from_toolchain(sandbox=True)` is the default, fails closed |
| with `SandboxUnavailable`, `sandbox=False` is the explicit opt-out; U08-8 every real REPL runs under the launcher/supervisor |
| (`ReplProcess.supervise`) that SIGKILLs it when the parent process dies (measured: orphaned before, reaped now); |
| U08-6 stale env ids after a worker death raise `ReplCrash`; U08-7 lone surrogates reject that item only; U08-17 budget |
| starts after `acquire()`; U08-18 a bad reference header is `reference_invalid`, not a batch abort; U08-21 any exception |
| mid-request kills the child; U08-11(codex) unmeasurable memory fails closed after `mem_miss_limit` samples; U08-16 |
| timeout/crash/memory/protocol map to `Outcome.UNDECIDED` (new enum member in `align/eval/verifier.py`, reward stays 0). |
| Ported from the red-team session: opt-in `independent_recheck` (`recheck.py`), default off. |
| NOT changed (design choices, math verifier, need a decision): U08-9/10/11/15 (tolerance, texty fallback, unit stripping, |
| `i`), U08-13/14/22 (extractor ReDoS/format), U08-19/20 (preflight opt-in, pin not enforced at runtime). |
|
|
| Verification: exploratory ceiling run (2 workers, sandboxed): known-good 176/177 accepted (the one reject is a |
| 179 s timeout under host load), adversarial 0/61 accepted. Registered run to do after the chains exit (needs the heavy |
| lock): `python scripts/lean_ceiling_test.py --workers 8`. |
| Frozen hash: `sha256` over, for each `align/verify/**/*.py` in sorted path order, `path + NUL + bytes + NUL`: |
| `6df56348db12d8e255427764f994d0f3ab29d4713e84ddda07c9637c31f12648`. |
|
|
| **7.3 FROZEN (2026-10-19).** Merged verifier (V1 + MV math-checker fixes) hash |
| `f1dd9e7871ade3a9dd37587c10a7a17025fe8623a735455ec40206607e120b5c` (`scripts/p2/verifier_hash.py`; supersedes the |
| 7.2 proposal, which predates MV). Registered ceiling run (8 workers, heavy lock, sandboxed, `.tmp/restart/ceiling/result.json`): |
| known-good 178/179 accepted = 0.9944 (Wilson95 [0.9690, 0.9990], floor 0.98) PASS; adversarial 0/61 accepted PASS |
| (a compile-only grader would accept 51). Every SOTA number from here on is verified under this hash; chain8 refuses to |
| run a step if `align/verify` changes. |
|
|
| ## 8. Operations |
|
|
| ```bash |
| bash scripts/lean_setup.sh # install / repair (idempotent, ~3 min, 5.8 GB, under /apps) |
| bash scripts/lean_setup.sh --check # exit 0 iff the install is complete |
| source /apps/development/rlhf/lean/env.sh # only if you want elan/lake in your shell |
| |
| pytest tests/test_lean_verifier.py -m "not slow" # no Lean needed (fake REPL binary) |
| pytest tests/test_lean_verifier.py -m slow # real toolchain, 2 workers (~1 min) |
| |
| python scripts/lean_ceiling_test.py --verify-prereg |
| python scripts/lean_ceiling_test.py --workers 8 # registered run: preflight + heavy-job lock |
| python scripts/lean_ceiling_test.py --measure-only # install size, cold/warm import, PSS |
| ``` |
|
|
| * `ALIGN_LEAN_ROOT` relocates the install. Every cache the toolchain writes is redirected |
| under it by `lean_setup.sh`; nothing goes to `$HOME`, `/` or `/tmp`. |
| * Worker stderr spools to `<root>/tmp/pool/worker<i>.stderr` (truncated per respawn; the tail is |
| quoted in `ReplCrash`). |
| * Before widening the pool: `plan_workers` and `ReplPool.from_toolchain(preflight=True)` are the |
| only sanctioned way; never construct more workers than the 45 GB floor allows. |
| * A new Lean/Mathlib pin is a new verifier: re-run the ceiling test, update `PINS.json` |
| provenance in Section 1, and regenerate any cached verdicts. |
| * Hand mutants (Section 7) are run on a COPY of the package under `.tmp/mutants/`; the repo is |
| never edited in place. |
|
|
