From Black Box to Executable Logic: Explainable Reinforcement Learning through Prolog Expert Systems

# From Black Box to Executable Logic: Explainable Reinforcement Learning through Prolog Expert Systems
Source: [https://arxiv.org/html/2607.15459](https://arxiv.org/html/2607.15459)
Eduardo C\. Garrido\-Merchán Institute of Research in Technology \(IIT\), Universidad Pontificia Comillas DIGNUM Center for AI Ethics and Data Rights Madrid, Spain ecgarrido@comillas\.edu

###### Abstract

A trained deep reinforcement learning policy is a black box, and we ask whether it can be made explainable by rewriting it as an executable logic program that reproduces its behaviour and that a person can read, a logic engine can run, and an optimizer can edit\. We present a three\-stage post\-hoc transformation that extracts a frozen proximal policy optimization teacher, induces an ordered rule list from its decisions in the manner of classical relational learning, and emits the result as a Prolog program whose every decision is executed by an off\-the\-shelf logic engine; a subsequent expansion stage edits the rule base and accepts an edit only when policy evaluation certifies a return increase\. We prove four guarantees\. A return\-loss bound makes the distilled program a machine\-checkable certificate in a finite Markov decision process, and the expansion loop improves monotonically and terminates\. For the continuous\-observation setting we answer whether the conversion is possible at all: the propositional threshold instantiation converts the network to arbitrary fidelity as the resolutionBBgrows, with disagreementO​\(1/B\)O\(1/B\)and a return gap that closes at the same rate, and a matching lower bound shows the cost is exponential in the observation dimension,Ω​\(Bd−1\)\\Omega\(B^\{d\-1\}\)rules for an oblique decision boundary\. Empirically, on a two\-room key\-and\-door task with16,94416\{,\}944reachable states the expanded Prolog program attains exact optimal return in every seed and, in a budget\-capped regime, exceeds the stochastic teacher on exact return in ten of ten seeds\. On three continuous\-control tasks the emitted program substitutes the network, matching the neural teacher within noise on Acrobot with eleven clauses and recovering about97%97\\%of its return on CartPole, while on the finer\-control LunarLander it recovers only partially, exactly the ceiling the exponential lower bound predicts\.

## 1Introduction

A trained deep reinforcement learning policy is a dense numerical object, and the practical question of what it has learned is usually answered indirectly, through saliency maps, surrogate scores, or counterfactual probes, none of which yields an artefact one can read, execute, and edit\. The oldest form of artificial intelligence offers a different kind of answer\. A symbolic expert system states its behaviour as a set of rules that a human can inspect and a logic engine can run, and recent work has shown that the two traditions can be brought into contact, with large language models used to draft the rule bases of classical expert systems\(Garrido\-Merchán and Puente,[2025](https://arxiv.org/html/2607.15459#bib.bib7)\)\. This paper takes the converse direction inside reinforcement learning: rather than write the rules by hand or by prompting, we recover them from a trained neural policy, and we ask how far the recovered symbolic program can be pushed\. The object we produce is not a heat map or an approximate score but a Prolog program that plays the task, and the question we answer is whether such a program can be made to match or surpass the network it was distilled from\.

Three properties distinguish the artefact we target\. First, the extraction is post\-hoc: the teacher is any frozen policy, here a proximal policy optimization agent\(Schulman et al\.,[2017](https://arxiv.org/html/2607.15459#bib.bib17)\), and nothing in its training is modified to make it interpretable\. Second, the student is an executable first\-order logic program, an ordered list of clauses over a predicate vocabulary that runs unchanged under SWI\-Prolog\(Wielemaker et al\.,[2012](https://arxiv.org/html/2607.15459#bib.bib23)\), rather than a propositional decision tree or a fitted scoring function\. Third, the pipeline does not stop at imitation\. Once the rule base exists, a return\-maximizing expansion stage edits it and keeps only the edits that a policy\-evaluation oracle certifies to raise the return, so the symbolic student can move away from the teacher wherever the teacher was wrong\.

We make three contributions\. The first is the transformation pipeline itself, comprising an extraction stage that queries the frozen teacher’s greedy action over the full reachable state census and over its own visitation, an induction stage that greedily grows an ordered first\-order rule list in the manner of the FOIL algorithm\(Quinlan,[1990](https://arxiv.org/html/2607.15459#bib.bib15)\), and an expansion stage that hill climbs on the exact return over the space of rule\-base edits\. The second is a theoretical account\. We prove a return\-loss bound: the return lost by replacing the greedy teacher with the distilled program is at most2​Rmax​ϵ†/\(1−γ\)22R\_\{\\max\}\\epsilon^\{\\dagger\}/\(1\-\\gamma\)^\{2\}, whereϵ†\\epsilon^\{\\dagger\}is the disagreement rate weighted by the teacher’s discounted visitation, and we show that in a finite Markov decision process this inequality becomes a machine\-checkable certificate because both of its sides are computed exactly by solving linear systems\. We prove in addition that the expansion loop improves the return monotonically and halts\. For the continuous\-observation setting we answer whether the conversion is possible in principle: the propositional threshold instantiation converts the network to arbitrary fidelity as the resolution grows, with disagreement and return gap both closing at rateO​\(1/B\)O\(1/B\), and this conversion obeys a curse of dimensionality that we make precise as anΩ​\(Bd−1\)\\Omega\(B^\{d\-1\}\)lower bound on the number of rules an oblique decision boundary forces on any axis\-aligned rule list\. The third contribution is an experimental study on a two\-room key\-and\-door environment small enough to admit exact policy evaluation, in which the expanded Prolog program reaches exact optimal return in every seed of both a converged and a budget\-capped teacher regime, and in the capped regime exceeds the stochastic teacher on exact return in ten of ten seeds by a mean paired margin of0\.1000\.100with a95%95\\%confidence interval of\[0\.096,0\.104\]\[0\.096,0\.104\]\. We then show that the same pipeline, run in its propositional form on three continuous\-control tasks where the census gives way to a DAgger loop\(Ross et al\.,[2011](https://arxiv.org/html/2607.15459#bib.bib16)\)and exact evaluation to Monte Carlo, produces a Prolog program that substitutes the network on CartPole and Acrobot and recovers it only partially on the finer\-control LunarLander, which both demonstrates that the transformation scales past the enumerable regime and marks where the propositional student’s precision runs out\. We report throughout the interquartile mean with stratified bootstrap intervals in the manner ofAgarwal et al\. \([2021](https://arxiv.org/html/2607.15459#bib.bib1)\), and we are explicit about what the data do not support, including the vacuity of the return\-loss certificate at the discount factor we use and the absence of a statistically significant separation between the distilled and the expanded program after correction for multiple comparisons\.

## 2Related work

The distillation of a trained policy into an interpretable surrogate is by now a mature line\. VIPER extracts a decision tree from a deep Q\-network with a DAgger\-style procedure and proves a return bound for the tree student\(Bastani et al\.,[2018](https://arxiv.org/html/2607.15459#bib.bib2)\); programmatically interpretable reinforcement learning searches a domain\-specific program space guided by a neural oracle\(Verma et al\.,[2018](https://arxiv.org/html/2607.15459#bib.bib21)\), and its imitation\-projected successor casts the search as mirror descent\(Verma et al\.,[2019](https://arxiv.org/html/2607.15459#bib.bib22)\)\. Linear model U\-trees fit piecewise\-linear trees to a network’s behaviour\(Liu et al\.,[2018](https://arxiv.org/html/2607.15459#bib.bib13)\), and more recent work distils policies into editable programmatic trees and studies when they can be corrected by hand\(Kohler et al\.,[2024](https://arxiv.org/html/2607.15459#bib.bib10)\)\. Our extraction and induction stages sit squarely in this tradition, and Theorem[1](https://arxiv.org/html/2607.15459#Thmtheorem1)is the decision\-list analogue of the VIPER tree bound, with the difference that in our finite setting the error rate is computed exactly rather than estimated\. The classical reduction of imitation to no\-regret online learning\(Ross et al\.,[2011](https://arxiv.org/html/2607.15459#bib.bib16)\)is the tool that would replace our exhaustive census once the state space is too large to enumerate\.

The target language separates our work from most of this line\. A parallel body of research learns first\-order logic policies directly, either by training a differentiable inductive logic layer\(Jiang and Luo,[2019](https://arxiv.org/html/2607.15459#bib.bib8)\), by guiding symbolic rule search with a pretrained neural agent\(Delfosse et al\.,[2023](https://arxiv.org/html/2607.15459#bib.bib4)\), by inventing explanatory predicates in games\(Sha et al\.,[2024](https://arxiv.org/html/2607.15459#bib.bib18)\), or by blending symbolic and neural policies in a single trainable model\(Shindo et al\.,[2025](https://arxiv.org/html/2607.15459#bib.bib19)\); concept\-bottleneck agents align a policy to object\-centric concepts for the same interpretability end\(Delfosse et al\.,[2024](https://arxiv.org/html/2607.15459#bib.bib5)\)\. These methods train the logic, whereas we extract it post\-hoc from a fixed neural teacher\. The closest post\-hoc work synthesises set\-valued propositional rules from a reinforcement learning policy and refines them in the environment\(Coppens et al\.,[2021](https://arxiv.org/html/2607.15459#bib.bib3)\); our student is a first\-order, executable Prolog program rather than a propositional rule set, and our expansion stage optimizes exact return rather than repairing fidelity\. The observation that symbolic policies can outperform deep networks has been made for symbolic regression of closed\-form controllers\(Landajuela et al\.,[2021](https://arxiv.org/html/2607.15459#bib.bib12)\), and finite\-state controllers have been extracted from recurrent policies\(Koul et al\.,[2019](https://arxiv.org/html/2607.15459#bib.bib11)\), but neither closes the loop in which an extracted logic program is expanded past its own teacher\. Relational reinforcement learning\(Dzeroski et al\.,[2001](https://arxiv.org/html/2607.15459#bib.bib6)\)is the intellectual ancestor of the first\-order representation we use, and the recent survey of explainable reinforcement learning\(Milani et al\.,[2024](https://arxiv.org/html/2607.15459#bib.bib14)\)places the entire distillation family in context and leaves the post\-hoc first\-order executable cell that our method occupies essentially open\.

## 3Problem setting

We work in the infinite\-horizon discounted setting with a finite state and action space\. All results in this paper rest on the following assumption, which we reference by number throughout\.

###### Assumption 1\(Finite discounted MDP with bounded reward\)\.

The environment is a Markov decision processM=\(𝒮,𝒜,P,r,γ,μ0\)M=\(\\mathcal\{S\},\\mathcal\{A\},P,r,\\gamma,\\mu\_\{0\}\)in which the state space𝒮\\mathcal\{S\}and the action space𝒜\\mathcal\{A\}are finite,P\(⋅∣s,a\)P\(\\cdot\\mid s,a\)is a probability distribution on𝒮\\mathcal\{S\}for every pair\(s,a\)∈𝒮×𝒜\(s,a\)\\in\\mathcal\{S\}\\times\\mathcal\{A\}, the reward functionr:𝒮×𝒜→ℝr\\colon\\mathcal\{S\}\\times\\mathcal\{A\}\\to\\mathbb\{R\}satisfies\|r​\(s,a\)\|≤Rmax\|r\(s,a\)\|\\leq R\_\{\\max\}for a known constantRmax<∞R\_\{\\max\}<\\infty, the discount factor satisfiesγ∈\(0,1\)\\gamma\\in\(0,1\), andμ0\\mu\_\{0\}is a probability distribution on𝒮\\mathcal\{S\}from which the initial state is drawn\.

A*stationary policy*is a mapπ:𝒮→Δ​\(𝒜\)\\pi\\colon\\mathcal\{S\}\\to\\Delta\(\\mathcal\{A\}\), whereΔ​\(𝒜\)\\Delta\(\\mathcal\{A\}\)denotes the set of probability distributions on𝒜\\mathcal\{A\}; we writeπ​\(a∣s\)\\pi\(a\\mid s\)for the probability thatπ\\piselects actionaain statess\. A*deterministic policy*is a mapπ:𝒮→𝒜\\pi\\colon\\mathcal\{S\}\\to\\mathcal\{A\}, identified with the stationary policy that puts all mass onπ​\(s\)\\pi\(s\)\. Given a policyπ\\pi, the process\(st,at\)t≥0\(s\_\{t\},a\_\{t\}\)\_\{t\\geq 0\}withs0∼μ0s\_\{0\}\\sim\\mu\_\{0\},at∼π\(⋅∣st\)a\_\{t\}\\sim\\pi\(\\cdot\\mid s\_\{t\}\), andst\+1∼P\(⋅∣st,at\)s\_\{t\+1\}\\sim P\(\\cdot\\mid s\_\{t\},a\_\{t\}\)is the trajectory distribution induced byπ\\pi, and we writePrμ0π\\Pr^\{\\pi\}\_\{\\mu\_\{0\}\}and𝔼μ0π\\mathbb\{E\}^\{\\pi\}\_\{\\mu\_\{0\}\}for probabilities and expectations under it\.

###### Definition 1\(Value functions and return\)\.

Under Assumption[1](https://arxiv.org/html/2607.15459#Thmassumption1), the*state value function*of a policyπ\\piis

Vπ​\(s\)=𝔼π​\[∑t=0∞γt​r​\(st,at\)\|s0=s\],V^\{\\pi\}\(s\)=\\mathbb\{E\}^\{\\pi\}\\Biggl\[\\,\\sum\_\{t=0\}^\{\\infty\}\\gamma^\{t\}r\(s\_\{t\},a\_\{t\}\)\\,\\Bigm\|\\,s\_\{0\}=s\\Biggr\],the*action value function*is

Qπ​\(s,a\)=r​\(s,a\)\+γ​∑s′∈𝒮P​\(s′∣s,a\)​Vπ​\(s′\),Q^\{\\pi\}\(s,a\)=r\(s,a\)\+\\gamma\\sum\_\{s^\{\\prime\}\\in\\mathcal\{S\}\}P\(s^\{\\prime\}\\mid s,a\)\\,V^\{\\pi\}\(s^\{\\prime\}\),and the*advantage function*isAπ​\(s,a\)=Qπ​\(s,a\)−Vπ​\(s\)A^\{\\pi\}\(s,a\)=Q^\{\\pi\}\(s,a\)\-V^\{\\pi\}\(s\)\. The*return*ofπ\\piisJ​\(π\)=𝔼s∼μ0​\[Vπ​\(s\)\]J\(\\pi\)=\\mathbb\{E\}\_\{s\\sim\\mu\_\{0\}\}\[V^\{\\pi\}\(s\)\]\.

The series definingVπV^\{\\pi\}converges absolutely because\|r​\(st,at\)\|≤Rmax\|r\(s\_\{t\},a\_\{t\}\)\|\\leq R\_\{\\max\}andγ∈\(0,1\)\\gamma\\in\(0,1\), and the geometric\-series bound yields

\|Vπ​\(s\)\|≤Rmax1−γ,\|Qπ​\(s,a\)\|≤Rmax1−γ,\|Aπ​\(s,a\)\|≤2​Rmax1−γ\|V^\{\\pi\}\(s\)\|\\leq\\frac\{R\_\{\\max\}\}\{1\-\\gamma\},\\qquad\|Q^\{\\pi\}\(s,a\)\|\\leq\\frac\{R\_\{\\max\}\}\{1\-\\gamma\},\\qquad\|A^\{\\pi\}\(s,a\)\|\\leq\\frac\{2R\_\{\\max\}\}\{1\-\\gamma\}\(1\)for everyπ\\pi,ss, andaa\. The bound onAπA^\{\\pi\}follows from the triangle inequality applied to the definitionAπ=Qπ−VπA^\{\\pi\}=Q^\{\\pi\}\-V^\{\\pi\}\. The ranges in \([1](https://arxiv.org/html/2607.15459#S3.E1)\) supply the constants in Theorem[1](https://arxiv.org/html/2607.15459#Thmtheorem1)and Proposition[1](https://arxiv.org/html/2607.15459#Thmproposition1)\.

###### Definition 2\(Teacher and argmax teacher\)\.

The*teacher*πT\\pi\_\{T\}is a fixed stochastic stationary policy, in our experiments the softmax policy of a converged or budget\-capped PPO agent\(Schulman et al\.,[2017](https://arxiv.org/html/2607.15459#bib.bib17)\), frozen after training\. Fix a total order on𝒜\\mathcal\{A\}\. The*argmax action*of the teacher at statessis

aT​\(s\)=min⁡\{a∈𝒜:πT​\(a∣s\)=maxa′∈𝒜⁡πT​\(a′∣s\)\},a\_\{T\}\(s\)=\\min\\Bigl\\\{a\\in\\mathcal\{A\}:\\pi\_\{T\}\(a\\mid s\)=\\max\_\{a^\{\\prime\}\\in\\mathcal\{A\}\}\\pi\_\{T\}\(a^\{\\prime\}\\mid s\)\\Bigr\\\},the minimum taken with respect to the fixed order on𝒜\\mathcal\{A\}, so that ties are broken deterministically\. The*argmax teacher*is the deterministic policyπ¯T​\(s\)=aT​\(s\)\\bar\{\\pi\}\_\{T\}\(s\)=a\_\{T\}\(s\)\.

Throughout the paper the imitation target of the distillation stage is the argmax teacherπ¯T\\bar\{\\pi\}\_\{T\}, not the stochastic policyπT\\pi\_\{T\}\. This convention is stated once here and used consistently: the student is trained to reproduceaT​\(s\)a\_\{T\}\(s\), the return\-loss bound of Theorem[1](https://arxiv.org/html/2607.15459#Thmtheorem1)is stated againstJ​\(π¯T\)J\(\\bar\{\\pi\}\_\{T\}\), and the gapJ​\(πT\)−J​\(π¯T\)J\(\\pi\_\{T\}\)\-J\(\\bar\{\\pi\}\_\{T\}\)between the stochastic teacher and its argmax counterpart is a separate, sign\-indefinite quantity that we compute exactly rather than bound \(Corollary[1](https://arxiv.org/html/2607.15459#Thmcorollary1)and Proposition[2](https://arxiv.org/html/2607.15459#Thmproposition2)\)\.

We now define the student class\. The student is an ordered list of first\-order clauses over a fixed predicate vocabulary, executed with decision\-list semantics and emitted as a Prolog program\.

###### Definition 3\(Predicate vocabulary and grounded literals\)\.

A*predicate vocabulary*is a finite set𝒫=\{p1,…,pn\}\\mathcal\{P\}=\\\{p\_\{1\},\\dots,p\_\{n\}\\\}of predicate symbols, eachpip\_\{i\}with an arityki≥0k\_\{i\}\\geq 0and, for each argument position, a finite argument domain \(in our instantiation, object constants such askey\\mathrm\{key\},door\\mathrm\{door\},goal\\mathrm\{goal\}and direction constants such asup\\mathrm\{up\},down\\mathrm\{down\},left\\mathrm\{left\},right\\mathrm\{right\}\), together with an*interpretation map*that assigns to every states∈𝒮s\\in\\mathcal\{S\}and every tuple of arguments drawn from the argument domains a truth value\. An*atom*is an expressionpi​\(u1,…,uki\)p\_\{i\}\(u\_\{1\},\\dots,u\_\{k\_\{i\}\}\)whose argumentsuju\_\{j\}are constants from the corresponding domains or variables; a*literal*is an atom or a negated atom\. A*grounding*of a set of literals is a substitution of constants for all of its variables; a grounding is*satisfied*in statesswhen every positive literal evaluates to true and every negated literal evaluates to false under the interpretation map atss\.

###### Definition 4\(Ordered decision list and student class\)\.

A*clause*is a pairc=\(B,α\)c=\(B,\\alpha\)in which the bodyBBis a finite conjunction of literals over the vocabulary𝒫\\mathcal\{P\}and the headα\\alphais either a constant action in𝒜\\mathcal\{A\}or an action term containing variables that also appear inBB\. An*ordered decision list*is a finite sequenceL=\(c1,…,cm,cdef\)L=\(c\_\{1\},\\dots,c\_\{m\},c\_\{\\mathrm\{def\}\}\)of clauses whose last elementcdefc\_\{\\mathrm\{def\}\}, the*default clause*, has an empty body and a constant action head\. The listLLdefines a policyπL\\pi\_\{L\}as follows\. Fix a total order on the finite set of groundings of each clause body \(in the executable program, the order in which SLD resolution enumerates solutions\)\. At statess, letcjc\_\{j\}be the first clause in the list whose body admits a satisfied grounding atss, letσ\\sigmabe the first satisfied grounding of its body, and setπL​\(s\)\\pi\_\{L\}\(s\)to the action obtained by applyingσ\\sigmato the head ofcjc\_\{j\}\. The*student class*Πℒ\\Pi\_\{\\mathcal\{L\}\}is the set of all policiesπL\\pi\_\{L\}representable by ordered decision lists over𝒫\\mathcal\{P\}\.

Because the default clause has an empty body, it admits the empty grounding at every state, so some clause fires at everyss; because the first firing clause and its first satisfied grounding are determined by the fixed orders, the firing clause selects a unique action\. Consequently everyπL∈Πℒ\\pi\_\{L\}\\in\\Pi\_\{\\mathcal\{L\}\}is a total deterministic policy, andΠℒ\\Pi\_\{\\mathcal\{L\}\}is a subset of the set𝒜𝒮\\mathcal\{A\}^\{\\mathcal\{S\}\}of deterministic policies\. The results below use only this property; the first\-order structure ofΠℒ\\Pi\_\{\\mathcal\{L\}\}matters for compactness and interpretability, not for the validity of the bounds\. In the algorithmic sections the generic symbolπS\\pi\_\{S\}denotes the deterministic student, and in all instantiationsπS∈Πℒ\\pi\_\{S\}\\in\\Pi\_\{\\mathcal\{L\}\}\.

###### Definition 5\(Discounted occupancy measure\)\.

Under Assumption[1](https://arxiv.org/html/2607.15459#Thmassumption1), the*normalized discounted occupancy measure*of a policyπ\\piis the probability distribution on𝒮\\mathcal\{S\}given by

dπ​\(s\)=\(1−γ\)​∑t=0∞γt​Prμ0π⁡\(st=s\)\.d^\{\\pi\}\(s\)=\(1\-\\gamma\)\\sum\_\{t=0\}^\{\\infty\}\\gamma^\{t\}\\,\\Pr^\{\\pi\}\_\{\\mu\_\{0\}\}\(s\_\{t\}=s\)\.

The prefactor\(1−γ\)\(1\-\\gamma\)normalizes the geometric series, so∑sdπ​\(s\)=1\\sum\_\{s\}d^\{\\pi\}\(s\)=1and expressions of the form𝔼s∼dπ​\[f​\(s\)\]\\mathbb\{E\}\_\{s\\sim d^\{\\pi\}\}\[f\(s\)\]are ordinary expectations\. The occupancy measure weights states by how often, in discounted terms, the policyπ\\pivisits them fromμ0\\mu\_\{0\}; it is the correct measure under which to count imitation errors, because the performance\-difference identity of Lemma[1](https://arxiv.org/html/2607.15459#Thmlemma1)integrates advantages precisely against it\.

###### Definition 6\(Disagreement rates\)\.

LetπS\\pi\_\{S\}be a deterministic student policy\. The*disagreement rate under the stochastic teacher*is

ϵ=Prs∼dπT⁡\[πS​\(s\)≠aT​\(s\)\]=∑s∈𝒮dπT​\(s\)​1​\[πS​\(s\)≠aT​\(s\)\],\\epsilon=\\Pr\_\{s\\sim d^\{\\pi\_\{T\}\}\}\\bigl\[\\pi\_\{S\}\(s\)\\neq a\_\{T\}\(s\)\\bigr\]=\\sum\_\{s\\in\\mathcal\{S\}\}d^\{\\pi\_\{T\}\}\(s\)\\,\\mathbf\{1\}\\bigl\[\\pi\_\{S\}\(s\)\\neq a\_\{T\}\(s\)\\bigr\],and the*disagreement rate under the argmax teacher*is

ϵ†=Prs∼dπ¯T⁡\[πS​\(s\)≠aT​\(s\)\]=∑s∈𝒮dπ¯T​\(s\)​1​\[πS​\(s\)≠aT​\(s\)\],\\epsilon^\{\\dagger\}=\\Pr\_\{s\\sim d^\{\\bar\{\\pi\}\_\{T\}\}\}\\bigl\[\\pi\_\{S\}\(s\)\\neq a\_\{T\}\(s\)\\bigr\]=\\sum\_\{s\\in\\mathcal\{S\}\}d^\{\\bar\{\\pi\}\_\{T\}\}\(s\)\\,\\mathbf\{1\}\\bigl\[\\pi\_\{S\}\(s\)\\neq a\_\{T\}\(s\)\\bigr\],where𝟏​\[⋅\]\\mathbf\{1\}\[\\cdot\]denotes the indicator function\.

Both rates measure the same event, disagreement with the argmax actionaT​\(s\)a\_\{T\}\(s\), under two different visitation measures\. The rateϵ†\\epsilon^\{\\dagger\}is the quantity that enters the return\-loss bound of Theorem[1](https://arxiv.org/html/2607.15459#Thmtheorem1), because the bound comparesπS\\pi\_\{S\}with the deterministic targetπ¯T\\bar\{\\pi\}\_\{T\}and the performance\-difference identity then integrates againstdπ¯Td^\{\\bar\{\\pi\}\_\{T\}\}\. The rateϵ\\epsilonis the fidelity statistic most natural to report against the deployed stochastic teacher\. In the finite setting of Assumption[1](https://arxiv.org/html/2607.15459#Thmassumption1)with a known model, both are computed exactly by the census \(Proposition[2](https://arxiv.org/html/2607.15459#Thmproposition2)\), so no change\-of\-measure or concentrability argument is needed to relate them: the experiments report both numbers\.

## 4Extraction, induction, and expansion

The pipeline maps a frozen teacher policyπT\\pi\_\{T\}to an executable logic program in three stages, whose formal guarantees are the subject of Section[5](https://arxiv.org/html/2607.15459#S5)and whose interfaces to those guarantees are the visitation measures and disagreement rates of Section[3](https://arxiv.org/html/2607.15459#S3)\. Figure[1](https://arxiv.org/html/2607.15459#S4.F1)summarizes the flow of artefacts\.

The extraction stage records what the teacher does\. Under the model access of Assumption[3](https://arxiv.org/html/2607.15459#Thmassumption3)the reachable set𝒮r\\mathcal\{S\}\_\{\\mathrm\{r\}\}is enumerated once, and the teacher’s greedy actionaT​\(s\)a\_\{T\}\(s\)of Definition[2](https://arxiv.org/html/2607.15459#Thmdefinition2)is queried at every reachable state, producing a complete census of the target policyπ¯T\\bar\{\\pi\}\_\{T\}\. The same rollouts that estimate the teacher’s discounted visitationdπTd^\{\\pi\_\{T\}\}are retained, because the induction stage weights states by visitation and the two disagreement rates of Definition[6](https://arxiv.org/html/2607.15459#Thmdefinition6)are reported against both the census measure and the visitation measure\. The census is the finite\-state instrument that replaces the sampling of a DAgger loop\(Ross et al\.,[2011](https://arxiv.org/html/2607.15459#bib.bib16)\): because every reachable state is labelled, the induction stage never queries the teacher off its own distribution, and the disagreement rate that enters the return\-loss bound is exact\.

The induction stage grows an ordered decision list of the class in Definition[4](https://arxiv.org/html/2607.15459#Thmdefinition4)\. Following the greedy set\-covering strategy of FOIL\(Quinlan,[1990](https://arxiv.org/html/2607.15459#bib.bib15)\), the algorithm repeatedly selects the action head and the conjunction of literals that best separate the states still labelled by the teacher, scoring a candidate clause by the product of its coverage and its precision under the visitation weights, specializing a clause by adding up to three literals from the predicate vocabulary, and admitting the shared direction variable that lets a single clause such asact​\(s,move​\(D\)\)←dir​\_​to​\(s,key,D\)\\mathrm\{act\}\(s,\\mathrm\{move\}\(D\)\)\\leftarrow\\mathrm\{dir\\\_to\}\(s,\\mathrm\{key\},D\)ground to whichever compass action points along the path to the key\. The list is closed with a default clause set to the teacher’s most frequent residual action, which by the argument following Definition[4](https://arxiv.org/html/2607.15459#Thmdefinition4)makes the induced policy total and deterministic\. The result is written to disk as a Prolog program: a perception layer defines the state predicates, a tabled breadth\-first search computes the path\-aware direction predicate while respecting walls and the locked door, and the decision list is compiled to clauses with a first\-match cut discipline so that the first applicable rule fires exactly as the decision\-list semantics prescribe\. The program is executable input to SWI\-Prolog\(Wielemaker et al\.,[2012](https://arxiv.org/html/2607.15459#bib.bib23)\), and at run time we assert on a sample of states that the Prolog engine and the reference evaluator select identical actions, so the artefact we analyse and the artefact we execute are the same policy\.

The expansion stage improves the program\. It hill climbs over rule\-base edits, adding a specialized clause at a chosen position, reordering clauses, or pruning a clause other than the default, and it accepts an edit only when the exact return of Definition[1](https://arxiv.org/html/2607.15459#Thmdefinition1)increases by at least a marginτ\\tau\. The exact return is available because the environment is a finite Markov decision process with a known model, so the acceptance test solves one linear system rather than averaging noisy rollouts, and Proposition[1](https://arxiv.org/html/2607.15459#Thmproposition1)shows the loop improves monotonically and terminates\. Because the acceptance criterion is return, not fidelity, an accepted edit can move the student away from the teacher on states the teacher visits rarely, and this is precisely the mechanism by which the symbolic student surpasses the network that produced it\.

PPO teacherπT\\pi\_\{T\}\(frozen\)Extractcensus\+\+dπTd^\{\\pi\_\{T\}\}InduceFOIL rule listProlog program\.plExpandexact\-JJhill climbexactJJvia Bellman solve\(I−γ​Pπ\)​v=rπ\(I\-\\gamma P\_\{\\pi\}\)v=r\_\{\\pi\}

DAKGA agentK keyD locked doorG goal

Figure 1:Above, the transformation pipeline: a frozen PPO teacher is censused and rolled out, a FOIL\-style ordered rule list is induced and emitted as an executable Prolog program, and an expansion loop edits the program, accepting an edit only when an exact\-return oracle certifies an increase\. Below, the KeyDoor environment: the agent must fetch the key in the left room and open the locked door before it can reach the goal in the right room\. Colours encode the semantic roles used in every figure, with the teacher in ink, the distilled student in grey, and the expanded student in gold\.
## 5Theory

We now state the guarantees\. The first bounds the return the distilled program forfeits relative to the greedy teacher\. The second shows the expansion loop is well behaved\. The third turns the first into a certificate that is checked, not merely asserted, on every run of the experiments\. The fourth answers, for the continuous\-observation setting of the later experiments, the question of whether a neural policy can be converted into a threshold\-rule expert system at all: it establishes that the conversion is arbitrarily faithful as the resolution grows, that the return gap then closes, and that the cost of doing so is exponential in the observation dimension\.

We now bound the return lost by replacing the argmax teacher with the distilled student\. The strategy is the standard one for imitation\-style guarantees, instantiated for a deterministic logic\-program student and, in our finite setting, with an exactly computable error rate rather than an estimated one\. The single technical ingredient is the performance\-difference lemma ofKakade and Langford \([2002](https://arxiv.org/html/2607.15459#bib.bib9)\): the return gap between two policies equals the discounted aggregate of the advantages of one policy’s actions measured under the other policy’s value function and occupancy\. On states where the student reproduces the argmax action the advantage of the teacher’s action under the student’s own value function vanishes, because the advantage of a deterministic policy’s own action is identically zero; on the remaining states the advantage is bounded by the range \([1](https://arxiv.org/html/2607.15459#S3.E1)\)\. The disagreement rateϵ†\\epsilon^\{\\dagger\}of Definition[6](https://arxiv.org/html/2607.15459#Thmdefinition6)then converts the pointwise bound into the final estimate\. The only subtlety is the choice of imitation target: we compare the student with the deterministic argmax teacherπ¯T\\bar\{\\pi\}\_\{T\}of Definition[2](https://arxiv.org/html/2607.15459#Thmdefinition2), and we account for the stochastic teacher separately in Corollary[1](https://arxiv.org/html/2607.15459#Thmcorollary1), because the gapJ​\(πT\)−J​\(π¯T\)J\(\\pi\_\{T\}\)\-J\(\\bar\{\\pi\}\_\{T\}\)is sign\-indefinite in general and is computed exactly by the census of Proposition[2](https://arxiv.org/html/2607.15459#Thmproposition2)\.

We first state and prove the performance\-difference lemma in the form we use\. The result is due toKakade and Langford \([2002](https://arxiv.org/html/2607.15459#bib.bib9)\); we include the short telescoping proof to keep the paper self\-contained and because the certificate of Proposition[2](https://arxiv.org/html/2607.15459#Thmproposition2)checks this identity numerically\.

###### Lemma 1\(Performance\-difference lemma,Kakade and Langford,[2002](https://arxiv.org/html/2607.15459#bib.bib9)\)\.

Let Assumption[1](https://arxiv.org/html/2607.15459#Thmassumption1)hold, and letπ\\piandπ′\\pi^\{\\prime\}be stationary policies\. Then

J​\(π\)−J​\(π′\)=11−γ​𝔼s∼dπ​𝔼a∼π\(⋅∣s\)​\[Aπ′​\(s,a\)\]\.J\(\\pi\)\-J\(\\pi^\{\\prime\}\)=\\frac\{1\}\{1\-\\gamma\}\\,\\mathbb\{E\}\_\{s\\sim d^\{\\pi\}\}\\,\\mathbb\{E\}\_\{a\\sim\\pi\(\\cdot\\mid s\)\}\\bigl\[A^\{\\pi^\{\\prime\}\}\(s,a\)\\bigr\]\.\(2\)

###### Proof\.

Let\(st,at\)t≥0\(s\_\{t\},a\_\{t\}\)\_\{t\\geq 0\}be the trajectory process induced byπ\\pifroms0∼μ0s\_\{0\}\\sim\\mu\_\{0\}\. SinceJ​\(π′\)=𝔼s0∼μ0​\[Vπ′​\(s0\)\]J\(\\pi^\{\\prime\}\)=\\mathbb\{E\}\_\{s\_\{0\}\\sim\\mu\_\{0\}\}\[V^\{\\pi^\{\\prime\}\}\(s\_\{0\}\)\]by Definition[1](https://arxiv.org/html/2607.15459#Thmdefinition1), we may write the gap as

J​\(π\)−J​\(π′\)\\displaystyle J\(\\pi\)\-J\(\\pi^\{\\prime\}\)=𝔼μ0π​\[∑t=0∞γt​r​\(st,at\)\]−𝔼μ0π​\[Vπ′​\(s0\)\]\\displaystyle=\\mathbb\{E\}^\{\\pi\}\_\{\\mu\_\{0\}\}\\Biggl\[\\,\\sum\_\{t=0\}^\{\\infty\}\\gamma^\{t\}r\(s\_\{t\},a\_\{t\}\)\\Biggr\]\-\\mathbb\{E\}^\{\\pi\}\_\{\\mu\_\{0\}\}\\bigl\[V^\{\\pi^\{\\prime\}\}\(s\_\{0\}\)\\bigr\]=𝔼μ0π​\[∑t=0∞γt​\(r​\(st,at\)\+γ​Vπ′​\(st\+1\)−Vπ′​\(st\)\)\]\.\\displaystyle=\\mathbb\{E\}^\{\\pi\}\_\{\\mu\_\{0\}\}\\Biggl\[\\,\\sum\_\{t=0\}^\{\\infty\}\\gamma^\{t\}\\Bigl\(r\(s\_\{t\},a\_\{t\}\)\+\\gamma V^\{\\pi^\{\\prime\}\}\(s\_\{t\+1\}\)\-V^\{\\pi^\{\\prime\}\}\(s\_\{t\}\)\\Bigr\)\\Biggr\]\.The second equality holds because the added terms telescope: the partial sum∑t=0Tγt​\(γ​Vπ′​\(st\+1\)−Vπ′​\(st\)\)\\sum\_\{t=0\}^\{T\}\\gamma^\{t\}\\bigl\(\\gamma V^\{\\pi^\{\\prime\}\}\(s\_\{t\+1\}\)\-V^\{\\pi^\{\\prime\}\}\(s\_\{t\}\)\\bigr\)equalsγT\+1​Vπ′​\(sT\+1\)−Vπ′​\(s0\)\\gamma^\{T\+1\}V^\{\\pi^\{\\prime\}\}\(s\_\{T\+1\}\)\-V^\{\\pi^\{\\prime\}\}\(s\_\{0\}\), and the boundary termγT\+1​Vπ′​\(sT\+1\)\\gamma^\{T\+1\}V^\{\\pi^\{\\prime\}\}\(s\_\{T\+1\}\)vanishes asT→∞T\\to\\inftyby the value bound \([1](https://arxiv.org/html/2607.15459#S3.E1)\) andγ<1\\gamma<1; the interchange of limit and expectation is justified by dominated convergence, the summands being uniformly bounded by\(Rmax\+\(1\+γ\)​Rmax/\(1−γ\)\)​γt\(R\_\{\\max\}\+\(1\+\\gamma\)R\_\{\\max\}/\(1\-\\gamma\)\)\\gamma^\{t\}, a summable envelope\. Next, conditioning each term on\(st,at\)\(s\_\{t\},a\_\{t\}\)and using the Markov property,

𝔼μ0π​\[Vπ′​\(st\+1\)∣st,at\]=∑s′∈𝒮P​\(s′∣st,at\)​Vπ′​\(s′\),\\mathbb\{E\}^\{\\pi\}\_\{\\mu\_\{0\}\}\\bigl\[V^\{\\pi^\{\\prime\}\}\(s\_\{t\+1\}\)\\mid s\_\{t\},a\_\{t\}\\bigr\]=\\sum\_\{s^\{\\prime\}\\in\\mathcal\{S\}\}P\(s^\{\\prime\}\\mid s\_\{t\},a\_\{t\}\)\\,V^\{\\pi^\{\\prime\}\}\(s^\{\\prime\}\),so that, by the definition ofQπ′Q^\{\\pi^\{\\prime\}\}in Definition[1](https://arxiv.org/html/2607.15459#Thmdefinition1),

𝔼μ0π​\[r​\(st,at\)\+γ​Vπ′​\(st\+1\)−Vπ′​\(st\)\|st,at\]=Qπ′​\(st,at\)−Vπ′​\(st\)=Aπ′​\(st,at\)\.\\mathbb\{E\}^\{\\pi\}\_\{\\mu\_\{0\}\}\\Bigl\[r\(s\_\{t\},a\_\{t\}\)\+\\gamma V^\{\\pi^\{\\prime\}\}\(s\_\{t\+1\}\)\-V^\{\\pi^\{\\prime\}\}\(s\_\{t\}\)\\Bigm\|s\_\{t\},a\_\{t\}\\Bigr\]=Q^\{\\pi^\{\\prime\}\}\(s\_\{t\},a\_\{t\}\)\-V^\{\\pi^\{\\prime\}\}\(s\_\{t\}\)=A^\{\\pi^\{\\prime\}\}\(s\_\{t\},a\_\{t\}\)\.Substituting and exchanging summation overttwith the expectation, which is again licensed by the summable envelopeγt​2​Rmax/\(1−γ\)\\gamma^\{t\}\\,2R\_\{\\max\}/\(1\-\\gamma\)on\|Aπ′\|\|A^\{\\pi^\{\\prime\}\}\|, we obtain

J​\(π\)−J​\(π′\)\\displaystyle J\(\\pi\)\-J\(\\pi^\{\\prime\}\)=∑t=0∞γt​𝔼μ0π​\[Aπ′​\(st,at\)\]\\displaystyle=\\sum\_\{t=0\}^\{\\infty\}\\gamma^\{t\}\\,\\mathbb\{E\}^\{\\pi\}\_\{\\mu\_\{0\}\}\\bigl\[A^\{\\pi^\{\\prime\}\}\(s\_\{t\},a\_\{t\}\)\\bigr\]=11−γ​∑s∈𝒮dπ​\(s\)​∑a∈𝒜π​\(a∣s\)​Aπ′​\(s,a\),\\displaystyle=\\frac\{1\}\{1\-\\gamma\}\\sum\_\{s\\in\\mathcal\{S\}\}d^\{\\pi\}\(s\)\\sum\_\{a\\in\\mathcal\{A\}\}\\pi\(a\\mid s\)\\,A^\{\\pi^\{\\prime\}\}\(s,a\),where the last step unpacks𝔼μ0π​\[Aπ′​\(st,at\)\]=∑sPrμ0π⁡\(st=s\)​∑aπ​\(a∣s\)​Aπ′​\(s,a\)\\mathbb\{E\}^\{\\pi\}\_\{\\mu\_\{0\}\}\[A^\{\\pi^\{\\prime\}\}\(s\_\{t\},a\_\{t\}\)\]=\\sum\_\{s\}\\Pr^\{\\pi\}\_\{\\mu\_\{0\}\}\(s\_\{t\}=s\)\\sum\_\{a\}\\pi\(a\\mid s\)A^\{\\pi^\{\\prime\}\}\(s,a\)and applies the definition of the occupancy measure \(Definition[5](https://arxiv.org/html/2607.15459#Thmdefinition5)\), whose factor\(1−γ\)\(1\-\\gamma\)produces the prefactor1/\(1−γ\)1/\(1\-\\gamma\)\. This is \([2](https://arxiv.org/html/2607.15459#S5.E2)\)\. ∎

###### Theorem 1\(Return\-loss bound for the distilled student\)\.

Let Assumption[1](https://arxiv.org/html/2607.15459#Thmassumption1)hold\. Letπ¯T\\bar\{\\pi\}\_\{T\}be the argmax teacher of Definition[2](https://arxiv.org/html/2607.15459#Thmdefinition2), letπS\\pi\_\{S\}be any deterministic policy, in particular any decision\-list studentπS∈Πℒ\\pi\_\{S\}\\in\\Pi\_\{\\mathcal\{L\}\}of Definition[4](https://arxiv.org/html/2607.15459#Thmdefinition4), and letϵ†=Prs∼dπ¯T⁡\[πS​\(s\)≠aT​\(s\)\]\\epsilon^\{\\dagger\}=\\Pr\_\{s\\sim d^\{\\bar\{\\pi\}\_\{T\}\}\}\[\\pi\_\{S\}\(s\)\\neq a\_\{T\}\(s\)\]be the disagreement rate of Definition[6](https://arxiv.org/html/2607.15459#Thmdefinition6)\. Then

J​\(π¯T\)−J​\(πS\)≤2​Rmax​ϵ†\(1−γ\)2,J\(\\bar\{\\pi\}\_\{T\}\)\-J\(\\pi\_\{S\}\)\\leq\\frac\{2R\_\{\\max\}\\,\\epsilon^\{\\dagger\}\}\{\(1\-\\gamma\)^\{2\}\},\(3\)and the same right\-hand side bounds\|J​\(π¯T\)−J​\(πS\)\|\\bigl\|J\(\\bar\{\\pi\}\_\{T\}\)\-J\(\\pi\_\{S\}\)\\bigr\|\. In particular, ifϵ†=0\\epsilon^\{\\dagger\}=0thenJ​\(πS\)=J​\(π¯T\)J\(\\pi\_\{S\}\)=J\(\\bar\{\\pi\}\_\{T\}\)\.

###### Proof\.

Apply Lemma[1](https://arxiv.org/html/2607.15459#Thmlemma1)withπ=π¯T\\pi=\\bar\{\\pi\}\_\{T\}andπ′=πS\\pi^\{\\prime\}=\\pi\_\{S\}\. Sinceπ¯T\\bar\{\\pi\}\_\{T\}is deterministic withπ¯T​\(s\)=aT​\(s\)\\bar\{\\pi\}\_\{T\}\(s\)=a\_\{T\}\(s\), the inner expectation over actions collapses to a point evaluation and \([2](https://arxiv.org/html/2607.15459#S5.E2)\) reads

J​\(π¯T\)−J​\(πS\)=11−γ​∑s∈𝒮dπ¯T​\(s\)​AπS​\(s,aT​\(s\)\)\.J\(\\bar\{\\pi\}\_\{T\}\)\-J\(\\pi\_\{S\}\)=\\frac\{1\}\{1\-\\gamma\}\\sum\_\{s\\in\\mathcal\{S\}\}d^\{\\bar\{\\pi\}\_\{T\}\}\(s\)\\,A^\{\\pi\_\{S\}\}\\bigl\(s,a\_\{T\}\(s\)\\bigr\)\.\(4\)We split the sum according to whether the student agrees with the argmax action atss\. On the agreement set\{s:πS​\(s\)=aT​\(s\)\}\\\{s:\\pi\_\{S\}\(s\)=a\_\{T\}\(s\)\\\}the summand vanishes, because for a deterministic policy the advantage of its own action is zero:

AπS​\(s,πS​\(s\)\)=QπS​\(s,πS​\(s\)\)−VπS​\(s\)=0,A^\{\\pi\_\{S\}\}\\bigl\(s,\\pi\_\{S\}\(s\)\\bigr\)=Q^\{\\pi\_\{S\}\}\\bigl\(s,\\pi\_\{S\}\(s\)\\bigr\)\-V^\{\\pi\_\{S\}\}\(s\)=0,where the second equality holds sinceVπS​\(s\)=QπS​\(s,πS​\(s\)\)V^\{\\pi\_\{S\}\}\(s\)=Q^\{\\pi\_\{S\}\}\(s,\\pi\_\{S\}\(s\)\)for deterministicπS\\pi\_\{S\}, by Definition[1](https://arxiv.org/html/2607.15459#Thmdefinition1)\. On the disagreement setD=\{s:πS​\(s\)≠aT​\(s\)\}D=\\\{s:\\pi\_\{S\}\(s\)\\neq a\_\{T\}\(s\)\\\}we invoke the advantage range \([1](https://arxiv.org/html/2607.15459#S3.E1)\), which gives\|AπS​\(s,aT​\(s\)\)\|≤2​Rmax/\(1−γ\)\|A^\{\\pi\_\{S\}\}\(s,a\_\{T\}\(s\)\)\|\\leq 2R\_\{\\max\}/\(1\-\\gamma\)pointwise\. Combining the two cases in \([4](https://arxiv.org/html/2607.15459#S5.E4)\),

J​\(π¯T\)−J​\(πS\)\\displaystyle J\(\\bar\{\\pi\}\_\{T\}\)\-J\(\\pi\_\{S\}\)=11−γ​∑s∈Ddπ¯T​\(s\)​AπS​\(s,aT​\(s\)\)\\displaystyle=\\frac\{1\}\{1\-\\gamma\}\\sum\_\{s\\in D\}d^\{\\bar\{\\pi\}\_\{T\}\}\(s\)\\,A^\{\\pi\_\{S\}\}\\bigl\(s,a\_\{T\}\(s\)\\bigr\)≤11−γ⋅2​Rmax1−γ​∑s∈Ddπ¯T​\(s\)\\displaystyle\\leq\\frac\{1\}\{1\-\\gamma\}\\cdot\\frac\{2R\_\{\\max\}\}\{1\-\\gamma\}\\sum\_\{s\\in D\}d^\{\\bar\{\\pi\}\_\{T\}\}\(s\)=2​Rmax​ϵ†\(1−γ\)2,\\displaystyle=\\frac\{2R\_\{\\max\}\\,\\epsilon^\{\\dagger\}\}\{\(1\-\\gamma\)^\{2\}\},where the final equality is the definition ofϵ†\\epsilon^\{\\dagger\}\(Definition[6](https://arxiv.org/html/2607.15459#Thmdefinition6)\)\. The same computation applied to the absolute value of \([4](https://arxiv.org/html/2607.15459#S5.E4)\), using the triangle inequality before bounding\|AπS\|\|A^\{\\pi\_\{S\}\}\|, yields\|J​\(π¯T\)−J​\(πS\)\|≤2​Rmax​ϵ†/\(1−γ\)2\|J\(\\bar\{\\pi\}\_\{T\}\)\-J\(\\pi\_\{S\}\)\|\\leq 2R\_\{\\max\}\\epsilon^\{\\dagger\}/\(1\-\\gamma\)^\{2\}\. Finally, ifϵ†=0\\epsilon^\{\\dagger\}=0thendπ¯T​\(s\)=0d^\{\\bar\{\\pi\}\_\{T\}\}\(s\)=0for everys∈Ds\\in D, so every summand in \([4](https://arxiv.org/html/2607.15459#S5.E4)\) vanishes and the gap is exactly zero\. ∎

###### Corollary 1\(Accounting for the stochastic teacher\)\.

Under the conditions of Theorem[1](https://arxiv.org/html/2607.15459#Thmtheorem1), withΔT=J​\(πT\)−J​\(π¯T\)\\Delta\_\{T\}=J\(\\pi\_\{T\}\)\-J\(\\bar\{\\pi\}\_\{T\}\)the argmax gap of the stochastic teacher,

J​\(πT\)−J​\(πS\)≤ΔT\+2​Rmax​ϵ†\(1−γ\)2\.J\(\\pi\_\{T\}\)\-J\(\\pi\_\{S\}\)\\leq\\Delta\_\{T\}\+\\frac\{2R\_\{\\max\}\\,\\epsilon^\{\\dagger\}\}\{\(1\-\\gamma\)^\{2\}\}\.

###### Proof\.

WriteJ​\(πT\)−J​\(πS\)=\(J​\(πT\)−J​\(π¯T\)\)\+\(J​\(π¯T\)−J​\(πS\)\)J\(\\pi\_\{T\}\)\-J\(\\pi\_\{S\}\)=\\bigl\(J\(\\pi\_\{T\}\)\-J\(\\bar\{\\pi\}\_\{T\}\)\\bigr\)\+\\bigl\(J\(\\bar\{\\pi\}\_\{T\}\)\-J\(\\pi\_\{S\}\)\\bigr\)and bound the second summand by Theorem[1](https://arxiv.org/html/2607.15459#Thmtheorem1)\. ∎

The quantityΔT\\Delta\_\{T\}carries no general sign:aT​\(s\)a\_\{T\}\(s\)maximizes the teacher’s action probability, not the teacher’s action value, so the argmax teacher can be better or worse than the stochastic teacher it is derived from\. We therefore do not boundΔT\\Delta\_\{T\}; under Assumption[1](https://arxiv.org/html/2607.15459#Thmassumption1)with a known model it is computed exactly by solving two Bellman linear systems \(Proposition[2](https://arxiv.org/html/2607.15459#Thmproposition2)\), and the experiments report it alongside both sides of \([3](https://arxiv.org/html/2607.15459#S5.E3)\)\.

Theorem[1](https://arxiv.org/html/2607.15459#Thmtheorem1)says the following\. If the student reproduces the argmax teacher’s action on all but anϵ†\\epsilon^\{\\dagger\}\-fraction of states, the fraction weighted by the argmax teacher’s own discounted visitation, then the student forfeits at most2​Rmax​ϵ†/\(1−γ\)22R\_\{\\max\}\\epsilon^\{\\dagger\}/\(1\-\\gamma\)^\{2\}return, and a perfectly faithful student forfeits nothing\. The theorem does not say that the student tracks the stochastic teacherπT\\pi\_\{T\}; that comparison acquires the sign\-indefinite offsetΔT\\Delta\_\{T\}of Corollary[1](https://arxiv.org/html/2607.15459#Thmcorollary1)\. Nor does it say anything about disagreements on states the argmax teacher rarely visits: a state withdπ¯T​\(s\)≈0d^\{\\bar\{\\pi\}\_\{T\}\}\(s\)\\approx 0contributes nothing toϵ†\\epsilon^\{\\dagger\}, which is precisely the blind spot the census of Proposition[2](https://arxiv.org/html/2607.15459#Thmproposition2)exposes and the EXPAND loop of Proposition[1](https://arxiv.org/html/2607.15459#Thmproposition1)exploits\. The bound is the decision\-list analogue of the tree\-student guarantee of VIPER\(Bastani et al\.,[2018](https://arxiv.org/html/2607.15459#bib.bib2)\), with one material difference: in our finite settingϵ†\\epsilon^\{\\dagger\}is computed exactly rather than estimated from rollouts, so \([3](https://arxiv.org/html/2607.15459#S5.E3)\) is a certificate rather than a high\-probability statement\. The constant is the standard one for imitation by action matching: the factor2​Rmax/\(1−γ\)2R\_\{\\max\}/\(1\-\\gamma\)is the worst\-case advantage of a single deviation, the additional1/\(1−γ\)1/\(1\-\\gamma\)reflects the compounding of deviations along the discounted horizon, and the quadratic horizon dependence cannot be improved in general for disagreement\-based bounds\. In the myopic limitγ→0\\gamma\\to 0the bound degenerates gracefully to the single\-step statementJ​\(π¯T\)−J​\(πS\)≤2​Rmax​ϵ†J\(\\bar\{\\pi\}\_\{T\}\)\-J\(\\pi\_\{S\}\)\\leq 2R\_\{\\max\}\\epsilon^\{\\dagger\}, the largest possible one\-step reward difference incurred with probabilityϵ†\\epsilon^\{\\dagger\}\. The bound is informative only whenϵ†=O​\(\(1−γ\)2\)\\epsilon^\{\\dagger\}=O\\bigl\(\(1\-\\gamma\)^\{2\}\\bigr\): with the KeyDoor instantiationγ=0\.99\\gamma=0\.99the prefactor is2​Rmax⋅1042R\_\{\\max\}\\cdot 10^\{4\}, so the certificate has teeth only for the very small exact disagreement rates the census measures, which is the regime the experiments target\.

The EXPAND stage performs hill climbing on the return over the decision\-list class\. An*edit operator*maps an ordered decision list to another ordered decision list; the operators we use add a specialized clause at a chosen position, reorder existing clauses, or prune a clause other than the default clause, so every edit output remains a well\-formed list in the sense of Definition[4](https://arxiv.org/html/2607.15459#Thmdefinition4)and in particular remains total and deterministic\. For a listLL, letℰ​\(L\)\\mathcal\{E\}\(L\)denote the set of candidate lists proposed forLL, that is, the images ofLLunder the admissible edit operators instantiated over the candidate pool\. The loop maintains a current listLkL\_\{k\}, evaluatesJ​\(πL′\)J\(\\pi\_\{L^\{\\prime\}\}\)for candidatesL′∈ℰ​\(Lk\)L^\{\\prime\}\\in\\mathcal\{E\}\(L\_\{k\}\), accepts a candidate if it clears the current return by at least a marginτ\\tau, and stops when no candidate does\.

###### Assumption 2\(Exact evaluation and finite proposals\)\.

The EXPAND loop has access to an oracle that returns the exact returnJ​\(πL\)J\(\\pi\_\{L\}\)of Definition[1](https://arxiv.org/html/2607.15459#Thmdefinition1)for every queried listLL, the acceptance margin satisfiesτ\>0\\tau\>0, the candidate setℰ​\(L\)\\mathcal\{E\}\(L\)is finite for every listLL, and an editL→L′L\\to L^\{\\prime\}is accepted only ifJ​\(πL′\)≥J​\(πL\)\+τJ\(\\pi\_\{L^\{\\prime\}\}\)\\geq J\(\\pi\_\{L\}\)\+\\tau\.

Under Assumption[1](https://arxiv.org/html/2607.15459#Thmassumption1)the exact\-oracle requirement is not an idealization: Proposition[2](https://arxiv.org/html/2607.15459#Thmproposition2)shows thatJ​\(πL\)J\(\\pi\_\{L\}\)is obtained by solving one linear system, so acceptance decisions are free of Monte Carlo noise\. We call a listLLa*τ\\tau\-local optimum*with respect toℰ\\mathcal\{E\}whenJ​\(πL′\)<J​\(πL\)\+τJ\(\\pi\_\{L^\{\\prime\}\}\)<J\(\\pi\_\{L\}\)\+\\taufor everyL′∈ℰ​\(L\)L^\{\\prime\}\\in\\mathcal\{E\}\(L\), that is, when no admissible edit improves the return by the margin\.

###### Proposition 1\(Monotone improvement and finite termination of EXPAND\)\.

Let Assumptions[1](https://arxiv.org/html/2607.15459#Thmassumption1)and[2](https://arxiv.org/html/2607.15459#Thmassumption2)hold, and letL0,L1,L2,…L\_\{0\},L\_\{1\},L\_\{2\},\\dotsbe the sequence of lists produced by the EXPAND loop, whereLk\+1∈ℰ​\(Lk\)L\_\{k\+1\}\\in\\mathcal\{E\}\(L\_\{k\}\)is an accepted candidate\. First, the returns increase monotonically:J​\(πLk\+1\)≥J​\(πLk\)\+τJ\(\\pi\_\{L\_\{k\+1\}\}\)\\geq J\(\\pi\_\{L\_\{k\}\}\)\+\\taufor every accepted edit, so the last iterate is also the best iterate\. Second, the numberNNof accepted edits satisfies

N≤Jmax−J​\(πL0\)τ≤2​Rmax\(1−γ\)​τ,N\\;\\leq\\;\\frac\{J\_\{\\max\}\-J\(\\pi\_\{L\_\{0\}\}\)\}\{\\tau\}\\;\\leq\\;\\frac\{2R\_\{\\max\}\}\{\(1\-\\gamma\)\\,\\tau\},whereJmax=maxπ⁡J​\(π\)≤Rmax/\(1−γ\)J\_\{\\max\}=\\max\_\{\\pi\}J\(\\pi\)\\leq R\_\{\\max\}/\(1\-\\gamma\)is the optimal return, the maximum over all stationary policies being attained by an optimal deterministic policy, which exists in a finite discounted MDP under Assumption[1](https://arxiv.org/html/2607.15459#Thmassumption1)\. Third, the loop terminates after finitely many oracle calls, and its final list is aτ\\tau\-local optimum with respect toℰ\\mathcal\{E\}\.

###### Proof\.

The first claim restates the acceptance rule of Assumption[2](https://arxiv.org/html/2607.15459#Thmassumption2): an edit is accepted only if it increases the exact return by at leastτ\\tau, and since the oracle is exact the recorded improvement is the true improvement; monotonicity of the sequence\(J​\(πLk\)\)k\(J\(\\pi\_\{L\_\{k\}\}\)\)\_\{k\}follows by induction onkk, and the last iterate maximizesJJover the iterates because each term dominates its predecessors\. For the second claim, chain the accepted improvements: afterNNaccepted edits,

J​\(πLN\)\\displaystyle J\(\\pi\_\{L\_\{N\}\}\)=J​\(πL0\)\+∑k=0N−1\(J​\(πLk\+1\)−J​\(πLk\)\)\\displaystyle=J\(\\pi\_\{L\_\{0\}\}\)\+\\sum\_\{k=0\}^\{N\-1\}\\bigl\(J\(\\pi\_\{L\_\{k\+1\}\}\)\-J\(\\pi\_\{L\_\{k\}\}\)\\bigr\)≥J​\(πL0\)\+N​τ,\\displaystyle\\geq J\(\\pi\_\{L\_\{0\}\}\)\+N\\tau,where the inequality applies the acceptance margin to each summand\. SinceJ​\(πLN\)≤JmaxJ\(\\pi\_\{L\_\{N\}\}\)\\leq J\_\{\\max\}by definition ofJmaxJ\_\{\\max\}, rearranging givesN≤\(Jmax−J​\(πL0\)\)/τN\\leq\(J\_\{\\max\}\-J\(\\pi\_\{L\_\{0\}\}\)\)/\\tau\. The coarser bound follows from the value range \([1](https://arxiv.org/html/2607.15459#S3.E1)\), which givesJmax≤Rmax/\(1−γ\)J\_\{\\max\}\\leq R\_\{\\max\}/\(1\-\\gamma\)andJ​\(πL0\)≥−Rmax/\(1−γ\)J\(\\pi\_\{L\_\{0\}\}\)\\geq\-R\_\{\\max\}/\(1\-\\gamma\), henceJmax−J​\(πL0\)≤2​Rmax/\(1−γ\)J\_\{\\max\}\-J\(\\pi\_\{L\_\{0\}\}\)\\leq 2R\_\{\\max\}/\(1\-\\gamma\)\. For the third claim we observe that each iteration of the loop either accepts an edit or exhausts the finite candidate setℰ​\(Lk\)\\mathcal\{E\}\(L\_\{k\}\)without acceptance and stops\. Acceptances occur at mostN≤2​Rmax/\(\(1−γ\)​τ\)N\\leq 2R\_\{\\max\}/\(\(1\-\\gamma\)\\tau\)times by the second claim, and every iteration issues at most\|ℰ​\(Lk\)\|<∞\|\\mathcal\{E\}\(L\_\{k\}\)\|<\\inftyoracle calls by Assumption[2](https://arxiv.org/html/2607.15459#Thmassumption2), so the total number of oracle calls is finite and the loop halts\. At the halting listLfinL\_\{\\mathrm\{fin\}\}no candidateL′∈ℰ​\(Lfin\)L^\{\\prime\}\\in\\mathcal\{E\}\(L\_\{\\mathrm\{fin\}\}\)satisfiesJ​\(πL′\)≥J​\(πLfin\)\+τJ\(\\pi\_\{L^\{\\prime\}\}\)\\geq J\(\\pi\_\{L\_\{\\mathrm\{fin\}\}\}\)\+\\tau, which is the definition of aτ\\tau\-local optimum\. ∎

Proposition[1](https://arxiv.org/html/2607.15459#Thmproposition1)is a statement about the loop, not about global optimality: the final list is unimprovable by single admissible edits at marginτ\\tau, and nothing more\. The guarantee is a last\-iterate guarantee, and by monotonicity the last iterate coincides with the best iterate, so no averaging over iterates is involved\. Two consequences matter for the paper’s claims\. First, EXPAND never degrades the distilled student: combining the monotonicity with Theorem[1](https://arxiv.org/html/2607.15459#Thmtheorem1)applied to the initial list givesJ​\(πLfin\)≥J​\(πL0\)≥J​\(π¯T\)−2​Rmax​ϵ0†/\(1−γ\)2J\(\\pi\_\{L\_\{\\mathrm\{fin\}\}\}\)\\geq J\(\\pi\_\{L\_\{0\}\}\)\\geq J\(\\bar\{\\pi\}\_\{T\}\)\-2R\_\{\\max\}\\epsilon^\{\\dagger\}\_\{0\}/\(1\-\\gamma\)^\{2\}, whereϵ0†\\epsilon^\{\\dagger\}\_\{0\}is the disagreement rate of the initial list\. Second, nothing upper\-boundsJ​\(πLfin\)J\(\\pi\_\{L\_\{\\mathrm\{fin\}\}\}\)byJ​\(π¯T\)J\(\\bar\{\\pi\}\_\{T\}\)orJ​\(πT\)J\(\\pi\_\{T\}\): when the teacher is imperfect on states of low teacher visitation, an accepted edit that changes actions only on such states raises the student strictly above the teacher, and the acceptance test certifies each such crossing exactly\. The bound onNNdepends only onRmaxR\_\{\\max\},γ\\gamma, andτ\\tau; it is loose in practice, since typical runs accept far fewer edits than2​Rmax/\(\(1−γ\)​τ\)2R\_\{\\max\}/\(\(1\-\\gamma\)\\tau\), and it becomes weak asτ→0\\tau\\to 0orγ→1\\gamma\\to 1, the price of a guarantee that holds for every edit sequence the heuristic proposer may generate\.

Theorem[1](https://arxiv.org/html/2607.15459#Thmtheorem1)relates three quantities, the two returns and the disagreement rate\. In a finite MDP with a known model all three are exactly computable, so the bound is not merely a guarantee about unseen quantities: both sides of \([3](https://arxiv.org/html/2607.15459#S5.E3)\) can be evaluated and the inequality checked mechanically\. This section records the computation and its correctness\. We need one assumption beyond Assumption[1](https://arxiv.org/html/2607.15459#Thmassumption1)\.

###### Assumption 3\(Exact model access\)\.

The transition kernelPP, the reward functionrr, the discount factorγ\\gamma, and the initial distributionμ0\\mu\_\{0\}of Assumption[1](https://arxiv.org/html/2607.15459#Thmassumption1)are known, and the environment exposes a procedure that enumerates the reachable state set

𝒮r=⋃k≥0𝒮k,𝒮0=supp⁡\(μ0\),𝒮k\+1=𝒮k∪\{s′:P​\(s′∣s,a\)\>0​for some​s∈𝒮k,a∈𝒜\}\.\\mathcal\{S\}\_\{\\mathrm\{r\}\}=\\bigcup\_\{k\\geq 0\}\\mathcal\{S\}\_\{k\},\\qquad\\mathcal\{S\}\_\{0\}=\\operatorname\{supp\}\(\\mu\_\{0\}\),\\qquad\\mathcal\{S\}\_\{k\+1\}=\\mathcal\{S\}\_\{k\}\\cup\\bigl\\\{s^\{\\prime\}:P\(s^\{\\prime\}\\mid s,a\)\>0\\text\{ for some \}s\\in\\mathcal\{S\}\_\{k\},\\,a\\in\\mathcal\{A\}\\bigr\\\}\.

The set𝒮r\\mathcal\{S\}\_\{\\mathrm\{r\}\}is finite because𝒮\\mathcal\{S\}is finite, the increasing union stabilizes after at most\|𝒮\|\|\\mathcal\{S\}\|steps, and𝒮r\\mathcal\{S\}\_\{\\mathrm\{r\}\}is closed under every transition of every policy: ifs∈𝒮rs\\in\\mathcal\{S\}\_\{\\mathrm\{r\}\}andP​\(s′∣s,a\)\>0P\(s^\{\\prime\}\\mid s,a\)\>0for anyaa, thens′∈𝒮rs^\{\\prime\}\\in\\mathcal\{S\}\_\{\\mathrm\{r\}\}by construction\. Consequently every trajectory fromμ0\\mu\_\{0\}under any policy remains in𝒮r\\mathcal\{S\}\_\{\\mathrm\{r\}\}with probability one, every occupancy measure of Definition[5](https://arxiv.org/html/2607.15459#Thmdefinition5)is supported on𝒮r\\mathcal\{S\}\_\{\\mathrm\{r\}\}, and all linear algebra below may be carried out on vectors and matrices indexed by𝒮r\\mathcal\{S\}\_\{\\mathrm\{r\}\}alone\. We writen=\|𝒮r\|n=\|\\mathcal\{S\}\_\{\\mathrm\{r\}\}\|and treat functions on𝒮r\\mathcal\{S\}\_\{\\mathrm\{r\}\}as vectors inℝn\\mathbb\{R\}^\{n\}\.

For a stationary policyπ\\pi, define the policy\-induced reward vector and transition matrix

rπ​\(s\)=∑a∈𝒜π​\(a∣s\)​r​\(s,a\),Pπ​\(s,s′\)=∑a∈𝒜π​\(a∣s\)​P​\(s′∣s,a\),r\_\{\\pi\}\(s\)=\\sum\_\{a\\in\\mathcal\{A\}\}\\pi\(a\\mid s\)\\,r\(s,a\),\\qquad P\_\{\\pi\}\(s,s^\{\\prime\}\)=\\sum\_\{a\\in\\mathcal\{A\}\}\\pi\(a\\mid s\)\\,P\(s^\{\\prime\}\\mid s,a\),fors,s′∈𝒮rs,s^\{\\prime\}\\in\\mathcal\{S\}\_\{\\mathrm\{r\}\}; for a deterministic policy these reduce torπ​\(s\)=r​\(s,π​\(s\)\)r\_\{\\pi\}\(s\)=r\(s,\\pi\(s\)\)andPπ\(s,⋅\)=P\(⋅∣s,π\(s\)\)P\_\{\\pi\}\(s,\\cdot\)=P\(\\cdot\\mid s,\\pi\(s\)\)\. The matrixPπP\_\{\\pi\}is row\-stochastic, since each row is a mixture of the probability vectorsP\(⋅∣s,a\)P\(\\cdot\\mid s,a\)and𝒮r\\mathcal\{S\}\_\{\\mathrm\{r\}\}is closed, so no mass escapes the index set\.

###### Proposition 2\(Exact census and machine\-checkable certificate\)\.

Let Assumptions[1](https://arxiv.org/html/2607.15459#Thmassumption1)and[3](https://arxiv.org/html/2607.15459#Thmassumption3)hold, and letπ\\pibe any stationary policy\. First, the matrixI−γ​PπI\-\\gamma P\_\{\\pi\}is invertible, and the value vectorvπ=\(Vπ​\(s\)\)s∈𝒮rv^\{\\pi\}=\(V^\{\\pi\}\(s\)\)\_\{s\\in\\mathcal\{S\}\_\{\\mathrm\{r\}\}\}is the unique solution of the Bellman linear system

vπ=rπ\+γ​Pπ​vπ,that is,vπ=\(I−γ​Pπ\)−1​rπ,v^\{\\pi\}=r\_\{\\pi\}\+\\gamma P\_\{\\pi\}v^\{\\pi\},\\qquad\\text\{that is,\}\\qquad v^\{\\pi\}=\(I\-\\gamma P\_\{\\pi\}\)^\{\-1\}r\_\{\\pi\},\(5\)so thatJ​\(π\)=μ0⊤​vπJ\(\\pi\)=\\mu\_\{0\}^\{\\top\}v^\{\\pi\}\. Second, the occupancy measure of Definition[5](https://arxiv.org/html/2607.15459#Thmdefinition5)satisfies

dπ=\(1−γ\)​\(I−γ​Pπ⊤\)−1​μ0\.d^\{\\pi\}=\(1\-\\gamma\)\\bigl\(I\-\\gamma P\_\{\\pi\}^\{\\top\}\\bigr\)^\{\-1\}\\mu\_\{0\}\.\(6\)Third, applying \([5](https://arxiv.org/html/2607.15459#S5.E5)\) toπT\\pi\_\{T\},π¯T\\bar\{\\pi\}\_\{T\}, andπS\\pi\_\{S\}, and \([6](https://arxiv.org/html/2607.15459#S5.E6)\) toπT\\pi\_\{T\}andπ¯T\\bar\{\\pi\}\_\{T\}, yields in finitely many arithmetic operations the exact values ofJ​\(πT\)J\(\\pi\_\{T\}\),J​\(π¯T\)J\(\\bar\{\\pi\}\_\{T\}\),J​\(πS\)J\(\\pi\_\{S\}\),ΔT\\Delta\_\{T\},ϵ\\epsilon, andϵ†\\epsilon^\{\\dagger\}, and therefore of both sides of \([3](https://arxiv.org/html/2607.15459#S5.E3)\); the certified inequality

2​Rmax​ϵ†\(1−γ\)2≥J​\(π¯T\)−J​\(πS\)\\frac\{2R\_\{\\max\}\\,\\epsilon^\{\\dagger\}\}\{\(1\-\\gamma\)^\{2\}\}\\;\\geq\\;J\(\\bar\{\\pi\}\_\{T\}\)\-J\(\\pi\_\{S\}\)holds by Theorem[1](https://arxiv.org/html/2607.15459#Thmtheorem1)and is verifiable by evaluating both sides\.

###### Proof\.

We prove the three claims in order\. For the first, invertibility follows from a norm bound on the spectral radius\. SincePπP\_\{\\pi\}is row\-stochastic, its inducedℓ∞\\ell\_\{\\infty\}operator norm is‖Pπ‖∞=maxs​∑s′\|Pπ​\(s,s′\)\|=1\\\|P\_\{\\pi\}\\\|\_\{\\infty\}=\\max\_\{s\}\\sum\_\{s^\{\\prime\}\}\|P\_\{\\pi\}\(s,s^\{\\prime\}\)\|=1, hence‖γ​Pπ‖∞=γ<1\\\|\\gamma P\_\{\\pi\}\\\|\_\{\\infty\}=\\gamma<1\. The spectral radius of a matrix is bounded by any induced operator norm, soρ​\(γ​Pπ\)≤γ<1\\rho\(\\gamma P\_\{\\pi\}\)\\leq\\gamma<1, no eigenvalue ofγ​Pπ\\gamma P\_\{\\pi\}equals11, andI−γ​PπI\-\\gamma P\_\{\\pi\}is invertible with convergent Neumann series

\(I−γ​Pπ\)−1=∑t=0∞γt​Pπt,‖\(I−γ​Pπ\)−1‖∞≤∑t=0∞γt​‖Pπ‖∞t=11−γ\.\(I\-\\gamma P\_\{\\pi\}\)^\{\-1\}=\\sum\_\{t=0\}^\{\\infty\}\\gamma^\{t\}P\_\{\\pi\}^\{t\},\\qquad\\bigl\\\|\(I\-\\gamma P\_\{\\pi\}\)^\{\-1\}\\bigr\\\|\_\{\\infty\}\\leq\\sum\_\{t=0\}^\{\\infty\}\\gamma^\{t\}\\\|P\_\{\\pi\}\\\|\_\{\\infty\}^\{t\}=\\frac\{1\}\{1\-\\gamma\}\.\(7\)Next we showvπv^\{\\pi\}solves \([5](https://arxiv.org/html/2607.15459#S5.E5)\)\. For the state process underπ\\pi, which is Markov on𝒮r\\mathcal\{S\}\_\{\\mathrm\{r\}\}with transition matrixPπP\_\{\\pi\}, the expected reward at timettstarted fromssis𝔼π​\[r​\(st,at\)∣s0=s\]=\(Pπt​rπ\)​\(s\)\\mathbb\{E\}^\{\\pi\}\[r\(s\_\{t\},a\_\{t\}\)\\mid s\_\{0\}=s\]=\(P\_\{\\pi\}^\{t\}r\_\{\\pi\}\)\(s\); this follows by induction ontt, the base caset=0t=0being the definition ofrπr\_\{\\pi\}as the expected immediate reward undera0∼π\(⋅∣s\)a\_\{0\}\\sim\\pi\(\\cdot\\mid s\), and the inductive step being the Markov property together with the tower rule\. Summing the absolutely convergent series of Definition[1](https://arxiv.org/html/2607.15459#Thmdefinition1)termwise,

vπ\\displaystyle v^\{\\pi\}=∑t=0∞γt​Pπt​rπ\\displaystyle=\\sum\_\{t=0\}^\{\\infty\}\\gamma^\{t\}P\_\{\\pi\}^\{t\}r\_\{\\pi\}=rπ\+γ​Pπ​∑t=0∞γt​Pπt​rπ\\displaystyle=r\_\{\\pi\}\+\\gamma P\_\{\\pi\}\\sum\_\{t=0\}^\{\\infty\}\\gamma^\{t\}P\_\{\\pi\}^\{t\}r\_\{\\pi\}=rπ\+γ​Pπ​vπ,\\displaystyle=r\_\{\\pi\}\+\\gamma P\_\{\\pi\}v^\{\\pi\},where the second line reindexes the series, which is permitted by absolute convergence under the bound‖γt​Pπt​rπ‖∞≤γt​Rmax\\\|\\gamma^\{t\}P\_\{\\pi\}^\{t\}r\_\{\\pi\}\\\|\_\{\\infty\}\\leq\\gamma^\{t\}R\_\{\\max\}\. Uniqueness holds because \([5](https://arxiv.org/html/2607.15459#S5.E5)\) is a linear system with the invertible matrixI−γ​PπI\-\\gamma P\_\{\\pi\}, and comparing the series representation ofvπv^\{\\pi\}with \([7](https://arxiv.org/html/2607.15459#S5.E7)\) confirmsvπ=\(I−γ​Pπ\)−1​rπv^\{\\pi\}=\(I\-\\gamma P\_\{\\pi\}\)^\{\-1\}r\_\{\\pi\}\. The identityJ​\(π\)=μ0⊤​vπJ\(\\pi\)=\\mu\_\{0\}^\{\\top\}v^\{\\pi\}is Definition[1](https://arxiv.org/html/2607.15459#Thmdefinition1)\.

For the second claim, the marginal distribution of the state at timettis the row vectorμ0⊤​Pπt\\mu\_\{0\}^\{\\top\}P\_\{\\pi\}^\{t\}, again by induction onttusing the Markov property\. Definition[5](https://arxiv.org/html/2607.15459#Thmdefinition5)then gives, as a column vector,

dπ\\displaystyle d^\{\\pi\}=\(1−γ\)​∑t=0∞γt​\(Pπ⊤\)t​μ0\\displaystyle=\(1\-\\gamma\)\\sum\_\{t=0\}^\{\\infty\}\\gamma^\{t\}\\bigl\(P\_\{\\pi\}^\{\\top\}\\bigr\)^\{t\}\\mu\_\{0\}=\(1−γ\)​\(I−γ​Pπ⊤\)−1​μ0,\\displaystyle=\(1\-\\gamma\)\\bigl\(I\-\\gamma P\_\{\\pi\}^\{\\top\}\\bigr\)^\{\-1\}\\mu\_\{0\},where the second line applies the Neumann series \([7](https://arxiv.org/html/2607.15459#S5.E7)\) toPπ⊤P\_\{\\pi\}^\{\\top\}, valid becauseρ​\(γ​Pπ⊤\)=ρ​\(γ​Pπ\)≤γ<1\\rho\(\\gamma P\_\{\\pi\}^\{\\top\}\)=\\rho\(\\gamma P\_\{\\pi\}\)\\leq\\gamma<1, a matrix and its transpose having the same spectrum\.

For the third claim, each of the five linear solves is a finite computation onnn\-dimensional data, and the derived quantities are finite arithmetic expressions in their outputs:JJvalues are inner productsμ0⊤​vπ\\mu\_\{0\}^\{\\top\}v^\{\\pi\}, the argmax gap isΔT=J​\(πT\)−J​\(π¯T\)\\Delta\_\{T\}=J\(\\pi\_\{T\}\)\-J\(\\bar\{\\pi\}\_\{T\}\), and the disagreement rates of Definition[6](https://arxiv.org/html/2607.15459#Thmdefinition6)are the finite sumsϵ=∑sdπT​\(s\)​𝟏​\[πS​\(s\)≠aT​\(s\)\]\\epsilon=\\sum\_\{s\}d^\{\\pi\_\{T\}\}\(s\)\\mathbf\{1\}\[\\pi\_\{S\}\(s\)\\neq a\_\{T\}\(s\)\]andϵ†=∑sdπ¯T​\(s\)​𝟏​\[πS​\(s\)≠aT​\(s\)\]\\epsilon^\{\\dagger\}=\\sum\_\{s\}d^\{\\bar\{\\pi\}\_\{T\}\}\(s\)\\mathbf\{1\}\[\\pi\_\{S\}\(s\)\\neq a\_\{T\}\(s\)\], whose indicator entries require one evaluation ofπS\\pi\_\{S\}and one ofaTa\_\{T\}per state in𝒮r\\mathcal\{S\}\_\{\\mathrm\{r\}\}\. The certified inequality is precisely \([3](https://arxiv.org/html/2607.15459#S5.E3)\), which holds by Theorem[1](https://arxiv.org/html/2607.15459#Thmtheorem1), and both of its sides are among the computed quantities\. ∎

Two remarks on the computation\. First, the certificate is numerically benign: from‖I−γ​Pπ‖∞≤1\+γ\\\|I\-\\gamma P\_\{\\pi\}\\\|\_\{\\infty\}\\leq 1\+\\gammaand the resolvent bound in \([7](https://arxiv.org/html/2607.15459#S5.E7)\), the condition number satisfiesκ∞​\(I−γ​Pπ\)≤\(1\+γ\)/\(1−γ\)\\kappa\_\{\\infty\}\(I\-\\gamma P\_\{\\pi\}\)\\leq\(1\+\\gamma\)/\(1\-\\gamma\), which is about199199forγ=0\.99\\gamma=0\.99, so double\-precision solves determine both sides of the certificate to far more digits than the comparison requires; whenPP,rr,γ\\gamma, andμ0\\mu\_\{0\}are rational, as in the KeyDoor environment, all quantities are rational and the check can be run in exact arithmetic\. Second, the proposition is what elevates Theorem[1](https://arxiv.org/html/2607.15459#Thmtheorem1)from a guarantee to a certificate: the experiments report, per seed and per regime, the measured gapJ​\(π¯T\)−J​\(πS\)J\(\\bar\{\\pi\}\_\{T\}\)\-J\(\\pi\_\{S\}\), the bound2​Rmax​ϵ†/\(1−γ\)22R\_\{\\max\}\\epsilon^\{\\dagger\}/\(1\-\\gamma\)^\{2\}, the argmax gapΔT\\Delta\_\{T\}of Corollary[1](https://arxiv.org/html/2607.15459#Thmcorollary1), and the two disagreement rates, and the verification that the bound dominates the gap is a mechanical comparison of two exactly computed numbers, with no sampling error and no confidence level\. What the proposition does not provide is scalability: the census costsO​\(n3\)O\(n^\{3\}\)per linear solve in dense form \(structured sparsity reduces this in practice\), which is the deliberate price of exactness at then≈104n\\approx 10^\{4\}to10510^\{5\}scale of our environment, and Monte Carlo estimation with concentration bounds would replace it beyond that scale at the cost of reintroducing confidence parameters into the certificate\.

The continuous\-control experiments of Section[1](https://arxiv.org/html/2607.15459#LST1)replace the enumerable state space of the finite study with a compact observation spaceX⊂ℝdX\\subset\\mathbb\{R\}^\{d\}and replace the reachable census with a data\-driven threshold grid controlled by a single resolution parameterBB\. We now make precise the sense in which the propositional student recovers the network policy asBBgrows, and the sense in which it cannot\. The teacher here is the greedy policy of Definition[2](https://arxiv.org/html/2607.15459#Thmdefinition2)read over a continuous observation; we write itπN:X→𝒜\\pi\_\{N\}\\colon X\\to\\mathcal\{A\}to stress its origin as the frozen network, so thatπN​\(x\)=aT​\(x\)\\pi\_\{N\}\(x\)=a\_\{T\}\(x\)is the argmax action at the observationxxand the imitation target is again the deterministic argmax teacherπ¯T\\bar\{\\pi\}\_\{T\}with visitation measureμ=dπ¯T\\mu=d^\{\\bar\{\\pi\}\_\{T\}\}onXX\(Definition[5](https://arxiv.org/html/2607.15459#Thmdefinition5)\)\. For a deterministic studentπS\\pi\_\{S\}the disagreement rate of Definition[6](https://arxiv.org/html/2607.15459#Thmdefinition6)reads, in this continuous instantiation,

ϵ†​\(πS\)=μ​\(\{x∈X:πS​\(x\)≠πN​\(x\)\}\)\.\\epsilon^\{\\dagger\}\(\\pi\_\{S\}\)=\\mu\\bigl\(\\\{x\\in X:\\pi\_\{S\}\(x\)\\neq\\pi\_\{N\}\(x\)\\\}\\bigr\)\.
###### Assumption 4\(Continuous\-observation instantiation\)\.

The observation spaceX⊂ℝdX\\subset\\mathbb\{R\}^\{d\}is compact\. The greedy teacherπN:X→𝒜\\pi\_\{N\}\\colon X\\to\\mathcal\{A\}of Definition[2](https://arxiv.org/html/2607.15459#Thmdefinition2)is Borel measurable and piecewise constant, with decision regionsXa=\{x∈X:πN​\(x\)=a\}X\_\{a\}=\\\{x\\in X:\\pi\_\{N\}\(x\)=a\\\}fora∈𝒜a\\in\\mathcal\{A\}and boundaryΓ:=⋃a∈𝒜∂Xa\\Gamma:=\\bigcup\_\{a\\in\\mathcal\{A\}\}\\partial X\_\{a\}, the union of the topological boundaries of the regions, satisfyingLeb​\(Γ\)=0\\mathrm\{Leb\}\(\\Gamma\)=0, whereLeb\\mathrm\{Leb\}denotes Lebesgue measure onℝd\\mathbb\{R\}^\{d\}\. The visitation measureμ=dπ¯T\\mu=d^\{\\bar\{\\pi\}\_\{T\}\}is absolutely continuous with respect toLeb\\mathrm\{Leb\}with a density bounded byρmax<∞\\rho\_\{\\max\}<\\inftyand compact, convex supportsupp​μ\\mathrm\{supp\}\\,\\mu; convexity is used only so that a grid cell carrying mass on two regions meets the boundary within the support, and the box\[0,1\]d\[0,1\]^\{d\}of Proposition[3](https://arxiv.org/html/2607.15459#Thmproposition3)and the box\-shaped observation spaces of Section[1](https://arxiv.org/html/2607.15459#LST1)satisfy it\. The intersectionΓ∩supp​μ\\Gamma\\cap\\mathrm\{supp\}\\,\\muis\(d−1\)\(d\-1\)\-rectifiable with finite\(d−1\)\(d\-1\)\-dimensional Hausdorff measureP:=ℋd−1​\(Γ∩supp​μ\)<∞P:=\\mathcal\{H\}^\{d\-1\}\(\\Gamma\\cap\\mathrm\{supp\}\\,\\mu\)<\\infty\. Finally, each marginal cumulative distribution functionFjF\_\{j\}is bi\-Lipschitz on the coordinate projection ofsupp​μ\\mathrm\{supp\}\\,\\mu, equivalently the marginal densities are bounded away from zero there; the uniform law of Proposition[3](https://arxiv.org/html/2607.15459#Thmproposition3)and the visitation measures of Section[1](https://arxiv.org/html/2607.15459#LST1)satisfy this\.

The conditionLeb​\(Γ\)=0\\mathrm\{Leb\}\(\\Gamma\)=0makes the labelling ambiguous only on a null set, soπN\\pi\_\{N\}is well definedμ\\mu\-almost everywhere; the density boundρmax\\rho\_\{\\max\}converts Lebesgue estimates intoμ\\mu\-mass estimates; and the finite boundary contentPPis the geometric quantity that governs the rate, playing the role that the reachable count played in the finite study\.

###### Definition 7\(Threshold decision\-list class at resolutionBB\)\.

Fix an integer resolutionB≥2B\\geq 2\. For each coordinatej∈\{1,…,d\}j\\in\\\{1,\\dots,d\\\}letFjF\_\{j\}be the cumulative distribution function of thejj\-th marginal ofμ\\mu, and placeB−1B\-1*thresholds*tj,i=Fj−1​\(i/B\)t\_\{j,i\}=F\_\{j\}^\{\-1\}\(i/B\)fori=1,…,B−1i=1,\\dots,B\-1at thei/Bi/Bquantiles of that marginal, whereFj−1F\_\{j\}^\{\-1\}is the generalized inverse\. The base predicates are the axis\-aligned threshold testsfeatj≥t\\mathrm\{feat\}\_\{j\}\\geq twitht∈\{tj,i\}t\\in\\\{t\_\{j,i\}\\\}, and their exact complementsfeatj<t\\mathrm\{feat\}\_\{j\}<t\. The*threshold decision\-list class at resolutionBB*, writtenLBL\_\{B\}, is the subset of the student classΠℒ\\Pi\_\{\\mathcal\{L\}\}of Definition[4](https://arxiv.org/html/2607.15459#Thmdefinition4)whose clause bodies are conjunctions of these threshold literals and which is closed by a default clause\. The thresholds cutXXinto the cells of theBB\-adic quantile grid𝒢B\\mathcal\{G\}\_\{B\}, whose cells are the productsQ=∏j=1d\[tj,kj,tj,kj\+1\)Q=\\prod\_\{j=1\}^\{d\}\[\\,t\_\{j,k\_\{j\}\},t\_\{j,k\_\{j\}\+1\}\)withkj∈\{0,…,B−1\}k\_\{j\}\\in\\\{0,\\dots,B\-1\\\}and the conventionstj,0=−∞t\_\{j,0\}=\-\\infty,tj,B=\+∞t\_\{j,B\}=\+\\inftyat the extremes\.

Every policy inLBL\_\{B\}is constant on each cell of𝒢B\\mathcal\{G\}\_\{B\}, because the truth value of every base predicatefeatj≥tj,i\\mathrm\{feat\}\_\{j\}\\geq t\_\{j,i\}is constant across a cell, so any clause body either fires everywhere or nowhere on a given cell and the first firing clause selects one action for the whole cell\. Conversely, a single cellQQis cut out exactly by the conjunction of at most two threshold literals per coordinate, one lower testfeatj≥tj,kj\\mathrm\{feat\}\_\{j\}\\geq t\_\{j,k\_\{j\}\}and one upper testfeatj<tj,kj\+1\\mathrm\{feat\}\_\{j\}<t\_\{j,k\_\{j\}\+1\}, so a clause of length at most2​d2disolatesQQ; listing one such clause per cell, in any order, followed by a default clause realizes any prescribed cell\-to\-action map\. ConsequentlyLBL\_\{B\}is exactly the set of deterministic policies that are measurable with respect to the finiteσ\\sigma\-algebra generated by𝒢B\\mathcal\{G\}\_\{B\}, with one clause per cell in the worst case\. This identity is what lets us reason about the classLBL\_\{B\}through the grid𝒢B\\mathcal\{G\}\_\{B\}rather than through individual programs: the best achievable fidelity at resolutionBBis a property of the partition, and the induction algorithm of Section[4](https://arxiv.org/html/2607.15459#S4)is one particular search for a short list that attains it\.

###### Theorem 2\(Consistency and rate of the threshold conversion\)\.

Under Assumption[4](https://arxiv.org/html/2607.15459#Thmassumption4), let

ϵB†:=infπS∈LBϵ†​\(πS\)\\epsilon^\{\\dagger\}\_\{B\}:=\\inf\_\{\\pi\_\{S\}\\in L\_\{B\}\}\\epsilon^\{\\dagger\}\(\\pi\_\{S\}\)be the best disagreement rate attainable by a threshold decision list at resolutionBB\. ThenϵB†→0\\epsilon^\{\\dagger\}\_\{B\}\\to 0asB→∞B\\to\\infty, and there is a constantCC, depending on the dimensionddand on the bi\-Lipschitz moduli of the marginals and reducing to a function ofddalone whenμ\\muis uniform on its support, such that

ϵB†≤C​ρmax​PB\.\\epsilon^\{\\dagger\}\_\{B\}\\leq\\frac\{C\\,\\rho\_\{\\max\}\\,P\}\{B\}\.\(8\)

###### Proof\.

FixBBand construct the cell\-majority policyπB⋆∈LB\\pi\_\{B\}^\{\\star\}\\in L\_\{B\}: on each cellQ∈𝒢BQ\\in\\mathcal\{G\}\_\{B\}withμ​\(Q\)\>0\\mu\(Q\)\>0setπB⋆≡a⋆​\(Q\)\\pi\_\{B\}^\{\\star\}\\equiv a^\{\\star\}\(Q\)for somea⋆​\(Q\)∈arg⁡maxa∈𝒜⁡μ​\(Q∩Xa\)a^\{\\star\}\(Q\)\\in\\arg\\max\_\{a\\in\\mathcal\{A\}\}\\mu\(Q\\cap X\_\{a\}\), and assign an arbitrary action on theμ\\mu\-null cells\. By the equivalence established after Definition[7](https://arxiv.org/html/2607.15459#Thmdefinition7),πB⋆\\pi\_\{B\}^\{\\star\}is realizable inLBL\_\{B\}, soϵB†≤ϵ†​\(πB⋆\)\\epsilon^\{\\dagger\}\_\{B\}\\leq\\epsilon^\{\\dagger\}\(\\pi\_\{B\}^\{\\star\}\)\. Since the student is constant on each cell and the cells partitionXX,

ϵ†​\(πB⋆\)\\displaystyle\\epsilon^\{\\dagger\}\(\\pi\_\{B\}^\{\\star\}\)=∑Q∈𝒢Bμ​\(\{x∈Q:πB⋆​\(x\)≠πN​\(x\)\}\)\\displaystyle=\\sum\_\{Q\\in\\mathcal\{G\}\_\{B\}\}\\mu\\bigl\(\\\{x\\in Q:\\pi\_\{B\}^\{\\star\}\(x\)\\neq\\pi\_\{N\}\(x\)\\\}\\bigr\)=∑Q∈𝒢B\(μ​\(Q\)−μ​\(Q∩Xa⋆​\(Q\)\)\),\\displaystyle=\\sum\_\{Q\\in\\mathcal\{G\}\_\{B\}\}\\Bigl\(\\mu\(Q\)\-\\mu\\bigl\(Q\\cap X\_\{a^\{\\star\}\(Q\)\}\\bigr\)\\Bigr\),\(9\)where the second line uses that onQQthe student equalsa⋆​\(Q\)a^\{\\star\}\(Q\)and disagrees withπN\\pi\_\{N\}precisely offXa⋆​\(Q\)X\_\{a^\{\\star\}\(Q\)\}\.

We treat the cells in two groups\. The first group consists of the cells contained, up to aμ\\mu\-null set, in a single regionXaX\_\{a\}\. For such a cellμ​\(Q∩Xa⋆​\(Q\)\)=μ​\(Q\)\\mu\(Q\\cap X\_\{a^\{\\star\}\(Q\)\}\)=\\mu\(Q\), so its summand in \([9](https://arxiv.org/html/2607.15459#S5.E9)\) is zero: an interior cell is labelled correctly by its majority action\. The second group consists of the cells that meet at least two regions\. A cellQQthat carriesμ\\mu\-mass on two distinct regionsXaX\_\{a\}andXa′X\_\{a^\{\\prime\}\}meets both of the closed setsXaX\_\{a\}andXa′X\_\{a^\{\\prime\}\}and hence, being connected, meets their common boundary, which lies inΓ\\Gamma; asQQalso carries mass, it meetsΓ∩supp​μ\\Gamma\\cap\\mathrm\{supp\}\\,\\mu\. For every such cell the summand in \([9](https://arxiv.org/html/2607.15459#S5.E9)\) is bounded byμ​\(Q\)\\mu\(Q\), sinceμ​\(Q∩Xa⋆​\(Q\)\)≥0\\mu\(Q\\cap X\_\{a^\{\\star\}\(Q\)\}\)\\geq 0\. WritingℬB\\mathcal\{B\}\_\{B\}for the collection of cells meetingΓ∩supp​μ\\Gamma\\cap\\mathrm\{supp\}\\,\\mu, the two groups combine to

ϵB†≤∑Q∈ℬBμ​\(Q\)=μ​\(⋃Q∈ℬBQ\),\\epsilon^\{\\dagger\}\_\{B\}\\leq\\sum\_\{Q\\in\\mathcal\{B\}\_\{B\}\}\\mu\(Q\)=\\mu\\Bigl\(\\textstyle\\bigcup\_\{Q\\in\\mathcal\{B\}\_\{B\}\}Q\\Bigr\),\(10\)the equality holding because distinct cells are disjoint\.

It remains to bound theμ\\mu\-mass of the union of boundary cells\. LetδB\\delta\_\{B\}be the largest Euclidean diameter of a cell inℬB\\mathcal\{B\}\_\{B\}\. Every point of a cell inℬB\\mathcal\{B\}\_\{B\}lies within distanceδB\\delta\_\{B\}of a point ofΓ∩supp​μ\\Gamma\\cap\\mathrm\{supp\}\\,\\mu, so⋃Q∈ℬBQ⊆𝒯δB\\bigcup\_\{Q\\in\\mathcal\{B\}\_\{B\}\}Q\\subseteq\\mathcal\{T\}\_\{\\delta\_\{B\}\}, where𝒯δ:=\{x:dist​\(x,Γ∩supp​μ\)≤δ\}\\mathcal\{T\}\_\{\\delta\}:=\\\{x:\\mathrm\{dist\}\(x,\\Gamma\\cap\\mathrm\{supp\}\\,\\mu\)\\leq\\delta\\\}is the closedδ\\delta\-tube around the boundary\. By the density bound and the Minkowski\-content estimate for a\(d−1\)\(d\-1\)\-rectifiable set of finite Hausdorff measure, there are a thresholdδ0\>0\\delta\_\{0\}\>0and a dimensional constantcdc\_\{d\}with

μ​\(𝒯δ\)≤ρmax​Leb​\(𝒯δ\)≤ρmax​cd​P​δ\(0<δ≤δ0\),\\mu\(\\mathcal\{T\}\_\{\\delta\}\)\\leq\\rho\_\{\\max\}\\,\\mathrm\{Leb\}\(\\mathcal\{T\}\_\{\\delta\}\)\\leq\\rho\_\{\\max\}\\,c\_\{d\}\\,P\\,\\delta\\qquad\(0<\\delta\\leq\\delta\_\{0\}\),\(11\)the first inequality byμ≪Leb\\mu\\ll\\mathrm\{Leb\}with density at mostρmax\\rho\_\{\\max\}, and the second because the Lebesgue measure of theδ\\delta\-tube of a\(d−1\)\(d\-1\)\-rectifiable set is at mostcd​ℋd−1​δc\_\{d\}\\,\\mathcal\{H\}^\{d\-1\}\\,\\deltafor smallδ\\delta\.

Finally we controlδB\\delta\_\{B\}through the probability integral transform\. The mapT​\(x\)=\(F1​\(x1\),…,Fd​\(xd\)\)T\(x\)=\(F\_\{1\}\(x\_\{1\}\),\\dots,F\_\{d\}\(x\_\{d\}\)\)carries the quantile grid𝒢B\\mathcal\{G\}\_\{B\}onto the uniform grid of side1/B1/Bon\[0,1\]d\[0,1\]^\{d\}, whose cells have Euclidean diameterd/B\\sqrt\{d\}/B; by the bi\-Lipschitz marginals of Assumption[4](https://arxiv.org/html/2607.15459#Thmassumption4),TTrestricted tosupp​μ\\mathrm\{supp\}\\,\\muis bi\-Lipschitz, so each cell meeting the support hasxx\-diameter at mostcd′/Bc\_\{d\}^\{\\prime\}/Bfor a constantcd′c\_\{d\}^\{\\prime\}determined by the bi\-Lipschitz modulus ofTT\. HenceδB≤cd′/B\\delta\_\{B\}\\leq c\_\{d\}^\{\\prime\}/B, and forBBlarge enough thatδB≤δ0\\delta\_\{B\}\\leq\\delta\_\{0\}the bounds \([10](https://arxiv.org/html/2607.15459#S5.E10)\) and \([11](https://arxiv.org/html/2607.15459#S5.E11)\) giveϵB†≤ρmax​cd​cd′​P/B\\epsilon^\{\\dagger\}\_\{B\}\\leq\\rho\_\{\\max\}\\,c\_\{d\}\\,c\_\{d\}^\{\\prime\}\\,P/B, which is \([8](https://arxiv.org/html/2607.15459#S5.E8)\) withC=cd​cd′C=c\_\{d\}\\,c\_\{d\}^\{\\prime\}\. This is derived forBBpast the threshold at whichδB≤δ0\\delta\_\{B\}\\leq\\delta\_\{0\}; becauseϵB†≤1\\epsilon^\{\\dagger\}\_\{B\}\\leq 1and only finitely many coarser resolutions precede that threshold, enlargingCCextends \([8](https://arxiv.org/html/2607.15459#S5.E8)\) to everyBBwhenP\>0P\>0, whileP=0P=0makesΓ\\Gammaaμ\\mu\-null set andϵB†=0\\epsilon^\{\\dagger\}\_\{B\}=0outright\. In the canonical caseμ∝Leb\\mu\\propto\\mathrm\{Leb\}on its support the transform is affine andCCis a pure function ofdd; in generalCCabsorbs the bi\-Lipschitz modulus of the marginals granted by Assumption[4](https://arxiv.org/html/2607.15459#Thmassumption4), which reduces to a dimensional constant in the uniform setting of Proposition[3](https://arxiv.org/html/2607.15459#Thmproposition3)and the visitation measures of Section[1](https://arxiv.org/html/2607.15459#LST1)\.

For consistency, note that the summand in \([10](https://arxiv.org/html/2607.15459#S5.E10)\) already givesϵB†≤μ​\(𝒯δB\)\\epsilon^\{\\dagger\}\_\{B\}\\leq\\mu\(\\mathcal\{T\}\_\{\\delta\_\{B\}\}\)for everyBB\. Along the dyadic subsequenceB=2nB=2^\{n\}the quantile levelsi/2ni/2^\{n\}are nested, sincei/2n=2​i/2n\+1i/2^\{n\}=2i/2^\{n\+1\}, so the partitions𝒢2n\\mathcal\{G\}\_\{2^\{n\}\}are nested and, the marginals being atomless becauseμ≪Leb\\mu\\ll\\mathrm\{Leb\}, their common refinement generates the Borelσ\\sigma\-algebra onsupp​μ\\mathrm\{supp\}\\,\\mu\. Thus the grid\-measurable simple functions are dense inL1​\(μ\)L^\{1\}\(\\mu\), and the piecewise\-constantπN\\pi\_\{N\}is approximated inμ\\mu\-measure by cell\-majority policies, whenceϵ2n†→0\\epsilon^\{\\dagger\}\_\{2^\{n\}\}\\to 0; this dyadic\-scale consistency uses only the density upper bound, not the bi\-Lipschitz marginals\. Equivalentlyδ2n→0\\delta\_\{2^\{n\}\}\\to 0, so𝒯δ2n↓Γ∩supp​μ\\mathcal\{T\}\_\{\\delta\_\{2^\{n\}\}\}\\downarrow\\Gamma\\cap\\mathrm\{supp\}\\,\\mu, and continuity of the finite measureμ\\mufrom above withμ​\(Γ\)=0\\mu\(\\Gamma\)=0, which holds becauseLeb​\(Γ\)=0\\mathrm\{Leb\}\(\\Gamma\)=0andμ≪Leb\\mu\\ll\\mathrm\{Leb\}, forcesμ​\(𝒯δ2n\)→0\\mu\(\\mathcal\{T\}\_\{\\delta\_\{2^\{n\}\}\}\)\\to 0\. The rate \([8](https://arxiv.org/html/2607.15459#S5.E8)\) extends the conclusion to everyBB, since it boundsϵB†\\epsilon^\{\\dagger\}\_\{B\}monotonically to zero\. ∎

###### Corollary 2\(Return recovery in the fine\-resolution limit\)\.

Under Assumption[4](https://arxiv.org/html/2607.15459#Thmassumption4), letπS∈LB\\pi\_\{S\}\\in L\_\{B\}attain the infimumϵB†\\epsilon^\{\\dagger\}\_\{B\}of Theorem[2](https://arxiv.org/html/2607.15459#Thmtheorem2)\. Then

J​\(πN\)−J​\(πS\)≤2​Rmax\(1−γ\)2​ϵB†≤2​C​Rmax​ρmax​P\(1−γ\)2⋅1B→B→∞0\.J\(\\pi\_\{N\}\)\-J\(\\pi\_\{S\}\)\\leq\\frac\{2R\_\{\\max\}\}\{\(1\-\\gamma\)^\{2\}\}\\,\\epsilon^\{\\dagger\}\_\{B\}\\leq\\frac\{2CR\_\{\\max\}\\,\\rho\_\{\\max\}\\,P\}\{\(1\-\\gamma\)^\{2\}\}\\cdot\\frac\{1\}\{B\}\\;\\xrightarrow\[B\\to\\infty\]\{\}\\;0\.\(12\)

###### Proof\.

The performance\-difference identity of Lemma[1](https://arxiv.org/html/2607.15459#Thmlemma1)and the return\-loss argument of Theorem[1](https://arxiv.org/html/2607.15459#Thmtheorem1)use only that the advantage is bounded by2​Rmax/\(1−γ\)2R\_\{\\max\}/\(1\-\\gamma\), the range \([1](https://arxiv.org/html/2607.15459#S3.E1)\) that follows from\|r\|≤Rmax\|r\|\\leq R\_\{\\max\}andγ<1\\gamma<1, and thatϵ†\\epsilon^\{\\dagger\}is the visitation measure of the disagreement set; both hold verbatim on the general measurable observation spaceXXwithdπ¯T=μd^\{\\bar\{\\pi\}\_\{T\}\}=\\mu, the finite sums over𝒮\\mathcal\{S\}becoming integrals againstμ\\mu\. Applying Theorem[1](https://arxiv.org/html/2607.15459#Thmtheorem1)toπS\\pi\_\{S\}, whose disagreement rate isϵB†\\epsilon^\{\\dagger\}\_\{B\}by the choice ofπS\\pi\_\{S\}, gives the first inequality of \([12](https://arxiv.org/html/2607.15459#S5.E12)\); the bound \([8](https://arxiv.org/html/2607.15459#S5.E8)\) of Theorem[2](https://arxiv.org/html/2607.15459#Thmtheorem2)gives the second; and1/B→01/B\\to 0gives the limit\. ∎

The corollary states that the best threshold list at resolutionBBrecovers the network’s return in the fine\-resolution limit: the return gap closes at least as fast as1/B1/B\. Combined with the expansion stage of Proposition[1](https://arxiv.org/html/2607.15459#Thmproposition1), which relabels states the argmax teacher underweights, the student can also exceed the teacher, as the finite KeyDoor case exhibits; \([12](https://arxiv.org/html/2607.15459#S5.E12)\) bounds only the loss relative toπN\\pi\_\{N\}and does not preclude such gains\.

We now show that the linear rate inBBcannot be escaped and that the number of cells needed grows exponentially indd\.

###### Proposition 3\(Necessity and the curse of dimensionality\)\.

Letμ\\mube the uniform distribution onX=\[0,1\]dX=\[0,1\]^\{d\}, so thatρmax=1\\rho\_\{\\max\}=1, and let the teacher be the oblique half\-space policyπN​\(x\)=𝟏​\[w⋅x≥b\]\\pi\_\{N\}\(x\)=\\mathbf\{1\}\[\\,w\\cdot x\\geq b\\,\]with a normalwwthat is not parallel to any coordinate axis, that is, with at least two nonzero components\. There is a constantc\>0c\>0, depending onwwanddd, such that everyπS∈LB\\pi\_\{S\}\\in L\_\{B\}hasϵ†​\(πS\)≥c/B\\epsilon^\{\\dagger\}\(\\pi\_\{S\}\)\\geq c/B\. Consequently, attainingϵ†​\(πS\)≤ϵ\\epsilon^\{\\dagger\}\(\\pi\_\{S\}\)\\leq\\epsilonrequires resolutionB≥c/ϵB\\geq c/\\epsilonand a decision list that distinguishesΩ​\(\(1/ϵ\)d−1\)\\Omega\\bigl\(\(1/\\epsilon\)^\{d\-1\}\\bigr\)grid cells, andΩ​\(Bd−1\)\\Omega\(B^\{d\-1\}\)cells carry the boundary at resolutionBB\.

###### Proof\.

Becauseμ\\muis uniform, the marginalsFjF\_\{j\}are the identity on\[0,1\]\[0,1\], the quantile thresholds aretj,i=i/Bt\_\{j,i\}=i/B, and𝒢B\\mathcal\{G\}\_\{B\}is the uniform grid of cells of side1/B1/Bwith centerscQ=\(\(k1\+12\)/B,…,\(kd\+12\)/B\)c\_\{Q\}=\(\(k\_\{1\}\+\\tfrac\{1\}\{2\}\)/B,\\dots,\(k\_\{d\}\+\\tfrac\{1\}\{2\}\)/B\)\. The boundary is the hyperplane pieceΓ∩X=\{x∈\[0,1\]d:w⋅x=b\}\\Gamma\\cap X=\\\{x\\in\[0,1\]^\{d\}:w\\cdot x=b\\\}, which we take nondegenerate, meaning it meets the open cube; normalize‖w‖2=1\\\|w\\\|\_\{2\}=1\. As in \([9](https://arxiv.org/html/2607.15459#S5.E9)\), the minimal disagreement is realized by the cell\-majority policy and equals

ϵB†=∑Q∈𝒢Bmin⁡\(μ​\(Q∩X1\),μ​\(Q∩X0\)\),\\epsilon^\{\\dagger\}\_\{B\}=\\sum\_\{Q\\in\\mathcal\{G\}\_\{B\}\}\\min\\bigl\(\\mu\(Q\\cap X\_\{1\}\),\\,\\mu\(Q\\cap X\_\{0\}\)\\bigr\),whereX1=\{w⋅x≥b\}X\_\{1\}=\\\{w\\cdot x\\geq b\\\}andX0X\_\{0\}is its complement, since on each cell the better of the two constant labels leaves exactly the smaller of the two parts in error and noπS∈LB\\pi\_\{S\}\\in L\_\{B\}can do better than label each cell by its majority\. Only cells the hyperplane crosses contribute\.

Consider the cells whose center lies in the thin slab\{x:\|w⋅x−b\|≤τ/B\}\\\{x:\|w\\cdot x\-b\|\\leq\\tau/B\\\}for a constantτ∈\(0,12\)\\tau\\in\(0,\\tfrac\{1\}\{2\}\)to be fixed\. For such a cell the hyperplane passes withinxx\-distanceτ/B\\tau/Bof the center, while the cell has half\-width1/\(2​B\)1/\(2B\)in each coordinate; becausewwis oblique the plane is parallel to no face of the cell, so forτ\\tausmall the plane passes through the cell interior and cuts each half\-space to a piece of volume at leastβ/Bd\\beta/B^\{d\}for a constantβ\>0\\beta\>0depending onwwandddthrough the obliqueness of the normal, whence the minority part of the cell hasμ\\mu\-mass at leastβ/Bd\\beta/B^\{d\}\. It remains to count these cells\. A cell center satisfies the slab condition iff the integer vector\(k1,…,kd\)\(k\_\{1\},\\dots,k\_\{d\}\)obeys∑jwj​\(kj\+12\)∈\[B​b−τ,B​b\+τ\]\\sum\_\{j\}w\_\{j\}\(k\_\{j\}\+\\tfrac\{1\}\{2\}\)\\in\[Bb\-\\tau,\\,Bb\+\\tau\]\. Fix a coordinateℓ\\ellwithwℓ≠0w\_\{\\ell\}\\neq 0, which exists by hypothesis\. Askℓk\_\{\\ell\}ranges over\{0,…,B−1\}\\\{0,\\dots,B\-1\\\}with the other indices held fixed, the value∑jwj​\(kj\+12\)\\sum\_\{j\}w\_\{j\}\(k\_\{j\}\+\\tfrac\{1\}\{2\}\)moves in steps of\|wℓ\|\|w\_\{\\ell\}\|, so the admissible interval of width2​τ2\\taucontains at most one qualifyingkℓk\_\{\\ell\}and, sincewwis oblique andbbinterior, exactly one for a positive fraction of theBd−1B^\{d\-1\}assignments of the remaining indices, namely those for which the hyperplane enters the corresponding column within the cube\. The number of qualifying cells is therefore at leastαw​Bd−1\\alpha\_\{w\}B^\{d\-1\}for a constantαw\>0\\alpha\_\{w\}\>0\. Summing the per\-cell lower bound over these cells,

ϵB†≥αwBd−1⋅βBd=αw​βB=:cB,\\displaystyle\\epsilon^\{\\dagger\}\_\{B\}\\;\\geq\\;\\alpha\_\{w\}B^\{d\-1\}\\cdot\\frac\{\\beta\}\{B^\{d\}\}\\;=\\;\\frac\{\\alpha\_\{w\}\\beta\}\{B\}\\;=:\\;\\frac\{c\}\{B\},\(13\)andϵ†​\(πS\)≥ϵB†≥c/B\\epsilon^\{\\dagger\}\(\\pi\_\{S\}\)\\geq\\epsilon^\{\\dagger\}\_\{B\}\\geq c/Bfor everyπS∈LB\\pi\_\{S\}\\in L\_\{B\}\. Ifϵ†​\(πS\)≤ϵ\\epsilon^\{\\dagger\}\(\\pi\_\{S\}\)\\leq\\epsilonthenc/B≤ϵc/B\\leq\\epsilon, soB≥c/ϵB\\geq c/\\epsilon\. The number of cells the hyperplane crosses, each of which the optimal list must devote a distinct cell\-label to, isΘ​\(Bd−1\)\\Theta\(B^\{d\-1\}\), since a generic hyperplane meetsΘ​\(Bd−1\)\\Theta\(B^\{d\-1\}\)of theBdB^\{d\}cells of side1/B1/B; substitutingB≥c/ϵB\\geq c/\\epsilongivesΩ​\(\(1/ϵ\)d−1\)\\Omega\\bigl\(\(1/\\epsilon\)^\{d\-1\}\\bigr\)\. ∎

Two honest qualifications frame these results\. First, exact zero\-error conversion at a finite resolution holds only in degenerate cases\. WhenXXis finite, as in the reachable census of the KeyDoor experiment, a large enough grid separates every reachable observation andϵB†=0\\epsilon^\{\\dagger\}\_\{B\}=0is attained; likewise whenΓ\\Gammais itself axis\-aligned, a grid whose thresholds fall on the boundary planes labels every cell correctly\. Outside these casesΓ\\Gammacrosses the axis\-aligned cells and recovery is only asymptotic, so the correct claim is arbitrarily faithful conversion in the limitB→∞B\\to\\infty, by Theorem[2](https://arxiv.org/html/2607.15459#Thmtheorem2)and Corollary[2](https://arxiv.org/html/2607.15459#Thmcorollary2), not finite exactness in general\. Second, Theorem[2](https://arxiv.org/html/2607.15459#Thmtheorem2)and Corollary[2](https://arxiv.org/html/2607.15459#Thmcorollary2)bound the best list inLBL\_\{B\}; they are representational, or realizability, guarantees about the class, not about any particular induced program\. Whether the greedy clause induction under the DAgger relabelling of Section[1](https://arxiv.org/html/2607.15459#LST1)attains that optimum is the empirical content of the experiments, and theBd−1B^\{d\-1\}lower bound of Proposition[3](https://arxiv.org/html/2607.15459#Thmproposition3)is the obstruction those experiments display: the eight\-dimensional LunarLander exhibits the ceiling the exponent predicts, retaining a return gap at the swept resolutions, while the four\-dimensional CartPole and the six\-dimensional Acrobot, with a boundary of lower codimension to cover, recover the teacher within the same budget\.

The two exponents are confirmed numerically on the oblique\-boundary reference of Proposition[3](https://arxiv.org/html/2607.15459#Thmproposition3)by the scripttheory/verify\_resolution\.py, which measures a disagreement rateϵ​\(B\)\\epsilon\(B\)whose log\-log slope againstBBis−0\.995\-0\.995,−1\.060\-1\.060, and−1\.045\-1\.045ford=2,3,4d=2,3,4, matching the predicted−1\-1of \([8](https://arxiv.org/html/2607.15459#S5.E8)\), and a boundary\-cell count whose log\-log slope is\+1\.000\+1\.000,\+2\.011\+2\.011, and\+2\.909\+2\.909for the same dimensions, matching the predictedd−1d\-1of Proposition[3](https://arxiv.org/html/2607.15459#Thmproposition3)\.

## 6Experiments

We validate the transformation in two regimes that stress complementary questions\. The first is an exact finite Markov decision process, the KeyDoor gridworld, in which every quantity of the theory is computed in closed form, so the return\-loss certificate and the expansion guarantee are checked rather than estimated and the distilled program is a first\-order relational rule list\. The second is a family of continuous\-control tasks, where no reachable census exists and the pipeline runs in its propositional form with the census replaced by a DAgger loop and exact evaluation by Monte Carlo, the regime in which Theorem[2](https://arxiv.org/html/2607.15459#Thmtheorem2)and Proposition[3](https://arxiv.org/html/2607.15459#Thmproposition3)predict what the conversion can and cannot achieve\. We present the exact study first\.

The environment, called KeyDoor, is a finite deterministic gridworld built on the Gymnasium interface\(Towers et al\.,[2024](https://arxiv.org/html/2607.15459#bib.bib20)\)\. A full\-height interior wall at a fixed column divides a four\-row playing field into a left room of three columns and a right room of two columns, with a single door cell in the wall whose row is drawn per episode\. The agent and the key spawn in the left room and the goal spawns in the right room; the agent must step onto the key and pick it up, step next to the door and toggle it open, and only then can it cross into the right room and reach the goal\. The six actions are the four moves, a pickup, and a toggle; the reward is\+1\+1on reaching the goal and−0\.01\-0\.01per step, the discount factor isγ=0\.99\\gamma=0\.99, and the horizon is120120\. Reaching the goal terminates the episode, which removes from the reachable set those layouts in which the goal sits behind itself, and the exact enumeration yields16,94416\{,\}944reachable states, a set small enough for the linear solves of Proposition[2](https://arxiv.org/html/2607.15459#Thmproposition2)and large enough that distillation is not trivial\. The maximum absolute one\-step reward isRmax=0\.99R\_\{\\max\}=0\.99\.

The teacher is a proximal policy optimization agent\(Schulman et al\.,[2017](https://arxiv.org/html/2607.15459#bib.bib17)\)with a two\-layer tanh actor\-critic, eight synchronous environments, and standard hyperparameters, trained on the flat one\-hot observation of the state\. We study two teacher regimes over ten seeds each\. The converged regime, denoted R1, trains up to800800k environment steps with an early stop when the exact success of the greedy policy reaches0\.950\.95, which every seed attains between369369k and451451k steps\. The capped regime, denoted R2, fixes a budget of299,008299\{,\}008steps, chosen so that the greedy policy is left visibly short of convergence, which is the regime in which expansion has room to improve on the teacher\. All twenty runs use the same environment, pinned by the SHA\-256 hash of its source file, and the same package versions, and the full learning\-telemetry panel is written to disk per update; an audit of all twenty traces with the accompanying monitor reports no explained\-variance collapse, no approximate\-KL spike, no entropy collapse, and no excessive clip fraction, so the teachers are healthy and the comparison is between converged or deliberately\-undertrained networks and their distillates, not between broken training runs\.

All headline quantities are exact\. For each policy, the stochastic teacher, the greedy teacher, the distilled program, and the expanded program, the exact returnJJand the exact success probability within the horizon are obtained by the linear solves of Proposition[2](https://arxiv.org/html/2607.15459#Thmproposition2), so no Monte Carlo noise enters the reported numbers\. We aggregate across the ten seeds with an own implementation of the interquartile mean and the stratified bootstrap confidence interval in the style ofAgarwal et al\. \([2021](https://arxiv.org/html/2607.15459#bib.bib1)\), using ten thousand bootstrap resamples, and we report per\-seed paired differences with a two\-sided exact Wilcoxon signed\-rank test, correcting for the six paired tests within a regime by the Bonferroni rule\.

Figure[2](https://arxiv.org/html/2607.15459#S6.F2)shows why the two teacher regimes differ and why the distinction matters for a distillation study\. During training the stochastic policy solves the task early, but the greedy policy that distillation actually targets lags far behind, and in the capped regime the greedy policy is still well short of the stochastic one at the budget\. Distilling the greedy policy of a capped teacher therefore starts from an imperfect target, which is the headroom the expansion stage exploits\.

0224400\.50\.511environment stepsexact success probabilityR1 \(converged\)stochastic teachergreedy teacher0112233⋅105\\cdot 10^\{5\}00\.50\.511environment stepsR2 \(capped\)stochastic teachergreedy teacherFigure 2:Exact success of the stochastic and greedy PPO policies during training, interquartile mean over ten seeds\. The greedy policy, the target of distillation, trails the stochastic policy throughout, and in the capped regime R2 it is left far short of it, creating the headroom that expansion exploits\.The endpoint comparison is the core result and is shown in Figure[3](https://arxiv.org/html/2607.15459#S6.F3)\. In the converged regime the distilled program already attains exact return0\.81220\.8122and exact success1\.01\.0in every seed with six clauses, and the expansion loop accepts no edit in any seed, so the expanded and distilled programs coincide\. The interesting fact about R1 is that plain distillation already exceeds both teachers: against the stochastic teacher the mean paired improvement in exact return is0\.03950\.0395with a95%95\\%confidence interval of\[0\.0360,0\.0428\]\[0\.0360,0\.0428\]over ten of ten seeds, because the induced rule list generalizes the greedy action over the census and repairs the states on which the network is imperfect\. In the capped regime the distilled program is markedly weaker and more variable, with an interquartile mean return of0\.65600\.6560and a confidence interval of\[0\.5244,0\.7865\]\[0\.5244,0\.7865\], and it is worse than the stochastic teacher in six of the ten seeds, which is the expected consequence of distilling an undertrained greedy target\. The expanded program removes this deficit entirely\. In every seed of both regimes the expanded Prolog program attains exactlyJ=0\.812204J=0\.812204and exact success1\.01\.0, and in the capped regime it exceeds the stochastic teacher on exact return in ten of ten seeds, with a mean paired improvement of0\.10010\.1001and a confidence interval of\[0\.0961,0\.1040\]\[0\.0961,0\.1040\], a two\-sided exact Wilcoxonp=0\.0020p=0\.0020, the minimum attainable at ten seeds, and a Bonferroni\-correctedp=0\.0117p=0\.0117\. Against the greedy teacher that distillation targets, the capped\-regime improvement is larger still, a mean paired gain in return of0\.56520\.5652with interval\[0\.4979,0\.6327\]\[0\.4979,0\.6327\]and in success of0\.30010\.3001with interval\[0\.2610,0\.3380\]\[0\.2610,0\.3380\]\.

teachergreedydistilledexpanded0\.60\.60\.70\.70\.80\.8exact returnJJR1 \(converged\)teachergreedydistilledexpanded0\.20\.20\.40\.40\.60\.60\.80\.8R2 \(capped\)Figure 3:Exact return by policy class, interquartile mean with95%95\\%stratified bootstrap confidence intervals over ten seeds\. The expanded student, in gold, reaches the same exact optimum0\.8122040\.812204in every seed of both regimes, with a degenerate zero\-width interval\. In the capped regime R2 it exceeds the stochastic teacher and dominates the greedy teacher and the distilled program, whose interval is wide because capped\-teacher distillation is seed\-sensitive\.Two qualifications belong here rather than in a footnote\. First, although the expanded program strictly improves the distilled program in six of the ten capped\-regime seeds, the mean paired improvement being0\.17210\.1721with a bootstrap interval of\[0\.0777,0\.2812\]\[0\.0777,0\.2812\]that excludes zero, the two\-sided exact Wilcoxon test givesp=0\.0312p=0\.0312because four seeds are tied, and this does not survive the six\-test Bonferroni correction, so we do not claim a statistically significant separation between the distilled and the expanded program in R2 and present the expansion effect through the endpoint distributions and the per\-seed repair trajectories instead\. Figure[4](https://arxiv.org/html/2607.15459#S6.F4)shows those trajectories: each accepted edit raises the exact return, and every seed reaches the common optimum after at most two edits, the monotone behaviour that Proposition[1](https://arxiv.org/html/2607.15459#Thmproposition1)guarantees\. Second, expansion is not a fidelity\-improving operation\. The expanded program’s fidelity to the stochastic teacher under rollout visitation is about0\.710\.71in the capped regime, and its disagreement rate against the greedy teacher can rise after expansion, because accepted edits deliberately move the student away from an imperfect teacher\. Fidelity is the accounting quantity of Theorem[1](https://arxiv.org/html/2607.15459#Thmtheorem1), not the objective of Proposition[1](https://arxiv.org/html/2607.15459#Thmproposition1), and the student is best understood as a repaired program rather than a faithful clone\.

011220\.40\.40\.60\.60\.80\.8stochastic teacherJJaccepted edit indexexact returnJJFigure 4:Capped\-regime expansion trajectories, exact return after each accepted edit, one grey line per seed\. Every accepted edit increases the exact return, as Proposition[1](https://arxiv.org/html/2607.15459#Thmproposition1)requires, and all ten seeds reach the common optimum0\.8122040\.812204after at most two edits, crossing above the stochastic teacher’s return, shown as the gold dashed reference\.The return\-loss certificate of Proposition[2](https://arxiv.org/html/2607.15459#Thmproposition2)was evaluated on all forty combinations of regime, seed, and student, and the results are summarized in Table[1](https://arxiv.org/html/2607.15459#S6.T1)\. The inequality of Theorem[1](https://arxiv.org/html/2607.15459#Thmtheorem1)holds in every record, but it holds vacuously: atγ=0\.99\\gamma=0\.99the prefactor2​Rmax/\(1−γ\)22R\_\{\\max\}/\(1\-\\gamma\)^\{2\}is about2×1042\\times 10^\{4\}, and the measured disagreement rateϵ†\\epsilon^\{\\dagger\}lies between0\.240\.24and0\.860\.86, so the bound’s right\-hand side is between4\.7×1034\.7\\times 10^\{3\}and1\.7×1041\.7\\times 10^\{4\}while the value range has diameter only198198\. The certificate would have teeth only forϵ†\\epsilon^\{\\dagger\}below about1−γ=0\.011\-\\gamma=0\.01, which is the vacuity regime that Theorem[1](https://arxiv.org/html/2607.15459#Thmtheorem1)itself identifies\. What the certificate does establish is that the measured return gap is negative in all forty records, meaning that every distilled and every expanded program exactly exceeds its greedy teacher, and this is a statement of exact two\-sided accounting rather than of a tight bound\. We report both sides per record so that the reader can see the bound is satisfied and see by how much it is slack\.

Table 1:The Theorem[1](https://arxiv.org/html/2607.15459#Thmtheorem1)certificate over all forty \(regime, seed, student\) records, aggregated per regime\. The bound holds everywhere but vacuously atγ=0\.99\\gamma=0\.99; the measured gapJ​\(π¯T\)−J​\(πS\)J\(\\bar\{\\pi\}\_\{T\}\)\-J\(\\pi\_\{S\}\)is negative throughout, so every student exactly exceeds its greedy teacher\. Ranges are over the twenty records per regime\.The artefact the pipeline produces is a program one can read\. Listing[1](https://arxiv.org/html/2607.15459#LST1)shows the decision list of the expanded program for the first capped\-regime seed, verbatim from the emitted file\. The rules read as a strategy: follow the path to the goal if one exists, otherwise pick up the key when standing on it, otherwise walk to the key, otherwise toggle the door when adjacent and carrying the key, and so on, with the path\-aware direction predicate hiding the navigation in a single tabled breadth\-first search\. The first clause is subtler than it looks, because the direction predicate to the goal succeeds only when a path exists, so the clause fires only once the door is open and otherwise falls through to the key\-fetching logic\. The full program, including the perception layer and the breadth\-first search, is133133lines and is machine\-verified to select the same action as the reference evaluator on every state at which it was queried\.

Listing 1:The decision list of the expanded Prolog program for capped\-regime seed0, copied verbatim from the emitted file\. The perception layer and the tabled path\-aware direction predicatedir\_to/3, together133133lines, are omitted here and run unchanged under SWI\-Prolog\.act\(S,move\(D\)\):\-dir\_to\(S,goal,D\),\!\.

act\(S,pickup\):\-on\_key\(S\),\\\+door\_open\(S\),\\\+same\_room\_goal\(S\),\!\.

act\(S,move\(D\)\):\-dir\_to\(S,key,D\),\!\.

act\(S,toggle\):\-adj\_door\(S\),carrying\(S\),\!\.

act\(S,move\(D\)\):\-dir\_to\(S,door,D\),carrying\(S\),\!\.

act\(S,pickup\):\-\\\+adj\_door\(S\),\!\.

act\(\_S,move\(up\)\)\.

act\(\_S,move\(right\)\)\.

The KeyDoor study buys exactness with enumerability, and the natural question is what survives when the state space is continuous and no reachable census exists\. We therefore run the same pipeline, in its propositional instantiation, on three continuous\-observation control tasks from the Gymnasium suite\(Towers et al\.,[2024](https://arxiv.org/html/2607.15459#bib.bib20)\): LunarLander with an eight\-dimensional observation and four actions, CartPole with a four\-dimensional observation and two actions, and Acrobot with a six\-dimensional observation and three actions\. Two things change relative to KeyDoor, and both are the substitutions anticipated in the discussion of scale\. First, the reachable\-state census is replaced by the DAgger reduction of imitation to no\-regret online learning\(Ross et al\.,[2011](https://arxiv.org/html/2607.15459#bib.bib16)\), the same loop VIPER uses to extract a tree student\(Bastani et al\.,[2018](https://arxiv.org/html/2607.15459#bib.bib2)\): the student is rolled out, the states it visits are relabelled by the frozen teacher, and the union of teacher\-visited and student\-visited states drives the next induction, so the student is trained exactly on the off\-distribution states its own errors produce\. Second, exact policy evaluation is replaced by Monte\-Carlo evaluation over a fixed episode\-seed stream shared by the teacher and every student, so all comparisons within a task are paired at the level of initial conditions and every reported return carries a95%95\\%percentile\-bootstrap confidence interval over episodes\.

The student class is the propositional specialization of Definition[4](https://arxiv.org/html/2607.15459#Thmdefinition4)\. Each continuous feature is discretized by a data\-driven grid of thresholds placed at the empirical quantiles of the teacher’s visited values, controlled by a single resolution parameterBBthat fixes the number of bins per feature; a base predicate is a threshold testfeat≥t\\mathrm\{feat\}\\geq t, its negation is the exact complementfeat<t\\mathrm\{feat\}<t, and the induction of Section[4](https://arxiv.org/html/2607.15459#S4)grows an ordered list of clauses over these threshold literals exactly as before\. The resolutionBBinterpolates between readability and precision: atB=2B=2a single median threshold per feature yields a handful of broad clauses, and asBBgrows the grid carves the state space into finer axis\-aligned regions each labelled by an action, which is the propositional form of the partition that replaces the network\. We sweepB∈\{2,3,4,6,8,12\}B\\in\\\{2,3,4,6,8,12\\\}over five PPO teacher seeds per task, emit every student as an executable SWI\-Prolog program whose action is asserted to match the reference evaluator on at least five hundred sampled states, and aggregate across seeds with the interquartile mean and a stratified bootstrap in the manner ofAgarwal et al\. \([2021](https://arxiv.org/html/2607.15459#bib.bib1)\)\. Because the sample is five seeds, the two\-sided exact Wilcoxon signed\-rank test floors atp=0\.0625p=0\.0625, so the claims below rest on effect sizes and confidence intervals rather than on significance thresholds\. All ten teachers solve their task, with the greedy policy that distillation targets clearing the solved threshold on the shared evaluation stream, and the learning\-telemetry audit is clean on the approximate KL, the entropy, and the clip fraction throughout\. The one exception is that explained variance stays low on the fast\-solving CartPole seeds, which is the expected consequence of a near\-constant value target once the pole is balanced rather than a training pathology, and it does not bear on the distilled student because the target of distillation is the greedy action, not the critic; every teacher’s success on the evaluation stream confirms that a healthy network is being distilled\.

Figure[5](https://arxiv.org/html/2607.15459#S6.F5)shows the central finding, that the recovered symbolic program substitutes the network at a task\-dependent resolution, and that the three tasks form a gradient in how hard the substitution is\. On LunarLander the naive one\-pass distillation fails at every resolution, flying the lander into the ground with a return between−467\-467and−240\-240and a success rate near zero even as its held\-out agreement with the teacher rises withBB, which is the textbook signature of behavioural\-cloning distribution shift: agreement on the teacher’s own states does not prevent compounding error once the coarse student drifts off that distribution\. DAgger repairs this monotonically, climbing from a return of−201\-201atB=2B=2to\+155\+155atB=12B=12and turning positive fromB=6B=6, but it does not reach the teacher’s221221, because the propositional threshold list has a genuine ceiling on the fine continuous control that a soft landing demands\. CartPole and Acrobot tell the complementary story\. On CartPole, whose teacher balances for the full horizon at a return of496496, the DAgger program recovers about97%97\\%of that return with a compact rule set, reaching482482atB=3B=3with roughly thirty\-four clauses and484484atB=12B=12, and it improves on the naive student at every resolution with a paired\-difference interval that excludes zero fromB=4B=4upward\. On Acrobot, whose teacher raises the tip in about eighty\-four steps, the DAgger program matches the network within noise atB=8B=8, with a return of−83\.5\-83\.5against the teacher’s−83\.8\-83\.8and three of five seeds at or above the teacher, and even the coarsest readable list atB=2B=2, some eleven clauses, reaches−90\.7\-90\.7with a0\.840\.84success rate\. The distribution\-shift gradient is visible across the three panels: on Acrobot, a locally self\-correcting swing\-up task, the naive and DAgger curves nearly coincide; on CartPole DAgger clearly helps; on LunarLander DAgger is indispensable\. Both CartPole and Acrobot exhibit a single non\-monotone dip at an intermediate resolution,B=4B=4for the former andB=3B=3for the latter, where the quantile grid places its thresholds across the decision boundary particularly poorly and the return recovers at finer resolution; we report the dip rather than smooth it\. These curves are the empirical face of the theory of Section[5](https://arxiv.org/html/2607.15459#S5): Corollary[2](https://arxiv.org/html/2607.15459#Thmcorollary2)guarantees that the return gap closes as the resolution grows, and Proposition[3](https://arxiv.org/html/2607.15459#Thmproposition3)explains why an eight\-dimensional observation makes that closure expensive enough to leave a visible gap on LunarLander at the resolutions we sweep, while the four\-dimensional CartPole and the six\-dimensional Acrobot, with a boundary of lower codimension to carve, close it within the same budget\.

224466881212−400\-400−200\-2000200200resolutionBBMonte\-Carlo returnLunarLandernaiveDAggerteacher224466881212200200300300400400500500resolutionBBCartPole224466881212−150\-150−100\-100resolutionBBAcrobotFigure 5:Monte\-Carlo return of the propositional student against resolutionBBon three continuous\-control tasks, interquartile mean over five seeds with95%95\\%bootstrap confidence intervals on the DAgger curve\. The naive one\-pass student is in grey, the DAgger student in gold, and the neural teacher’s return is the ink dotted line\. The naive student fails on LunarLander at every resolution and recovers on the more forgiving CartPole and Acrobot; the DAgger student climbs toward the teacher on all three, reaching it within noise on Acrobot atB=8B=8and recovering about97%97\\%of it on CartPole, while retaining a genuine gap on the fine\-control LunarLander task\. The intermediate\-resolution dips on CartPole \(B=4B=4\) and Acrobot \(B=3B=3\) are honest non\-monotonicities of the quantile grid\.The resolution sweep is itself a direct test of Theorem[2](https://arxiv.org/html/2607.15459#Thmtheorem2)on the trained policies rather than on the synthetic boundary of Proposition[3](https://arxiv.org/html/2607.15459#Thmproposition3), and Figure[6](https://arxiv.org/html/2607.15459#S6.F6)reports its two governing quantities\. The held\-out fidelity, the fraction of teacher states on which the student agrees with the network, rises monotonically with the resolution on every task, which is the empirical face of the vanishing disagreementϵB†→0\\epsilon^\{\\dagger\}\_\{B\}\\to 0that the theorem guarantees\. The three curves are ordered by difficulty rather than strictly by dimension: CartPole and Acrobot reach fidelity above0\.950\.95byB=8B=8, whereas the eight\-dimensional LunarLander plateaus near0\.780\.78at the finest resolution we sweep, the same task on which the return gap stays open, so the fidelity ceiling and the return ceiling are one phenomenon seen through two metrics\. The clause count is the interpretability price of that fidelity: it grows with the resolution on every task, from nine to about a hundred and thirty on CartPole and from twenty to about three hundred on LunarLander, so the resolution parameter is literally the exchange rate between how finely the program partitions the state space and how many rules a reader must hold in mind\. We do not claim the induced clause count follows theBd−1B^\{d\-1\}law of Proposition[3](https://arxiv.org/html/2607.15459#Thmproposition3), which counts the cells a worst\-case oblique boundary forces and is confirmed on that boundary in Section[5](https://arxiv.org/html/2607.15459#S5); the induced count is the task\-dependent number the greedy covering actually emits, and it is reported as the measured cost, not as a test of the exponent\.

2244668812120\.40\.40\.60\.60\.80\.811resolutionBBheld\-out fidelity to the networkCartPole \(d=4d\{=\}4\)Acrobot \(d=6d\{=\}6\)LunarLander \(d=8d\{=\}8\)2244668812120100100200200300300resolutionBBclauses \(interpretability cost\)Figure 6:The resolution sweep as a test of the conversion theory, DAgger student, interquartile mean over five seeds\. Left, held\-out fidelity to the network rises with the resolution on every task, the empiricalϵB†→0\\epsilon^\{\\dagger\}\_\{B\}\\to 0of Theorem[2](https://arxiv.org/html/2607.15459#Thmtheorem2); the eight\-dimensional LunarLander plateaus below the lower\-dimensional tasks, the fidelity face of the return ceiling\. Right, the clause count, the interpretability price of that fidelity, grows with the resolution, soBBis the exchange rate between how finely the rules partition the state space and how many of them a reader must hold in mind\.The artefact remains a program one reads, and the interpretability cost is explicit\. On Acrobot the eleven\-clause list induced atB=2B=2, shown in Listing[2](https://arxiv.org/html/2607.15459#LST2), reads as a hand\-writable swing\-up controller that torques the inner link in the direction of its angular velocity and torques toward the raised configuration otherwise, and it scores a return of−90\-90with a success rate of0\.840\.84, close to the teacher with a rule base a human can audit at a glance\. The number of clauses grows with resolution, from about eleven atB=2B=2to about eighty\-four atB=12B=12on Acrobot and from nine to roughly a hundred and thirty on CartPole, so the resolution knob is precisely the exchange rate between how finely the program partitions the state space and how much of it a reader can hold in mind\. CartPole supplies the cautionary dual: its nine\-clauseB=2B=2list reads as the textbook pole balancer, pushing toward the side the pole is tipping, and it agrees with the network on94%94\\%of held\-out states, yet it scores only198198with a zero success rate, because coarse thresholds accumulate error over the long balancing horizon\. Fidelity to the teacher is necessary but not sufficient for closed\-loop return, and the resolution knob is what buys the missing precision, withB≥3B\\geq 3clearing the solved line\.

Listing 2:The Acrobot expert system induced by DAgger at resolutionB=2B=2, seed0, copied verbatim from the emitted file and lightly aligned\. Eleven clauses over threshold literals on the six observation features partition the state space into torque regions; the program runs unchanged under SWI\-Prolog and scores a Monte\-Carlo return of−90\-90with a0\.840\.84success rate, against the teacher’s−84\-84\.act\(S,torque\_pos\):\-ang\_vel2\(S\)\>=0\.148,ang\_vel1\(S\)<\-0\.022,\!\.

act\(S,torque\_neg\):\-ang\_vel1\(S\)\>=\-0\.022,ang\_vel2\(S\)<0\.148,\!\.

act\(S,torque\_neg\):\-sin1\(S\)<\-0\.027,cos1\(S\)<0\.746,\!\.

act\(S,torque\_pos\):\-cos2\(S\)\>=0\.416,sin2\(S\)<0\.089,\!\.

act\(S,torque\_neg\):\-cos1\(S\)\>=0\.746,ang\_vel1\(S\)<\-0\.022,\!\.

act\(S,torque\_neg\):\-sin2\(S\)\>=0\.089,cos1\(S\)<0\.746,\!\.

act\(S,torque\_pos\):\-ang\_vel1\(S\)\>=\-0\.022,sin1\(S\)\>=\-0\.027,\!\.

act\(S,torque\_zero\):\-sin1\(S\)\>=\-0\.027,\!\.

act\(S,torque\_neg\):\-cos2\(S\)\>=0\.416,\!\.

act\(S,torque\_pos\):\-\!\.

act\(\_S,torque\_pos\)\.

## 7Discussion and limitations

The results support a narrow and a broad reading\. The narrow reading is that on a task small enough to admit exact evaluation, a trained neural policy can be rewritten as a short, executable, human\-readable logic program that plays the task at least as well, and after a return\-driven expansion better, than the network it came from\. The broad reading is that post\-hoc interpretability need not trade away performance, because the symbolic artefact is not constrained to imitate the teacher once a policy\-evaluation oracle is available to certify improvements\. Both readings are bounded by the assumptions that make the exact oracle possible\.

The first limitation is scale\. Proposition[2](https://arxiv.org/html/2607.15459#Thmproposition2)and the expansion oracle rely on model access and on an enumerable reachable set, and the census costs a linear solve per evaluation, which is the deliberate price of exactness at the10410^\{4\}\-state scale of KeyDoor\. The continuous\-control study of Section[1](https://arxiv.org/html/2607.15459#LST1)is what the method becomes beyond that scale: the census gives way to the DAgger sampling ofRoss et al\. \([2011](https://arxiv.org/html/2607.15459#bib.bib16)\)and the exact solves to Monte Carlo evaluation with bootstrap intervals, at the cost of reintroducing confidence parameters into what is a certificate in the finite case, and the propositional student trades the exact\-return guarantee for a resolution knob whose ceiling is visible on LunarLander even as it suffices to substitute the network on CartPole and Acrobot\. The second limitation is the predicate vocabulary, which we fixed by hand; the direction and adjacency predicates encode task knowledge, and although the induction and expansion stages choose how to combine them, they cannot invent a predicate the vocabulary lacks, which is exactly the gap that predicate\-invention methods address\(Sha et al\.,[2024](https://arxiv.org/html/2607.15459#bib.bib18)\)and that object\-centric extractors\(Delfosse et al\.,[2024](https://arxiv.org/html/2607.15459#bib.bib5)\)would fill automatically\. The third limitation is the certificate itself, which is vacuous atγ=0\.99\\gamma=0\.99; a tight version would require either a horizon\-aware refinement of the bound or the smaller effective horizons under which the prefactor is benign, and the present contribution of Proposition[2](https://arxiv.org/html/2607.15459#Thmproposition2)is the exact two\-sided accounting rather than a tight guarantee\.

The natural continuation returns to the framing that motivated this work\. If the predicate vocabulary and the candidate rules can be proposed by a generative model rather than fixed in advance, the extraction and expansion loop becomes a way to let a large language model draft the symbolic theory of a neural agent and let exact policy evaluation keep only the drafts that improve the return, joining the post\-hoc distillation studied here to the generative construction of expert systems\(Garrido\-Merchán and Puente,[2025](https://arxiv.org/html/2607.15459#bib.bib7)\)\. The guarantees would remain those of Section[5](https://arxiv.org/html/2607.15459#S5): the acceptance oracle certifies every edit, whoever proposes it\.

## 8Conclusion

We introduced a post\-hoc transformation that distils a frozen deep reinforcement learning policy into an executable Prolog program and then expands the program by exact\-return hill climbing until it matches or surpasses its teacher\. We proved a return\-loss bound that is a machine\-checkable certificate in a finite Markov decision process and a monotone\-improvement guarantee for the expansion loop, and we showed on a two\-room key\-and\-door task that the expanded symbolic program reaches exact optimal return in every seed and, in the budget\-capped regime, exceeds the stochastic teacher on exact return in ten of ten seeds\. Run in its propositional form on three continuous\-control tasks, the same pipeline substitutes the neural network with a compact readable Prolog rule list on CartPole and Acrobot and recovers it partially on LunarLander, so the transformation reaches past the enumerable regime that makes the exact guarantees possible, and the resolution at which the symbolic program matches the network is itself a legible measure of how much of the task the rules must carve\. The symbolic student is not a faithful clone of the network but a repaired program, and the mechanism that lets it surpass the teacher, the certification of each edit by exact policy evaluation, is the same mechanism that would let a generative proposer of rules improve a neural agent under a guarantee\.

## References

- Agarwal et al\. \(2021\)Rishabh Agarwal, Max Schwarzer, Pablo Samuel Castro, Aaron C\. Courville, and Marc G\. Bellemare\.Deep reinforcement learning at the edge of the statistical precipice\.In Marc’Aurelio Ranzato, Alina Beygelzimer, Yann N\. Dauphin, Percy Liang, and Jennifer Wortman Vaughan, editors,*Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021, NeurIPS 2021, December 6\-14, 2021, virtual*, pages 29304–29320, 2021\.URL[https://proceedings\.neurips\.cc/paper/2021/hash/f514cec81cb148559cf475e7426eed5e\-Abstract\.html](https://proceedings.neurips.cc/paper/2021/hash/f514cec81cb148559cf475e7426eed5e-Abstract.html)\.
- Bastani et al\. \(2018\)Osbert Bastani, Yewen Pu, and Armando Solar\-Lezama\.Verifiable reinforcement learning via policy extraction\.In Samy Bengio, Hanna M\. Wallach, Hugo Larochelle, Kristen Grauman, Nicolò Cesa\-Bianchi, and Roman Garnett, editors,*Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3\-8, 2018, Montréal, Canada*, pages 2499–2509, 2018\.URL[https://proceedings\.neurips\.cc/paper/2018/hash/e6d8545daa42d5ced125a4bf747b3688\-Abstract\.html](https://proceedings.neurips.cc/paper/2018/hash/e6d8545daa42d5ced125a4bf747b3688-Abstract.html)\.
- Coppens et al\. \(2021\)Youri Coppens, Denis Steckelmacher, Catholijn M\. Jonker, and Ann Nowé\.Synthesising reinforcement learning policies through set\-valued inductive rule learning\.arXiv preprint arXiv:2106\.06009, 2021\.
- Delfosse et al\. \(2023\)Quentin Delfosse, Hikaru Shindo, Devendra Singh Dhami, and Kristian Kersting\.Interpretable and explainable logical policies via neurally guided symbolic abstraction\.In Alice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine, editors,*Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 \- 16, 2023*, 2023\.URL[http://papers\.nips\.cc/paper\_files/paper/2023/hash/9f42f06a54ce3b709ad78d34c73e4363\-Abstract\-Conference\.html](http://papers.nips.cc/paper_files/paper/2023/hash/9f42f06a54ce3b709ad78d34c73e4363-Abstract-Conference.html)\.
- Delfosse et al\. \(2024\)Quentin Delfosse, Sebastian Sztwiertnia, Mark Rothermel, Wolfgang Stammer, and Kristian Kersting\.Interpretable concept bottlenecks to align reinforcement learning agents\.In Amir Globersons, Lester Mackey, Danielle Belgrave, Angela Fan, Ulrich Paquet, Jakub M\. Tomczak, and Cheng Zhang, editors,*Advances in Neural Information Processing Systems 37: Annual Conference on Neural Information Processing Systems 2024, NeurIPS 2024, Vancouver, BC, Canada, December 10 \- 15, 2024*, 2024\.URL[http://papers\.nips\.cc/paper\_files/paper/2024/hash/7b76eea0c3683e440c3d362620f578cd\-Abstract\-Conference\.html](http://papers.nips.cc/paper_files/paper/2024/hash/7b76eea0c3683e440c3d362620f578cd-Abstract-Conference.html)\.
- Dzeroski et al\. \(2001\)Saso Dzeroski, Luc De Raedt, and Kurt Driessens\.Relational reinforcement learning\.*Mach\. Learn\.*, 43\(1/2\):7–52, 2001\.doi:10\.1023/A:1007694015589\.URL[https://doi\.org/10\.1023/A:1007694015589](https://doi.org/10.1023/A:1007694015589)\.
- Garrido\-Merchán and Puente \(2025\)Eduardo C\. Garrido\-Merchán and Cristina Puente\.GOFAI meets Generative AI: Development of expert systems by means of Large Language Models\.arXiv preprint arXiv:2507\.13550, 2025\.
- Jiang and Luo \(2019\)Zhengyao Jiang and Shan Luo\.Neural logic reinforcement learning\.In Kamalika Chaudhuri and Ruslan Salakhutdinov, editors,*Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9\-15 June 2019, Long Beach, California, USA*, volume 97 of*Proceedings of Machine Learning Research*, pages 3110–3119\. PMLR, 2019\.URL[http://proceedings\.mlr\.press/v97/jiang19a\.html](http://proceedings.mlr.press/v97/jiang19a.html)\.
- Kakade and Langford \(2002\)Sham M\. Kakade and John Langford\.Approximately optimal approximate reinforcement learning\.In Claude Sammut and Achim G\. Hoffmann, editors,*Machine Learning, Proceedings of the Nineteenth International Conference \(ICML 2002\), University of New South Wales, Sydney, Australia, July 8\-12, 2002*, pages 267–274\. Morgan Kaufmann, 2002\.
- Kohler et al\. \(2024\)Hector Kohler, Quentin Delfosse, Riad Akrour, Kristian Kersting, and Philippe Preux\.Interpretable and editable programmatic tree policies for reinforcement learning\.arXiv preprint arXiv:2405\.14956, 2024\.
- Koul et al\. \(2019\)Anurag Koul, Alan Fern, and Sam Greydanus\.Learning finite state representations of recurrent policy networks\.In*7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6\-9, 2019*\. OpenReview\.net, 2019\.URL[https://openreview\.net/forum?id=S1gOpsCctm](https://openreview.net/forum?id=S1gOpsCctm)\.
- Landajuela et al\. \(2021\)Mikel Landajuela, Brenden K\. Petersen, Sookyung Kim, Cláudio P\. Santiago, Ruben Glatt, T\. Nathan Mundhenk, Jacob F\. Pettit, and Daniel M\. Faissol\.Discovering symbolic policies with deep reinforcement learning\.In Marina Meila and Tong Zhang, editors,*Proceedings of the 38th International Conference on Machine Learning, ICML 2021, 18\-24 July 2021, Virtual Event*, volume 139 of*Proceedings of Machine Learning Research*, pages 5979–5989\. PMLR, 2021\.URL[http://proceedings\.mlr\.press/v139/landajuela21a\.html](http://proceedings.mlr.press/v139/landajuela21a.html)\.
- Liu et al\. \(2018\)Guiliang Liu, Oliver Schulte, Wang Zhu, and Qingcan Li\.Toward interpretable deep reinforcement learning with linear model U\-Trees\.In Michele Berlingerio, Francesco Bonchi, Thomas Gärtner, Neil Hurley, and Georgiana Ifrim, editors,*Machine Learning and Knowledge Discovery in Databases \- European Conference, ECML PKDD 2018, Dublin, Ireland, September 10\-14, 2018, Proceedings, Part II*, volume 11052 of*Lecture Notes in Computer Science*, pages 414–429\. Springer, 2018\.doi:10\.1007/978\-3\-030\-10928\-8“˙25\.URL[https://doi\.org/10\.1007/978\-3\-030\-10928\-8\_25](https://doi.org/10.1007/978-3-030-10928-8_25)\.
- Milani et al\. \(2024\)Stephanie Milani, Nicholay Topin, Manuela Veloso, and Fei Fang\.Explainable reinforcement learning: A survey and comparative review\.*ACM Comput\. Surv\.*, 56\(7\):168:1–168:36, 2024\.doi:10\.1145/3616864\.URL[https://doi\.org/10\.1145/3616864](https://doi.org/10.1145/3616864)\.
- Quinlan \(1990\)J\. Ross Quinlan\.Learning logical definitions from relations\.*Mach\. Learn\.*, 5:239–266, 1990\.doi:10\.1007/BF00117105\.URL[https://doi\.org/10\.1007/BF00117105](https://doi.org/10.1007/BF00117105)\.
- Ross et al\. \(2011\)Stéphane Ross, Geoffrey J\. Gordon, and Drew Bagnell\.A reduction of imitation learning and structured prediction to no\-regret online learning\.In Geoffrey J\. Gordon, David B\. Dunson, and Miroslav Dudík, editors,*Proceedings of the Fourteenth International Conference on Artificial Intelligence and Statistics, AISTATS 2011, Fort Lauderdale, USA, April 11\-13, 2011*, volume 15 of*JMLR Proceedings*, pages 627–635\. JMLR\.org, 2011\.URL[http://proceedings\.mlr\.press/v15/ross11a/ross11a\.pdf](http://proceedings.mlr.press/v15/ross11a/ross11a.pdf)\.
- Schulman et al\. \(2017\)John Schulman, Filip Wolski, Prafulla Dhariwal, Alec Radford, and Oleg Klimov\.Proximal policy optimization algorithms\.arXiv preprint arXiv:1707\.06347, 2017\.
- Sha et al\. \(2024\)Jingyuan Sha, Hikaru Shindo, Quentin Delfosse, Kristian Kersting, and Devendra Singh Dhami\.EXPIL: Explanatory predicate invention for learning in games\.arXiv preprint arXiv:2406\.06107, 2024\.
- Shindo et al\. \(2025\)Hikaru Shindo, Quentin Delfosse, Devendra Singh Dhami, and Kristian Kersting\.BlendRL: A framework for merging symbolic and neural policy learning\.In*The Thirteenth International Conference on Learning Representations, ICLR 2025, Singapore, April 24\-28, 2025*\. OpenReview\.net, 2025\.URL[https://openreview\.net/forum?id=60i0ksMAhd](https://openreview.net/forum?id=60i0ksMAhd)\.
- Towers et al\. \(2024\)Mark Towers, Ariel Kwiatkowski, Jordan Terry, John U\. Balis, Gianluca De Cola, Tristan Deleu, Manuel Goulão, Andreas Kallinteris, Markus Krimmel, Arjun KG, Rodrigo Perez\-Vicente, Andrea Pierré, Sander Schulhoff, Jun Jet Tai, Hannah Tan, and Omar G\. Younis\.Gymnasium: A standard interface for reinforcement learning environments\.arXiv preprint arXiv:2407\.17032, 2024\.
- Verma et al\. \(2018\)Abhinav Verma, Vijayaraghavan Murali, Rishabh Singh, Pushmeet Kohli, and Swarat Chaudhuri\.Programmatically interpretable reinforcement learning\.In Jennifer G\. Dy and Andreas Krause, editors,*Proceedings of the 35th International Conference on Machine Learning, ICML 2018, Stockholmsmässan, Stockholm, Sweden, July 10\-15, 2018*, volume 80 of*Proceedings of Machine Learning Research*, pages 5045–5054\. PMLR, 2018\.URL[http://proceedings\.mlr\.press/v80/verma18a\.html](http://proceedings.mlr.press/v80/verma18a.html)\.
- Verma et al\. \(2019\)Abhinav Verma, Hoang Minh Le, Yisong Yue, and Swarat Chaudhuri\.Imitation\-projected programmatic reinforcement learning\.In Hanna M\. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d’Alché\-Buc, Emily B\. Fox, and Roman Garnett, editors,*Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8\-14, 2019, Vancouver, BC, Canada*, pages 15726–15737, 2019\.URL[https://proceedings\.neurips\.cc/paper/2019/hash/5a44a53b7d26bb1e54c05222f186dcfb\-Abstract\.html](https://proceedings.neurips.cc/paper/2019/hash/5a44a53b7d26bb1e54c05222f186dcfb-Abstract.html)\.
- Wielemaker et al\. \(2012\)Jan Wielemaker, Tom Schrijvers, Markus Triska, and Torbjörn Lager\.SWI\-Prolog\.*Theory Pract\. Log\. Program\.*, 12\(1\-2\):67–96, 2012\.doi:10\.1017/S1471068411000494\.URL[https://doi\.org/10\.1017/S1471068411000494](https://doi.org/10.1017/S1471068411000494)\.