File size: 3,651 Bytes
d909bd8 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 | # 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"
|