{"id":"f694e800-426b-47d2-8ff5-db0d25a148c6","arxiv_id":"2501.03888","paper_version":4,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":5,"one_line_summary":"A differentiable DNF-based RL actor with a softmax-style activation can be trained end-to-end and then converted into editable ProbLog or ASP rule sets.","lead":"This paper introduces neural DNF-MT, a differentiable rule-based neural network for reinforcement learning that can be converted into readable logic programs after training. It aims to give AI agents the performance of black-box deep RL while letting humans inspect and edit the learned policy.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Thresholding to {−6,0,6} is the unproven bridge: Appendix A proves equivalence only after thresholding, while Section 5/Listing 6 show thresholding can flip a disjunctive output and break logical mutual exclusivity.","rationale":"The reader's verdict (CONDITIONAL) identifies the same load-bearing weakness: the thresholding step is not faithful in general. My stress test sharpens this: the failure is not hypothetical; it is exhibited by the authors in Section 5 and in the Door Corridor statistics (25 of 32 successful runs). The Appendix A proof is sound for the already-thresholded network, and the mutex-tanh construction genuinely satisfies probabilistic mutual exclusivity, but neither proves that the extracted program approximates the trained policy. Because the paper's two headline contributions, interpretable extraction and editable port-back, both require the extracted logic program to represent the learned policy, this gap is central. The appropriate outcome is still CONDITIONAL rather than REJECT: the method is novel, clearly described, and has public code; the proof covers the translation itself, and the stochastic tasks show only modest degradation. The condition should be that the authors quantify thresholding error and either guarantee mutual exclusivity after thresholding (e.g., by checking all reachable states) or report success rates that include failed runs. I find no basis for a stronger attack on the mutex-tanh math or the bidirectional translation of thresholded networks, and I credit the authors for surfacing the failure rather than hiding it.","tokens_in":38397,"tokens_out":6984,"duration_ms":70892,"concrete_test":"With the public repo, run the full post-training pipeline on all 32 Door Corridor seeds and enumerate every reachable 3×3 observation. For each seed compute (a) the original neural actor's mutex-tanh action distribution, (b) the distribution and argmax after thresholding step 2(b) at the reported tau, and (c) the extracted ASP program's chosen action. Report the maximum and mean L1 probability distance between (a) and (b), the number of seeds with any argmax flip or more than one positive disjunctive output, and the success rate counting all 6 truncated seeds as failures. If any seed violates logical mutual exclusivity or changes argmax, the close-approximation claim is not established as stated; if all 32 seeds pass within a stated tolerance, the concern is settled.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim that a trained neural DNF-MT actor can be directly translated into a close-approximation logic program (abstract, Contribution 2) depends on the post-training thresholding step (Section 3.3, Step 2). This step snaps weights to {−6,0,6} and replaces tanh with a step function; no guarantee or tolerance bound is given that the thresholded model preserves the original policy. Appendix A's bidirectional equivalence proof (Propositions A.1–A.2) assumes Condition (10), w∈{−6,0,6}^I, i.e. it applies only after thresholding; it does not justify the thresholding operation itself. The authors' own Section 5/Listing 6/Table 3 provide a concrete counterexample: for x2=−1, x7=1, x9=1, x13=−1, the pre-threshold output has y3=−0.86 (so action 1 is the unique true action), but after thresholding y3=1.00, giving two true actions and violating P2. Appendix F shows why: the max-based bias in Eq (1) encodes input importance, which thresholding discards. Since at least one trained Door Corridor run fails in exactly this way and 6 further runs cannot finish (Section 4.4: 25 of 32 runs contribute to the reported −8.000 result), the headline parity and interpretability claims currently hold only for a subset of trained models. This is not a disagreement with external consensus; it is an internal gap between the architecture's proven part and the extraction pipeline's unproven part.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes neural DNF-MT, a differentiable neuro-symbolic architecture for reinforcement learning policies, built on pix2rule's semi-symbolic DNF layers but adding a mutex-tanh activation that makes the action distribution mutually exclusive by construction. The authors claim that trained neural DNF-MT actors can be directly translated into ProbLog programs for stochastic policies and ASP programs for deterministic policies, that this translation is bidirectional, and that edited ASP policies can be ported back into the neural model. They evaluate on Switcheroo Corridor, Blackjack, Taxi, and Door Corridor environments, reporting performance at the level of MLP baselines while providing interpretable logic programs, and they demonstrate policy intervention on two Door Corridor variants. The paper includes a formal equivalence proof in Appendix A for the neural-to-logic and logic-to-neural translation for thresholded weights in {-6,0,6}.","tokens_in":38704,"tokens_out":3190,"duration_ms":31571,"significance":"If the central extraction claim held, this would be a valuable contribution: it offers a principled way to obtain standard ProbLog/ASP policies from differentiable RL actors, with a bidirectional translation that supports manual policy editing. The mutex-tanh activation is a clean mechanism for enforcing probabilistic mutual exclusivity, and the proof in Appendix A is a genuine formalization for the thresholded case. The policy intervention demonstration (DC-T, DC-OT) is a compelling proof of concept. However, the significance is currently conditional because the post-training thresholding step—the bridge between the trained continuous model and the provably translatable discrete model—is shown by the authors' own experiments to fail on a concrete instance (Listing 6), and the reported experimental results omit failed runs. The paper is honest about this limitation, but the central 'direct translation' contribution (Contribution 2) is not yet supported at the level claimed.","major_comments":[{"comment":"The core extraction claim rests on an unproven thresholding step. Propositions A.1 and A.2 prove truth-value equivalence only under Condition (10), w ∈ {-6,0,6}^I, i.e., after thresholding; they do not establish that thresholding preserves the policy. Section 5 and Listing 6 give a concrete counterexample: for x2=-1, x7=1, x9=1, x13=-1, the pre-threshold disjunctive output is y3=-0.86 (only action 1 true) while after thresholding y3=1.00, producing two true actions and violating P2. This directly contradicts the claim that a trained actor 'can be directly translated' into a close approximation of the learned policy. The manuscript needs either a guarantee or a probabilistic tolerance bound for thresholding, or a substantial reframing of the contribution as a heuristic extraction with failure cases.","section":"Section 3.3, Step 2; Appendix A; Section 5, Listing 6"},{"comment":"The reporting of Door Corridor results is inconsistent and the headline parity result omits failed runs. Section 4.4 states that out of 32 runs, 6 cannot finish training and 1 of the remaining 26 fails to maintain mutual exclusivity after thresholding, leaving 25 interpretable runs. Yet Table 6 reports 16 runs per model for Door Corridor and lists Neural DNF-MT* as -8.000 ± 0.000, which appears to average only the successful 25 runs. The discrepancy between 32 and 16 runs needs clarification, and the abstract's claim of performing 'at the level of competing black-box methods' must be reported with the success rate (25/32) and the two distinct failure modes explicitly shown, rather than as an unconditional parity result.","section":"Section 4.4 and Table 6"},{"comment":"Appendix F's analysis shows why thresholding is not semantics-preserving: the max-based bias in Eq. (1) encodes input importance, and thresholding to {−6,0,6} discards that weighting. The example with weights [3,1,1] and inputs [1,-1,1] yields a positive node output under the max bias, although the intended conjunction is false; this means the trained continuous model does not necessarily respect the DNF semantics that the extracted rules assume. This is not a minor technicality but a fundamental mismatch between the training objective (which uses importance-weighted inputs) and the post-training interpretation (which treats all weights as ±6). The paper should either adopt the min-based bias (or an alternative) to align training with the extraction semantics, or explicitly characterize which trained models are safe to extract.","section":"Appendix F and Eq. (1)"}],"minor_comments":[{"comment":"The keywords line contains a typo: 'Neuro-symobilc' should be 'Neuro-symbolic'.","section":"Abstract/Keywords"},{"comment":"The number of runs for Door Corridor is inconsistent (16 in Table 6 caption versus 32 in Section 4.4). Please reconcile these numbers and state the run counts for each environment precisely.","section":"Table 6 caption and Section 4.4"},{"comment":"Listing 6 leaves bias terms uncalculated, which makes the thresholding counterexample difficult to verify. Please include the full learned weights and biases for that run, or provide a link to the exact trained model checkpoint used in the example.","section":"Listing 6"},{"comment":"The logical formula for logical mutual exclusivity uses the symbols 'Ü' and 'Û' which appear to be rendering artifacts for OR (∨) and AND (∧). Please fix the notation.","section":"Definition 3.2"},{"comment":"The ProbLog run-time comparison for Taxi is based on a synthetic program format rather than on actual extracted programs; the authors acknowledge this, but the conclusion would be stronger with timings for the real extracted ProbLog programs from Section 4.3, even if approximate.","section":"Appendix E"}],"recommendation":"major_revision","confidential_remarks":"The paper is transparent about its limitations, but the central contribution is currently undermined by the thresholding gap. This is fixable: the authors could narrow the claim to 'provably correct for thresholded models, with thresholding as a heuristic step that succeeds in most but not all cases,' and report the failure rate honestly. I would also request a careful reconciliation of the Door Corridor run counts between Section 4.4 and Table 6. The self-citation to pix2rule and DNF-EO is heavy but justified given the direct architectural lineage."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The bottom line: this is a solid increment in neuro-symbolic RL, and the authors are honest about their main weakness. The mutex-tanh activation is a real fix for probabilistic mutual exclusivity, and the bidirectional ProbLog/ASP extraction plus the editing loop is a genuine contribution. The translation proof in Appendix A is sound for models already snapped to {-6,0,6}, and the code is public.\n\nThe soft spot is the thresholding step. The paper claims a trained actor can be directly translated into a logic program that closely approximates the policy, but the proof only covers models already thresholded. The snapping itself can change the logic: Listing 6 shows a Door Corridor actor where thresholding flips a disjunctive output and produces two true actions, violating the logical mutual exclusivity the design is supposed to guarantee. The authors acknowledge this and leave it to future work, which is good, but it means the headline parity claim rests on a subset of runs. Door Corridor reports 25 of 32 runs, with the excluded cases including this failure mode.\n\nNone of this kills the paper. The core idea is promising, the mutex-tanh activation is mathematically clean, and the policy intervention demonstration works on the successful runs. The performance loss in Blackjack and Taxi is also disclosed. This deserves a conditional accept: publish the architecture, but the extraction pipeline needs a formal tolerance bound or a statistical guarantee, or a replacement for the thresholding step.\n\nI'd bring this to a reading group. I'd cite it in my own work if I were in interpretable RL. The authors are thinking straight and the limitations are stated, not hidden. A serious referee should engage.","headline":"A genuine increment in neuro-symbolic policy learning whose main extraction claim is only proven after a thresholding step that the authors themselves show can break mutual exclusivity.","tokens_in":39295,"tokens_out":1708,"would_cite":true,"duration_ms":16865,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68T07","68T27","68T05"],"pacs":[],"model":"deepseek-v4-flash","headline":"Trained neural DNF-MT actors translate directly into editable ProbLog or ASP policies, with a bidirectional neural-logic mapping.","keywords":["neuro-symbolic learning","neuro-symbolic reinforcement learning","interpretable policies","probabilistic logic programs","answer set programming","disjunctive normal form","mutex-tanh activation","policy distillation"],"falsifier":"Evaluate the Door Corridor actor from Listing 6 on the input $x_2=-1, x_7=1, x_9=1, x_{13}=-1$: before thresholding only action 1 is true, whereas after thresholding both action 1 and action 3 are true, which directly violates logical mutual exclusivity. More generally, one can scan any trained actor for a state where thresholding changes the sign of any disjunctive node or makes two disjunctive nodes positive; finding a single such state is enough to show the extraction pipeline is not faithful for that actor without additional correction.","tokens_in":38091,"feed_emoji":"🧠","tokens_out":7198,"duration_ms":64546,"temperature":0.7,"pith_summary":"Neural DNF-MT is a fully differentiable neural architecture for reinforcement learning that is designed so a trained actor can be read out as a standard logic program: ProbLog annotated disjunctions for stochastic policies and ASP rules for deterministic policies. The paper's central claim is that this gives the performance of a black-box neural actor together with an interpretable, manually editable policy, and that for bivalent logic the translation is bidirectional, so an edited ASP program can be written back into the neural model and executed with equivalent truth values. The architecture uses a disjunctive-normal-form network whose final activation, mutex-tanh, maps outputs to probabilities that sum to one, and auxiliary losses push activations and weights toward values that make logical extraction faithful. Evaluations on corridor tasks, Blackjack, Taxi, and Door Corridor show extracted ASP policies matching the neural actors in deterministic settings, while ProbLog extraction in Blackjack and Taxi loses some performance. The paper isolates the post-training thresholding step, which snaps continuous weights to $\\{-6, 0, 6\\}$, as the cause, and gives a concrete Door Corridor counterexample where thresholding flips a disjunctive output and creates two simultaneously true actions.","feed_headline":"RL policies become logic programs you can hand-edit","feed_subtitle":"Neural DNF-MT trains like a neural actor, then reads out as ProbLog or ASP rules that can be edited and ported back.","key_machinery":"The load-bearing object is the mutex-tanh activation, defined as $\\mathrm{mutex\\text{-}tanh}(\\mathbf{d})_k = 2\\,\\mathrm{softmax}(\\mathbf{d})_k - 1$, applied to the disjunctive layer of a neural DNF model. It maps any real pre-activation vector to $(-1,1)^N$ in a way that makes the interpreted probabilities $(\\tilde{y}_i+1)/2$ sum to $1$, satisfying probabilistic mutual exclusivity; with auxiliary losses that drive conjunctive activations and disjunctive weights toward $\\pm1$ and $\\pm6$, the same network can also satisfy logical mutual exclusivity after thresholding. The conjunctive layer remains a tanh-activated semi-symbolic layer whose bias is computed from the max-absolute weight, and the whole actor can be preceded by a trainable encoder that invents predicate-like features from complex observations. This combination is what lets one network serve both as a differentiable policy and as a source of extractable ProbLog or ASP rules.","core_discovery":"The authors claim that a neural DNF-MT actor, a semi-symbolic network with a conjunctive layer followed by a disjunctive layer, can be trained end-to-end with actor-critic PPO (or distilled from an MLP actor) and then translated, without retraining, into a close logical approximation of the learned policy. For stochastic policies the translation is a ProbLog program whose annotated disjunctions carry the action probabilities, with the mutex-tanh activation guaranteeing that the probabilities sum to one. For deterministic policies the translation is an ASP program whose rules are read off after weights are thresholded to $\\{-6, 0, 6\\}$ and activations are replaced by step functions; the paper proves in Appendix A that with such weights the truth value of the ASP program equals the bivalent interpretation of the neural activations, in both directions. This bidirectional property is what makes policy intervention possible: a user can change the ASP rules to adapt to a new termination condition, port the edited program back into a neural actor, and run it without further training.","pith_inferences":["I infer that if thresholding were replaced by a sign-preserving discretisation, for instance using the min-based bias derived in Appendix F or per-node scaling, the extraction failure described in Listing 6 would be avoidable and the bidirectional edit loop would be reliable for any trained actor; the paper leaves this as future work.","I infer that the same softmax-derived exactly-one activation could be applied to other neural classifiers that need both probabilistic calibration and logical mutual exclusivity, not just RL policies.","I infer that the demonstrated policy intervention suggests a practical workflow for environment-rule changes: patch a few ASP clauses instead of fine-tuning a network, then port the edited program back for parallel execution."],"forward_implications":["A trained neural DNF-MT actor yields an inspectable policy: the extracted ASP rules for deterministic environments are short human-readable clauses, e.g., `action(left) :- in_s_1.`, and ProbLog rules carry explicit action probabilities.","The bidirectional neural-to-bivalent translation means manual policy intervention does not require retraining: editing the ASP program and porting it back produced optimal behaviour in two Door Corridor variants where an MLP actor failed.","Inference stays fast because execution happens in the neural actor; running the extracted ProbLog program is orders of magnitude slower, so the logic program serves as the interpretable specification rather than the runtime engine.","Because the model trains with a standard MLP critic and PPO, and supports end-to-end predicate invention, it avoids rule templates or mode declarations used by several prior neuro-symbolic approaches.","The extracted logic policy is only a close approximation, not a guaranteed copy, of the neural policy; in Blackjack and Taxi the ProbLog extraction degraded performance, which the paper attributes to thresholding."],"supporting_citations":[{"why":"Supplies the semi-symbolic layer and neural DNF architecture on which neural DNF-MT is built.","marker":"[7]"},{"why":"Identifies the missing exactly-one constraint in neural DNF for multi-class output, which mutex-tanh addresses while adding probabilistic interpretation.","marker":"[3]"},{"why":"Defines ProbLog, the target language for extracted stochastic policies via annotated disjunctions.","marker":"[9]"},{"why":"Defines answer set programming, the target language for extracted deterministic policies and the bidirectional translation proof.","marker":"[21]"},{"why":"Provides the PPO algorithm used to train neural DNF-MT actors with an MLP critic.","marker":"[30]"},{"why":"Source of the Switcheroo Corridor and Blackjack environments and the Q-table baseline used for comparison.","marker":"[33]"},{"why":"Supplies the Taxi environment used in the distillation experiment.","marker":"[11]"},{"why":"Inspiration for the Door Corridor environment with image-like observations.","marker":"[6]"}],"fun_headline_variants":["Train like a neural net, edit like a logic program","RL policies become editable logic programs","Neural policy to ASP/ProbLog, then edit and re-import","Hand-edit learned RL policies via logic programs"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that snapping the trained continuous weights to the three values $-6$, $0$, $6$ preserves the sign of every node output (and hence the chosen action and the exclusivity of the policy); the paper's own Listing 6 shows a Door Corridor actor where thresholding flips a disjunctive output from negative to positive, making two actions true at once.","fun_headline_variants_meta":{"raw":{"variants":["Train like a neural net, edit like a logic program","RL policies become editable logic programs","Neural policy to ASP/ProbLog, then edit and re-import","Hand-edit learned RL policies via logic programs"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000205,"raw_usage":{"total_tokens":1400,"prompt_tokens":959,"completion_tokens":441,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":575,"completion_tokens_details":{"reasoning_tokens":386}},"tokens_in":575,"tokens_out":441,"duration_ms":4459,"temperature":1.0,"reasoning_tokens":386,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T21:44:45.176027+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Evaluate the Door Corridor actor from Listing 6 on the input $x_2=-1, x_7=1, x_9=1, x_{13}=-1$: before thresholding only action 1 is true, whereas after thresholding both action 1 and action 3 are true, which directly violates logical mutual exclusivity. More generally, one can scan any trained actor for a state where thresholding changes the sign of any disjunctive node or makes two disjunctive nodes positive; finding a single such state is enough to show the extraction pipeline is not faithful for that actor without additional correction.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the semi-symbolic layer and neural DNF architecture on which neural DNF-MT is built."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Identifies the missing exactly-one constraint in neural DNF for multi-class output, which mutex-tanh addresses while adding probabilistic interpretation."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Defines ProbLog, the target language for extracted stochastic policies via annotated disjunctions."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the Taxi environment used in the distillation experiment."}],"review_version":1}