Analyzing Symbolic Properties for DRL Agents in Systems and Networking

Mohammad Zangooei; Jannis Weil; Amr Rizk; Mina Tahmasbi Arashloo; Raouf Boutaba

cs.NIApr 6, 2026

Analyzing Symbolic Properties for DRL Agents in Systems and Networking

Authors: Mohammad Zangooei, Jannis Weil, Amr Rizk, Mina Tahmasbi Arashloo, Raouf Boutaba

Organizations: University of Waterloo, Waterloo, Canada · Leibniz University Hannover, Hannover, Germany

Abstract

Deep reinforcement learning (DRL) has shown remarkable performance on complex control problems in systems and networking, including adaptive video streaming, wireless resource management, and congestion control. For safe deployment, however, it is critical to reason about how agents behave across the range of system states they encounter in practice. Existing verification-based methods in this domain primarily focus on point properties, defined around fixed input states, which offer limited coverage and require substantial manual effort to identify relevant input-output pairs for analysis. In this paper, we study symbolic properties, that specify expected behavior over ranges of input states, for DRL agents in systems and networking. We present a generic formulation for symbolic properties, with monotonicity and robustness as concrete examples, and show how they can be analyzed using existing DNN verification engines. Our approach encodes symbolic properties as comparisons between related executions of the same policy and decomposes them into practically tractable sub-properties. These techniques serve as practical enablers for applying existing verification tools to symbolic analysis. Using our framework, diffRL, we conduct an extensive empirical study across three DRL-based control systems, adaptive video streaming, wireless resource management, and congestion control. Through these case studies, we analyze symbolic properties over broad input ranges, examine how property satisfaction evolves during training, study the impact of model size on verifiability, and compare multiple verification backends. Our results show that symbolic properties provide substantially broader coverage than point properties and can uncover non-obvious, operationally meaningful counterexamples, while also revealing practical solver trade-offs and limitations.

Figures & tables

Figure 1. Point-wise versus symbolic property analysis. Left (Prior Work): Analysis is performed at individual points that humans provide, checking that the property holds under bounded perturbations around one concrete point in the input space. In this example, the property asserts that the output action does not change. Checking properties only at individual points results in limited coverage of the input space and may miss unsafe behavior outside the considered points. Right (This Work): Analysis is performed over an entire operational region using symbolic properties. This provides higher coverage of the input space and enables the detection of unsafe points that are difficult to uncover with point properties. Comparison between point-based and symbolic property verification. Prior work verifies properties on individually provided input points, resulting in low coverage and potential missed unsafe behaviors. In contrast, this work verifies properties over an entire operational region, enabling higher coverage of the input space and improved detection of unsafe points.

Figure 2. Symbolic properties over DRL agent execution pairs (§ 3 ). A symbolic input $x$ from the region of interest in the input space and its bounded perturbation $x+s$ induce two executions of the agent’s policy $\pi$ . The policy $\pi$ is based on a non-linear DNN. As such, input perturbations may result in jumps in the DNN’s multi-dimensional continuous output space (see blue highlights in the center). The DNN’s output may represent predicted action values or action probabilities, which we refer to as action logits in general. For deterministic agents with discrete actions (§ 2 ), the policy $\pi$ is defined as the $argmax$ of these logits. Our symbolic properties constrain the two resulting actions $\pi(x)$ and $\pi(x+s)$ with a function $f$ and tolerance $d$ . This figure illustrates the mapping from the input space to the action logit space through a deep neural network (DNN), and how properties are evaluated on the resulting policy. A small perturbation $s$ around an input $x$ is propagated through the DNN, producing corresponding logits $L_x$ and $L_{x+s}$. After applying the $\arg\max$ operator, the resulting actions $\pi(x)$ and $\pi(x+s)$ are compared via a property function $f(\cdot)$ to verify whether a specified constraint (e.g., bounded deviation $\leqd$) holds. — Figure 2. Symbolic properties over DRL agent execution pairs (§ 3 ). A symbolic input $x$ from the region of interest in the input space and its bounded perturbation $x+s$ induce two executions of the agent’s policy $\pi$ . The policy $\pi$ is based on a non-linear DNN. As such, input perturbations may result in jumps in the DNN’s multi-dimensional continuous output space (see blue highlights in the center). The DNN’s output may represent predicted action values or action probabilities, which we refer to as action logits in general. For deterministic agents with discrete actions (§ 2 ), the policy $\pi$ is defined as the $argmax$ of these logits. Our symbolic properties constrain the two resulting actions $\pi(x)$ and $\pi(x+s)$ with a function $f$ and tolerance $d$ . This figure illustrates the mapping from the input space to the action logit space through a deep neural network (DNN), and how properties are evaluated on the resulting policy. A small perturbation $s$ around an input $x$ is propagated through the DNN, producing corresponding logits $L_x$ and $L_{x+s}$ . After applying the $\arg\max$ operator, the resulting actions $\pi(x)$ and $\pi(x+s)$ are compared via a property function $f(\cdot)$ to verify whether a specified constraint (e.g., bounded deviation $\leqd$ ) holds.

