Source author record

Sicun Gao

Sicun Gao appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Catalog footprint

What is connected

14works
12topics
4close collaborators

Actions

Connect this record

Log in to claim

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

14 published item(s)

preprint2026arXiv

Learning to Nudge: A Scalable Barrier Function Framework for Safe Robot Interaction in Dense Clutter

Robots operating in everyday environments must navigate and manipulate within densely cluttered spaces, where physical contact with surrounding objects is unavoidable. Traditional safety frameworks treat contact as unsafe, restricting robots to collision avoidance and limiting their ability to function in dense, everyday settings. As the number of objects grows, model-based approaches for safe manipulation become computationally intractable; meanwhile, learned methods typically tie safety to the task at hand, making them hard to transfer to new tasks without retraining. In this work we introduce Dense Contact Barrier Functions(DCBF). Our approach bypasses the computational complexity of explicitly modeling multi-object dynamics by instead learning a composable, object-centric function that implicitly captures the safety constraints arising from physical interactions. Trained offline on interactions with a few objects, the learned DCBFcomposes across arbitrary object sets at runtime, producing a single global safety filter that scales linearly and transfers across tasks without retraining. We validate our approach through simulated experiments in dense clutter, demonstrating its ability to enable collision-free navigation and safe, contact-rich interaction in suitable settings.

preprint2023arXiv

Accelerating Multi-Agent Planning Using Graph Transformers with Bounded Suboptimality

Conflict-Based Search is one of the most popular methods for multi-agent path finding. Though it is complete and optimal, it does not scale well. Recent works have been proposed to accelerate it by introducing various heuristics. However, whether these heuristics can apply to non-grid-based problem settings while maintaining their effectiveness remains an open question. In this work, we find that the answer is prone to be no. To this end, we propose a learning-based component, i.e., the Graph Transformer, as a heuristic function to accelerate the planning. The proposed method is provably complete and bounded-suboptimal with any desired factor. We conduct extensive experiments on two environments with dense graphs. Results show that the proposed Graph Transformer can be trained in problem instances with relatively few agents and generalizes well to a larger number of agents, while achieving better performance than state-of-the-art methods.

preprint2022arXiv

Quantifying Safety of Learning-based Self-Driving Control Using Almost-Barrier Functions

Path-tracking control of self-driving vehicles can benefit from deep learning for tackling longstanding challenges such as nonlinearity and uncertainty. However, deep neural controllers lack safety guarantees, restricting their practical use. We propose a new approach of learning almost-barrier functions, which approximately characterizes the forward invariant set for the system under neural controllers, to quantitatively analyze the safety of deep neural controllers for path-tracking. We design sampling-based learning procedures for constructing candidate neural barrier functions, and certification procedures that utilize robustness analysis for neural networks to identify regions where the barrier conditions are fully satisfied. We use an adversarial training loop between learning and certification to optimize the almost-barrier functions. The learned barrier can also be used to construct online safety monitors through reachability analysis. We demonstrate effectiveness of our methods in quantifying safety of neural controllers in various simulation environments, ranging from simple kinematic models to the TORCS simulator with high-fidelity vehicle dynamics simulation.

preprint2020arXiv

Provably Efficient Model-based Policy Adaptation

The high sample complexity of reinforcement learning challenges its use in practice. A promising approach is to quickly adapt pre-trained policies to new environments. Existing methods for this policy adaptation problem typically rely on domain randomization and meta-learning, by sampling from some distribution of target environments during pre-training, and thus face difficulty on out-of-distribution target environments. We propose new model-based mechanisms that are able to make online adaptation in unseen target environments, by combining ideas from no-regret online learning and adaptive control. We prove that the approach learns policies in the target environment that can quickly recover trajectories from the source environment, and establish the rate of convergence in general settings. We demonstrate the benefits of our approach for policy adaptation in a diverse set of continuous control tasks, achieving the performance of state-of-the-art methods with much lower sample complexity.

