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

**URL:** <https://discuss.huggingface.co/t/agent-prosat-for-cot-via-verifiable-programmatic-solver-coding-for-cot-synthesis-feedback-appreciated/177992>\
**Category:** Research\
**Created:** [July 19, 2026, 11:40am UTC](https://discuss.huggingface.co/t/agent-prosat-for-cot-via-verifiable-programmatic-solver-coding-for-cot-synthesis-feedback-appreciated/177992 "2026-07-19T11:40:55Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![ShehabAnwer](https://sea2.discourse-cdn.com/hellohellohello/user_avatar/discuss.huggingface.co/shehabanwer/32/60873_2.png) [@ShehabAnwer](https://discuss.huggingface.co/u/ShehabAnwer)\
**Post date:** [July 19, 2026, 11:40am UTC](https://discuss.huggingface.co/t/agent-prosat-for-cot-via-verifiable-programmatic-solver-coding-for-cot-synthesis-feedback-appreciated/177992/1 "2026-07-19T11:40:55Z")

</div>

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.

 ![image](https://us1.discourse-cdn.com/hellohellohello/original/3X/b/f/bf2e658bdffa5b7af3819f1ffd886b6c6b75bea8.jpeg)

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](https://github.com/The-Adimension/Agent-ProSAT/)
- Kaggle Notebook: [Nemotron ATLAS | Kaggle](https://www.kaggle.com/code/habanwer/nemotron-atlas) (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.

---

<div class="post-metadata">

**Author:** ![John6666](https://sea2.discourse-cdn.com/hellohellohello/user_avatar/discuss.huggingface.co/john6666/32/27664_2.png) [@John6666](https://discuss.huggingface.co/u/John6666)\
**Post date:** [July 20, 2026, 11:30pm UTC](https://discuss.huggingface.co/t/agent-prosat-for-cot-via-verifiable-programmatic-solver-coding-for-cot-synthesis-feedback-appreciated/177992/2 "2026-07-20T23:30:13Z")

</div>

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](https://aclanthology.org/2025.emnlp-main.1260/) extracts deterministic execution traces and turns them into natural-language supervision. [Think Like You Execute](https://aclanthology.org/2026.acl-industry.53/) 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

```plaintext
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](https://developer.nvidia.com/blog/lessons-from-the-leaderboard-what-5000-kagglers-taught-us-about-improving-ai-reasoning/) 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:

```yaml
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:

1. keep structured execution evidence as the canonical audit record;
2. generate natural-language rationales as replaceable training views;
3. run cheap deterministic checks on every sample;
4. defer ambiguous cases to stronger verification;
5. audit a small stratified sample before another large run;
6. compare answer-only, short, structured, and long-trace conditions;
7. evaluate generated answers on grouped holdouts;
8. 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:
> 
> ```json
> {
> "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:
> 
> ```plaintext
> 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
> 
> ```plaintext
> 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?](https://discuss.huggingface.co/t/when-should-llms-verify-instead-of-think-longer/176974) 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?](https://proceedings.mlr.press/v267/jia25f.html) 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](https://github.com/open-thought/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](https://hypothesis.readthedocs.io/) 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:
> 
> ```plaintext
> 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:
> 
> ```plaintext
> 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](https://huggingface.co/docs/trl/en/sft_trainer) 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:
> 
> ```json
> {
> "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:
> 
> - [Dataset Card guidance](https://huggingface.co/docs/datasets/en/dataset_card)
> - [Model Card guidance](https://huggingface.co/docs/hub/en/model-cards)
> 
> 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](https://aclanthology.org/2025.emnlp-main.1260/)  
> Deterministic execution traces converted into natural-language reasoning supervision.
> 
> - [Think Like You Execute: Verifiable Chain of Thought from Program Traces](https://aclanthology.org/2026.acl-industry.53/)  
> Instrumentation, trace narration, and verification of the resulting rationale.
> 
> - [NExT: Teaching Large Language Models to Reason about Code Execution](https://arxiv.org/abs/2404.14662)  
> Execution-aware data derived from program state.
> 
> ### Procedural and verifiable environments
> 
> - [Reasoning Gym](https://github.com/open-thought/reasoning-gym)  
> Procedural generation with seeds, adjustable complexity, metadata, and algorithmic scoring.
> 
> - [NVIDIA’s Nemotron challenge postmortem](https://developer.nvidia.com/blog/lessons-from-the-leaderboard-what-5000-kagglers-taught-us-about-improving-ai-reasoning/)  
> 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?](https://proceedings.mlr.press/v267/jia25f.html)  
> A useful reason not to assume that denser process verification is universally superior.
> 
> ### Practical testing and training
> 
> - [Hypothesis](https://hypothesis.readthedocs.io/)
> - [TRL SFT Trainer](https://huggingface.co/docs/trl/en/sft_trainer)
> - [Hugging Face Dataset Cards](https://huggingface.co/docs/datasets/en/dataset_card)
> - [Hugging Face Model Cards](https://huggingface.co/docs/hub/en/model-cards)
> 
> None of these is an exact match for Agent-ProSAT. Together, however, they support a useful working pattern:
> 
> ```plaintext
> 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.

---

<div class="post-metadata">

**Author:** ![ShehabAnwer](https://sea2.discourse-cdn.com/hellohellohello/user_avatar/discuss.huggingface.co/shehabanwer/32/60873_2.png) [@ShehabAnwer](https://discuss.huggingface.co/u/ShehabAnwer)\
**Post date:** [July 22, 2026, 6:35pm UTC](https://discuss.huggingface.co/t/agent-prosat-for-cot-via-verifiable-programmatic-solver-coding-for-cot-synthesis-feedback-appreciated/177992/3 "2026-07-22T18:35:18Z")

</div>

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:**

1. 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?

2. 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](https://github.com/habanwer/autoresearch-MIL) ) 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

---

<div class="post-metadata">

**Author:** ![John6666](https://sea2.discourse-cdn.com/hellohellohello/user_avatar/discuss.huggingface.co/john6666/32/27664_2.png) [@John6666](https://discuss.huggingface.co/u/John6666)\
**Post date:** [July 23, 2026, 3:20am UTC](https://discuss.huggingface.co/t/agent-prosat-for-cot-via-verifiable-programmatic-solver-coding-for-cot-synthesis-feedback-appreciated/177992/4 "2026-07-23T03:20:03Z")

</div>

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:

1. **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.**
2. **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:

```plaintext
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](https://proceedings.mlr.press/v119/mozannar20b.html), 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:

```plaintext
answer_status
witness_status
renderer_status
training_view_status

```

For example:

```plaintext
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:

```json
{
  "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:

```plaintext
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:

```plaintext
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`](https://github.com/The-Adimension/Agent-ProSAT/tree/84c548c5c5ccef3af86a6c26787fea70ef91aaa3). 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:

1. Multiple demonstration-consistent candidates were common in the current compact candidate space.
2. 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`](https://github.com/The-Adimension/Agent-ProSAT/blob/84c548c5c5ccef3af86a6c26787fea70ef91aaa3/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:
> 
> ```plaintext
> 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:
> 
> ```plaintext
> 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:
> 
> ```plaintext
> 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:
> 
> ```plaintext
> 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:
> 
> ```plaintext
> 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:

```plaintext
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](https://huggingface.co/blog/open-r1/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](https://arxiv.org/abs/2006.12638) 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:

```plaintext
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**
>
> ```plaintext
> 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](https://github.com/The-Adimension/Agent-ProSAT) 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](https://github.com/habanwer/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](https://github.com/habanwer/autoresearch-MIL/blob/master/README.md) and [`program.md`](https://github.com/habanwer/autoresearch-MIL/blob/master/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**

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

```

**Agent-owned**

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

```

**Per-run artifacts**

```plaintext
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:

```plaintext
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:
> 
> ```plaintext
> 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`](https://github.com/The-Adimension/Agent-ProSAT/blob/84c548c5c5ccef3af86a6c26787fea70ef91aaa3/assess.py) makes the twin-blind computed-answer comparison a hard gate.

The separate [`tests/verify_blind.py`](https://github.com/The-Adimension/Agent-ProSAT/blob/84c548c5c5ccef3af86a6c26787fea70ef91aaa3/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:

```plaintext
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](https://aclanthology.org/2025.emnlp-main.1260/).

### 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:

```plaintext
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](https://arxiv.org/abs/1506.02629) is the classic reference.

## Metrics I would watch

At minimum:

```plaintext
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:

```plaintext
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](https://proceedings.mlr.press/v97/geifman19a.html) 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:

```plaintext
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:

```plaintext
defer_reason
candidate_set
target_output_set
failed_invariant
counterexample
unsupported_operator_set

```

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

Measure:

```plaintext
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.

For example:

```plaintext
dataset_revision
source_row_id
generator_commit
solver_commit
witness_schema_version
renderer_version
verifier_version
candidate_set_hash
decision
defer_reason
escalation_target
escalation_model_and_prompt_version
final_output_hash
parent_run_id

```

I would keep three things separate:

```plaintext
append-only audit events
current materialized training view
raw unresolved/deferred queue

```

That way:

- the audit record is not rewritten when policy changes;
- the training view can be regenerated;
- and deferred items can be replayed after a solver or schema update.

## My suggested implementation order

If I were sequencing it, I would probably do:

1. Emit canonical structured witnesses.
2. Separate answer, witness, renderer, and training-view statuses.
3. Record candidate sets and target-output sets where enumeration is feasible.
4. Add reason-coded `Accept / Reject / Defer`.
5. Use bounded escalation only when the route can add checkable evidence.
6. Keep unresolved cases replayable offline.
7. Borrow MIL’s ownership, run logging, failure persistence, and lineage patterns.
8. Add witness-side target-isolation and hidden promotion checks.
9. Compare routing arms on a small stratified deferred set.
10. Learn or tune routing only after outcome logs exist.

So, to answer the original either/or directly:

> **For the dataset-generation phase, I would queue unresolved ambiguity offline by default, while dynamically escalating only the repairable or candidate-generating cases where the stronger model can produce something that the deterministic harness can verify.**

And for the second question:

> **Yes, I think the earlier MIL harness is relevant—but mainly as a source of governance, append-only experiment records, failure memory, and ownership boundaries around Agent-ProSAT’s existing loop.**

That seems like the lowest-cost route that preserves the audit/training-view separation while still letting the system improve iteratively.