| # P2 single-turn on-policy RL for Qwen3-8B-family Lean provers (lane R; docs/SOTA_PLAN.md L5 / K1 / Phase 0b item 1). | |
| # | |
| # CPU-only loop + vLLM generation child + torchrun training child, one after the other (never concurrently): | |
| # .venv/bin/python scripts/p2/rl_lean.py run configs/p2_rl_lean.toml --set run_dir=<RUN> --set problems=<POOL.jsonl> | |
| # Phase 0b probe (one real iteration, 4-8 prompts x G=8): see docs/RL_LEAN.md. | |
| # | |
| # Every value below is a DEFAULT of this lane, not a pre-registered number: the knobs the plan freezes | |
| # ([loss] eps_high, [optim] lr, [lora] r) are marked [TBD pre-reg]. Struct mode: unknown keys are errors. | |
| run_name = "p2-rl-lean" | |
| run_dir = "" # set per run | |
| # Goedel-Prover-V2-8B snapshot; Kimina-Distill-8B for the K arms (docs/KIMINA_BASE.md) | |
| model_snapshot = "/apps/development/rlhf/hf_cache/hub/models--Goedel-LM--Goedel-Prover-V2-8B/snapshots/dfd02e6271a58375dfbf3ece0175277cf6b6a89a" | |
| problems = "" # P2 problem JSONL (training pool; never an eval split) | |
| iterations = 20 | |
| prompts_per_iter = 16 | |
| seed = 0 | |
| keep_checkpoints = 2 # adapter checkpoints are small; the bound is for disk hygiene | |
| export_merged = false # true only with rollout.adapter_mode = "merged_export" (lossy bf16 fallback) | |
| replay_from = "" # K1: reuse another run's gens/ver (same cached rollouts, different loss.mode) | |
| verify_workers = 8 # <= 8 (scripts/p2/verify_generations.py rule); >2 takes the heavy lock itself | |
| verify_budget_s = 180.0 | |
| verify_python = ".venv/bin/python" | |
| [rollout] | |
| top_p = 1.0 # REQUIRED (Codex P13-32): behaviour logprobs are only meaningful un-truncated | |
| top_k = 0 | |
| temperature = 1.0 # trainer scores under the same T (validated equal to loss.temperature) | |
| cap_tokens = 16384 | |
| max_model_len = 20480 | |
| tp = 4 | |
| adapter_mode = "unmerged" # vLLM LoRARequest on the base (needs lean_gen --lora-adapter); "merged_export" = fallback | |
| rollout_python = ".venv-rollout/bin/python" | |
| gen_extra_args = [] | |
| [batch] | |
| group_size = 8 # G | |
| min_valid_per_group = 2 # after masking timeouts | |
| no_signal_reasons = ["timeout", "crash", "protocol"] # masked, never scored 0 | |
| ei_keep_all_solved = true # ei mode: keep positives of all-solved groups | |
| micro_tokens = 16384 # padded tokens per micro-batch; measured envelope of the SFT probe (configs/p2_sft.toml) | |
| max_total_len = 18432 # drop longer prompt+completion rows (counted); 0 = off | |
| [loss] | |
| mode = "cispo" # cispo | dr_grpo | ei | |
| eps_high = 4.0 # [TBD pre-reg] CISPO IS-weight clamp; sweep {0.272, 1.0, 4.0} | |
| # eps_low omitted = no lower clamp (paper). neg_seq_ratio_floor omitted = off. | |
| clip_lower = 0.2 # dr_grpo PPO clip | |
| clip_higher = 0.28 | |
| norm = "global_token_mean" # explicit global response-token count over micro-batches and ranks | |
| fp32_head = false # MiniMax-M1 3.2; Phase 0b: if memory is short at 16k, leave off and watch old_vs_behaviour | |
| fp32_head_chunk_tokens = 2048 | |
| temperature = 1.0 | |
| max_grad_norm = 1.0 | |
| [optim] | |
| lr = 1e-5 # [TBD pre-reg]; RL on an already post-trained prover: small | |
| betas = [0.9, 0.95] | |
| weight_decay = 0.0 | |
| eps = 1e-8 | |
| warmup_iters = 2 | |
| steps_per_iteration = 1 # one optimizer step per rollout batch (strictly on-policy) | |
| [lora] | |
| r = 64 # [TBD pre-reg] | |
| alpha = 128.0 | |
| rslora = false | |
| targets = ["q_proj", "k_proj", "v_proj", "o_proj", "gate_proj", "up_proj", "down_proj"] | |
| adapter = "policy" | |