Figure 3. diffRL ’s overview (§ 4 ). Starting from a trained DNN and a symbolic property specification, diffRL applies a comparative encoding to construct two coupled executions of the same policy under a bounded input perturbation. The resulting formulation is decomposed into multiple queries, dispatched to heterogeneous solvers. The individual solver outcomes are then aggregated to produce the final verification result. Overview of the diffRL framework: property specifications are encoded and decomposed into solver-compatible queries evaluated across multiple verification engines, with aggregated results yielding the final property assessment for the DNN policy.

Figure 4. (a) and (b) illustrate the analysis results for the Capacity Utilization property for DRL agents

\pi^{\text{Pensieve}}_{128}

and

\pi^{\text{Pensieve}}_{64}

, respectively. Each group of six cells represents the results for a specific model checkpoint ( ckpt ) throughout training (x-axis) and a specific per-input-feature coverage percentage (y-axis). Each cell in the group corresponds to one of the queries generated by diffRL through property decomposition. (c) presents the training reward curves for

\pi^{\text{Pensieve}}_{128}

and

\pi^{\text{Pensieve}}_{64}

, with vertical dashed lines indicating the checkpoints at which models are extracted for analysis. This figure analyzes capacity utilization properties of Pensieve policies during training. Subfigures (a) and (b) show verification outcomes for models with 128 and 64 hidden units across checkpoints and input ranges (60%-100%), with results categorized as safe, unsafe, or unknown, and annotated by which solver (MIP or CROWN) provided a decision. Subfigure (c) plots the training reward over time for both models, illustrating the relationship between policy performance and property satisfaction across training.

Figure 5. Query execution time comparison for verifying Capacity Utilization property of Pensieve policies with different model sizes and verification backends. The figure presents the distribution of query execution times (in seconds, shown on a logarithmic scale) for four configurations: Pensieve-64 with CROWN, Pensieve-64 with MIP, Pensieve-128 with CROWN, and Pensieve-128 with MIP.

Figure 6. Analysis results for Rebuffering Avoidance (left) and Robustness (right) for

\pi^{\text{Pensieve}}_{64}

(top) and

\pi^{\text{Pensieve}}_{128}

(bottom) at different training checkpoints (rows) from Fig. 4 (c). Each column corresponds to a coverage level of the input domain (60%, 80%, and 100%). For each model checkpoint and coverage, the stacked horizontal bars show the total number of verification queries classified as safe (green), unsafe (red), and unknown (gray), with the exact counts annotated inside each segment. Verification results across training checkpoints for rebuffering avoidance and robustness properties in Pensieve models, showing the distribution of safe, unsafe, and unknown cases under varying input ranges.

Figure 7. Comparison of analysis outcomes across solvers and properties. The figure reports the number of safe , unsafe , and unknown results obtained using Marabou, MIP, and Alpha-Beta-CROWN for queries generated by diffRL for three properties evaluated on different CMARS policies. Each horizontal bar corresponds to a property-policy pair, with segment lengths and overlaid counts indicating the solver’s outcome distribution. Comparison of verification outcomes (safe, unsafe, unknown) across multiple solvers for CMARS policies under different configurations and property types.

