{"id":"7fc98839-d48b-4cf5-a1ae-88aaa1616479","arxiv_id":"2607.15459","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":4,"one_line_summary":"A trained PPO policy is distilled into an executable first-order Prolog decision list that, after exact-return expansion, can match or exceed the teacher, with certified return loss and an O(1/B) fidelity/resolution theory.","lead":"This paper rewrites a trained reinforcement-learning policy into a readable, runnable Prolog program of if-then rules, then lets small edits improve the program beyond the original network, with mathematical guarantees. It shows the approach works exactly on small gridworlds and transfers across grid sizes, while on ordinary continuous-control tasks it trades away performance to decision trees.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Continuous-conversion guarantees rest on unverified Assumption 4; deterministic PPO occupancy may be singular, so Theorem 2 and Corollary 3 need not apply.","rationale":"The reader's weakest assumption is exactly the load-bearing gap I identify: Assumption 4 is the hinge for the continuous-conversion guarantee, and it is not verified in the experiments. This is more consequential than the abstract's 'ten of ten' versus 'fifteen of fifteen' discrepancy, since it affects the validity of one of the four stated theoretical contributions for the actual PPO teachers. The paper is unusually honest about other limitations (Section 7), but it does not flag the empirical status of Assumption 4, and Figure 9's 'direct test of Theorem 2' only shows monotone fidelity, not the O(1/B) rate. The finite KeyDoor certificate and the expansion monotonicity/termination guarantees are unaffected, and the paper's own conditional framing already invites the needed verification, so the reader's CONDITIONAL verdict remains appropriate; I recommend no change.","tokens_in":36433,"tokens_out":13018,"duration_ms":138924,"concrete_test":"For each continuous teacher, collect ≥10^6 states from the deterministic greedy policy's discounted occupancy using the exact reset distribution; estimate the intrinsic support dimension (e.g., two-nearest-neighbour estimator or PCA participation ratio) and the minimum of each marginal density on the support. If the effective dimension is < d, or any marginal density vanishes on a positive-measure set, Assumption 4 is violated and Theorem 2/Corollary 3 cannot be applied to that task. A stronger check: compute the empirical disagreement rate of the cell-majority policy in L_B against the teacher for B = 2, 3, 4, 6, 8, 12; if the log-log slope of ϵ versus B is not approximately −1, or the rate plateaus before reaching noise, the claimed O(1/B) bound is not present in the actual setting.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's headline continuous guarantee — Theorem 2's O(1/B) disagreement rate (14) and Corollary 3's return recovery (18) — is conditional on Assumption 4, which the Section 6 experiments never check. Assumption 4 requires the greedy teacher π_N to be piecewise constant with finite (d−1)-Hausdorff boundary mass, and requires μ = d_π̄_T to be absolutely continuous with bounded density, compact convex support, and bi-Lipschitz marginal CDFs. In the continuous-control tasks, μ is the discounted occupancy of the deterministic greedy network under Gymnasium dynamics. If the reset distribution or dynamics concentrate reachable states on a lower-dimensional set — a genuine risk for Acrobot and for any deterministic controlled system — then μ is singular, the marginal CDFs are step functions, the probability integral transform is not bi-Lipschitz, and the tube estimate μ(T_δ) ≤ ρ_max c_d P δ that produces the 1/B rate is invalid. The reported monotone fidelity in Figure 9 does not establish the O(1/B) law, and the paper never estimates the support dimension, marginal density lower bounds, or the boundary measure P. The finite KeyDoor results and Proposition 1 are independent of this concern; the gap is specific to the continuous-conversion claims.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a three-stage post-hoc pipeline that turns a frozen PPO policy into an executable first-order Prolog decision list: extraction labels a reachable-state census (or DAgger samples), FOIL-style induction builds an ordered rule list, and an 'expand' stage hill-climbs on exact return, accepting an edit only when an exact Bellman-solve oracle certifies a return increase. The theory section proves a performance-difference return-loss bound (Theorem 1), an advantage-localized certificate (Proposition 3), monotone termination of the expansion loop (Proposition 1), exact finite-MDP computation (Proposition 2), and, under Assumption 4, an O(1/B) disagreement/return-gap conversion rate (Theorem 2, Corollary 3) with an Ω(B^{d-1}) lower bound (Proposition 4). Experiments cover an exact 16,944-state KeyDoor MDP (expanded Prolog attains exact optimal return and beats the capped teacher), MiniGrid DoorKey cross-size transfer, and CartPole/Acrobot/LunarLander continuous control with an explicit baseline comparison.","tokens_in":36729,"tokens_out":17357,"duration_ms":184810,"significance":"If the finite-MDP and relational-transfer results stand, the paper makes a meaningful contribution: it produces readable, executable artifacts with exact certificates, demonstrates monotone improvement via an exact-return oracle, and it transparently reports where the relational representation wins (DoorKey) and loses (propositional control). The exact KeyDoor certificates, the pinned reproducible pipeline, and the honest negative results are clear strengths. However, the continuous-conversion claims are conditional on a regularity assumption that is not checked in the experiments, and the lower-bound proof has a gap; the continuous part therefore needs revision before the full claim is established.","major_comments":[{"comment":"The continuous headline guarantees, Eqs. (14) and (18), are conditional on Assumption 4, but the Section 6 experiments never verify it. The discounted occupancy μ of a deterministic greedy policy under deterministic Gymnasium dynamics must be absolutely continuous with bounded density and bi-Lipschitz marginal CDFs, and the decision boundary must have finite (d-1)-Hausdorff content with a linear Minkowski-content tube bound. None of these is estimated: support dimension, marginal density lower bounds, and boundary measure P are not reported. The parenthetical in Assumption 4 asserting that 'the visitation measures of Section 6 satisfy this' is not demonstrated, and CartPole/Acrobot observation spaces are not compact boxes because velocity coordinates are unbounded. Figure 9's monotone fidelity does not establish the O(1/B) rate. Please either verify a sufficient condition on the actual t","section":"Assumption 4, Theorem 2/Corollary 3, Section 6"},{"comment":"The proof lower-bounds the disagreement rate of any cell-majority policy by c/B and shows that Ω(B^{d-1}) grid cells are crossed by the oblique hyperplane. But the theorem's conclusion — that a decision list must 'distinguish' Ω((1/ε)^{d-1}) cells and hence the cost is exponential in d — does not follow from counting cells. A single axis-aligned clause can cover many cells, and no argument is given that a short list can approximate the halfspace only with error Ω(1/B). The sentence 'each of which the optimal list must devote a distinct cell-label to' is asserted. This step is load-bearing for the abstract's 'matching lower bound' and for the interpretation of the LunarLander ceiling. A rigorous lower bound on the number of clauses in L_B, or a corrected statement (e.g., a lower bound on the number of grid cells rather than rules), is needed.","section":"Proposition 4"},{"comment":"The Acrobot rows for CART and VIPER report our-list-minus-baseline = -15.0 and -14.0 with P(improve)=0.00 and Holm-corrected p = 3.7×10^{-4}, yet the verdict column reads 'matches'. A significant negative delta in all fifteen seeds is a loss, not a match. The same inconsistency appears in the Section 7 sentence 'matches rather than beats them on Acrobot.' This does not change the overall negative-result message, but the statistical conclusion should be corrected.","section":"Table 2 and Section 7"}],"minor_comments":[{"comment":"Clauses 6 and 7 are both labeled default with empty bodies; under Definition 4 the first empty-body clause fires at every state and the second is dead. Please clarify whether the listing is abridged or the program has a redundant clause.","section":"Listing 1"},{"comment":"The R2 expanded row reports 14/15 non-vacuous seeds, while the text says 'below unity in all fifteen seeds'. Reconcile the table with the prose.","section":"Table 1"},{"comment":"The claim that the box-shaped observation spaces of Section 6 satisfy the compact-support and marginal-CDF conditions is inaccurate: CartPole and Acrobot velocity coordinates are unbounded. If the empirical support is compact in practice, say so with evidence.","section":"Assumption 4"},{"comment":"The text says held-out fidelity 'rises monotonically' with B; the curves increase overall but appear to have small non-monotonicities at low B. Please state the precise monotonicity claim or plot individual points.","section":"Figure 9"}],"recommendation":"major_revision","confidential_remarks":"The paper is worth pursuing: the finite-MDP and DoorKey parts are strong, and the exact certificates are a genuine asset. The continuous part needs either stronger verification of Assumption 4 or weaker claims, and the lower-bound proof in Proposition 4 needs a rigorous cells-to-clauses argument. The Acrobot table inconsistency should be fixed before acceptance."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Read it. The paper deserves a serious look. The genuinely new piece is the finite-MDP pipeline: a post-hoc FOIL-style induction into an executable first-order Prolog program, an exact-return expansion stage that provably improves monotonically and halts, and an advantage-gap certificate that is exact, machine-checkable, and non-vacuous in practice. That part is clean. The KeyDoor experiments are credible: 16,944 states, exact Bellman solves, fifteen seeds, optimal return in all but one capped seed. The DoorKey transfer result — a first-order list distilled on 8x8 transferring to 6x6 and 16x16 while coordinate trees collapse — is a nice empirical demonstration of the representational point.\n\nThe continuous-case theory is the soft spot. Theorem 2 and Corollary 3 give the O(1/B) fidelity and return-recovery rates, but the whole chain rests on Assumption 4: piecewise-constant teacher, finite (d−1)-Hausdorff boundary mass, absolutely continuous occupancy with bounded density and bi-Lipschitz marginals. The paper never checks any of that on CartPole, Acrobot, or LunarLander. For deterministic dynamics, occupancy can easily concentrate on low-dimensional sets; the tube estimate then fails and the 1/B law need not hold. The synthetic verification (theory/verify_resolution.py) confirms the exponents for a uniform measure, not for the actual PPO teachers. This is a conditional theorem with no condition check. I'd want the authors to estimate support dimension or density bounds, or weaken the claim.\n\nTwo smaller issues. Table 2 labels the Acrobot loss against CART/VIPER as 'matches', but the confidence intervals are [-28.2,-11.7] and [-27.6,-10.5] with P(improve)=0.00. That is a loss, not a match. The abstract says 'ten of ten seeds' while Section 6 reports fifteen; a stale copy-paste. Both easy fixes.\n\nIn proportion: the paper is honest about its negatives, explicit about what is exact and what is sampled, and the finite-MDP contribution stands on its own. The continuous part is a worthwhile conditional result, but the experiments need to verify the condition before the faithfulness claim is earned. I'd send it to review, and ask for an Assumption 4 check plus the two label fixes. If the author adds a small empirical estimate of the occupancy dimension, I'd be satisfied.","headline":"Finite-MDP part is solid and genuinely new; continuous-case guarantees rest on an unverified Assumption 4, plus two small reporting fixes (Acrobot 'matches' label, stale 'ten of ten' in abstract).","tokens_in":37231,"tokens_out":3751,"would_cite":true,"duration_ms":40384,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68T05","68N17"],"pacs":[],"model":"deepseek-v4-flash","headline":"A frozen neural policy can be rewritten as a Prolog program that plays the task as well as or better than the network.","keywords":["explainable reinforcement learning","policy distillation","Prolog","first-order logic","decision lists","return certificate","performance-difference lemma","resolution theory"],"falsifier":"Run the threshold conversion on a continuous task whose teacher has a fuzzy or stochastic decision rule (so the boundary has positive measure) or whose visited states lie on a lower-dimensional manifold; if the disagreement rate does not fall toward zero as resolution grows, or falls far slower than 1/B, Assumption 4 is violated and Theorem 2's guarantee fails. Alternatively, in the finite setting, construct an MDP where the student does not weakly dominate the teacher on disagreeing states and check whether the advantage-gap certificate remains non-vacuous; if it ever understates the exact ga","tokens_in":36295,"feed_emoji":"⚙️","tokens_out":4108,"duration_ms":38770,"temperature":0.7,"pith_summary":"The paper claims that a trained deep reinforcement learning policy can be converted after the fact into an executable, human-readable Prolog program, and that this conversion can be certified and improved. The authors prove that in a finite MDP the return lost by the distilled program is bounded by an exactly computable certificate, and that an expansion loop that accepts only edits with certified return increases improves monotonically and terminates, reaching exact optimal return on a 16,944-state task. For continuous observations they prove the threshold-rule conversion becomes arbitrarily faithful as resolution grows, with disagreement vanishing as 1/B, but the number of rules explodes as Ω(B^{d-1}) for oblique decision boundaries, which explains why high-dimensional control eludes them. If true, the work offers a path from black-box policies to auditable, editable controllers with formal guarantees.","feed_headline":"Logic program beats its own neural teacher","feed_subtitle":"Readable Prolog rules are certified and expanded to outperform the PPO policy they were distilled from.","key_machinery":"The load-bearing objects are the ordered decision list over a first-order predicate vocabulary (with a default clause, making the student a total deterministic policy); the performance-difference identity, which expresses the return gap between teacher and student as the teacher's discounted visitation integral of the advantage of the teacher's action under the student's value function; and the advantage-gap certificate, which bounds that gap by the advantage-weighted disagreement instead of the worst-case advantage. For continuous observations, the threshold decision-list class at resolution B — clauses built from quantile threshold tests on each coordinate — is the object that yields the O","core_discovery":"The central claim is that a frozen PPO policy can be distilled into an ordered first-order decision list emitted as a Prolog program, then expanded under an exact-return oracle until it matches or surpasses the network. The authors establish four formal results: a return-loss bound making the distilled program a machine-checkable certificate; an advantage-gap refinement that removes a horizon factor and is exact when the student weakly dominates the teacher; monotone termination of the expansion loop; and a resolution theory showing the propositional threshold conversion has disagreement O(1/B) and a matching Ω(B^{d-1}) lower bound on rules for an oblique boundary. Empirically the expanded p","pith_inferences":["The expansion oracle makes the rule proposer interchangeable; any source of candidate edits (including a generative model) is audited by exact policy evaluation, so the certificate is the enforcement mechanism.","The advantage-gap certificate could be applied outside this pipeline, e.g., to measure where any imitator's errors actually matter under the teacher's visitation, possibly guiding data collection in imitation learning.","The exponential lower bound suggests that for high-dimensional control, the pipeline needs relational or object-centric features to break the curse; this is testable by combining the first-order form with automatically extracted object predicates.","The O(1/B) rate should degrade visibly when the teacher's decision boundary is not piecewise smooth or when state visitation concentrates on lower-dimensional sets; a targeted experiment on such a task would directly probe Assumption 4."],"forward_implications":["Distilled policies can be certified: the exact return gap is bounded by an exactly computed quantity in finite MDPs, checked rather than estimated.","The expansion loop guarantees monotone improvement, so the symbolic student can surpass its neural teacher wherever the teacher is imperfect.","Relational clause structure gives size-generalization: a program induced on one MiniGrid layout transfers to unseen sizes, while coordinate-based trees collapse.","The resolution theory sets a limit: continuous control in high dimension cannot be faithfully converted to axis-aligned threshold rules without exponential cost, explaining the LunarLander ceiling."],"fun_headline_variants":["Prolog rules outplay the neural network they learned from","Certified Prolog program beats its own PPO teacher","Readable logic surpasses the neural teacher it distilled","Prolog program beats its own neural teacher, certified","From black box to executable logic: outperforms the teacher"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The proof that continuous conversion is arbitrarily faithful requires the teacher's decision regions to be piecewise constant with a boundary of measure zero, and the teacher's discounted state visitation to be absolutely continuous with bounded density and bi-Lipschitz marginals; if the visits concentrate on lower-dimensional sets, the guarantees lapse.","fun_headline_variants_meta":{"raw":{"variants":["Prolog rules outplay the neural network they learned from","Certified Prolog program beats its own PPO teacher","Readable logic surpasses the neural teacher it distilled","Prolog program beats its own neural teacher, certified","From black box to executable logic: outperforms the teacher"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000757,"raw_usage":{"total_tokens":3250,"prompt_tokens":845,"completion_tokens":2405,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":589,"completion_tokens_details":{"reasoning_tokens":2326}},"tokens_in":589,"tokens_out":2405,"duration_ms":16583,"temperature":1.0,"reasoning_tokens":2326,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-01T23:17:50.906224+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the threshold conversion on a continuous task whose teacher has a fuzzy or stochastic decision rule (so the boundary has positive measure) or whose visited states lie on a lower-dimensional manifold; if the disagreement rate does not fall toward zero as resolution grows, or falls far slower than 1/B, Assumption 4 is violated and Theorem 2's guarantee fails. Alternatively, in the finite setting, construct an MDP where the student does not weakly dominate the teacher on disagreeing states and check whether the advantage-gap certificate remains non-vacuous; if it ever understates the exact ga","supporting_citations":[],"review_version":1}