Skip to content

lab: optimization phase — fingering optimality gap (CP-SAT oracle vs production DP and human tabs) - #197

Open
PhysShell wants to merge 17 commits into
mainfrom
claude/lab-optimization-gap
Open

PhysShell wants to merge 17 commits into
mainfrom
claude/lab-optimization-gap

Conversation

@PhysShell

@PhysShell PhysShell commented Sep 16, 2026

Copy link
Copy Markdown
Owner

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 main at e871a44, which brings in #201#204, and was re-measured on that head with the same protocol and weights.

  • Corpus. 8,966 lines, of which 1,945 are holdout.
  • CP-SAT. 1,831 holdout problems kept their verified records (unchanged fingerprints); the other 114 were solved again. All 1,945 are proven, and the gap is 0 for v1 and v1-fit.
  • 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. 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 production v1 objective, pinned against infer_positions by 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.rsfit (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)

Production DP vs verified CP-SAT optimum gap 0 on 9,150 / 9,150 lines, both v1 weight sets; hand DP gap 0 on 1,930 proven holdout lines
Per-note agreement with tab author lowest-fret 31.8% · v1 34.0% · v1-fit 40.1% · hand-fit 40.6%
Human fingering optimal under the model v1 19.0% · hand-fit 35.4%
Agreement ceiling over all optimal fingerings (all lines) v1 37.2% (DP 36.7%) · v1-fit 52.3% (DP 42.4%)
Repeated 6-note figures fingered identically tab authors 98.2% · DP 82.2% · solver + constraint 100%
Agreement with repeat consistency enforced 41.3% → 40.2% (negative result)

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 separate core change.

Hand-model oracle (holdout songs)

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. ~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 --check clean; clippy clean at the crate's deny level (pedantic too_many_lines warnings only).
  • The lab crate is not built by CI (workspace exclude), as for the July spike.

🤖 Generated with Claude Code

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>
@coderabbitai

coderabbitai Bot commented Sep 16, 2026

Copy link
Copy Markdown

Important

  • 🔍 Trigger review

This repository does not receive automatic reviews because it has fewer than 10 stars.

⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Advanced

Run ID: fefd3082-5c48-4e80-9cdd-c69c03496c54


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.

❤️ Share

Comment @coderabbitai help to get the list of available commands.

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>
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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants