RL on formal verification via Tinker: de-risked

The whole pipeline, in plain terms

1 · One RL iteration, end to end

Sampling and gradient steps run remotely on Tinker; grading is a plain local Python function call in between — no container, no build system. That is the whole reason this task family was picked for de-risking.

 data/tasks_v3.jsonl
        │  pick 16 problems
        ▼
 ┌─────────────────┐   8 samples each   ┌──────────────────┐
 │  build prompt   │ ─────────────────▶ │  Tinker sampler  │  (remote GPU)
 └─────────────────┘                    └────────┬─────────┘
                                                 │ 128 completions
                                                 ▼
                                        extract_proof()  ← last ```lean fence
                                                 │
        ┌────────────── GRADER (local, in-process) ───────────────────┐
        │ 1. regex guards (sorry/axiom/#/macro/…)  ── hit? → fail      │
        │ 2. splice tactic block into statement + add #print axioms    │
        │ 3. tempfile → subprocess `lean` (60s timeout, ≤16 parallel)  │
        │ 4. axiom report ⊆ {propext, Quot.sound, Classical.choice}?   │
        └───────────────────────────┬──────────────────────────────────┘
                                    │ reward ∈ {0,1} per sample
                                    ▼
                     advantage = reward − group mean
                     (all-pass / all-fail groups dropped)
                                    │
                                    ▼
 ┌──────────────────┐ forward_backward + optim_step ┌──────────────────┐
 │  build Datums    │ ─────────────────────────────▶│  Tinker trainer  │ (remote)
 └──────────────────┘                               └────────┬─────────┘
                                                             │ new LoRA weights
                                                             ▼
                                                  refresh sampler ─▶ next iter

2 · What's on disk

experiments/2026-07-08--aengus--tinker-rl-derisk/
├── data/tasks_v3.jsonl        # tasks: defs + statement + gold proof + split
├── src/
│   ├── tasks.py               # Task dataclass, file_with_proof() splicer
│   ├── prompts.py             # prompt builder, extract_proof()
│   ├── grader.py              # THE GRADER — grade_sync(), ~100 lines
│   ├── rl.py                  # GRPO loop (calls the grader inline)
│   └── engine.py / evalrun.py # eval path (same grader)
├── results/<run>/
│   ├── config.json            # hparams
│   ├── metrics.jsonl          # 1 line per RL iteration
│   └── rollouts.jsonl         # every sample + reward + fail reason
└── (machine-wide) ~/.elan/…/bin/lean   # Lean 4.14.0 — the only external dep

3 · How the dataset was built (and iterated)

Two candidate task families existed in the real repos. Family A (full Rocq→Lean translation, containerized, tool-driven) was rejected for de-risking: it needs Docker per rollout and base models score 0.0 — no gradient signal to learn from. Family B (Lean proof completion) won on three tests: locally gradeable in ~0.07s, base models in the 15–60% trainable band, objectively binary reward.

The build recipe, per version: write definition blocks → write theorem statements over them → write a gold proof for every task → run every gold proof through the actual grader (anything failing gets fixed or dropped, so 100% of shipped tasks are provably solvable) → freeze into JSONL with a split-preserving --freeze flag so the held-out comparator never shifts. For v4, hand-writing was replaced by six parametric generators (affine identities, repeat-sums, double recursions) stamped from random seeds; generated gold proofs still had to pass the grader.

ID vs OOD. In-distribution = the 26 frozen v3 held-out tasks (same families as training, unseen theorems). Out-of-distribution = the v2 families never present in training — rl1/rl5 transferring to ~90% there is the strongest evidence this is generalization, not memorization.

4 · How this compares to the real Rocq→Lean task

Honestly: a deliberately simplified proxy. The real task is Rocq→Lean translation plus equivalence proofs, with the agent inside a Docker container running bash, a file editor, a Rocq REPL and lean_export, up to 300 turns, 32k context, and a weighted multi-file reward — base models score 0.0 on it. This proxy is single-turn, text-only, one theorem, binary reward. It validates the GRPO plumbing, group-variance economics, SFT bootstrapping, and that most base-model failure is fixable output protocol. It does not validate long-horizon credit assignment, tool-call round-tripping, debugging from compiler errors over many turns, container state, or the translation step itself — see the bridging ladder in the findings.

5 · Inference on open models

All inference goes through Tinker's sampling API: a model registry maps each model to its chat renderer and per-token prices; an async engine caps 100 concurrent requests, logs JSONL transcripts, and meters cost live; the parser takes the last ```lean fence. Grid 1: 5 models × 46 tasks × 4 samples for $1.40 total — gpt-oss-120b best and cheapest per pass (59.8%); gpt-oss-20b at 23.4% had both headroom and gradient signal, so it became the RL workhorse. Completions are thinking-dominated: ~2.4k sampled tokens/attempt on gpt-oss-20b, ~9.3k on Qwen3.5-4B, versus final proofs of 1–10 tactic lines.

