Agent-ProSAT for CoT via verifiable programmatic solver coding for CoT synthesis - Feedback Appreciated!

ShehabAnwer · July 19, 2026, 11:40am

Dear Hugging Face Community & Developers

I’ve recently open-sourced Agent-Prosat, heavily inspired by Karpathy’s autoresearch, this pipeline tackles the bottleneck of manually curating quality Chain-of-Thought (CoT) datasets or the costs of model-driven forms by redirecting AI from CoT generation (liable to hallucination or model architecture or capabilities), into coding of solver thar can be improved by iteration or through human-in-the-loop, to programmatic review of the underlying code, and better control token utilisation in SFT/RL pipelines.

Agent-ProSAT utilizes programmatic, self-correcting loops with programmatic harness that provide guardrails while the agent codes the solvers, then assess it, against gound truth and against held-out sample (with blinded/unblinded programmatic script that the agent is prohibited from tampering) to eventually edit prosat.py that solves the various puzzle types to incorporate into generation of the CoT reasoning traces.

I’ve been benchmarking this on the “Alice in Wonderland” (AIW) logic puzzles from NVIDIA’s Nemotron Reasoning Challenge to stress-test how the loops handle edge-case spatial and logical constraints. Output dataset has been released on Hugging Face:

The Features are:

Programmatic Data Synthesis: Autonomous generation of multi-step CoT traces.
Validation Loops: Built-in, self-correcting reflection to validate logical soundness.
Agentic Curation: Karpathy’s autoresearch-style iterative workflows directly into data formatting.

I would love to collaborate with others working on synthetic data and agentic workflows. Specifically:

CoT Schemas: What structural formats are you finding most effective when prepping synthetic reasoning traces for downstream fine-tuning?
Validation Overhead: How are you balancing token-efficiency and accuracy during automated self-reflection steps?

More Info, codebase, case-study on Nemotron Reasoning/AIW and the ProSAT CoT dataset are available under:

GitHub Repository: GitHub - The-Adimension/Agent-ProSAT: Agent-driven Programmatic Solver Traces for Alice in Wonderland puzzles! · GitHub
Kaggle Notebook: Nemotron ATLAS | Kaggle (SFT on AIW ProSAT CoT)
Framework behind the work: doi: /10.1093/ehjimp/qyaf038

If you are experimenting with programmatic reasoning data or iterative agentic loops, I’d love to hear from you, and most importantly to validate and review the work I share with the community!

Best,
Shehab Anwer, MD
Cardiologist, Data Engineering & AI enthusiast.

John6666 · July 20, 2026, 11:30pm

For now, after looking into this briefly from the angle of making the pipeline more verifiable at lower cost, my rough take is:

The part I find most interesting here is the shift from paying a model to generate every rationale individually toward using the model to improve a reusable solver whose outputs can be inspected, replayed, and rendered into different training formats.

My direct answer

For the CoT schema, my default would be:

Keep structured solver events as the canonical audit record, then derive compact natural-language traces as replaceable training views.

For validation overhead, I would use:

Cheap deterministic checks for every sample, with stronger replay, model review, or human review only for cases that cannot be decided cheaply.

In practice, I would separate four things that are easy to conflate:

Layer	Purpose
Solver execution	What the program actually computed
Verification evidence	Why the result was accepted, rejected, or deferred
Natural-language rendering	How the computation is explained to a reader or student model
Training target	What the particular student is asked to imitate

This means the natural-language rationale does not have to carry the entire burden of reproducibility. It becomes one view over a more durable machine-readable record.

This pattern has close precedents in adjacent settings. Code Execution as Grounded Supervision extracts deterministic execution traces and turns them into natural-language supervision. Think Like You Execute goes a step further by checking the rendered rationale against the original trace. These are code-execution tasks rather than AIW hidden-rule puzzles, so I would treat them as useful design precedents, not proof that one schema is already optimal here.

A default route I would test

problem
  ↓
parse and classify
  ↓
infer one or more candidate rules
  ↓
execute the selected rule
  ↓
record structured events / witnesses
  ↓
run deterministic checks
  ↓
accept / reject / defer
  ↓
render a compact natural-language trace
  ↓
check the rendering against the events
  ↓
export:
  - audit record
  - selected training view

The audit record answers:

What happened, what evidence supports it, and what was checked?

The training view answers:

What should this particular student model imitate?

That distinction matters because an auditably correct trace can still be a poor training target: it may be too long, too compressed, too implementation-specific, or simply mismatched to the student model.

I would first run a small evidence-integrity audit

Before choosing a final CoT format or starting another large training run, a small stratified audit across the puzzle families could separate several possible bottlenecks.

For each sampled item:

recompute the final answer from the stored events;
distinguish exact agreement from case-insensitive or numeric-tolerance agreement;
check that the rendered or boxed answer matches the computed answer;
map every stated intermediate value to an execution event;
detect whether several candidate rules fit the demonstrations;
apply one or two semantics-preserving transformations, such as renaming symbols or reordering examples;
introduce a few known solver or verifier defects and check whether the harness catches them.