preprint2015arXiv

Towards Personalized Prostate Cancer Therapy Using Delta-Reachability Analysis

Recent clinical studies suggest that the efficacy of hormone therapy for prostate cancer depends on the characteristics of individual patients. In this paper, we develop a computational framework for identifying patient-specific androgen ablation therapy schedules for postponing the potential cancer relapse. We model the population dynamics of heterogeneous prostate cancer cells in response to androgen suppression as a nonlinear hybrid automaton. We estimate personalized kinetic parameters to characterize patients and employ $δ$-reachability analysis to predict patient-specific therapeutic strategies. The results show that our methods are promising and may lead to a prognostic tool for personalized cancer therapy.

preprint2014arXiv

Delta-Complete Analysis for Bounded Reachability of Hybrid Systems

We present the framework of delta-complete analysis for bounded reachability problems of general hybrid systems. We perform bounded reachability checking through solving delta-decision problems over the reals. The techniques take into account of robustness properties of the systems under numerical perturbations. We prove that the verification problems become much more mathematically tractable in this new framework. Our implementation of the techniques, an open-source tool dReach, scales well on several highly nonlinear hybrid system models that arise in biomedical and robotics applications.

preprint2014arXiv

Descriptive Control Theory: A Proposal

Logic is playing an increasingly important role in the engineering of real-time, hybrid, and cyber-physical systems, but mostly in the form of posterior verification and high-level analysis. The core methodology in the design of real-world systems consists mainly of control theory and numerical analysis, and has remained mostly free of logic and formal approaches. As a result, besides facing extreme difficulty in guaranteeing the reliability of these systems, engineers are also missing out the computational power of logic-based methods that has greatly advanced in the past decades. To change this situation, we need a logical and computational foundation for control theory. The name "descriptive control theory" emphasizes the overarching theme of using logic to express, analyze, and solve problems in control theory. If the program is successfully carried out, logical approaches will significantly extend existing engineering methods towards a unified methodology for handling nonlinear and hybrid systems, and bring design automation and reliability to an unprecedented level in the broad field of engineering.

preprint2014arXiv

Parameter Synthesis for Cardiac Cell Hybrid Models Using Delta-Decisions

A central problem in systems biology is to identify parameter values such that a biological model satisfies some behavioral constraints (\eg, time series). In this paper we focus on parameter synthesis for hybrid (continuous/discrete) models, as many biological systems can possess multiple operational modes with specific continuous dynamics in each mode. These biological systems are naturally modeled as hybrid automata, most often with nonlinear continuous dynamics. However, hybrid automata are notoriously hard to analyze --- even simple reachability for hybrid systems with linear differential dynamics is an undecidable problem. In this paper we present a parameter synthesis framework based on $δ$-complete decision procedures that sidesteps undecidability. We demonstrate our method on two highly nonlinear hybrid models of the cardiac cell action potential. The results show that our parameter synthesis framework is convenient and efficient, and it enabled us to select a suitable model to study and identify crucial parameter ranges related to cardiac disorders.

preprint2014arXiv

Proof Generation from Delta-Decisions

We show how to generate and validate logical proofs of unsatisfiability from delta-complete decision procedures that rely on error-prone numerical algorithms. Solving this problem is important for ensuring correctness of the decision procedures. At the same time, it is a new approach for automated theorem proving over real numbers. We design a first-order calculus, and transform the computational steps of constraint solving into logic proofs, which are then validated using proof-checking algorithms. As an application, we demonstrate how proofs generated from our solver can establish many nonlinear lemmas in the the formal proof of the Kepler Conjecture.

preprint2014arXiv

Revisiting the Complexity of Stability of Continuous and Hybrid Systems

