Analyzing Symbolic Properties for DRL Agents in Systems and Networking

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 (8)

• 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.
• Figure 2: Symbolic properties over DRL agent execution pairs (§\ref{['sec:prop']}). 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 (§\ref{['sec:scope']}), 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$.
• Figure 3: diffRL's overview (§\ref{['sec:diffrl']}). 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.
• 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.
• Figure 5: Query execution time comparison for verifying Capacity Utilization property of Pensieve policies with different model sizes and verification backends.