Qwen3.5-4B Active Counterexample Trace Selection

Finished2026-06-24imported · line ZActive Evidence Acquisition Evidence-Conditioned Selection Reliability and Safety Structured Execution and Compilers GitHub ↗

The one idea you need

A detective faces hundreds of suspects whose alibis all fit the few known facts. Rather than asking random questions, she asks the one question where their stories diverge most, collapsing the crowd to the single guilty one fastest.

The question

When a small model writes hundreds of programs that all match the examples you already have, how do you find the one that is actually correct?

What we found

Yes, but choose them well. Committing on the visible examples alone left about a quarter of picks secretly wrong, even though every one passed all the examples shown. Requesting six new test cases where the surviving programs disagreed most lifted correctness from 78% to 97%, and beat the same number of random tests at every budget.

Why it matters

When a model emits many candidate programs that all fit your examples, don't trust the fit. Actively probe inputs where the candidates disagree most; a handful of targeted checks catches silent bugs that random testing misses.

Correct picks: commit on shown examples, then add six well-chosen tests78% → 97%share of picks passing every hidden case

Six targeted test cases versus six random ones, same budget97% vs 91%correct picks at the six-case budget

Hardest batch: from committing blind to twelve targeted tests70% → 100%every pick correct after twelve targeted cases

The exact right program was always among the generated candidates100%so wrong picks were selection mistakes, not missing candidates

On this page

Results at a glance
Overview
Report
Experiment log
Figures
Data files
Reproduce
Related

Results at a glance 3

Smart extra test cases close the hidden-failure gap

How to read

Left to right, more extra test cases are requested; higher means more programs pass every hidden test (better). One line picks the most revealing test each time, one picks at random, and a top line marks the best any chooser could do.

Takeaway → The smart-test line rises well above the random line at every budget, so deliberately chosen tests weed out wrong programs far faster.

Data table

extra execution cases queried	active max-split	random extra cases	oracle elimination
0	77.5%	77.5%	77.5%
1	85.8%	82.1%	95%
2	88.3%	84.6%	96.7%
3	91.7%	87.5%	98.3%
6	96.7%	91.2%	98.3%
12	97.5%	96.2%	98.3%

Numbers from experiments/qwen35_4b_active_counterexample_trace_selection/reports/policy_summary.csv

Technical framing

Actively queried counterexamples close the hidden-failure gap (ceiling split) — Visible-only selection passes 77.5% hidden; actively chosen counterexamples reach 97.5% at +12 queries, beating random at every budget.

Six smart test cases beat random on all three batches

How to read

Each group of bars is one batch of problems; taller means more programs pass every hidden test (better). Within a group, bars run from committing with no extra tests, to six random tests, to six smart tests, to the best-possible chooser.

Takeaway → The six-smart-test bar nearly matches the best-possible bar and towers over the random bar on every batch.

Data table

eval split	visible only (0 queries)	random extra (+6)	active max-split (+6)	oracle elimination (+6)
ceiling	77.5%	91.2%	96.7%	98.3%
support	70%	91.2%	99.2%	100%
IID	76.7%	93.3%	98.3%	98.3%

Numbers from experiments/qwen35_4b_active_counterexample_trace_selection/reports/policy_summary.csv

Technical framing

Selection policy comparison at a 6-query budget, across splits — Six actively chosen cases recover most of the oracle's gain on all three splits; random queries at the same budget lag well behind.

On the hardest batch, smart tests reach every-program-correct

How to read

Takeaway → The smart-test line climbs to fully correct by twelve tests, matching the best-possible line, while random tests stall below it.

Data table

extra execution cases queried	active max-split	random extra cases	oracle elimination
0	70%	70%	70%
1	74.2%	74.6%	90.8%
2	83.3%	80%	97.5%
3	94.2%	83.8%	99.2%
6	99.2%	91.2%	100%
12	100%	95.8%	100%

Numbers from experiments/qwen35_4b_active_counterexample_trace_selection/reports/policy_summary.csv

Technical framing

