Influence-Guided Concolic Testing of Transformer Robustness

2025/09/28 by Hong, Chih-Duo, Wang, Yu, Chang, Yao-Chen +1
#FOS: Computer and information sciences #Machine Learning (cs.LG) #Software Engineering (cs.SE)

paper · doi:10.48550/arxiv.2509.23806

Abstract

Concolic testing for deep neural networks alternates concrete execution with constraint solving to search for inputs that flip decisions. We present an influence-guided concolic tester for Transformer classifiers that ranks path predicates by SHAP-based estimates of their impact on the model output. To enable SMT solving on modern architectures, we prototype a solver-compatible, pure-Python semantics for multi-head self-attention and introduce practical scheduling heuristics that temper constraint growth on deeper models. In a white-box study on compact Transformers under small L₀ budgets, influence guidance finds label-flip inputs more efficiently than a FIFO baseline and maintains steady progress on deeper networks. Aggregating successful attack instances with a SHAP-based critical decision path analysis reveals recurring, compact decision logic shared across attacks. These observations suggest that (i) influence signals provide a useful search bias for symbolic exploration, and (ii) solver-friendly attention semantics paired with lightweight scheduling make concolic testing feasible for contemporary Transformer models, offering potential utility for debugging and model auditing.

Citations

• Extracting Robust Register Automata from Neural Networks over Data Sequences
• Concolic Testing on Individual Fairness of Neural Network Models
• Constraint-based Adversarial Example Synthesis
• A DPLL(T) Framework for Verifying Deep Neural Networks
• Convex Bounds on the Softmax Function with Applications to Robustness Verification
• On Neural Network Equivalence Checking using SMT Solvers
• NPC: Neuron Path Coverage via Characterizing Decision Logic of Deep Neural Networks
• Verifying Quantized Neural Networks using SMT-Based Model Checking
• Gradient-based Adversarial Attacks against Text Transformers
• TAG: Gradient Attack on Transformer-based Language Models
• Scalable Verification of Quantized Neural Networks (Technical Report)
• Robustness Verification for Transformers
• Efficient Neural Network Robustness Certification with General Activation Functions
• Efficient Formal Safety Analysis of Neural Networks
• TensorFuzz: Debugging Neural Networks with Coverage-Guided Fuzzing
• Concolic Testing for Deep Neural Networks
• Formal Security Analysis of Neural Networks using Symbolic Intervals
• Testing Deep Neural Networks
• One Pixel Attack for Fooling Deep Neural Networks
• Attention Is All You Need
• A Unified Approach to Interpreting Model Predictions
• Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks
• Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks
• DeepFool: a simple and accurate method to fool deep neural networks
• Explaining and Harnessing Adversarial Examples
• Deep Neural Networks are Easily Fooled: High Confidence Predictions for\n Unrecognizable Images
• Intriguing properties of neural networks
• ImageNet classification with deep convolutional neural networks
• Deep Neural Networks for Acoustic Modeling in Speech Recognition: The Shared Views of Four Research Groups
• On the Adversarial Robustness of Vision Transformers

Related

• BlockCert: Certified Blockwise Extraction of Transformer Mechanisms
• Transformers as Statisticians: Provable In-Context Learning with In-Context Algorithm Selection
• The Devil is in the Detail: Simple Tricks Improve Systematic\n Generalization of Transformers
• Rationalizing Transformer Predictions via End-To-End Differentiable Self-Training
• Inverse-Free Wilson Loops for Transformers: A Practical Diagnostic for Invariance and Order Sensitivity