This separates:

Question	Possible bottleneck
Can the rule be represented?	Solver search space
Is the rule identifiable from the examples?	Rule ambiguity
Can the calculation be replayed?	Execution validity
Does the prose match the calculation?	Renderer fidelity
Does the harness reject representative defects?	Verifier quality
Does the representation improve generation?	Student utility

I would avoid reducing all of these to one verified = true field.

The smallest schema ablation that seems informative

I would compare at least these four conditions:

Arm	Training target
A	Answer only
B	One short canonical rationale
C	Verified structured events plus a short rendered rationale
D	The current longer or multiply paraphrased rationale

The answer-only condition is important. Without it, an improvement might come from adding more correct problem–answer pairs rather than from the reasoning representation itself.

I would evaluate each condition on three axes.

Fidelity

event replay success;
intermediate-value consistency;
rendered-answer versus computed-answer agreement;
proportion of claims grounded in stored events.

Student utility

generated final-answer exact match;
answer-parser success;
puzzle-family accuracy;
performance on an unseen seed, template, rule, or rule composition.

Cost

training tokens;
generated tokens;
verifier runtime;
escalation rate;
accepted traces per unit of compute;
downstream gain per training token.

Where practical, both sample-matched and token-matched comparisons would help. Otherwise, a longer condition may partly win because it supplies more supervised tokens.

The NVIDIA Nemotron challenge postmortem reaches a broadly compatible practical conclusion: solver-generated traces, intermediate auditing, compact representations, and evaluation by task and failure type were more useful than simply accumulating unfiltered reasoning text.

A reproducibility note

Before interpreting an ablation, I would pin the exact generation and training lineage in one small manifest:

generator_commit:
input_dataset_revision:
input_digest:
generation_command:
generation_config_digest:
seed:
renderer_version:
verifier_version:
output_digest:
split_script_commit:
training_notebook_commit:
base_model_revision:
adapter_revision:
evaluation_harness_commit:

This is less about formal documentation than debugging. Code, generated datasets, notebooks, adapters, and evaluation scripts can otherwise evolve independently.

The dataset already separates target, computed answer, and reasoning fields. I would extend that separation by recording exact, case-insensitive, tolerance-based, boxed-answer, replay, and renderer-consistency results independently.

Short takeaway

My default path would therefore be:

keep structured execution evidence as the canonical audit record;
generate natural-language rationales as replaceable training views;
run cheap deterministic checks on every sample;
defer ambiguous cases to stronger verification;
audit a small stratified sample before another large run;
compare answer-only, short, structured, and long-trace conditions;
evaluate generated answers on grouped holdouts;
pin the complete generator-to-evaluation lineage.

This would make both of your questions empirical:

Which representation actually helps this student model?
Which verification layers provide enough value to justify their cost?

Suggested audit schema and lower-cost verification cascade

Suggested audit schema

A possible internal record could look like this:

{
  "problem_id": "example-id",
  "puzzle_type": "binary",
  "source": {
    "dataset_revision": "revision",
    "generator_commit": "commit",
    "config_digest": "digest"
  },
  "parsed_problem": {
    "demonstrations": [],
    "query": {}
  },
  "rule_search": {
    "candidate_rules": [],
    "selected_rule": {},
    "selection_criterion": "criterion",
    "is_unique_on_demonstrations": false
  },
  "execution": {
    "events": [],
    "witnesses": [],
    "computed_answer": "answer"
  },
  "verification": {
    "parse_valid": true,
    "execution_valid": true,
    "target_exact": true,
    "target_casefold_equal": true,
    "target_numeric_tolerance_valid": true,
    "boxed_equals_computed": true,
    "renderer_event_consistent": true,
    "metamorphic_checks": []
  },
  "rendering": {
    "renderer_version": "version",
    "style": "short-canonical",
    "reasoning": "rendered explanation",
    "boxed_answer": "answer"
  }
}

Different training views can then be generated without changing the audit record:

View A: prompt → answer

View B: prompt → short rule summary → answer

View C: prompt → canonical event serialization → answer

View D: prompt → full rendered explanation → answer

The relevant question becomes:

Which view transfers the desired behavior to the target model most efficiently?

rather than:

What is the universally correct CoT schema?

The answer may depend on the base model, tokenizer, context length, loss mask, and puzzle family.

A verification cascade

Can the final answer be checked deterministically?
├── Yes
│   └── Check every sample.
└── No
    └── Use a bounded external check or mark it unresolved.

Are machine-readable intermediate events available?
├── Yes
│   ├── Replay the events.
│   ├── Check puzzle-family invariants.
│   └── Compare the replayed answer with the exported answer.
└── No
    └── Do not label the prose as fully process-verified.

Does exactly one supported rule fit the demonstrations?
├── Yes
│   └── Continue.
└── No
    ├── test another instance from the same candidate rule,
    ├── apply an equivalent transformation,
    └── or mark the item as ambiguous.

