[TS PBT] Compare two-phase evidence-guided USVM with equal-budget controls #357

Scope agreed on 2026-10-16

One concrete PBT generation phase is followed by one USVM search phase. No return to random generation is required. Concrete replay and optional shrinking validate a USVM candidate; they are not a second PBT generation phase. This replaces the previous repeated-round acceptance.

Required comparisons

Start with PBT_ONLY, SYMBOLIC_ONLY, SEQUENTIAL (no PBT guidance), and the two-phase COVERAGE_FEEDBACK mode. When one-time relation guidance is implemented, add RELATION_FEEDBACK and COMBINED_FEEDBACK on their explicit supported subset.

Protocol

• Use the same original property, declared support, class/scenario universe and total budget. Fix the PBT/USVM allocation before looking at outcomes.
• Include observation collection, optional inference, mapping, startup/frontend work, symbolic search, native replay and shrinking in accountable elapsed cost. Preserve overruns and exclude late coverage from the primary result.
• Measure original-oracle-confirmed faults/time to confirmation and checked executable statement coverage per class. Report passing hypothesis refutations separately.
• Predeclare seeds/repetitions and state which component they randomize; do not label fixed symbolic repeats independent randomized seeds. Keep real programs, artificial rare-branch examples, validated mutants, correct controls and unsupported outcomes separate.
• If claiming observation value beyond coverage, compare one-time relation guidance with coverage-only and observation-independent templates using the same bounded vocabulary and budget. No no-return-loop ablation is needed because return-to-PBT generation is outside scope.
• Preserve regressions, zero-gain cases, timeouts, solver UNKNOWN and failures. Do not select cases from the winning mode or treat an unsupported class as a symbolic miss.

Acceptance

One command runs the frozen comparison and another regenerates tables from raw evidence. Claims distinguish implementation functionality from measured benefit. The existing 24-cell, one-seed large-class rerun remains a diagnostic pilot: it shows faster coverage processing and no 120-second coverage advantage, not a completed held-out study. #400-#403 and #481 are not prerequisites.

Delivery status (2026-10-17)

All predeclared measurements on frozen local assembly c447392006cb72b06ead3d857b639a23d7e259c9 are complete: 108 scalar cells, 18 independent attribution diagnostics, and 144 real/artificial class cells. No further experiments, tuning, replacements or new families were run after these results.

Scalar mechanism: all 108 cells eligible

One artificial family has six correct/mutant/no-benefit variants, three configured fast-check seeds and six treatments under the same 60-second total outer deadline. JVM startup, retained DSL compilation, collection, relation work and native confirmation are charged; a one-second serialization reserve is explicit. The original machine cap is 60 seconds and the runner uses remaining time. No watchdog kill, late artifact, nonzero exit or unexpected correct-control fault occurred. Raw runtime/source hashes stayed frozen.

At mutant input 417, original named check receipt is false and result is 415; the captured bound is true. The correct variant refutes the inferred equality while its complete original oracle holds. These scalar cells do not export all search inputs and do not measure complete checked class coverage. Wall times are time until a completed receipt, not first-hit/first-confirmation times. Three fast-check seeds do not make pure symbolic runs independent randomized repetitions: those repeat the same fixed BFS/randomSeed=0 machine.

Attribution: no demonstrated additional observation contribution

All 18 predeclared prefix-only diagnostics are eligible, with complete capture, zero late/phase-error/omitted-input outcomes and 36 checked full-original native records (30 HOLDS, six FALSE). Prefix/native-oracle execution reaches the same rare input 417 and both mutants in all three seeds without the learned equality. Therefore the scalar contrast does not establish incremental value from PBT-learned observations over observation-independent prefix/native candidate generation.

The prefix diagnostic uses a different 15-second-query/remaining-native-replay allocation under 60 seconds. It is not a seventh fair treatment, an official USVM WitnessConfirmation, or a native class coverage result. It refutes the claimed attribution for this example; it does not supply a fair speedup estimate.

Checked class coverage: 144 cells, 89 full eligible

Twelve profiles over five genuine classes and two artificial families use three seeds and four controls, 30-second total budgets, eight seconds for native class replay, a 1,000,000-run ceiling independent of capture limits, and source-qualified original class AST universes. Five real plus four artificial control/mutant bodies yield nine class groups. AST identifiers are unioned once per original class; profile denominators are not summed.

Strict four-mode pairing yields 14 of 27 class-by-seed rows, all with zero statement gain over PBT:

SinglyLinkedList, DoublyLinkedList, CircularQueue and RingBuffer control have no complete four-mode paired seed. Their missing/incomplete results are not zero-gain evidence. Both artificial mutants are found by all four controls in each paired seed. The genuine SinglyLinkedList defect was already found during native corpus validation; eligible PBT/hybrid cells reproduce it while standalone symbolic is incomplete.

All 213,094 saved native replay records verify successfully; zero native mismatches were observed. This count includes preserved partial cells and is not a count of independent tests/programs or a claim that every cell is complete.

Observed failure counts overlap: 47 external runner deadline kills, 45 missing-completed-artifact diagnostics, one recorded unterminated campaign JSON, eight saved campaigns with 94--251 unchecked symbolic inputs (one also killed), and one recorded Operation-not-permitted error. Thus 55 cells are ineligible. No cell exceeds the total accounted budget. #354/#612/#613 separate command deadline/publication work from these observations; empty stdout does not prove the cause of other killed cells.

The class metric counts admitted search inputs, not every execution: it excludes precondition execution/rejection, shrink/reduction trials, diagnostic calls and wrapper/foreign/model statements. All their costs still count. #611 credits only timely exact official original replay receipts and retains the original candidate, not reduction inputs.

The frozen manifests, raw artifacts, checked scalar/prefix summaries and class-ast-unions.json regenerate the reported result. Superseded 3-cell v1 and 12-cell v3 development protocols remain intact and excluded. This is a negative/limited development assessment, not a held-out study or evidence of real-program coverage superiority.