.png){kind=icon}
.png){kind=icon}
Return
Equivalent and Compact Representations of Neural Network Controllers With Decision Trees
.png){kind=icon}
PRE
AI
K
N
R
P
DOI：10.1109/tac.2026.3676368.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
Over the past decade, neural network (NN)-based controllers have demonstrated remarkable efficacy in a variety of decision-making tasks. However, their closed-box nature and the risk of unexpected behaviors pose a challenge to their deployment in real-world systems requiring strong guarantees of correctness and safety. We address these limitations by investigating the transformation of NN-based controllers into equivalent soft decision tree (SDT)-based controllers and its impact on verifiability. In contrast to existing work, we focus on discrete-output NN controllers, including rectified linear unit (ReLU) activation functions as well as argmax operations. We then devise an exact yet efficient transformation algorithm, which automatically prunes redundant branches. We evaluate our approach and demonstrate the practical efficacy of the transformation algorithm using three benchmarks from the OpenAI Gym environment, including an autonomous driving NN controller. Our results indicate that the SDT transformation can benefit formal verification, showing runtime improvements of up to <inline-formula xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink"><tex-math notation="LaTeX">$20\times$</tex-math></inline-formula>, <inline-formula xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink"><tex-math notation="LaTeX">$2\times$</tex-math></inline-formula>, and <inline-formula xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink"><tex-math notation="LaTeX">$20\times$</tex-math></inline-formula> for the MountainCar-v0, CartPole-v1, and CarRacing-v2 environments, respectively.
Keywords:
Control system
deep neural networks (NNs)
formal verification
soft decision trees (SDT)
Journal
IF:
7
Papers:
1.3W
Citations:
6.7W
Organization
Cited Papers