Did parsing, execution, replay, invariant checking, or rendering fail?
├── Yes
│   ├── reject if the contradiction is decisive;
│   └── otherwise defer to a stronger verifier.
└── No
    └── accept without expensive reflection.

The output can be three-way:

accept: cheap checks provide enough evidence;
reject: a decisive contradiction was found;
defer: the cheap verifier cannot determine validity reliably.

That avoids forcing every uncertain sample into a false binary decision.

Checks that can usually remain cheap

schema validation;
parsing;
execution success;
exact output comparison;
numeric comparison under an explicitly recorded tolerance;
type and range checks;
event replay;
puzzle-family invariants;
boxed-answer consistency;
duplicate detection;
token-length checks.

Conditions that may justify escalation

several rules fit the same demonstrations;
parsers disagree;
independent solvers disagree;
a semantics-preserving transformation changes the result;
the prose contains a claim with no corresponding event;
a repair changes an already correct answer;
the problem is outside the implemented rule family.

The HF Forum thread When should LLMs verify instead of think longer? considers a related inference-time routing problem. It is not the same pipeline, but it illustrates why verification may be better treated as a selective resource rather than an unconditional stage.

I would also avoid assuming that full process verification must always outperform outcome verification. Do We Need to Verify Step by Step? provides a theoretical counterpoint. For this project, the practical implication is to measure the marginal value of each verification layer rather than presuming it.

Evaluation controls, grouped splits, and failure handling

Different controls test different failure modes

Answer blinding is valuable, but it addresses a specific question:

Did the solver obtain its result from the supplied target-answer input?

It does not by itself test whether the inferred rule generalizes.

I would separate several controls:

Control	Main failure mode tested
Answer blinding	Direct use of the supplied target
Fresh-seed evaluation	Memorization of fixed instances
Template holdout	Dependence on surface phrasing
Rule-family holdout	Failure to generalize to unseen rules
Composition holdout	Failure on new combinations of known components
Metamorphic tests	Dependence on irrelevant representation details
Mutation tests	Weaknesses in the evaluator itself

Passing one does not imply passing the others.

Procedural holdouts

Useful possibilities include:

new random seed;
new surface template;
longer or more difficult input;
unseen rule;
unseen combination of known rule components.

Reasoning Gym is a useful reference for procedural reasoning tasks with seeds, adjustable complexity, metadata, and algorithmic scorers. It is not a drop-in replacement for AIW, but its separation of generator, metadata, and scorer is relevant.

Metamorphic checks

Apply a transformation that should preserve the underlying semantics:

rename symbols consistently;
reorder demonstrations;
change formatting without changing values;
permute irrelevant labels;
replace the query with another input governed by the same rule;
generate another example from the selected rule.

Then check whether the output changes in the expected way.

These test a different failure mode from answer blinding.

Evaluator stress tests

Introduce small known defects and confirm that the harness rejects them:

reverse a shift direction;
alter a rounding rule;
ignore one demonstration;
swap two mapping entries;
widen a numeric tolerance;
modify one intermediate value in the prose;
make the boxed answer differ from the computed answer.

This is similar in spirit to mutation testing: instead of only asking how many original cases pass, ask whether the evaluation harness detects representative wrong implementations.

Property-based testing tools such as Hypothesis can help generate edge cases and shrink failures into smaller counterexamples.

Split before augmentation

I would create train, validation, and test groups before paraphrasing or oversampling:

assign original problems to groups
  ↓
freeze the groups
  ↓
generate paraphrases and oversampled copies only inside train
  ↓
deduplicate validation and test

Possible grouping keys include:

original problem ID;
generator seed;
selected rule;
rule family;
template family;
canonicalized prompt;
normalized demonstration set.

A row-level random split can otherwise put alternate renderings or copies of the same underlying problem on both sides.

At minimum, I would distinguish:

Evaluation	Interpretation
Same rule, new instance	Basic interpolation
Same rule, new template	Surface robustness
Known components, new composition	Compositional generalization
New rule family	Rule induction beyond training support
Longer or harder instance	Difficulty extrapolation
Metamorphic variant	Invariance to irrelevant changes

Keep failures and ambiguous examples in the audit corpus

Even when they are excluded from ordinary positive SFT, failed or unresolved samples can remain useful.

A simple status taxonomy might be:

accepted
rejected_parse_failure
rejected_execution_failure
rejected_wrong_answer
rejected_renderer_mismatch
rejected_invariant_failure
deferred_multiple_rules
deferred_solver_disagreement
deferred_unsupported_rule
deferred_timeout

This allows:

failures to become regression fixtures;
unsupported rules to guide the next solver iteration;
ambiguous cases to remain distinct from incorrect ones;
renderer bugs to be repaired without repeating successful solver work;
per-family bottlenecks to remain visible.

I would not automatically mix failed reasoning into the same completion-SFT objective as valid reasoning.

