JS-SAM experiments: repair loop + JS-SAM-vs-TLA+ comparison - #2
Open
jdubray wants to merge 3 commits into
Open
Conversation
Feeds each model its own failing Phase-3 transitions (real pre/action/ post vs what its model produced) and asks it to fix the spec, then re-scores. One round, same 28-window corpus. Result — self-correction tracks capability, more sharply than one-shot: Opus 4.8 89.3% -> 100% (full repair) Fable 5 50.0% -> 100% (fully fixes its ReleaseLock defect, 0->100%) Sonnet 4.6 50.0% -> 60.7% (fixes AcquireLock; ReleaseLock still 0%) Haiku 4.5 21.4% -> 21.4% (no improvement) Fable's baseline defect turns out to be a recoverable slip, not a capability ceiling. Adds scripts/experiments/repair_phase3.py (driver) and docs/js_sam_repair_experiment.md (write-up + caveats). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The Phase-3 repair driver was placed under scripts/experiments/, which is gitignored, so the prior commit shipped the write-up without the script it references. Move it to scripts/repair_phase3.py and fix the doc reference. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Head-to-head on spin (same 4 models). Both languages: 4/4 pass syntax (P1). They diverge at model-checkability (P2): JS-SAM 4/4, TLA+ 1/4. Attributed precisely: - Opus & Sonnet: unbounded `CHOOSE v : v \notin Threads` for "no owner" — SANY accepts, TLC rejects. A TLA+ semantic trap absent in JS (native null). Caught 2/4 models incl. the strongest. - Haiku: harness config generation fell back -> no usable .cfg (0 states) — a config surface JS-SAM's self-contained module avoids entirely. - Fable: clean (574 states, 7 invariants). Direct evidence for the JS-SAM hypothesis, with honest caveats (the TLA+ gap mixes a real pitfall with a config-gen shortfall; single task; direct translator; Phase 3 not compared). Also fixes scripts/setup_tools.py: shutil.move ran inside the open NamedTemporaryFile block, truncating tla2tools.jar / CommunityModules on Windows (broken zips -> ClassNotFoundException: tla2sany.SANY). Flush and close before moving, and verify the byte count against Content-Length. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Two experiments enabled by the earlier JS-SAM work, plus a tooling fix.
Stacked on the follow-ups PR (base =
js-sam-followups); retarget after thatmerges. Diff here is only the experiment commits.
1. Phase-3 repair loop — self-correction from feedback
Each model is shown its own failing Phase-3 transitions (real pre/action/post vs.
what its model produced) and asked to fix the spec; one round, then re-scored.
Self-correction is a sharper capability gradient than the one-shot scores, and
Fable's baseline defect turns out to be a recoverable slip, not a ceiling.
Driver:
scripts/repair_phase3.py; write-up + caveats indocs/js_sam_repair_experiment.md.2. JS-SAM vs. TLA+ — same models, same task
The head-to-head the backend exists to inform.
Both write valid syntax; they diverge at checkability. Attributed precisely:
Opus & Sonnet hit an unbounded
CHOOSE(TLC rejects; a TLA+ trap JS avoids withnative
null); Haiku hit the harness config-generation surface (JS-SAM'sself-contained module has none); only Fable was clean. Honest caveats included
(the gap mixes a real pitfall with a config-gen shortfall; single task; direct
translator; Phase 3 not compared). Details in
docs/js_sam_vs_tla_comparison.md.3. Fix: truncated tool downloads
scripts/setup_tools.pymoved the temp file while it was still open inside theNamedTemporaryFileblock, truncatingtla2tools.jar/CommunityModulesonWindows (broken zips →
ClassNotFoundException: tla2sany.SANY). Flush+closebefore moving, and verify the byte count against
Content-Length. This is whatblocked every TLA+ phase until the jars were re-fetched.
🤖 Generated with Claude Code