Support split: active selection reaches 100% hidden full-pass at +12 queries — The hardest split for visible-only selection (70%) is fully solved by active querying at +12, matching the oracle upper bound.

In the author’s words from the Report · “Summary”

This standalone experiment tests whether a Qwen3.5-4B typed-sketch generator benefits from actively requested execution traces after candidate synthesis. The verifier first completes model-generated typed sketches into executable programs. Selection policies then choose whether to commit from the original visible trace or query additional cases from a held-out per-record pool. Best active ceiling result: 0.975 hidden full-pass rate at +12 queried cases.

Overview

Standalone experiment package for testing active execution-case acquisition after typed sketch synthesis.

The experiment trains a Qwen3.5-4B LoRA to emit typed DSL sketches, synthesizes executable candidate programs from those sketches, and compares selection policies that either commit from the original visible trace or request additional counterexample traces from a per-record query pool.

Large artifacts such as LoRA adapters and checkpoints are stored outside this directory under:

/workspace/large_artifacts/qwen35_4b_active_counterexample_trace_selection

Directory Layout

configs/: experiment configuration.
data/: generated JSONL datasets and manifests.
logs/: human-readable experiment log.
reports/: result JSON, figures, and final report.
run_logs/: command stdout/stderr captures.
scripts/: runnable experiment scripts.
src/: local DSL, data-generation, sketch, prompt, and modeling code.

Main Commands

python scripts/build_dataset.py
python scripts/train_adapter.py --task sketch --target-field target_sketch ...
python scripts/eval_active_selection.py --data data/eval/dsl_eval_ceiling.jsonl ...
python scripts/make_report.py

Report

Rendered from reports/qwen35_4b_active_counterexample_trace_selection_report.md

Summary

Best active ceiling result: 0.975 hidden full-pass rate at +12 queried cases.

Key Findings

Candidate coverage was not the bottleneck in this run: the exact target program was synthesized on every evaluated record across ceiling, support, and IID splits.
Visible-only selection left substantial hidden failures despite passing all observed cases: 77.5% ceiling, 70.0% support, and 76.7% IID hidden full-pass.
Active max-split counterexample selection closed most of that gap: ceiling reached 96.7% at +6 and 97.5% at +12; support reached 99.2% at +6 and 100% at +12; IID reached 98.3% at +6.
Active max-split consistently beat random extra cases at the same query budget, especially at low and medium budgets.
The remaining ceiling gap is a policy-selection gap, not a synthesis-coverage gap: candidate oracle was 100%, while oracle-elimination under the same capped query pool reached 98.3%.

Method

Each record provided six visible execution cases, eighteen hidden evaluation cases, and a deterministic active-query pool. Qwen3.5-4B generated typed sketches; the local verifier completed each sketch into executable DSL candidates; selection policies then chose programs after 0, 1, 2, 3, 6, or 12 additional queried execution cases.

Policy definitions:

visible_prior: commit using only the original visible cases.
random_extra: query random additional cases, averaged over two repeats.
active_max_split: greedily query the case that maximizes output-bucket entropy among currently viable candidates.
oracle_elimination: upper-bound policy that greedily chooses the case that eliminates the most currently viable wrong candidates using the case's true expected output.

Candidate Coverage

split	records	visible_selected_hidden_all_pct	candidate_oracle_hidden_all_pct	target_program_synthesized_pct	avg_synthesized_programs	avg_visible_consistent_candidates
ceiling	120	77.5	100	100	3235.56	643.6
iid	60	76.667	100	100	1108.07	59.883
support	120	70	100	100	3320.9	251.325

Candidate coverage

Policy Results