Negative traces may be useful for verifier training, preference data, contrastive learning, error localization, or repair tasks, but those are separate experiments.

Reproducibility, training checks, and related references

A compact reporting template

A comparison table such as this would make the schema experiment easier to interpret:

Condition	Train examples	Train tokens	Exact accuracy	Parse success	Event replay	Mean output tokens	Verification cost
Answer only					N/A
Short canonical
Structured events
Long rendered traces

A per-family table would also help:

Puzzle family	Solver coverage	Accepted traces	Student exact accuracy	Main failure type
Numeral
Unit conversion
Gravity
Cipher
Binary
Equation transform

And verification results could remain layered:

Gate	Pass	Fail	Defer
Parsing
Execution
Exact target comparison
Numeric-tolerance comparison
Boxed/computed agreement
Event replay
Renderer fidelity
Metamorphic checks

This prevents one aggregate “verified” count from hiding where samples were accepted, lost, or deferred.

Optional training-pipeline checks

These are secondary to the data and evaluation questions, but they can prevent pipeline behavior from being mistaken for a schema result.

Inspect the actual loss mask

For a small batch, inspect:

input tokens;
labels;
tokens whose label is -100;
prompt/completion boundary;
final-answer tokens;
truncation point.

This confirms which parts of the trace are actually supervised.

The current TRL SFT Trainer documentation distinguishes language-modeling, prompt–completion, and conversational datasets, and its loss masking and truncation behavior depend on the selected format and template.

Evaluate from raw generation

Store an evaluation record such as:

{
  "problem_id": "id",
  "puzzle_type": "type",
  "raw_generation": "text",
  "parsed_answer": "answer",
  "target_answer": "target",
  "exact_match": true,
  "tolerance_match": true,
  "format_valid": true,
  "output_tokens": 123,
  "failure_reason": null
}

This keeps answer-extraction failures distinct from reasoning failures.

Teacher-forced validation loss remains useful for optimization, but it does not directly measure whether the model independently generates a correct, parsable answer.

Audit the adapter path when comparing LoRA configurations

Log:

matched target modules or parameters;
trainable parameter count;
gradient norms;
adapter-weight changes after one optimizer step;
adapter revision loaded during evaluation.

This confirms what was actually trained before attributing a result to a particular module-selection strategy.

Documentation

Hugging Face provides natural places for this metadata:

The manifest does not need to be elaborate; even a small checked-in YAML or JSON file can close most of the lineage gap.

Related work and reusable components

The references I found most useful for this design question are:

Execution-grounded supervision

Code Execution as Grounded Supervision for LLM Reasoning
Deterministic execution traces converted into natural-language reasoning supervision.
Think Like You Execute: Verifiable Chain of Thought from Program Traces
Instrumentation, trace narration, and verification of the resulting rationale.
NExT: Teaching Large Language Models to Reason about Code Execution
Execution-aware data derived from program state.

Procedural and verifiable environments

Reasoning Gym
Procedural generation with seeds, adjustable complexity, metadata, and algorithmic scoring.
NVIDIA’s Nemotron challenge postmortem
Practical lessons from the same competition around solver-generated data, compact traces, verification, and failure-oriented evaluation.

Process versus outcome verification

Do We Need to Verify Step by Step?
A useful reason not to assume that denser process verification is universally superior.

Practical testing and training

None of these is an exact match for Agent-ProSAT. Together, however, they support a useful working pattern:

programmatic generation
→ machine-readable execution evidence
→ layered verification
→ replaceable training views
→ grouped evaluation
→ measured cost/utility trade-off

Overall, I think the promising part of Agent-ProSAT is not only that it can produce natural-language CoT at lower marginal cost. It is that the solver-development loop can potentially produce a reusable, executable evidence layer from which several supervision formats can be generated and compared.

Keeping that evidence layer separate from the prose would make it easier to improve the solver, change the renderer, audit failures, and answer the schema and validation-cost questions without committing the whole pipeline to one style of CoT.

ShehabAnwer · July 22, 2026, 6:35pm

Dear @John6666

I am incredibly grateful to you for taking the time to write out such a detailed, rigorous breakdown. This is exactly the feedback I was hoping for when releasing Agent-ProSAT and the ProSAT dataset.

I genuinely appreciate you diving into the architecture. You’ve essentially provided a blueprint for the next steps and answered questions I was actively wondering how to approach. THANK YOU!

I want to confirm I understand correctly: your core thesis is to decouple the canonical audit record (what is computed) from the training view (how it is explained) as the agent works on prosat.py, right? Given that Agent-ProSAT represents an iterative autoresearch loop where the LLM writes and refines the solver code based on harness feedback, I realize I was making the agent’s job unnecessarily hard. By being obsessed with rigorous determinism, I was forcing it to simultaneously figure out the logic and bake in the natural language formatting.

Here my summary and plan of action through the lens of your comments:

