JS-SAM follow-ups: broader traces, 4-model comparison, shared agent translator - #1
Open
jdubray wants to merge 4 commits into
Open
JS-SAM follow-ups: broader traces, 4-model comparison, shared agent translator#1jdubray wants to merge 4 commits into
jdubray wants to merge 4 commits into
Conversation
Broadens Phase-3 coverage from 8 to 28 windows. test_spin_seq exercises alternating holders, try_lock successes, and repeated failed contention (still single-CPU-safe). build_and_test.sh now takes the ktest name as an argument and run.sh loops over both scenarios into per-scenario NDJSON. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Generalizes the agent-based invariant translator so backends other than TLA+ can use it instead of remapping to a single direct LLM call (maintainer Open Question 4). - New evaluation/semantics/agent_translation.py: language-neutral core (CLI selection, workspace setup, subprocess exec, output read). Caller supplies the workspace files, agent instructions, and output parser. - TLA+ AgentInvariantTranslator now delegates to it (behavior preserved; its _select_agent_cli/_execute_agent_cli move into the shared module). - JS-SAM translate_invariants: translator=claude-code/codex now drives the agent CLI (JS predicates against the generated spec, reusing the existing JSON parser); "claude"/explicit model still uses the direct call. End-to-end agent runs require the claude-code/codex CLI. - Tests mock the CLI boundary: shared-core success/missing-output/failure /codex paths, JS-SAM agent routing, and TLA+ delegation. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Adds sonnet (Sonnet 4.6) and haiku (Haiku 4.5) model entries and records the three-model comparison across all four phases on the 28-window trace corpus. Transition validation (Phase 3) is the discriminating metric: Opus 89.3% > Sonnet 50.0% > Haiku 21.4%, while all three pass phases 1/2/4 — the clearest evidence that JS-SAM's signal is in reproducing real system behavior. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Fable 5 (Anthropic's most capable model) scores only 50.0% (14/28) on Phase 3 — below Opus 4.8 (89.3%) and tied with Sonnet — despite passing phases 1/2/4. Cause is systematic: its model no-ops every ReleaseLock (0/11), leaving the lock held after release. Demonstrates that general capability rankings do not automatically transfer to formal-modeling accuracy, and that transition validation catches whole-action defects the other phases miss. Fable 5 model entry sends no sampling params or thinking config (both removed on that model; adapter's _should_omit_sampling_params covers it). 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
Follow-up work building on specula-org#21 (which this PR is stacked on — base is the
js-sam-crossplatform-phase3branch, so the diff here is only the fourfollow-up commits; retarget to
mainonce specula-org#21 merges).Three enhancements plus a notable finding:
test_spin_seq)grows the transition-validation set from 8 to 28 windows.
build_and_test.shtakes the ktest name as an argument;
run.shloops over both scenarios.spin(all four phases, same 28-window corpus).language-neutral core (
evaluation/semantics/agent_translation.py) that TLA+now delegates to (behavior preserved) and JS-SAM now uses —
translator= claude-code/codexdrives the agent CLI to produce JS predicates against thegenerated spec, instead of remapping to a direct call. Tests mock the CLI.
Comparison result
Transition validation is the only discriminating phase (all models pass 1/2/4).
The headline finding: Claude Fable 5 — the most capable model — scores below
Opus and ties Sonnet, because its generated model no-ops every
ReleaseLock(leaves the lock held after release). General capability rankings do not
automatically transfer to formal-modeling accuracy, and Phase 3 catches the
whole-action defect the other phases miss. Details in
docs/js_sam_model_comparison.md.Tests
tests/test_evaluation/test_agent_translation.py(shared core: success /missing-output / CLI-failure / codex paths) and a JS-SAM agent-routing test.
Full JS-SAM suite (incl. real-Docker phases) stays green.
🤖 Generated with Claude Code