chattla-w4dg-120b-adapter

LoRA adapter for openai/gpt-oss-120b, trained on the W4 "diamond-gold" corpus of verifier-accepted TLA+ specifications (~5,010 surviving examples, 517 with liveness properties).

The merged full-weight model is at chattla-w4dg-120b — see that card for the full evaluation, including the caveats, which apply equally here.

Usage

from peft import PeftModel
from transformers import AutoModelForCausalLM, AutoTokenizer

base = AutoModelForCausalLM.from_pretrained("openai/gpt-oss-120b", device_map="auto")
model = PeftModel.from_pretrained(base, "EricSpencer00/chattla-w4dg-120b-adapter")
tok = AutoTokenizer.from_pretrained("openai/gpt-oss-120b")

For vLLM serving, prefer the pre-merged chattla-w4dg-120b.

Evaluation summary

Frozen 30-spec holdout, pass@32, scored by SANY + TLC:

• 16/30 generating a whole spec from a description (framing A)
• ~52% row-level pass repairing a corrupted spec (framing B, partial run)

No comparison against the previous checkpoint is statistically significant (McNemar exact p = 0.22 vs. 11/30). A control group of 17 identical-prompt specs showed spec-level verdicts moving by one and row-level counts swinging much harder across runs, so single-run pass@32 at k=32 should not be read as a capability signal without multiple seeds.

Only ~2% of framing-A attempts fail because the system was modeled incorrectly; the rest fail mechanically (parse errors, missing EXTENDS, name collisions). Budget for a repair loop.

Intended use

Research on LLM-assisted formal specification. Output is a candidate module, meaningful only once SANY/TLC accepts it — not a source of verified specs on its own.

Project repo: https://github.com/LUC-AI4FM/tla-prover