Updating Agent Directives: I will instruct the agent to generate code that strictly outputs a structured ExecutionWitness (JSON events). A separate, non-agentic renderer will handle the Views (A, B, C, D).
Upgrading the Assessment Loop: I’ll implement your 3-way verification cascade (Accept / Reject / Defer) in the evaluation harness to save token overhead and avoid forcing binary decisions on ambiguous cases.
Four-Arm Schema Ablation: Once the agent generates the JSON-emitting solvers, I’ll run the empirical ablation on the four views and track the generator-to-evaluation lineage in a manifest.

Two quick questions for you on the verification cascade:

When you hit a “Defer” case (e.g., multiple rules fit the demonstrations), do you route that to a stronger LLM dynamically during the run, or queue them up for an offline/human review batch?
Do you think a harness like my earlier work (autoresearch-MIL: GitHub - habanwer/autoresearch-MIL: AI agents running research on single-GPU nanochat training automatically · GitHub ) would improve the aforementioned roadmap?

Thanks again for the fantastic insights and pointing me toward the Code Execution as Grounded Supervision and Think Like You Execute precedents. I’m going to start building out the JSON audit schema and the 3-way verification cascade around the next week.

I’ll update the thread once the first ablation results are in!

Best,

Shehab

John6666 · July 23, 2026, 3:20am

Hmm. For now, based on the limited checks I was able to run on my side, I think it looks something like this:

Short answer

Yes, your summary of the separation is what I had in mind:

the structured ExecutionWitness is the canonical audit record;
the renderer is a separate, non-agentic component;
the training view is derived from the witness rather than being authored inside the solver;
and Accept / Reject / Defer applies to the evidence available for each layer, rather than forcing one binary verdict for the whole sample.

For the two questions:

For dataset construction, my default would be a reason-coded, offline-first hybrid rather than sending every Defer case directly to a stronger LLM or every case to humans.
I do think the autoresearch-MIL harness contains useful patterns, but I would borrow its ownership, logging, memory, and audit controls rather than replacing Agent-ProSAT’s existing inner research loop.

The key distinction for me is:

A stronger model is most useful when it can produce a new artifact that can be checked independently—not merely when it can express a stronger preference between rules that remain equally consistent with the same evidence.

So I would use the stronger LLM for bounded repair, candidate generation, structured conversion, or proposing a discriminating test. I would not treat “the stronger model chose rule B” as verification by itself.

My default routing policy

A practical initial policy could be:

Observed state	Default route
Parse or formatting failure	Deterministic repair first, then bounded LLM repair
No candidate, but the family is already supported	Generate additional candidates, then replay all demonstrations deterministically
No candidate because an operator or family is unsupported	Solver/schema development queue
Multiple candidates, but all predict the same target answer	The answer may be usable; keep the witness/rule ambiguous
Multiple candidates with different target answers	Generate a distinguishing query or keep the case offline
A distinguishing query exists and a reliable answer source exists	Ask the generator, oracle, or a human reviewer
A distinguishing query exists but no reliable answer source exists	Keep the candidate set unresolved and replayable
Timeout or resource failure	Bounded retry, then offline queue
Witness and renderer disagree	Deterministic rerender; reject the rendered view if it still disagrees
Dataset target, computed answer, and witness replay disagree	Audit queue rather than automatic promotion

In other words:

deterministic checks
→ classify why the item was deferred
→ choose the cheapest route that can add checkable information
→ replay deterministically
→ accept only the layer actually supported by that evidence

This is close in spirit to learning to defer, where the useful question is not only whether the first system is uncertain, but whether the downstream expert is actually likely to handle that kind of case better.

First separate what is being accepted

I would probably avoid giving the entire sample one status. There are at least four separable objects:

answer_status
witness_status
renderer_status
training_view_status

For example:

answer_status        = accepted
witness_status       = ambiguous
renderer_status      = not_applicable
training_view_status = answer_only

This matters because multiple rules may fit the demonstrations while still producing the same answer for the current target.

In that situation, the answer can be stable within the current candidate space even though the inferred rule is not unique. That does not prove that the answer is correct under every plausible latent rule, but it is a materially different state from a case where the candidates also disagree on the target answer.

Likewise:

a correct final answer does not automatically validate the witness;
a valid witness does not automatically validate every rendered explanation;
and a faithful rendered explanation is not automatically safe as a training view if it was conditioned on the target answer.

So I would make the cascade operate at those boundaries rather than treating Accept as one undifferentiated label.

Minimal decision record

Before choosing or learning a router, I would record something approximately like:

{
  "answer_status": "accepted|rejected|deferred",
  "witness_status": "accepted|rejected|ambiguous|unsupported",
  "renderer_status": "accepted|rejected|not_run",
  "training_view_status": "full|answer_only|excluded",
  "decision": "accept|reject|defer",
  "defer_reason": "multiple_candidates_different_answers",
  "candidate_count": 4,
  "target_output_count": 2,
  "escalation_target": "offline_oracle_queue",
  "resolution_evidence": null
}

