code/docs/KIMINA_SERVER_BACKEND.md

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