{"id":"f50b1f5e-af32-4a03-af7b-54eaad00ef5e","arxiv_id":"2607.03957","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":1,"one_line_summary":"NormWorlds-CF provides solver-verified normative reasoning tasks without LLM judges; answer-only RL saturates verdicts but not falsification, and class-conditioned GRPO improves some structural change fields.","lead":"This paper introduces a benchmark where a deterministic solver checks language models' normative answers, proofs, refutations, and counterfactual-change records in tiny executable rule worlds. The experiments show that training only on final answers can look perfect while missing all reasoning structure, and that a class-conditioned reward improves some structural fields.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Minimal-support selection in §2.2 has no stated tie-breaking; if order-sensitive, S is not deterministic, and surface-invariant labels plus support-change fields become artifacts of iteration order, undercutting the MR-GRPO comparison.","rationale":"The reader's weakest assumption was that the deterministic solver S correctly and completely implements the intended defeasible normative semantics, with no code or tests. I sharpen this to a specific, load-bearing gap: the minimal-support selection and, more broadly, the solver's order-invariance are underspecified. The central empirical claim — that MR-GRPO improves structural change fields — is entirely downstream of M(w,τ) = (rτ, D(S(w), S(τ(w)))). If S can return different support sets or statuses under harmless reorderings, then the four root-level metamorphic families and all change fields are not trustworthy, and the reward comparison may be training models to predict solver artifacts. This is not a disagreement with an external consensus; it is an internal completeness gap in the construction. The paper's deterministic scoring and honest negative results are genuine strengths, but they do not remove the need for a concrete test of S's determinism. The proposed permutation test is cheap and decisive: if it passes, the environment's advertised invariants hold and the central claim is substantially safer; if it fails, the benchmark's labels are partially invalid. Given that the reader already recommended CONDITIONAL because of the unreleased solver, this concern does not change the verdict — it reinforces it. I therefore recommend UNCHANGED: the paper should be accepted conditionally on releasing or independently verifying the solver and its tie-breaking behavior.","tokens_in":12039,"tokens_out":5389,"duration_ms":67935,"concrete_test":"Release S and M (or an independent reimplementation from §2.2) and run a permutation test: for each of the 270 root families, randomize fact order, rule order, and priority-edge order and verify that S(w) — answer, decisive rules, defeated alternatives, statuses, support set, attack edges — is bit-identical across all permutations. Then verify the intended semantics of each metamorphic operator directly: for every surface_invariant pair, require the full certificate trace to be identical; for every support_delta/priority_delta pair, require the trace differencing to contain exactly the field changes the operator is defined to produce. If any permutation changes a certificate or any invariant pair shows nonzero support/attack diffs, the solver is not order-invariant and the change labels are unreliable. This can be done on a sample of 100 worlds before full release.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's ground truth is the deterministic solver S (Eq. 1) and the change differencing M (Eq. 2). §2.2 specifies the certificate extraction pipeline, but the step 'Minimal support searches subsets of decisive rules sufficient to sustain the answer' does not state how ties between equally minimal supports are broken, nor whether S is invariant under fact/rule/priority order. If multiple minimal supports exist — e.g., two independent rules permit the same action — a reorder-only surface_invariant edit can flip the selected support, so D(S(w), S(τ(w))) reports support/attack changes that are artifacts of iteration order rather than normative effects. Conversely, a support_delta edit that removes one fact may silently switch to an alternative support, yielding an empty support-change field even though the intended edit should show a removal. The paper says family labels are 'validated against solver-computed pre- and postconditions'; an order-sensitive solver could either fail many cases silently or relabel them, breaking the advertised invariant/change distinction. Since every SFT target and every GRPO reward term (Eqs. 4–7) is a function of these labels, the central claim that MR-GRPO improves structural change fields inherits this risk. The paper provides no code, tests, or formal verification for S, so this is a concrete correctness risk, not merely a reproducibility gap.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces NormWorlds-CF, a solver-verified environment for counterfactual normative reasoning in executable rule worlds. A deterministic solver S (Eq. 1) produces final answers, proof/falsification certificates, argument statuses, minimal supports, and paired-world change labels via a metamorphic relation M (Eq. 2), so supervision, reward, and evaluation avoid LLM judges. Staged SFT diagnostics show that answer-only supervision saturates verdict accuracy but leaves joint falsification at zero, while full-mix training with targeted replay reaches 0.99 overall. On the compact paired-world change-record task, the paper compares answer-only, sparse, and class-conditioned MR-GRPO rewards under a matched Qwen3-1.7B continuation and a Qwen3-4B three-seed from-SFT validation. The central claim is a reward geometry: sparse reward preserves coarse relation labels, answer-only reward trades family structure for answer-local gains, and MR-GRPO improves answer/support/status change fields while keeping family structure, with exact full-record generation, invariant subtype recognition, and OOD transfer remaining open.","tokens_in":12434,"tokens_out":6932,"duration_ms":77287,"significance":"If the solver is correct and released, this is a valuable contribution to post-training evaluation and reward design for structured judgment tasks. The deterministic scoring, typed failure taxonomy, compact change-record interface, and the explicit separation of final-answer supervision from structural competence are constructive; the paper also states its limitations clearly and uses McNemar tests for the 1.7B held-out items. However, the significance is conditional on the correctness and order-invariance of the unreleased solver, on the statistical robustness of the three-seed 4B means, and on the availability of code/configurations for independent verification.","major_comments":[{"comment":"The description of minimal-support search is not order-invariant. The sentence 'Minimal support searches subsets of decisive rules sufficient to sustain the answer while defeating conflicting alternatives' specifies no tie-breaking rule. If two minimal supports exist (e.g., two independent rules both permit the same action), a surface_invariant edit that reorders facts/rules/priorities can change which support is selected, so D(S(w),S(τ(w))) can report spurious support or attack changes on an invariant edit; conversely, a support_delta edit can switch to an alternative support and report an empty support-change field. Since every SFT target and every reward term in Eqs. (4)–(7) is a function of these labels, the central MR-GRPO comparison inherits any such artifact. Please specify deterministic tie-breaking (e.g., lexicographic over rule IDs), provide an order-ablation experiment (permut","section":"§2.2, Eq. (2)"},{"comment":"The three-seed means are reported without variance, confidence intervals, or per-seed significance tests. The headline 4B claims ('MR-GRPO leads on answer-, support-, and status-change fields') rest on differences of 0.020–0.043 (e.g., support change 0.621 vs 0.597; status change 0.600 vs 0.571; all-changes exact 0.443 vs 0.435). With three seeds these differences are consistent with noise. Provide per-seed tables with CIs or paired tests, or explicitly hedge these as directional. Also report whether the sparse-vs-MR relation-family difference (0.790 vs 0.781) is within noise.","section":"§4.3, Table 7"},{"comment":"The 1.7B continuation is a single run per reward. The abstract and §4.2 say MR-GRPO 'improves' relation accuracy and 'reduces' wrong-family error, with McNemar p-values computed on held-out items. Those p-values quantify item-level agreement within one run, not run-to-run variance; the gains (relation +0.096, wrong-family −0.142) are plausible but need at least one additional seed or a bootstrap over runs to support the reward-geometry conclusion. The paper does acknowledge single runs, but the conclusion 'verified counterfactual structure can shape post-training' is carried largely by this 1.7B result.","section":"§4.2, Table 6"},{"comment":"No code, solver implementation, or supplementary material is provided, despite repeated references to 'supplementary material' for full weights (Eqs. 4–7), seeds/hardware, per-seed tables, and field breakdowns. Since the entire benchmark is generated by the unreleased solver S and all training uses reward coefficients that are not listed, none of the headline numbers can be independently reproduced or checked. Please make the solver, data-generation code, training configs, and coefficient values available, or include them in an appendix.","section":"Reproducibility (abstract, §2.2, §4.3)"}],"minor_comments":[{"comment":"The caption '896 / 280 from base' is unexplained; state what the two numbers denote (records and steps) and what 'from base' means.","section":"§2.3, Table 5"},{"comment":"The reference entry beginning 'sch 2021' is incomplete; provide full author, title, and venue.","section":"References"},{"comment":"Some symbols used in A_class (η_same, A_same, η_chg, A_chg, η_prs, A_prs, η_E) are not explicitly defined in the text. Please define all coefficients and score fields in one place or a table.","section":"Eq. (7)"},{"comment":"The term 'matched' is used loosely; Table 4 shows only initializer and steps. Specify which data, optimizer, group size, and hyperparameters are identical across the three 1.7B branches.","section":"§4.2"},{"comment":"The sentence 'OOD uses held-out structural family types (e.g., priority chains and distractor-conflict variants)' should clarify whether these are subtypes of the same four root-level families or new family types, since this affects interpretation of the OOD results.","section":"§2.3"}],"recommendation":"major_revision","confidential_remarks":"The contribution is potentially a good fit for the journal and the claims are presented with unusual care about limitations. The main blocker is not framing but verifiability: the oracle is unreleased and its minimal-support procedure is under-specified, and the 4B results lack error bars. I would be supportive after the solver and per-seed data are made available and the statistical claims are qualified accordingly."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Worth a serious referee, but the load-bearing assumption is the deterministic solver, and the paper doesn't back it up. The new things are real: a paired-world change-record benchmark for normative reasoning with solver-checked labels, MR-GRPO as a class-conditioned reward, and the SFT finding that answer-only supervision saturates verdict accuracy while leaving falsification at zero. The staging is careful, deterministic scoring is a plus, and the limitations (OOD, invariant subtypes, exact full-record) are reported honestly. The central claim—outcome supervision misses structural competence, and reward geometry matters—is plausible and well-argued. The main soft spot is the solver itself. Minimal support search is described as selecting subsets sufficient to sustain an answer, but no tie-breaking rule is stated. If multiple minimal supports exist, reordering facts or rules could flip the selected support, so a surface_invariant edit would produce spurious support changes. That would corrupt the change labels, and since every SFT target and every MR-GRPO reward term is computed from those labels, the headline comparison inherits the error. The paper calls the solver 'closed symbolic' and says labels are validated against pre/postconditions, but validation against an order-sensitive solver doesn't fix order-sensitivity. This is a correctness risk, not just a reproducibility gap, and it is aggravated by releasing no code, tests, or formal verification. Smaller issues: the 1.7B continuation is single-run, effect sizes are small (3–10 points on near-floor metrics), the 4B three-seed means lack variance or confidence intervals, reward coefficients are only partially specified, and the PICARD citation is garbled. None of these are fatal, but they cap confidence. On balance, the paper deserves peer review. The research question matters, the design is mostly careful, and the negative results (OOD ties, invariant subtypes weak) suggest the authors are not cherry-picking. But reviewers should demand the solver be released, tie-breaking be specified and tested, and seeds be added. If those are fixed, I would be happy to cite this and would bring it to a reading group to discuss what 'solver-verified' should mean in practice. As it stands, the verdict is an evidence-based maybe, not a yes.","headline":"Solver-verified counterfactual benchmark with a genuinely useful reward-geometry result, but ground truth rests on an unverified and possibly order-sensitive solver, so treat as a strong conditional.","tokens_in":732,"tokens_out":967,"would_cite":true,"duration_ms":34818,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Solver-verified counterfactual normative reasoning shows that models can reach perfect verdict accuracy while learning no falsification competence, and that a class-conditioned reward teaches structural change fields that final-answer rewar","keywords":["counterfactual normative reasoning","solver-verified benchmark","defeasible logic","metamorphic testing","GRPO","reward design","falsification certificates","structural change records"],"falsifier":"Take the prose description of the solver, reimplement the forward-chaining, attack-only-on-incompatible-labels, priority-by-directed-reachability, and minimal-support algorithm, and compare its outputs against the paper's reported ground truth on all 270 root families and 1080 canonical-to-variant pairs; a single mismatch in any relation family label would falsify the benchmark's ground truth and, with it, the reward-geometry conclusions.","tokens_in":11903,"feed_emoji":"⚖️","tokens_out":8126,"duration_ms":76626,"temperature":0.7,"pith_summary":"NormWorlds-CF argues that in normative reasoning, where verdicts come from a tiny label set, a language model can reach perfect answer accuracy while learning none of the structural competence—proof, falsification, and counterfactual change—that makes a verdict trustworthy. To test this, the paper builds a synthetic environment of executable rule worlds in which a deterministic solver emits answers, certificates, and paired-world change labels, so supervision and evaluation never rely on an LLM judge. The staged SFT diagnostics show that answer-only supervision saturates verdict accuracy but scores zero on joint falsification, while full-mix training with targeted replay reaches strong all-task accuracy. On the paired-world change task, a class-conditioned reward, MR-GRPO, measurably improves structural change fields compared with sparse or answer-only rewards, leading the paper to conclude that verified counterfactual structure can shape post-training beyond final answers and that reward geometry, not final-answer accuracy, is what determines whether structure is learned.","feed_headline":"Answer-only SFT hits 100% verdicts, 0% falsification","feed_subtitle":"Solver-verified counterfactual pairs show why final-answer rewards leave proof and falsification unlearned.","key_machinery":"The load-bearing object is the deterministic solver S(w) = (a, C), a closed symbolic procedure that maps an executable rule world to a final answer and a certificate (decisive rules, defeated alternatives, argument statuses, minimal support), together with its change-differencing operator M(w, τ) = (r_τ, D[S(w), S(τ(w))]) that derives paired-world metamorphic relation labels and fine-grained change fields by comparing two solver traces. This machinery carries the argument because every supervision target, GRPO reward, and reported metric is a downstream function of these solver outputs, never an LLM judge. The second key object is the class-conditioned metamorphic reward A_class, which group","core_discovery":"The paper's central discovery is a reward geometry: different supervision targets and rewards learn different slices of the same normative structure, and final-answer supervision is not a proxy for dialectical competence. Answer-only SFT reaches perfect answer accuracy but scores zero on joint falsification certificates; adding proof targets saturates proofs yet still leaves falsification at zero, and only full-mix training with targeted replay reaches 0.99 all-task accuracy. In the compact paired-world change task, answer-only GRPO shifts the relation prior toward change labels and improves answer-local fields at the expense of relation-family structure, while sparse exact/schema GRPO prese","pith_inferences":["The scarcity-inversion framing generalizes: any domain with a small verdict label set (medical triage, compliance checks, policy classification) should place reward on the structure that distinguishes a right answer from a right reason, not on the answer itself.","Because the solver is unreleased, the benchmark is not yet independently auditable; opening the solver or providing a formal specification would let other labs regenerate worlds and test reward designs against a checkable ground truth.","The proof-to-falsification non-transfer suggests critique is a separate capability from construction; a testable extension is whether training on falsification first transfers to proof, or whether the two require separate curricula.","MR-GRPO's class-conditioning could be extended from the invariant/change boundary to finer subtype distinctions (e.g., support_delta vs priority_delta) or adapted for OOD transfer by conditioning on structural invariants rather than family names."],"forward_implications":["If the paper is right, post-training for judgment-like tasks should not use answer-only rewards as a competence proxy: perfect verdicts can coexist with zero falsification ability.","Answer-only reward can actively distort structure in a low-entropy label setting: it biases the relation prior toward change labels, converting invariant examples into wrong-family errors.","Sparse exact rewards can starve GRPO when the target structure is nested rather than a rare token: zero within-group reward variance removes the ranking signal.","Class-conditioned partial credit along a diagnostic hierarchy (invariant vs change families) densifies structural reward without collapsing to the most visible answer field.","Solver-verified environments make failure attribution typed (answer vs proof vs falsification vs counterfactual errors), turning 'the model is wrong' into a researchable diagnosis."],"fun_headline_variants":["100% verdicts, 0% falsification: why answers aren't proof","Answer-only SFT: perfect verdicts, zero falsification","Solver-verified counterfactuals expose reward-blind spots","MR-GRPO teaches relation families that sparse rewards miss","Final answers don't imply falsification: a verified lesson"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The whole benchmark rests on the unreleased deterministic solver being a correct and complete implementation of the intended defeasible normative semantics; if the solver's design choices misrepresent dialectical reasoning, every ground-truth label, reward, and result inherits the error.","fun_headline_variants_meta":{"raw":{"variants":["100% verdicts, 0% falsification: why answers aren't proof","Answer-only SFT: perfect verdicts, zero falsification","Solver-verified counterfactuals expose reward-blind spots","MR-GRPO teaches relation families that sparse rewards miss","Final answers don't imply falsification: a verified lesson"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000278,"raw_usage":{"total_tokens":1542,"prompt_tokens":844,"completion_tokens":698,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":588,"completion_tokens_details":{"reasoning_tokens":611}},"tokens_in":588,"tokens_out":698,"duration_ms":7310,"temperature":1.0,"reasoning_tokens":611,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-02T08:43:45.538693+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take the prose description of the solver, reimplement the forward-chaining, attack-only-on-incompatible-labels, priority-by-directed-reachability, and minimal-support algorithm, and compare its outputs against the paper's reported ground truth on all 270 root families and 1080 canonical-to-variant pairs; a single mismatch in any relation family label would falsify the benchmark's ground truth and, with it, the reward-geometry conclusions.","supporting_citations":[],"review_version":2}