2025

1. [J32] Scalable synthesis of formally verified neural value function for hamilton-jacobi reachability analysis
   Yujie Yang, Hanjiang Hu, Tianhao Wei, Shengbo Eben Li and Changliu Liu
   Journal of Artificial Intelligence Research, 2025
   

   Preprint Abstract Cite

   Citation Formats: BibTeX Plain Text

   Abstract:
   

   Hamilton-Jacobi (HJ) reachability analysis provides a formal method for guaranteeing safety in constrained control problems. It synthesizes a value function to represent a long-term safe set called feasible region. Early synthesis methods based on state space discretization cannot scale to high-dimensional problems, while recent methods that use neural networks to approximate value functions result in unverifiable feasible regions. To achieve both scalability and verifiability, we propose a framework for synthesizing verified neural value functions for HJ reachability analysis. Our framework consists of three stages: pre-training, adversarial training, and verification-guided training. We design three techniques to address three challenges to improve scalability respectively: boundary-guided backtracking (BGB) to improve counterexample search efficiency, entering state regularization (ESR) to enlarge feasible region, and activation pattern alignment (APA) to accelerate neural network verification. We also provide a neural safety certificate synthesis and verification benchmark called Cersyve-9, which includes nine commonly used safe control tasks and supplements existing neural network verification benchmarks. Our framework successfully synthesizes verified neural value functions on all tasks, and our proposed three techniques exhibit superior scalability and efficiency compared with existing methods.

1. [C100] Modelverification. jl: a comprehensive toolbox for formally verifying deep neural networks
   Tianhao Wei, Hanjiang Hu, Luca Marzari, Kai S Yun, Peizhi Niu, Xusheng Luo and Changliu Liu
   Conference on Computer Aided Verification, 2025
   

   Preprint Abstract Cite

   Citation Formats: BibTeX Plain Text

   Abstract:
   

   Deep Neural Networks (DNN) are crucial in approximating nonlinear functions across diverse applications, ranging from image classification to control. Verifying specific input-output properties can be a highly challenging task due to the lack of a single, self-contained framework that allows a complete range of verification types. To this end, we present \textttModelVerification.jl (MV), the first comprehensive, cutting-edge toolbox that contains a suite of state-of-the-art methods for verifying different types of DNNs and safety specifications. This versatile toolbox is designed to empower developers and machine learning practitioners with robust tools for verifying and ensuring the trustworthiness of their DNN models.

2. [C93] Safe PDE Boundary Control with Neural Operators
   Hanjiang Hu and Changliu Liu
   Learning for Dynamics and Control Conference, 2025
   

   Preprint Code Abstract Cite

   Citation Formats: BibTeX Plain Text

   Abstract:
   

   The physical world dynamics are generally governed by underlying partial differential equations (PDEs) with unknown analytical forms in science and engineering problems. Neural network based data-driven approaches have been heavily studied in simulating and solving PDE problems in recent years, but it is still challenging to move forward from understanding to controlling the unknown PDE dynamics. PDE boundary control instantiates a simplified but important problem by only focusing on PDE boundary conditions as the control input and output. However, current model-free PDE controllers cannot ensure the boundary output satisfies some given user-specified safety constraint. To this end, we propose a safety filtering framework to guarantee the boundary output stays within the safe set for current model-free controllers. Specifically, we first introduce a general neural boundary control barrier function (BCBF) to ensure the feasibility of the trajectory-wise constraint satisfaction of boundary output. Based on a neural operator modeling the transfer function from boundary control input to output trajectories, we show that the change in the BCBF depends linearly on the change in input boundary, so quadratic programming-based safety filtering can be done for pre-trained model-free controllers. Extensive experiments under challenging hyperbolic, parabolic and Navier-Stokes PDE dynamics environments validate the effectiveness of the proposed method in achieving better general performance and boundary constraint satisfaction compared to the model-free controller baselines.

1. [W] Calibrating AI Trust in Complementary Human-AI Collaboration
   Hanjiang Hu, Yifan Sun and Changliu Liu
   ICRA 2025 Workshop on Workshop on Public Trust in Autonomous Systems, 2025
   

   Preprint Page Abstract Cite

   Citation Formats: BibTeX Plain Text

   Abstract:
   

   Human-AI collaboration is a powerful paradigm in decision-making systems, where humans and AI contribute different strengths with clear complementarity. Yet, achieving optimal team performance depends critically on proper trust in AI, ensuring humans rely on AI appropriately. In real-world scenarios, humans often lack the expertise or performance transparency to judge AI accuracy directly, creating a gap in appropriate trust calibration. In this paper, we address this challenge through three key contributions: (1) we propose a theoretical framework modeling the evolution of human trust in AI over time under AI performance uncertainty, (2) we investigate two self-calibrating trust methods, an instance-based cognitive model and a reinforcement learning (RL) model that learns trust calibration policies from experience, and (3) we conduct simulations comparing both approaches against a rule-based baseline under dynamically varying AI performance. Results show that RL-based trust calibration outperforms others in cumulative performance, while instance-based calibration offers interpretability and sample efficiency. These findings offer pathways for safe and adaptive trust alignment in human-AI collaboration toward trustworthy autonomy.

1. [U] Steering Dialogue Dynamics for Robustness against Multi-turn Jailbreaking Attacks
   Hanjiang Hu, Alexander Robey and Changliu Liu
   arXiv preprint arXiv:2503.00187, 2025
   

   Preprint Page Code Abstract Cite

   Citation Formats: BibTeX Plain Text

   Abstract:
   

   Large language models (LLMs) are shown to be vulnerable to jailbreaking attacks where adversarial prompts are designed to elicit harmful responses. While existing defenses effectively mitigate single-turn attacks by detecting and filtering unsafe inputs, they fail against multi-turn jailbreaks that exploit contextual drift over multiple interactions, gradually leading LLMs away from safe behavior. To address this challenge, we propose a safety steering framework grounded in safe control theory, ensuring invariant safety in multi-turn dialogues. Our approach models the dialogue with LLMs using state-space representations and introduces a novel neural barrier function (NBF) to detect and filter harmful queries emerging from evolving contexts proactively. Our method achieves invariant safety at each turn of dialogue by learning a safety predictor that accounts for adversarial queries, preventing potential context drift toward jailbreaks. Extensive experiments under multiple LLMs show that our NBF-based safety steering outperforms safety alignment, prompt-based steering and lightweight LLM guardrails baselines, offering stronger defenses against multi-turn jailbreaks while maintaining a better trade-off among safety, helpfulness and over-refusal. Check out the website here \urlhttps://sites.google.com/view/llm-nbf/home.