Author name cluster

Taylor T. Johnson

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

10 papers

2 author rows

JAIR Journal 2026 Journal Article

ModelStar: Reachability Analysis-based Safety Verification of Neural Networks Against Model Perturbations

Muhammad Usama Zubair
Taylor T. Johnson
Kanad Basu
Waseem Abbas

The widespread adoption of deep neural network (DNN)-based learning systems in safety-critical applications requires exceptional reliability. However, this reliability could be compromised by perturbations in model parameters, such as variations in neural network weights caused by hardware vulnerabilities and environmental factors, which can lead to mispredictions and compromise system safety. To address this, we propose ‘ModelStar’, an innovative framework leveraging reachability analysis to evaluate the robustness of DNNs against weight perturbations. ModelStar employs a linear set propagation technique to analyze the impact of an infinite family of parameter variations on DNN outputs. Our comprehensive analysis demonstrates that ModelStar not only establishes tighter robustness bounds but also verifies DNN robustness for up to 60% more samples from image classification datasets compared to existing methods. Furthermore, ModelStar extends safety verification to convolutional layers, advancing the state-of-the-art in neural network safety verification. These results highlight ModelStar’s efficacy in improving the reliability of DNNs in real-world, safety-critical scenarios.

PDF Details DOI

AAMAS Conference 2025 Conference Paper

Combining LLMs with a Logic-Based Framework to Explain MCTS

Ziyan An
Xia Wang
Hendrik Baier
Zirong Chen
Abhishek Dubey
Taylor T. Johnson
Jonathan Sprinkle
Ayan Mukhopadhyay

In response to the lack of trust in Artificial Intelligence (AI) for sequential planning, we design a Computational Tree Logic-guided large language model (LLM)-based natural language explanation framework designed for the Monte Carlo Tree Search (MCTS) algorithm. MCTS is often considered challenging to interpret due to the complexity of its search trees, but our framework is flexible enough to handle a wide range of free-form post-hoc queries and knowledge-based inquiries centered around MCTS and the Markov Decision Process (MDP) of the application domain. By transforming user queries into logic and variable statements, our framework ensures that the evidence obtained from the search tree remains factually consistent with the underlying environmental dynamics and any constraints in the actual stochastic control process. We evaluate the framework rigorously through quantitative assessments, where it demonstrates strong performance in terms of accuracy and factual consistency.

PDF

FormaliSE Conference 2025 Conference Paper

Robustness Verification of Video Classification Neural Networks

Samuel Sasaki
Diego Manzanas Lopez
Preston K. Robinette
Taylor T. Johnson

Deep neural networks (DNNs) have shown impressive performance in computer vision tasks, driven by the availability of large datasets and advanced deep learning techniques. This success has prompted the formal methods community to explore ways of evaluating and improving the reliability and correctness of these models. These verification efforts, however, have primarily focused on neural networks that process image or feature data, overlooking architectures designed for video data. This oversight hinders the deployment of advanced computer vision techniques for safety-critical tasks such as video surveillance, self-driving, and industrial automation, where reliable performance is required. In this work, we develop a formal verification approach for video classification tasks. This includes a novel abstract convex set definition that can represent video data (image data with a temporal component), as well as new reachability methods for layers commonly used by video classification neural networks such as three-dimensional convolutional and three-dimensional pooling layers. Additionally, we construct 3 datasets: Zoom In MNIST, Zoom Out MNIST, and GTRSB Video. These are built upon common datasets from image classification (MNIST, GTSRB). These three datasets and the ST-MNIST dataset are used to train a video classification neural network and then formally verify their robustness against $\mathrm{L}_{\infty}$ norm perturbations. Our results show the scalability of our approach to different input sizes and where the main challenges in this domain are.

Details

FormaliSE Conference 2024 Conference Paper

Case Study: Neural Network Malware Detection Verification for Feature and Image Datasets

Preston K. Robinette
Diego Manzanas Lopez
Serena Serbinowska
Kevin Leach
Taylor T. Johnson