Figure 8. Query execution time (in seconds, log scale) for verifying the channel compensation property of CMARS policies under different architectures and action-space sizes using three verification backends (Marabou, MIP, and Alpha-Beta-CROWN). Each subplot corresponds to a policy. The figure presents four boxplots comparing verification runtimes across solvers for CMARS policies with varying depth and action-space size, evaluated on the channel compensation property. The y-axis shows execution time on a logarithmic scale, while the x-axis lists the verification backends.

Property	Coverage	Marabou	MIP	Alpha-Beta-CROWN
Aurora Robustness	70%	safe	safe	safe
	100%	unknown	unsafe	unknown
Ack-Driven Capacity Utilization	70%	safe	safe	safe
	100%	unknown	unsafe	unknown
Latency-Aware Capacity Utilization	70%	safe	safe	safe
	100%	unknown	unsafe	unknown

Table 1. Aurora analysis results for different solvers and per-input-feature coverage ranges.

Reinforcement Learning

Reinforcement learning studies how agents learn sequential decisions from rewards and interaction, balancing exploration, performance, safety, and adaptation.

See all 1,717 papers

Learning from the Test: Self-Referential Differential Testing for Deep RL Agents
Aug 23, 2026Junda He, Jieke Shi, Zhou Yang +2Reinforcement Learning
Singapore Management University, Singapore · University of Alberta, Edmonton, Canada and Canada CIFAR AI Chair, Amii, Edmonton, Canada
Sample-efficient Neuro-symbolic Proximal Policy Optimization
Apr 28, 2026Simone Murari, Celeste Veronese, Daniele MeliReinforcement Learning Proximal Policy Optimization
Dept. of Computer Science, University of Verona, Italy
Formal Verification of Learned Multi-Agent Communication Policies via Decision Tree Distillation
Jun 17, 2026Ahmad Farooq, Kamran IqbalNeural Network Verification Formal Methods for RL
Department of Electrical and Computer Engineering, University of Arkansas at Little Rock, Little Rock, AR 72204 USA

Aug 23, 2026J/K move · Enter open · S save

Learning from the Test: Self-Referential Differential Testing for Deep RL Agents

Junda He, Jieke Shi, Zhou Yang, Mingfei Cheng+1

Singapore Management University, Singapore · University of Alberta, Edmonton, Canada and Canada CIFAR AI Chair, Amii, Edmonton, Canada

Reinforcement Learning

Open paper AskPDF arXiv

Deep Reinforcement Learning (DRL) has achieved significant success in complex decision-making problems. As DRL systems are increasingly deployed in real-world applications, ensuring their quality and reliability is paramount. Current works primarily focus on detecting safety-critical failures, often neglecting policy optimality, which can lead to reduced efficiency, user distrust, and economic losses. This oversight, compounded by the inherent "testing oracle problem" for optimality, leaves a significant gap in comprehensively evaluating DRL systems. To address this gap, we propose Delta (Differential Testing for DRL Agents), a novel and comprehensive framework that automatically identifies both safety-critical and optimality bugs in DRL agents. Delta employs a two-phase approach: (1) Safety Testing, where the Agent Under Test (AUT) is evaluated for catastrophic failures while collecting data from its decision-making policy, and (2) Optimality Testing, where this collected data from the prior phase is used to train a challenger agent via Offline Reinforcement Learning. Differential testing is then performed by comparing the challenger agent against the AUT; instances where the challenger achieves higher cumulative rewards indicate optimality issues in the AUT. We demonstrate Delta's effectiveness across five environments. We investigate the effectiveness of three offline RL algorithms (BC, BCQ, and CQL) in generating challenger agents. Experimental results demonstrate that safety testing datasets are valuable for training competent DRL agents. Challenger agents trained with BCQ proved most effective for identifying optimality issues within the framework of Delta. Across the five environments, Delta uncovered an average of 2,518 optimality issues, outperforming the baseline methods by 50.2%.

Abstract

Reinforcement Learning

Explore similar work

Learning from the Test: Self-Referential Differential Testing for Deep RL Agents

Sample-efficient Neuro-symbolic Proximal Policy Optimization

Formal Verification of Learned Multi-Agent Communication Policies via Decision Tree Distillation