We develop a framework to give upper bounds on the "practical" computational complexity of stability problems for a wide range of nonlinear continuous and hybrid systems. To do so, we describe stability properties of dynamical systems using first-order formulas over the real numbers, and reduce stability problems to the delta-decision problems of these formulas. The framework allows us to obtain a precise characterization of the complexity of different notions of stability for nonlinear continuous and hybrid systems. We prove that bounded versions of the stability problems are generally decidable, and give upper bounds on their complexity. The unbounded versions are generally undecidable, for which we give upper bounds on their degrees of unsolvability.

preprint2014arXiv

SReach: A Bounded Model Checker for Stochastic Hybrid Systems

In this paper we describe a new tool, SReach, which solves probabilistic bounded reachability problems for two classes of stochastic hybrid systems. The first one is (nonlinear) hybrid automata with parametric uncertainty. The second one is probabilistic hybrid automata with additional randomness for both transition probabilities and variable resets. Standard approaches to reachability problems for linear hybrid systems require numerical solutions for large optimization problems, and become infeasible for systems involving both nonlinear dynamics over the reals and stochasticity. Our approach encodes stochastic information by using random variables, and combines the randomized sampling, a $δ$-complete decision procedure, and statistical tests. SReach utilizes the $δ$-complete decision procedure to solve reachability problems in a sound manner, i.e., it always decides correctly if, for a given assignment to all random variables, the system actually reaches the unsafe region. The statistical tests adapted guarantee arbitrary small error bounds between probabilities estimated by SReach and real ones. Compared to standard simulation-based methods, our approach supports non-deterministic branching, increases the coverage of simulation, and avoids the zero-crossing problem. We demonstrate our method's feasibility by applying SReach to three representative biological models and to additional benchmarks for nonlinear hybrid systems with multiple probabilistic system parameters.

preprint2013arXiv

Satisfiability Modulo ODEs

We study SMT problems over the reals containing ordinary differential equations. They are important for formal verification of realistic hybrid systems and embedded software. We develop delta-complete algorithms for SMT formulas that are purely existentially quantified, as well as exists-forall formulas whose universal quantification is restricted to the time variables. We demonstrate scalability of the algorithms, as implemented in our open-source solver dReal, on SMT benchmarks with several hundred nonlinear ODEs and variables.

preprint2012arXiv

Delta-Complete Decision Procedures for Satisfiability over the Reals

We introduce the notion of "δ-complete decision procedures" for solving SMT problems over the real numbers, with the aim of handling a wide range of nonlinear functions including transcendental functions and solutions of Lipschitz-continuous ODEs. Given an SMT problem φand a positive rational number δ, a δ-complete decision procedure determines either that φis unsatisfiable, or that the "δ-weakening" of φis satisfiable. Here, the δ-weakening of φis a variant of φthat allows δ-bounded numerical perturbations on φ. We prove the existence of δ-complete decision procedures for bounded SMT over reals with functions mentioned above. For functions in Type 2 complexity class C, under mild assumptions, the bounded δ-SMT problem is in NP^C. δ-Complete decision procedures can exploit scalable numerical methods for handling nonlinearity, and we propose to use this notion as an ideal requirement for numerically-driven decision procedures. As a concrete example, we formally analyze the DPLL<ICP> framework, which integrates Interval Constraint Propagation (ICP) in DPLL(T), and establish necessary and sufficient conditions for its δ-completeness. We discuss practical applications of δ-complete decision procedures for correctness-critical applications including formal verification and theorem proving.

preprint2012arXiv

Delta-Decidability over the Reals

Given any collection F of computable functions over the reals, we show that there exists an algorithm that, given any L_F-sentence φcontaining only bounded quantifiers, and any positive rational number δ, decides either "φis true", or "a δ-strengthening of φis false". Under mild assumptions, for a C-computable signature F, the δ-decision problem for bounded Σ_k-sentences in L_F resides in (Σ_k^P)^C. The results stand in sharp contrast to the well-known undecidability results, and serve as a theoretical basis for the use of numerical methods in decision procedures for nonlinear first-order theories over the reals.