I would also retain, when available:

candidate_rule_ids
candidate_set_hash
hypothesis_space_version
target_output_set
failed_invariant
unsupported_operator_set
distinguishing_input
oracle_available
dataset_revision
source_row_id
solver_commit
witness_schema_version
renderer_version
verifier_version
escalation_model_version
escalation_prompt_version
parent_run_id

One field that may be especially useful is the difference between:

resolved_with_new_verifiable_evidence
resolved_by_unverified_preference

Those should not be counted as the same kind of “resolved.”

A small pinned probe

I ran two small CPU-only probes against the public binary/equation-transform data and the public solver snapshot at commit 84c548c. I would treat these only as instrumentation signals about that finite hypothesis space—not as a claim that every ambiguous item has the same underlying cause.

The two observations that changed my view most were:

Multiple demonstration-consistent candidates were common in the current compact candidate space.
A target answer could be correct even when the selected proxy transformation disagreed with the trace’s claimed transformation on other inputs.

That makes me lean toward inspecting and recording the candidate set before routing the case.

It also makes me think target-answer correctness and witness validity should be separate promotion conditions.

Probe setup, results, and limitations

Candidate-ambiguity probe

For the current binary and positional equation-transform candidate spaces, I enumerated the candidates that matched all available demonstrations instead of stopping at the first match.

The public solve_binary implementation currently selects the first per-bit function that matches all demonstrations and then breaks; the positional equation-transform path similarly selects the first matching input position. That behavior can be seen in the pinned prosat.py.

The probe covered:

Measurement	Binary	Equation transform
Rows examined	1,557	709
Representable in the tested candidate space	1,255	153
Multiple candidates among representable rows	1,233	37
Multiple candidates, same target output	204	3
Multiple candidates, different target outputs	1,029	34
First-versus-reversed-order output changed	877	34
Current first match gave the target answer	806	104
Ground-truth answer existed in candidate-output set	1,191	136

The “first versus reversed order” result is only a simple order-sensitivity proxy, not an exhaustive study of all candidate orderings.

A particularly relevant result was that, for binary rows where the first candidate was wrong, the correct target answer was often still produced by another demonstration-consistent candidate. For the ambiguous positional equation-transform rows, the first mapping was never correct in that probe, while the correct answer was present among the candidate outputs in most of those rows.

That suggests at least two distinct conditions:

candidate-generation failure
candidate-selection ambiguity

They should probably not receive the same Defer reason.

There were also rows with multiple candidates but a single target output. This gives an empirical reason to distinguish:

answer accepted
witness ambiguous

However, a small number of those target-invariant cases were still wrong relative to the dataset target, so invariance within the current candidate space is useful evidence, but not a standalone correctness proof.

Likewise, some rows had a unique candidate within the tested space but still produced the wrong target answer. Therefore:

candidate_count == 1

is not sufficient on its own. “Unique within this hypothesis space” and “correct latent rule” are different claims.

Trace-replay probe

For the binary subset, I also parsed the rule expression recorded after Identified: in the public traces and replayed it independently.

A lightweight parser handled 1,400 of 1,557 rows. For all 1,400 parsed rows, the replayed rule reproduced:

all listed demonstrations; and
the stored computed_answer.

It reproduced the dataset target in 1,383 of those 1,400 rows.

I then compared the current first-match solver’s transformation with the replayed claimed transformation over all 256 possible 8-bit inputs where that comparison was meaningful.

Among cases where the current solver got the target answer right and the two transformations were comparable:

366 matched the claimed transformation on all 256 inputs;
303 got the target right but diverged somewhere else in the input space.

So in that comparison set, target correctness did not reliably imply transformation equivalence.

Also, among 913 rows where the claimed transformation was expressible by the current compact per-bit library, the first-match solver selected the globally equivalent transformation in 366 cases.

That suggests:

expressible by the library
≠
selected correctly from the demonstrations

The operation-family differences were also informative. Simpler combinations involving shifts and bitwise OR/XOR were often representable, while families involving constructs such as CHOICE, MAJORITY, or more complex composed transformations were generally outside the compact per-bit candidate space.

This supports splitting at least:

selection ambiguity
unsupported hypothesis family
unsupported witness schema

rather than sending all three to the same escalation route.

Why I would not overinterpret this

These probes were run against:

a pinned public solver snapshot;
a pinned public dataset revision;
a deliberately finite candidate library;
primarily the binary subset;
and the rule stated in the generated trace as the replay reference.

Therefore they do not establish:

the intrinsic ambiguity rate of the original puzzle generator;
that every proxy divergence is a solver defect;
that the stated trace rule is necessarily the intended latent rule;
that full truth-table equivalence should be required for every task family;
or that one routing arm is empirically superior to another.

For an answer-only task, observational equivalence on the relevant input may be enough. The full 256-input comparison is instead useful when the object being promoted is meant to represent a reusable transformation witness.

Where a stronger LLM helps—and where it does not

