File size: 6,614 Bytes
d909bd8 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 | # Kimina Lean server as an optional pre-filter (evaluation, 2026-10-19)
Verdict: **built, pinned, safe by construction, and not worth adopting** as a throughput layer on the
P2 population. It cannot replace the strict verifier (compile-only: 40 of 54 code-bearing adversarial
cases compile clean) and as a pre-filter in front of it the pipeline is ~52 % slower than the strict
verifier alone. Code stays optional; nothing in `align/verify/lean/` changed.
## What was built (all under `/apps/development/rlhf/toolchains/`)
| | |
|---|---|
| Server | `project-numina/kimina-lean-server` @ `fb2393de` (server 2.0.0, Apache-2.0; its client package is MIT) in `src/kimina/kimina-lean-server`; venv `kimina-venv` (py3.11.13, fastapi 0.116.1, uvicorn 0.35.0, psutil 7.0.0, prisma client generated, no DB) |
| Lean / Mathlib | the SAME install as our verifier: Lean 4.9.0-rc1, Mathlib `d1d1e4b7` (`/apps/development/rlhf/lean/workspace`), selected with `LEAN_SERVER_PROJECT_DIR`; nothing rebuilt |
| REPL | `leanprover-community/repl@v4.9.0-rc1` (`7df77c0`) **+ cherry-pick `4fc1e6d` (flush stdout per reply)** in `work/kimina-repl49`, binary sha256 `699eed80...`. Our verifier's REPL (`32412d14...`) lacks that commit and relies on `stdbuf`; Kimina starts the REPL through `lake env` with plain pipes, so it needs the patch (Kimina's own `setup.sh` applies the same cherry-pick for Lean <= 4.9.0). The patch only flushes stdout. |
| Launch | `scripts/p2/kimina_server_start.sh`: scrubbed env, loopback only, `MAX_REPLS=4`, under `hostguard.py run --cores 4` |
Not pinnable / not built: **Pantograph** (leanprover/Pantograph, Apache-2.0): oldest tag `v0.2.18` needs Lean
4.10.0-rc1, current 4.31; no release for 4.9.0-rc1. **DeepSeek `xinhjBrant/repl@deepseek`** is the REPL fork
already used upstream of our pin (extra `allTactics`/`ast`/`premises` options we do not use); plain REPL variants
are what we already run. Kimina was the only candidate that serves our pin unchanged.
## Safety design (`align/verify_backends/kimina_server.py`)
* `PrefilterVerdict` is `reject | maybe | error`; no `accepted` field; `bool(verdict)` raises.
* `GatedVerifier.verify` reports an accept only from the wrapped `StrictVerifier`'s own verdict on the same
code. `maybe` and `error` (timeout, dead server, bad reply) always go to the strict verifier; only `reject`
short-circuits, which can lose recall but never soundness. Server down means "strict only".
* Loopback URLs only (the server has no sandbox, no axiom audit, no statement bridge, no lexical gate; it
applies only `RLIMIT_AS`).
* stdlib only (dependency firewall passes). `tests/test_kimina_backend.py`: 9 tests against a fake server,
including "server says it compiles, strict rejects => reject" and "no accept expression in the module".
## Measurements (`scripts/p2/backend_agreement.py`, report: `docs/results/kimina_agreement_report.json`)
741 items: 180 known-good (ceiling-test rows + restated), 61 adversarial, 500 random code-bearing records of
`gen_minif2f_c40960.jsonl` (seed 20261019, population 7632; `finish_reason=length` and code-less records are
excluded because both sides reject them without Lean). 4 workers/REPLs each, 180 s budget, phases run one at a
time. Control: our own REPL pool, compile-only, to separate server overhead from strict-tier overhead.
Agreement (rows ours, columns Kimina pre-filter):
| ours \ Kimina | maybe | reject | error |
|---|---|---|---|
| accept (485) | **485** | **0** | 0 |
| reject (213) | 40 | 173 | 0 |
| undecided (43: timeout/crash/memory) | 5 | 5 | 33 |
Known-good: ours accepts 177/180, Kimina passes 179/180. Adversarial: ours accepts 0/61, Kimina compile-only
passes 40 (all 40 are rejected by our lexical/target/header/axiom layers: axiom, native_decide, statement
changes, hole constructs, wrong names, banned constructs); gated accepts 0/61.
Sample (500): 308 strict accepts all passed the pre-filter; 155 rejects agree; **0 strict-only rejects** in the
sample (the policy layers matter on adversarial text, not on this honest-policy population).
Disagreements: 0 pre-filter false rejects. 40 strict-only rejects, all adversarial (listed in the report with
reasons). 43 undecided, all budget/limit effects: 33 where Kimina returned `error` (28 timeouts that ours also hit;
the 3 bomb cases: ours timeout / crash / memory kill, Kimina a 30 s timeout for each; 2 sample proofs that
ours memory-killed at ~21 s and Kimina answered HTTP 500 after ~129 s, i.e. its only memory defence is
`RLIMIT_AS`); 5 proofs where our
strict tier timed out at 180 s but Kimina decided `maybe` (81-152 s; incl. the known `lean_workbook_51088`,
`..._plus_64037`: the strict reference-env/audit layering slows borderline nlinarith, see LEAN_VERIFIER.md 5.1);
5 where strict timed out and Kimina found a compile error. Control: our compile-only vs Kimina agree on
648/650 jointly-decided items; the 2 diffs are instant `crash` records in the control pool (0.2 s,
harness artifact, both strict-accepted).
Throughput (same 680 kg+sample items, per-worker busy time, 4 cores):
| engine | proofs/s/core | total busy s |
|---|---|---|
| our strict verifier | 0.0491 | 13862 |
| our REPL, compile-only | 0.0585 | 11626 |
| Kimina server, compile-only | 0.0602 | 11300 |
Kimina is 2.8 % faster than our own REPL doing the same compile-only job (same Lean engine; Lean elaboration
is the cost, not the front end) and 18 % faster than the strict verifier, which includes reference env +
audit. Pipeline "Kimina then strict on survivors": 11300 + 9762 = 21061 s vs 13862 s strict alone (+52 %).
It rejects 160/680 (23.5 %) and saves 4100 s of strict work, but pays 11300 s up front. A pre-filter only
pays when its cost on rejects is far below the strict cost on rejects, which a same-engine compile cannot
be (mean per reject: Kimina 16.6 s vs strict 20.5 s; accepts, 76 % of survivors, are compiled twice).
## Recommendation
1. Do not put Kimina in the reward path as a pre-filter for P2-like populations (accept rate ~60 %).
2. It could only help if the survivor rate were very low (<~20 %) and a cheap budget (e.g. 10-20 s) were used
to reject; that is not the regime measured here, and a short budget turns slow valid proofs into losses.
3. Where it is useful: a loopback-only compile-feedback service (error positions for correction rounds)
and as an independent second implementation of "does it compile" for sanity checks.
4. The real strict-tier throughput lever is not the server: it is the per-proof REPL work (reference env,
audit prelude) and the heavy `nlinarith` tail (p90 92 s on the sample).
|