Malware, or software designed with harmful intent, is an ever-evolving threat that can have drastic effects on both individuals and institutions. Neural network malware classification systems are key tools for combating these threats but are vulnerable to adversarial machine learning attacks. These attacks perturb input data to cause misclassification, bypassing protective systems. Existing defenses often rely on enhancing the training process, thereby increasing the model’s robustness to these perturbations, which is quantified using verification. While training improvements are necessary, we propose focusing on the verification process used to evaluate improvements to training. As such, we present a case study that evaluates a novel verification domain that will help to ensure tangible safeguards against adversaries and provide a more reliable means of evaluating the robustness and effectiveness of anti-malware systems. To do so, we describe malware classification and two types of common malware datasets (feature and image datasets), demonstrate the certified robustness accuracy of malware classifiers using the Neural Network Verification (NNV) and Neural Network Enumeration (nnenum) tools 1, and outline the challenges and future considerations necessary for the improvement and refinement of the verification of malware classification. By evaluating this novel domain as a case study, we hope to increase its visibility, encourage further research and scrutiny, and ultimately enhance the resilience of digital systems against malicious attacks.

Details

AAAI Conference 2024 Conference Paper

Formal Logic Enabled Personalized Federated Learning through Property Inference

Ziyan An
Taylor T. Johnson
Meiyi Ma

Recent advancements in federated learning (FL) have greatly facilitated the development of decentralized collaborative applications, particularly in the domain of Artificial Intelligence of Things (AIoT). However, a critical aspect missing from the current research landscape is the ability to enable data-driven client models with symbolic reasoning capabilities. Specifically, the inherent heterogeneity of participating client devices poses a significant challenge, as each client exhibits unique logic reasoning properties. Failing to consider these device-specific specifications can result in critical properties being missed in the client predictions, leading to suboptimal performance. In this work, we propose a new training paradigm that leverages temporal logic reasoning to address this issue. Our approach involves enhancing the training process by incorporating mechanically generated logic expressions for each FL client. Additionally, we introduce the concept of aggregation clusters and develop a partitioning algorithm to effectively group clients based on the alignment of their temporal reasoning properties. We evaluate the proposed method on two tasks: a real-world traffic volume prediction task consisting of sensory data from fifteen states and a smart city multi-task prediction utilizing synthetic data. The evaluation results exhibit clear improvements, with performance accuracy improved by up to 54% across all sequential prediction models.

PDF Details DOI

ECAI Conference 2024 Conference Paper

Sanitizing Hidden Information with Diffusion Models

Preston K. Robinette
Daniel Moyer
Taylor T. Johnson

Information hiding is the process of embedding data within another form of data, often to conceal its existence or prevent unauthorized access. This process is commonly used in various forms of secure communications (steganography) that can be used by bad actors to propagate malware, exfiltrate victim data, and discreetly communicate. Recent work has utilized deep neural networks to remove this hidden information in a defense mechanism known as sanitization. Previous deep learning works, however, are unable to scale efficiently beyond the MNIST dataset. In this work, we present a novel sanitization method called DM-SUDS that utilizes a diffusion model framework to sanitize/remove hidden information from image-into-image universal and dependent steganography from CIFAR-10 and ImageNet datasets. We evaluate DM-SUDS against three different baselines using MSE, PSNR, SSIM, and NCC metrics and provide further detailed analysis through an ablation study. DM-SUDS outperforms all three baselines and significantly improves image preservation MSE by 50. 44%, PSNR by 12. 69%, SSIM by 11. 49%, and NCC by 3. 26% compared to previous deep learning approaches. Additionally, we introduce a novel evaluation specification that considers the successful removal of hidden information (safety) as well as the resulting quality of the sanitized image (utility). We further demonstrate the versatility of this method with an application in an audio case study, demonstrating its broad applicability to additional domains.

Details

ECAI Conference 2023 Conference Paper

SUDS: Sanitizing Universal and Dependent Steganography

Preston K. Robinette
Hanchen D. Wang
Nishan Shehadeh
Daniel Moyer
Taylor T. Johnson

Steganography, or hiding messages in plain sight, is a form of information hiding that is most commonly used for covert communication. As modern steganographic mediums include images, text, audio, and video, this communication method is being increasingly used by bad actors to propagate malware, exfiltrate data, and discreetly communicate. Current protection mechanisms rely upon steganalysis, or the detection of steganography, but these approaches are dependent upon prior knowledge, such as steganographic signatures from publicly available tools and statistical knowledge about known hiding methods. These dependencies render steganalysis useless against new or unique hiding methods, which are becoming increasingly common with the application of deep learning models. To mitigate the shortcomings of steganalysis, this work focuses on a deep learning sanitization technique called SUDS that is not reliant upon knowledge of steganographic hiding techniques and is able to sanitize universal and dependent steganography. SUDS is tested using least significant bit method (LSB), dependent deep hiding (DDH), and universal deep hiding (UDH). We demonstrate the capabilities and limitations of SUDS by answering five research questions, including baseline comparisons and an ablation study. Additionally, we apply SUDS to a real-world scenario, where it is able to increase the resistance of a poisoned classifier against attacks by 1375%.

