ChatTLA v2-sft2 — first verifier-gated RFT checkpoint with holdout passes

gpt-oss-20b fine-tuned on 260 verifier-certified TLA+ generation pairs (chattla-rft-corpora-v2) — every training example survived a hard-metric gate chain (SANY, TLC model-check, non-vacuity, mutation battery, decontamination; zero LLM-judge scoring). Targets are rendered through the gpt-oss harmony template with final-channel targets (plain-text SFT provably breaks gpt-oss channel discipline — that was this project's v2_sft1 lesson).

Training: experts-reaching LoRA (r=8, α=16; q/k/v/o_proj + target_parameters on mlp.experts.gate_up_proj/down_proj, MXFP4 dequantized to bf16), FSDP2, 4 epochs on 260 pairs, loss 2.67→0.52. This is a full merged bf16 model (verified: all 48 expert tensors present).

Honest evaluation (directional, NOT the project's frozen Gate-2 budget): NL→spec generation on a frozen 30-spec holdout, temp 0.8, TLC-verified:

  • pass@4 = 2/30 (specs that base gpt-oss-20b never passes even at pass@32)
  • base gpt-oss-20b comparison: pass@1 0/30, pass@32 4/30 (disjoint spec set → capability shift, not sampling luck)
  • Known limits: 20B (the project's target is 120B), k=4 vs the frozen k=32 budget; ~23% of samples still fail module extraction.

Part of the prove-TLA project: a verify-until-correct loop (SANY → TLC → non-vacuity → repair) provides a structural correctness guarantee; the model's job is only to make the loop converge. This checkpoint is the first evidence that training on the loop's own survivors transfers capability.

Downloads last month
396
Safetensors
Model size
21B params
Tensor type
BF16
·
Inference Providers NEW
This model isn't deployed by any Inference Provider. 🙋 Ask for provider support

Model tree for EricSpencer00/chattla-v2-sft2

Finetuned
(546)
this model

Dataset used to train EricSpencer00/chattla-v2-sft2