| # 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). |
| |