split	policy	budget	rows	hidden_all_pct	observed_all_pct	avg_hidden_passes	avg_queries_used
ceiling	active_max_split	0	120	77.5	100	17.2	0
ceiling	active_max_split	1	120	85.833	100	17.483	1
ceiling	active_max_split	2	120	88.333	100	17.625	2
ceiling	active_max_split	3	120	91.667	100	17.733	3
ceiling	active_max_split	6	120	96.667	100	17.908	6
ceiling	active_max_split	12	120	97.5	100	17.942	12
ceiling	oracle_elimination	0	120	77.5	100	17.2	0
ceiling	oracle_elimination	1	120	95	100	17.9	1
ceiling	oracle_elimination	2	120	96.667	100	17.958	2
ceiling	oracle_elimination	3	120	98.333	100	17.975	3
ceiling	oracle_elimination	6	120	98.333	100	17.975	6
ceiling	oracle_elimination	12	120	98.333	100	17.975	12
ceiling	random_extra	0	240	77.5	100	17.2	0
ceiling	random_extra	1	240	82.083	100	17.442	1
ceiling	random_extra	2	240	84.583	100	17.579	2
ceiling	random_extra	3	240	87.5	100	17.717	3
ceiling	random_extra	6	240	91.25	100	17.808	6
ceiling	random_extra	12	240	96.25	100	17.933	12
ceiling	visible_prior	0	120	77.5	100	17.2	0
iid	active_max_split	0	60	76.667	100	17.1	0
iid	active_max_split	1	60	86.667	100	17.483	1
iid	active_max_split	2	60	91.667	100	17.783	2
iid	active_max_split	3	60	96.667	100	17.917	3
iid	active_max_split	6	60	98.333	100	17.983	6
iid	active_max_split	12	60	98.333	100	17.983	12
iid	oracle_elimination	0	60	76.667	100	17.1	0
iid	oracle_elimination	1	60	95	100	17.75	1
iid	oracle_elimination	2	60	98.333	100	17.983	2
iid	oracle_elimination	3	60	98.333	100	17.983	3
iid	oracle_elimination	6	60	98.333	100	17.983	6
iid	oracle_elimination	12	60	98.333	100	17.983	12
iid	random_extra	0	120	76.667	100	17.1	0
iid	random_extra	1	120	83.333	100	17.508	1
iid	random_extra	2	120	86.667	100	17.642	2
iid	random_extra	3	120	90.833	100	17.792	3
iid	random_extra	6	120	93.333	100	17.883	6
iid	random_extra	12	120	95	100	17.925	12
iid	visible_prior	0	60	76.667	100	17.1	0
support	active_max_split	0	120	70	100	16.708	0
support	active_max_split	1	120	74.167	100	16.892	1
support	active_max_split	2	120	83.333	100	17.317	2
support	active_max_split	3	120	94.167	100	17.783	3
support	active_max_split	6	120	99.167	100	17.958	6
support	active_max_split	12	120	100	100	18	12
support	oracle_elimination	0	120	70	100	16.708	0
support	oracle_elimination	1	120	90.833	100	17.667	1
support	oracle_elimination	2	120	97.5	100	17.925	2
support	oracle_elimination	3	120	99.167	100	17.967	3
support	oracle_elimination	6	120	100	100	18	6
support	oracle_elimination	12	120	100	100	18	12
support	random_extra	0	240	70	100	16.708	0
support	random_extra	1	240	74.583	100	16.95	1
support	random_extra	2	240	80	100	17.179	2
support	random_extra	3	240	83.75	100	17.35	3
support	random_extra	6	240	91.25	100	17.696	6
support	random_extra	12	240	95.833	100	17.896	12
support	visible_prior	0	120	70	100	16.708	0

Ceiling success by budget

Support success by budget

IID success by budget

Split comparison budget 6

Split comparison budget 12

Ceiling active family heatmap

Interpretation

The primary question is whether extra traces close the gap between visible-trace selection and the candidate oracle. A large active improvement with a remaining oracle gap means the policy is useful but still leaves selection work. A small active improvement with a large oracle gap means the split heuristic is not finding the right discriminators. A small oracle gap means candidate synthesis is the current limiting factor.

Reproducibility

Dataset manifest: data/dataset_manifest.json
Config: configs/experiment.json
Eval JSON files: reports/eval/active_iid.json, reports/eval/active_support.json, reports/eval/active_ceiling.json
Policy summary CSV: reports/policy_summary.csv
Candidate summary CSV: reports/candidate_summary.csv
Large artifacts: /workspace/large_artifacts/qwen35_4b_active_counterexample_trace_selection