6 · Every RL run and its hyperparameters

Shared across all runs: GRPO with LoRA rank 32, importance-sampling loss, group-centered advantages (zero-variance groups dropped), lr 4e-5, group size 8, 16 problems/iter, temperature 1.0, 8192 max tokens, held-out eval every 5 iters at k=4 — deviations noted below.

7 · The grader, precisely

Everything happens in one function, grade_sync() in src/grader.py (~100 lines), whose Verdict.passed becomes the 0/1 reward. Four stages: (1) regex guards over the tactic block — sorry, admit, axiom, native_decide, ^#, macro/elab/set_option/unsafe — any hit fails before Lean ever runs; (2) splice the block after := by in the harness-owned statement and append #print axioms; (3) compile with plain lean (60s timeout, ≤16 parallel processes); (4) parse the axiom report — required because a file containing sorry still exits 0; the sorryAx axiom surfaces there instead. Every failure gets exactly one machine-readable reason (forbidden_token, compile_error, timeout, bad_axioms, no_axiom_report), and in the multi-turn variant the compile-error detail is the retry message. Reward-hack audits over 374 grid-1 and 676 rl1 passes: zero suspicious proofs.

RL scoreboard — all numbers on held-out tasks

The task, up close

Each task is one Lean 4 theorem over custom definitions (never library names — so simp can't just look the lemma up). The harness renders the full file with the proof replaced by sorry and shows it to the model inside an instruction prompt:

def myapp {α : Type} : List α → List α → List α
  | [], ys => ys
  | x :: xs, ys => x :: myapp xs ys

def myrev {α : Type} : List α → List α
  | [] => []
  | x :: xs => myapp (myrev xs) [x]

theorem myrev_involutive : ∀ (l : List Nat), myrev (myrev l) = l := by
  sorry

#print axioms myrev_involutive

How the agent interacts. There are no tools and no file editing. The model replies with ONE fenced code block containing only the tactic script; the harness splices it into the fixed theorem (Task.file_with_proof), appends #print axioms, runs lean file.lean (~0.07s), and parses the axiom report. Because the model never controls the statement, statement-weakening is impossible; sorry, injected axioms and native_decide all surface in the axiom report and score 0. A typical passing answer:

have happ_nil : ∀ (l : List Nat), myapp l [] = l := by
  intro l
  induction l with
  | nil => rfl
  | cons x xs ih => simp [myapp, ih]
have hrevapp : ∀ (l1 l2 : List Nat), myrev (myapp l1 l2) = myapp (myrev l2) (myrev l1) := by
  ...
intro l
induction l with
| nil => rfl
| cons x xs ih => simp [myrev, hrevapp, ih, myapp]

The dataset grew in four certified generations — every task ships with a gold proof that must pass the real grader before inclusion (this caught my own broken proofs ~10 times; failure modes: no ring_nf in core Lean, omega needing simp [Nat.mul_add, Nat.add_mul] to atomize nonlinear terms, indentation of multi-line case branches). Difficulty tiers: 1 = concrete computation (rfl closes it), 2 = one induction, 3 = helper lemmas, 4 = multi-helper (e.g. mymul_comm via three haves).

Splits are tier-stratified and FROZEN across generations (later builds pass --freeze), so one fixed 26-task heldout set anchors every RL comparison.

Multi-turn and retries. On failure the grader's actual output goes back as a user turn — "Your proof failed. Verdict: compile_error … Provide a corrected tactic block" — and the model tries again (≤3 turns in eval, ≤2 in RL). Who benefits from retries, per the solved-by-turn distribution (v3 heldout, 2 episodes/task):

Two distinct effects: for base models, retries are a big multiplier (compile errors carry real signal — the weak 20b uses all three turns; note its odd +4/+19 pattern: turn 2 often repeats the mistake, turn 3 fixes it). After RL, most value is already in turn 1 (42 of 49 solves) — and when we train through the retry loop (rl11: episode-level reward, per-turn credit), the policy internalizes the correction: mean episode length falls 1.9 → 1.17 turns while episode success rises ~40% → 92% peak. RL converts a retry technique into a first-try skill.

Where the SFT data came from. No external corpus: the dataset's own certified gold proofs. Each training example is the standard task prompt plus the gold tactic block wrapped in a ```lean fence as the assistant turn, rendered by the tinker-cookbook renderer's build_supervised_example — cross-entropy weights are non-zero only on the assistant tokens, so the model learns to EMIT proofs, not to parrot prompts. 291 examples × 3–4 epochs ≈ $0.30, lifting gpt-oss-20b 18.3% → 54.8% before any RL. (Same mechanism the rl-rocq-lean plan calls "gold traces"; here gold = generator templates, there gold = harvested successful rollouts.)

Before vs after: how the model's attempts change

Same model (gpt-oss-20b), same 20 held-out tasks, 8 samples each, before and after RL. To separate format from skill we re-grade every base attempt under a 3-step normalizer (raw → leading-by stripped → hanging-indent fixed); method and per-task table in scripts/analyze_format_vs_skill.py, data in results/format_vs_skill/.

Read this honestly: most of the headline RL lift on THIS model is output protocol, which reward fixes in ~4 iterations — and which a 20-line normalizer in the harness would also fix for free. The defensible skill claim is the last +10.6pts, and it concentrates exactly where you'd want: tier-3 helper-lemma tasks (myadd_comm 2/8 → 5/8, mylen_rev 4/8 → 7/8, mytake_drop_app 5/8 → 6/8 after full normalization), while mydouble_add stays 0/8 → 0/8 — RL sharpened competence, it did not invent mathematics.

What a genuine (non-format) base failure looks like — the most common skill error is inducting without generalizing, which leaves the induction hypothesis conditional and the goal unprovable (base attempt, format-normalized, still fails):

have h1 : myadd n m = n + m := by
  induction n with          ← no `generalizing m`
  | zero => simp [myadd]
  | succ n ih => simp [myadd, ih, Nat.add_comm, ...]
...
-- lean: unsolved goals
--   ih : myadd n m = n + m → myadd m n = m + n   ← ih is CONDITIONAL
--   ⊢ myadd m n + 1 = n + (m + 1)

The RL'd model's passing version of the same helper lemma — correct generalizing clause and a simp set that terminates:

intro n m
have h_add : ∀ n m, myadd n m = n + m := by
  intro n m
  induction n generalizing m with
  | zero => simp [myadd]
  | succ n ih =>
      simp [myadd, ih, Nat.succ_add, Nat.succ_eq_add_one,
        Nat.add_comm, Nat.add_left_comm, Nat.add_assoc]
simp [h_add, Nat.add_comm]

Thinking length barely changes (~2.5k → 2.9k tokens): the improvement is in the emitted proof, not extra deliberation. And the format lesson generalizes: protocol failure was also the real task's measured blocker (base models 0.0 because of lakefile.toml) — this experiment shows reward eliminates that failure class quickly once gradient exists.

Learning curves

Model selection (inference grid, pre-RL)

gpt-oss-120b is both the strongest and the cheapest evaluator (59.8%, $0.12/run). gpt-oss-20b was picked for RL: most headroom, cheapest training ($0.36/Mtok), and pass@4 = 50% meant half the task groups already carried gradient.

Transcripts on Docent

All 66,056 eval and RL transcripts are merged into one Docent collection, shared with the Theorem Labs organization (read access):

tinker-rl-derisk — ALL runs

Inside Docent, filter by metadata.run to isolate any experiment — e.g. grid1 (model-selection grid), rl5-gptoss20b-v3 (headline GRPO run), rl9-warmstart-pool (SFT warm-start), mt-rl5-20b (multi-turn retries), base-gptoss20b-heldout-v3 (base-model baseline). Each run also carries task_id, iter/sample, tier, pass/fail reason, and a reward/passed score. Known gap: rl11-multiturn rollouts were not uploaded (its trainer doesn't write rollouts.jsonl).

Registry: results/docent_collections.json (key __merged__); reproducible via scripts/merge_docent_collections.py.