My default rule would be:

Use a stronger LLM when it can produce something that can subsequently be checked, not merely when it can provide a more confident tie-break.

Good escalation candidates include:

repairing malformed structured output;
converting an unsupported expression into a candidate AST;
generating additional candidate rules;
proposing a distinguishing input;
identifying a specific failed invariant;
making a bounded local repair;
or summarizing candidate differences for a human reviewer.

Afterward, the result should return to the deterministic side:

LLM-produced candidate or repair
→ canonical structured form
→ replay demonstrations
→ run invariants/property checks
→ update the status only for the layer supported

A useful nearby example is the OpenR1 Update #2: rules-based verification was used first, and an LLM judge was explored for a subset of rejected answers whose references or formatting were difficult to validate automatically.

That is a good precedent for selective recovery of difficult-to-parse cases. I would not take it as evidence that an LLM judge can identify the intended latent rule when several rules remain exactly consistent with the same demonstrations.

The same OpenR1 write-up also reports that reward-model top-1 selection among correct generations did not improve over selecting a random correct generation in that ablation. The task is different, but it is another reason not to assume that a more elaborate ranker automatically identifies a better reasoning trace.

For true program ambiguity, the closer neighboring idea may be active program synthesis: preserve the consistent candidate set, find an input that is likely to separate those candidates, and ask for that input’s output. The Significant Inputs for Program Synthesis paper is a useful example of this pattern.

The important limitation is that a distinguishing input is only useful if there is also a reliable source for its answer:

distinguishing input exists
+ generator/oracle/human can answer
→ ambiguity can potentially be reduced

distinguishing input exists
+ no reliable answer source
→ keep the candidate set unresolved

A stronger LLM can suggest the question, but unless its answer is independently verifiable, using the same LLM as both question generator and oracle would not add much separation.

A more explicit Defer decision tree

Start
│
├─ Generate/collect candidate witnesses
│
├─ No candidate
│  │
│  ├─ Parse or formatting failure
│  │  ├─ Deterministic repair
│  │  ├─ Bounded LLM repair
│  │  └─ Replay all demonstrations
│  │
│  ├─ Known schema, candidate generator incomplete
│  │  ├─ Generate additional candidate
│  │  └─ Replay deterministically
│  │
│  ├─ Unsupported operator/family
│  │  └─ Solver/schema development queue
│  │
│  └─ Timeout/resource failure
│     └─ Bounded retry, then offline queue
│
├─ One candidate
│  │
│  ├─ Replay fails
│  │  └─ Reject candidate
│  │
│  ├─ Applicable property checks fail
│  │  └─ Defer or reject witness
│  │
│  └─ Checks pass
│     └─ Accept at the supported evidence level
│
└─ Multiple candidates
   │
   ├─ All candidates give the same target output
   │  ├─ Answer may be accepted conditionally
   │  ├─ Witness remains ambiguous
   │  └─ Use answer-only training view if appropriate
   │
   └─ Candidate target outputs differ
      │
      ├─ Distinguishing query can be generated
      │  │
      │  ├─ Reliable oracle/generator exists
      │  │  └─ Query it and replay candidates
      │  │
      │  ├─ Human can answer naturally
      │  │  └─ Clustered human review
      │  │
      │  └─ No reliable answer source
      │  │     └─ Offline unresolved queue
      │  │
      │  └─ No useful distinguishing query
      │     └─ Solver-development backlog

The decision tree does not need to be implemented all at once. The immediate high-information step is simply to retain the candidate count, target-output set, and defer reason.

What I would borrow from `autoresearch-MIL`

I would say yes, selectively.

The current Agent-ProSAT repository already contains the main inner loop:

agent.py edits the solver;
assess.py evaluates the result;
the run is committed or reverted;
and recent accepted/rejected trajectory information is returned to the next iteration.

So I do not think another harness is needed to create the basic research loop.

What looks useful from autoresearch-MIL is its control-plane discipline:

Existing Agent-ProSAT mechanism	MIL pattern worth borrowing
Mutable `prosat.py`	Explicit user-owned versus agent-owned files
`assess.py` evaluation	Evaluator and promotion policy outside the editable surface
Commit/revert	Hypothesis–commit–metrics linkage
`runs.tsv` trajectory	Append-only per-run record
Output/session files	Unique run IDs and raw logs
Accepted/rejected status	Persist crash, discard, reject, and defer artifacts
Per-family metrics	Branch-pinned research memory
Twin-blind check	Immutable evaluation and lineage metadata

The MIL README and program.md explicitly separate user-owned read-only files from agent-editable files, keep one append-only result row and raw log per run, and preserve crash/discard states.

That seems directly reusable here.

I would probably define something like:

User-owned or immutable during an experiment

evaluation code
hidden grouped-holdout registry
witness schema contract
promotion thresholds
renderer conformance tests
dataset revision policy

Agent-owned

prosat.py
candidate generators
family-specific solver modules
solver parameters
possibly renderer code, but under a separate test boundary