Experiment log 12

Show the running log (12 entries, 2026-06-24)

2026-06-24 02:26 UTC

Initialized a standalone active counterexample trace-selection experiment package.

Design commitments:

Use Qwen/Qwen3.5-4B.
Train a fresh local sketch LoRA for this experiment instead of depending on another run's adapter.
Keep checkpoints and adapters under /workspace/large_artifacts/qwen35_4b_active_counterexample_trace_selection.
Store each eval record with its own deterministic active-query case pool.
Compare original visible-trace selection against random extra cases, active max-split cases, and an oracle-elimination upper bound.

2026-06-24 02:34 UTC

Implemented:

scripts/build_dataset.py: dataset builder with per-record active query pools.
scripts/eval_active_selection.py: Qwen sketch generation, typed-sketch candidate synthesis, and active selection policies.
scripts/make_report.py: CSV summaries, plots, and final Markdown report generation.

Next check: syntax/import validation, then a target-sketch smoke run before model training.

2026-06-24 02:36 UTC

Dataset build iteration 1 failed before writing data:

TypeError: base_records() got an unexpected keyword argument 'case_pool_count'

Cause: the prior base-family record helper did not expose active query-pool generation.

Fix: patched local src/data_gen.py so base_records accepts case_pool_count and case_mode, passing both through to make_record.

2026-06-24 02:41 UTC

Target-sketch smoke iteration 1 was interrupted after ~74 seconds on record 1.

Cause: the evaluator called raw selection repeatedly, reparsing and reevaluating all programs against hidden cases for every policy snapshot.

Fixes:

Added ProgramBank to parse each candidate program once per record.
Cached program outputs by (program_index, case_key).
Replaced repeated raw selection with cached per-record selection.

2026-06-24 02:45 UTC

Target-sketch smoke iteration 2 still ran too slowly with a 384-case scoring pool.

Fix:

Added deterministic --max-query-pool-cases.
All policies now share the same capped per-record query pool.

2026-06-24 02:48 UTC

Target-sketch smoke iteration 3 completed:

Command: python scripts/eval_active_selection.py --data data/eval/dsl_eval_ceiling.jsonl --sketch-source target --output reports/eval/_smoke_target_ceiling10.json --max-records 10 --budgets 0,1,2,3,6 --random-repeats 2 --max-total-programs-per-record 4000 --max-policy-candidates 128 --max-query-pool-cases 48
Result: candidate oracle 10/10; visible-only selected 10/10.
Interpretation: smoke validates evaluator mechanics; it is not diagnostic because this first 10-record slice is already solved from visible traces.

Next step: train the experiment-local Qwen3.5-4B sketch LoRA.

2026-06-24 03:07 UTC

Sketch LoRA training completed successfully.

Command:

python scripts/train_adapter.py --train data/static_bridge_80/dsl_train.jsonl --eval data/eval/dsl_eval_iid.jsonl --task sketch --target-field target_sketch --prompt-mode trace --output-dir /workspace/large_artifacts/qwen35_4b_active_counterexample_trace_selection/models/sketch_lora --epochs 2.0 --lr 1.5e-4 --rank 32 --alpha 64 --dropout 0.05 --grad-accum 8 --save-steps 30 --eval-steps 30

Observed:

Trainable parameters: 42,467,328.
Step 30 eval loss: 0.0007196.
Step 60 eval loss: 0.0004834.
Train runtime: 959.9 seconds.
Final adapter/checkpoint tree size: 709M.
Large artifact location: /workspace/large_artifacts/qwen35_4b_active_counterexample_trace_selection/models/sketch_lora.

Next step: model-generated smoke eval on the ceiling split.

2026-06-24 03:12 UTC

Model-generated ceiling smoke completed.

Command:

python scripts/eval_active_selection.py --data data/eval/dsl_eval_ceiling.jsonl --adapter /workspace/large_artifacts/qwen35_4b_active_counterexample_trace_selection/models/sketch_lora --sketch-source model --output reports/eval/_smoke_model_ceiling10.json --max-records 10 --budgets 0,1,2,3,6 --random-repeats 2 --num-samples 3 --max-total-programs-per-record 4000 --max-policy-candidates 128 --max-query-pool-cases 48

Observed on the 10-record smoke slice:

Candidate oracle: 10/10.
Exact target synthesized: 10/10.
Visible-only hidden full-pass: 6/10.
Active max-split +1 query: 10/10.
Random +1 query: 15/20 over two repeats.

Interpretation: the full model-in-loop path is working, and the smoke directly exhibits the intended effect: active counterexample traces close a visible-selection ambiguity gap.

Next step: full ceiling eval with the same capped policy settings plus budget 12.

2026-06-24 03:51 UTC

Full ceiling eval completed.

Command:

python scripts/eval_active_selection.py --data data/eval/dsl_eval_ceiling.jsonl --adapter /workspace/large_artifacts/qwen35_4b_active_counterexample_trace_selection/models/sketch_lora --sketch-source model --output reports/eval/active_ceiling.json --budgets 0,1,2,3,6,12 --random-repeats 2 --num-samples 3 --max-total-programs-per-record 4000 --max-policy-candidates 128 --max-query-pool-cases 48

Primary results:

Candidate oracle: 120/120.
Exact target synthesized: 120/120.
Visible-only: 93/120 hidden full-pass.
Active max-split +1: 103/120.
Active max-split +3: 110/120.
Active max-split +6: 116/120.
Active max-split +12: 117/120.
Oracle elimination +12: 118/120.
Random +12: 231/240 over two repeats.

Interpretation: active counterexample traces substantially close the selection gap on the primary split; the remaining gap is selection-policy quality, not candidate coverage.

Next step: support and IID retention evals with the same settings.

2026-06-24 04:27 UTC

Full support eval completed.

Command:

python scripts/eval_active_selection.py --data data/eval/dsl_eval_support.jsonl --adapter /workspace/large_artifacts/qwen35_4b_active_counterexample_trace_selection/models/sketch_lora --sketch-source model --output reports/eval/active_support.json --budgets 0,1,2,3,6,12 --random-repeats 2 --num-samples 3 --max-total-programs-per-record 4000 --max-policy-candidates 128 --max-query-pool-cases 48

Results:

Candidate oracle: 120/120.
Exact target synthesized: 120/120.
Visible-only: 84/120.
Active max-split +1: 89/120.
Active max-split +3: 113/120.
Active max-split +6: 119/120.
Active max-split +12: 120/120.
Oracle elimination +6/+12: 120/120.
Random +12: 230/240 over two repeats.

Interpretation: active selection is not only a ceiling-split effect; it also closes nearly all support-selection ambiguity under the same policy.

Next step: IID retention eval.

2026-06-24 04:38 UTC

Full IID eval completed.

Command:

python scripts/eval_active_selection.py --data data/eval/dsl_eval_iid.jsonl --adapter /workspace/large_artifacts/qwen35_4b_active_counterexample_trace_selection/models/sketch_lora --sketch-source model --output reports/eval/active_iid.json --budgets 0,1,2,3,6,12 --random-repeats 2 --num-samples 3 --max-total-programs-per-record 4000 --max-policy-candidates 128 --max-query-pool-cases 48

Results:

Candidate oracle: 60/60.
Exact target synthesized: 60/60.
Visible-only: 46/60.
Active max-split +1: 52/60.
Active max-split +3: 58/60.
Active max-split +6: 59/60.
Active max-split +12: 59/60.
Oracle elimination +2/+3/+6/+12: 59/60.
Random +12: 114/120 over two repeats.

Interpretation: the same active-query selection mechanism improves IID retention too; one record remains unresolved even under the oracle-elimination policy within the capped candidate/pool policy settings.

Next step: generate report, plots, and CSV summaries.