lab: optimization phase — fingering optimality gap (CP-SAT oracle vs production DP and human tabs) - #197
Open
PhysShell wants to merge 17 commits into
Open
lab: optimization phase — fingering optimality gap (CP-SAT oracle vs production DP and human tabs)#197PhysShell wants to merge 17 commits into
PhysShell wants to merge 17 commits into
Conversation
Opens the Constraint Lab's optimization phase: the SAT/UNSAT IR gains an objective so an external solver can report the *best* admissible realization, and the fingering experiment pins what it will measure. optir: construction refusals (shared IR invariants, ambiguous cost tables, empty hard tables), canonical tables and order-insensitive fingerprints, exact re-scoring of every term kind including overflow, the wire shape an external adapter consumes and produces, and the verdict rules — a solver's optimum is accepted only when proven, admissible, and re-scored exactly; the agreement pass is recounted and pinned to the optimum. fingering: tablature-line extraction from GP-style tracks with every cut cause counted; the mirrored v1 objective is the one the production DP minimizes (exhaustive brute force); v1 and hand-model IR encodings score exactly like the domain evaluators; the hand DP and fixed-position hand DP are optimal against brute force; song-level holdout keys. All new public functions are todo!() stubs here; the suite compiles and fails (24 fingering + 12 optir red; the serde-derived wire-parse test is green by construction) so the API is pinned before the implementation. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
optir: validated, canonical optimization IR (binary hard tables; unary and pair cost tables, weighted |a−b| and [a≠b] terms), i128-checked re-scoring, the problem/solve wire records, and the verdicts that accept an external optimum only when proven, admissible, and exactly re-scored. fingering: - tab_lines cuts a track into human-fingered monophonic lines per voice, counting every refused note (chords, unpositioned, beyond max fret, position/pitch mismatch, rests, short lines); - v1_cost / v1_problem mirror the production infer_positions objective independently of the production code; - HandModel: hidden index-finger position, four-fret box with one-fret stretches, shift event + distance, string distance, neck height, open strings; best_hands scores fixed positions (e.g. a human tab) exactly, solve_hand is the exact joint DP with a factored O(K²H + KH²) step; hand_problem is the same model as IR; - song_key / holdout_bucket for song-level holdout splits. Contract suite green (24 fingering + 13 optir); the spike's 36 tests stay green; clippy clean at the crate's deny level. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Measured on the tab corpus: most GP6 (.gpx) guitar tracks import with a strictly ascending tuning, i.e. string 1 = lowest, while every GP3/4/5/7 track follows the glossary's string 1 = highest. Pitches stay consistent (position and tuning are mirrored together), but orientation-sensitive choices such as the DP's "lowest string first" tie-break then flip with the file format. Pins that tab_lines emits lines in griff's orientation: strictly ascending tunings are mirrored (tuning reversed, positions renumbered, pitches untouched) and counted in CutStats::mirrored_tracks; non-monotonic tunings are left as they are. The field is added but ignored here (2 red; the non-monotonic guard is green by construction). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
tab_lines checks each position against the imported tuning as-is, then emits it in griff's orientation: a strictly ascending tuning is reversed, positions are renumbered (n + 1 − string), pitches are untouched, and the track is counted in CutStats::mirrored_tracks. Non-monotonic tunings pass through unchanged. Suite green (26 fingering + 13 optir + 36 spike). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Research tooling for the optimization phase (no new library API): - fingering_gap fit: exhaustive integer grid for the production v1 weights and multi-start coordinate descent for the hand model, both scored by per-note agreement with the tab authors on train songs only (song-level holdout, bucket 0 of 5 = test); - fingering_gap export: one IR problem per tablature line per model, with the human strings as the agreement reference; - cpsat/solve_opt.py: untrusted OR-Tools CP-SAT adapter — proven optimum, bound, witness, and a lexicographic agreement pass (min scale·cost − matches in one solve; pinning cost == optimum as a constraint was ~100× slower on a 136-note line); - fingering_gap report: rebuilds every problem from the tabs, verifies each solver record (fingerprint, proof, admissibility, exact re-score, recounted agreement), compares with the in-repo DP optimum, and archives aggregates only. lab/out/ is git-ignored: problems, solver records and per-line data are derived from licensed tabs (ADR-0005). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Measured on the tab corpus: tab authors finger a repeated 6-note figure identically in 98.5% of 23,635 repeat pairs, while the chain DPs do so in 84.8% (fitted v1) and 88.7% (fitted hand model) — context at entry and exit pulls repeats apart. Equality between distant notes is out of reach of a chain DP's local state, but not of the IR. Pins: repeat_pairs (non-overlapping, single-pitch windows skipped); with_repeat_consistency adds equal-string hard tables for aligned notes and refuses out-of-range pairs; with_string_tiebreak rescales the objective so cost-optimal sets are unchanged and ties resolve deterministically — the basis for comparing constrained and unconstrained solver witnesses. Stubs are todo!() here (3 red). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
repeat_pairs scans a line for non-overlapping repeated pitch windows (single-pitch windows skipped). with_repeat_consistency adds, per aligned note pair, an equal-string table over the shared string domain — the global constraint a chain DP cannot hold in its local state — and lets IR validation name any dangling pair. with_string_tiebreak rescales every objective weight by notes·max_string + 1 and adds each note's string, so evaluate' = scale·evaluate + Σ string: optimal sets unchanged, ties deterministic. Suite green (29 fingering + 13 optir + 36 spike); clippy clean. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
fingering_gap repeat-export / repeat-report: for every line with a repeated 6-note figure, export the model under a deterministic string tie-break and the same problem plus the repeat-consistency constraint; the report verifies both solver records, then compares repeat consistency (human / chain DP / solver / solver + constraint), agreement with the tab author, and the cost the constraint adds. solve_opt.py: two-tier solving. The first corpus run with one CP-SAT worker per problem left ~2% of v1 lines (80–357 notes) unproven after 120 s, while the in-repo DP covers the whole corpus in milliseconds; the same lines were proven in 0.2–1.1 s by a 16-worker portfolio, whereas a tighter local-marginal encoding with one worker still timed out on one of five. Problems are now solved in a pool with a short limit and unproven records are re-solved sequentially with a multi-worker portfolio; the solver identity records the escalation. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
A holdout-only oracle run leaves most lines without a record; they are now reported as 'not run' (oracle table) or left out of the sample (repeat report) instead of being counted as invalid or refused. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Archives the optimization-phase results (aggregates only; corpus content stays out of git): zero solver gap for the production DP on all 9,150 lines under both v1 weight sets, a large model gap to human tablature with song-level holdout, tie-insensitive agreement ceilings, the negative repeat-consistency result, CP-SAT cost and escalation data, the GP6 string-orientation side finding, limitations, prior art and follow-ups. The hand-model oracle run on holdout songs is still in progress and will be recorded in a follow-up commit. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
|
Important
This repository does not receive automatic reviews because it has fewer than 10 stars. ⚙️ Run configurationConfiguration used: defaults Review profile: CHILL Plan: Advanced Run ID: Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
CP-SAT proved the optimum on 1,930 of 1,954 holdout lines for the fitted hand model; solve_hand matches it on every one (gap 0, no invalid records). 24 lines stayed unproven after the 16-worker, 60 s escalation and carry no claim. Median solve 61 ms, 3,676 s in total — about an hour for what the DP does over the whole corpus in ~120 ms. The oracle table now prints "—" instead of 0% for models whose agreement pass was not run. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The audit read the median human excess dropping from 45 (v1) to 6 (hand model) as the hand model describing human choices better. Excess is in each model's own cost units: v1 charges every note its fret number, the fitted models have no per-note term, so the drop mostly reflects weight scale. The human-optimal rate is scale-free but inflated by flat objectives, and all-zero weights make both metrics perfect, so neither is a training target. States which columns compare across models (agreement only), downgrades the hand-model bullet to a hint, and corrects the string-crossing reading: the hand model's string *distance* carries weight, while the v1 family's string *change* weight fitted to 0. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The audit's corpus import gave nearly every GP7 note the wrong pitch (fallback Standard E tuning, notes numbered from the low string; fixed in #198). Adds a dated Correction section with the re-measured numbers on the fixed importer — refitted weights, holdout agreement for all four models, human-optimal rates, and CP-SAT-verified ceilings for v1 (36.2% vs DP 35.8%) and v1-fit (55.5% vs 44.1%) with zero solver gap on all 1,954 holdout lines — and states which conclusions hold (all), which got stronger (v1-fit is too flat), which shifted (absolute agreement, fitted weights; the hand model no longer beats fitted v1 on agreement), and which results were not re-run (repeat consistency, hand-model oracle). The side-finding section now points at the GP7 half, and the decision record flags its numbers as pre-fix. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
# Conflicts: # docs/decisions.log.md
PhysShell
marked this pull request as ready for review
September 17, 2026 02:09
Brings #201 (GPIF techniques), #202 (tuplet durations), #203 (corpus source binding) and #204 (Generator Observatory) into the optimality-gap branch. The only conflict was docs/decisions.log.md, where both sides appended entries. Resolved in date order: this branch's 2026-09-16 entry comes first, then main's 2026-09-17 entries. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…202) This branch now contains #202, so the audit's post-#198 tables no longer describe what the head produces. A new "Re-measured after #202" section and the decision-log entry give the numbers measured on this branch merged with main at e871a44, with the same corpus, protocol and weights. - Corpus: 9,045 → 8,966 lines; holdout 1,954 → 1,945. - Oracle: 1,831 holdout problems keep unchanged fingerprints and their verified CP-SAT records; the 114 changed or new ones were solved again. All 1,945 are proven, and the DP gap is 0 for both models. - Holdout agreement: lowest-fret 33.0%, v1 35.4% (ceiling 35.8%), v1-fit 44.2% (ceiling 55.4%), hand-fit 44.7%. No conclusion changes. The run reproduces the impact sweep recorded before the legato census, figure for figure. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
PhysShell
pushed a commit
that referenced
this pull request
Sep 17, 2026
…tie-break Brings in the optimality-gap branch, which now includes main at e871a44 (#201, #202, #203, #204) and its re-measurement after #202. The only conflict was docs/decisions.log.md, and every entry involved is dated 2026-09-17. main's entries come first and this branch's tie-break entry comes after them, so once #197 lands this branch's decision-log diff is a single append. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
PhysShell
pushed a commit
that referenced
this pull request
Sep 17, 2026
…ue-aware Brings in the tie-break branch, which now contains main at e871a44 (#201, #202, #203, #204) and the post-#202 re-measurements of #197 and #199. Merged without conflicts. The decision log ends with main's entries, then the tie-break entry, then this branch's tap-attribution entry. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
PhysShell
pushed a commit
that referenced
this pull request
Sep 17, 2026
…inuity Brings in the tap-attribution branch, which now contains main at e871a44 (#203, #204 are new here) and the post-#202 re-measurements of #197, #199 and #200. Those re-measurements reproduce this stage's "Baselines after #202" impact sweep figure for figure. The only conflict was docs/decisions.log.md. This branch has no decision-log entry of its own, so the file is taken from the tap-attribution branch. That version includes the amended #197, #199 and #200 entries. No stage-2 content changes. Co-Authored-By: Claude Opus 5 <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
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.
What
The Constraint Lab's optimization phase. The July spike answered does an admissible realization exist?; this adds the SLOTHY-style question what does the best admissible realization cost, and how far from it is Griff? — on monophonic fretboard fingering, measured against a CP-SAT optimum verified in-repo and against the tab authors of a 410-file Guitar Pro corpus.
Research tooling only:
lab/stays outside the workspace, no production code or dependency changes, OR-Tools lives in a local venv.Full write-up:
docs/audit/2026-09-fingering-optimality-gap.md(aggregates only — tab content never enters git,lab/out/is ignored).Correction (2026-09-17)
The corpus import behind these numbers gave nearly every GP7 note the wrong pitch — fixed in #198. Re-measured on the fixed importer (holdout songs): lowest-fret 33.5%, v1 35.8% (ceiling at optimum 36.2%), v1-fit 44.1% (ceiling 55.5%), hand-fit 44.3%; CP-SAT gap still 0 on 1,954/1,954 lines for v1 and v1-fit. Every conclusion below holds; the v1-fit flatness finding got stronger, absolute agreement rose 2–4 points, and the hand model no longer beats fitted v1 on agreement. Details in the audit's Correction section. The table below is pre-fix.
Re-measured after #202 (tuplet durations)
This branch now includes
mainate871a44, which brings in #201–#204, and was re-measured on that head with the same protocol and weights.No conclusion changes. See the audit's Re-measured after #202 section.
Built (red → green per commit)
lab/src/optir.rs— solver-neutral IR with an objective (hard tables; unary/pair cost tables, weighted|a−b|and[a≠b]). The external solver is untrusted: an optimum counts only when proven, admissible, exactly re-scored, bound = objective; agreement passes are recounted and pinned to the optimum.lab/src/fingering.rs— tablature lines from GP tracks (every refused note counted); an independent mirror of the productionv1objective, pinned againstinfer_positionsby brute force; a hand-position model (ADR-0019 §7's deferred finger-span layer) with an exact factored DP; repeat-consistency global constraint and a deterministic tie-break.lab/src/bin/fingering_gap.rs—fit(song-level holdout),export,report,repeat-export,repeat-report; every solver record is re-verified against problems rebuilt from the tabs.lab/cpsat/solve_opt.py— OR-Tools CP-SAT adapter with a lexicographic agreement pass and a two-tier (single-worker pool → multi-worker portfolio) escalation.Results (holdout songs unless noted)
Reading: the search is not the problem (zero gap); the objective is — v1 caps at 37% even with perfect tie-breaking, fitted weights are too flat, and a human-true global constraint does not import human preference. CP-SAT is a fine offline oracle but costs 4–5 orders of magnitude over the DP and is sensitive to modelling details (hidden hand position, lexicographic scaling), confirming the contract's "never in production" stance.
Side finding
Most
.gpx(GP6) guitar tracks import with string 1 = lowest string (strictly ascending tuning), against the glossary. Pitches stay consistent, so 9073de1 did not surface it. The Lab normalizes it (CutStats::mirrored_tracks); the importer fix is left for a separatecorechange.Hand-model oracle (holdout songs)
CP-SAT proved the optimum on 1,930 of 1,954 holdout lines for the fitted hand model;
solve_handmatches it on every one (gap 0, no invalid records). 24 lines stayed unproven after the 16-worker, 60 s escalation and carry no claim. ~1 h of solver time vs ~120 ms for the DP over the whole corpus.Checks
cd lab && cargo test— 29 fingering + 13 optir + 36 spike tests green;cargo fmt --checkclean; clippy clean at the crate's deny level (pedantictoo_many_lineswarnings only).exclude), as for the July spike.🤖 Generated with Claude Code