Details

UAI Conference 2022 Conference Paper

Physics guided neural networks for spatio-temporal super-resolution of turbulent flows

Tianshu Bao
Shengyu Chen
Taylor T. Johnson
Peyman Givi
Shervin Sammak
Xiaowei Jia

Direct numerical simulation (DNS) of turbulent flows is computationally expensive and cannot be applied to flows with large Reynolds numbers. Low-resolution large eddy simulation (LES) is a popular alternative, but it is unable to capture all of the scales of turbulent transport accurately. Reconstructing DNS from low-resolution LES is critical for large-scale simulation in many scientific and engineering disciplines, but it poses many challenges to existing super-resolution methods due to the complexity of turbulent flows and computational cost of generating frequent LES data. We propose a physics-guided neural network for reconstructing frequent DNS from sparse LES data by enhancing its spatial resolution and temporal frequency. Our proposed method consists of a partial differential equation (PDE)-based recurrent unit for capturing underlying temporal processes and a physics-guided super-resolution model that incorporates additional physical constraints. We demonstrate the effectiveness of both components in reconstructing the Taylor-Green Vortex using sparse LES data. Moreover, we show that the proposed recurrent unit can preserve the physical characteristics of turbulent flows by leveraging the physical relationships in the Navier-Stokes equation.

Details

FormaliSE Conference 2019 Conference Paper

Parallelizable reachability analysis algorithms for feed-forward neural networks

Hoang-Dung Tran
Patrick Musau
Diego Manzanas Lopez
Xiaodong Yang
Luan Viet Nguyen
Weiming Xiang 0001
Taylor T. Johnson

Artificial neural networks (ANN) have displayed considerable utility in a wide range of applications such as image processing, character and pattern recognition, self-driving cars, evolutionary robotics, and non-linear system identification and control. While ANNs are able to carry out complicated tasks efficiently, they are susceptible to unpredictable and errant behavior due to irregularities that emanate from their complex non-linear structure. As a result, there have been reservations about incorporating them into safety-critical systems. In this paper, we present a reachability analysis method for feed-forward neural networks (FNN) that employ rectified linear units (ReLUs) as activation functions. The crux of our approach relies on three reachable-set computation algorithms, namely exact schemes, lazy-approximate schemes, and mixing schemes. The exact scheme computes an exact reachable set for FNN, while the lazy-approximate and mixing schemes generate an over-approximation of the exact reachable set. All schemes are designed efficiently to run on parallel platforms to reduce the computation time and enhance the scalability. Our methods are implemented in a toolbox called, NNV, and is evaluated using a set of benchmarks that consist of realistic neural networks with sizes that range from tens to a thousand neurons. Notably, NNV successfully computes and visualizes the exact reachable sets of the real world ACAS Xu deep neural networks (DNNs), which are a variant of a family of novel airborne collision detection systems known as the ACAS System X, using a representation of tens to hundreds of polyhedra.

Details

TCS Journal 2015 Journal Article

Safe and stabilizing distributed multi-path cellular flows

Taylor T. Johnson
Sayan Mitra

We study the problem of distributed traffic control in the partitioned plane, where the movement of all entities (robots, vehicles, etc.) within each geographic partition (cell) is the same. Each cell is controlled by software to move entities across the cell to route entities from sources to targets without collisions. We present a formal model of a distributed traffic control protocol that guarantees minimum separation between entities, even as the software controlling some cells fails by crashing. The distributed traffic control protocol relies on two principles: (a) temporary blocking entity transfers between adjacent cells for maintenance of safety and (b) local geographical routing for guaranteeing progress of entities to their targets. Establishing liveness in distributed traffic control systems is challenging, but liveness analysis will be necessary to apply distributed algorithms in applications like coordinating robot swarms and intelligent highway systems. Once new failures stop occurring, in the case of a single target cell, the protocol is guaranteed to self-stabilize and entities with feasible paths to the target cell make progress towards it. For multiple targets, failures may cause deadlocks in the system, so we identify a class of non-deadlocking failures where all entities are guaranteed to make progress to their respective targets. Our assertional proofs may serve as templates for the analysis of other distributed traffic control protocols. We also present simulation results to validate the formal model, and to provide estimates of entity throughput as a function of entity velocity, safety separation distance, single-target path complexity, failure-recovery rates, and multi-target path complexity.

Details DOI