# 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"