Per-run artifacts

run_id
hypothesis
parent_commit
result_commit
dataset_revision
solver_version
witness_schema_version
candidate_set_hash
defer_reason_counts
target-only accuracy
witness replay/property results
family metrics
crash/reject/defer status
raw log path
artifact hashes

I would also keep unsuccessful knowledge in memory, not only the best score:

failed hypotheses
known shortcut families
unsupported operators
false resolutions
defer clusters
canary failures

That would make autoresearch-MIL an audit and research-memory layer around Agent-ProSAT rather than a replacement for its solver-improvement loop.

Why I would avoid reducing promotion to one scalar too early

The MIL experiment loop is built around a clear primary metric for its training task.

Agent-ProSAT has several qualitatively different objectives:

target-answer correctness;
coverage;
target isolation;
witness replayability;
candidate ambiguity;
family-level non-regression;
renderer fidelity;
training-view safety;
runtime and trace cost;
and escalation cost.

I would therefore order the decision approximately as:

integrity gates
→ protected-family non-regression
→ answer coverage/correctness
→ witness coverage and ambiguity resolution
→ renderer/training-view checks
→ runtime, token, and escalation cost

A single combined score can be added later for ranking runs, but I would retain the components and keep some of them as hard gates.

Otherwise, an increase in coverage could hide:

a regression in one family;
an increase in unsupported proxy rules;
an increase in false ambiguity resolutions;
or target-correct traces that are not reusable witnesses.

Two guardrails I would add early

1. Extend the blind check to the witness/training view

The pinned public assess.py makes the twin-blind computed-answer comparison a hard gate.

The separate tests/verify_blind.py also counts exact reasoning matches between real-target and dummy-target runs.

Once the trace becomes training data, I would consider promoting the trace-side check as well:

real target vs dummy target
→ computed answer invariant
→ canonical witness invariant or semantically equivalent
→ rendered training view invariant

For structured JSON, canonical event equality or semantic replay equality may be more useful than raw string equality.

This is another benefit of the witness/renderer split: the canonical witness can be compared semantically, while harmless wording variation in a renderer does not have to invalidate the solver.

The broader idea also connects naturally to work on execution-grounded supervision, where executable traces can be checked separately from the natural-language rationale, such as Code Execution as Grounded Supervision for LLM Reasoning.

2. Separate development feedback from promotion evaluation

Because the agent receives prior run metrics and accepted/rejected feedback, it is adaptively optimizing against the assessment surface.

That is the intended loop, but it also means I would separate:

visible development set
hidden grouped promotion set
frozen final audit set

The visible development set can return detailed family-level failures.

The hidden promotion set can be grouped by puzzle family, generator lineage, or transformation family and return a more limited result.

The frozen audit set can be reserved for milestones.

This is not specific evidence that the current solver has overfit its evaluation data. It is just a general guardrail for any iterative agent that repeatedly receives evaluation feedback. Repeated adaptive reuse of a holdout can itself lead to holdout overfitting; Generalization in Adaptive Data Analysis and Holdout Reuse is the classic reference.

Metrics I would watch

At minimum:

accepted-answer correctness
answer coverage
accepted-witness correctness/replay rate
witness coverage
defer rate by reason
verified resolution rate
false resolution rate
cost per verified resolution
family non-regression

Additional useful diagnostics could include:

candidate multiplicity rate
target-output disagreement rate
answer-stable/witness-ambiguous rate
unsupported-family rate
parser-recovery rate
LLM-escalation rate
human minutes
replayability
target/computed/witness agreement
renderer fidelity
solver runtime
trace tokens

I would pay particular attention to false resolution:

a case that was genuinely unresolved under the available evidence, but was converted into an apparently confident single witness without new verifiable evidence.

Reducing the raw number of deferred cases is not necessarily progress if false resolution increases.

This is similar to the risk/coverage distinction in selective prediction: abstaining less is only useful when the accepted set remains reliable. SelectiveNet is a useful reference for that general framing, although the downstream routing problem here is broader.

A small routing pilot before learning a router

I would start with explicit reason-based rules rather than immediately training a learned router.

A small stratified pilot could compare:

A. deterministic processing only
B. deterministic → stronger LLM with structured failure evidence
C. offline replay after solver/schema updates
D. clustered oracle/human review

The stronger-LLM arm should receive structured context such as:

defer_reason
candidate_set
target_output_set
failed_invariant
counterexample
unsupported_operator_set

rather than only receiving the original puzzle and “try again.”

Measure:

verified resolution rate
false resolution rate
answer coverage
witness coverage
cost per verified resolution
human minutes
latency
replayability
family-level regression

Once enough outcome data exist, those logs could support a learned routing policy. Before that, a learned router would mostly be encoding assumptions without much direct evidence about which expert resolves which failure family.

Minimal lineage

I do not think this requires a large tracking platform initially. A checked-in JSON or YAML manifest plus append-only event records could be enough.