SearcharxivSearch

arXiv subjects

Yiqi Zhao

Publications and source records attributed to Yiqi Zhao.

17 recordsLinked to original sources

A Unified Perspective on Conformal Prediction and Wasserstein Distributionally Robust Optimization for Uncertainty Quantification

Uncertainty quantification from finite data is central to machine learning, optimization, and automation systems, where decisions must remain reliable under limited samples and test-time distribution shift. Conformal prediction (CP) and distributionally robust optimization (DRO) offer two complementary approaches: CP constructs data-dependent prediction sets with distribution-free finite-sample validity under exchangeability, while DRO optimizes worst-case performance over an ambiguity set around an empirical distribution. We develop a unified probabilistic perspective on CP and DRO by viewing both as ways to turn finite calibration data into a data-dependent quantile estimator that a test score falls below with high probability. From this perspective, CP and DRO correct the empirical quantile along two coordinates of the same family of estimators: CP inflates the quantile level, whereas DRO shifts the quantile value through an ambiguity radius. Both methods provide the same calibration-conditional guarantee for the true distribution, requiring the target coverage to hold with high probability over the calibration sample. Their constructions differ, however: CP uses a closed-form, distribution-free level correction, while DRO uses a value-space correction whose certified radius depends on properties of the unknown distribution and additionally guarantees coverage uniformly over the ambiguity set. This distinction emerges in the tails of the score distribution. Because CP relies on sparse upper-tail order statistics of the calibration samples, its level inflation barely moves the estimator when those samples are dense near the target quantile but overshoots when they are sparse, whereas a well-chosen DRO radius corrects in value space and may avoid this overshoot.

math.OC

Safety-aware Model Predictive Path Integral Control with Signal Temporal Logic

Safety-aware motion planning remains a challenge in robotics, especially when missions are time-critical and are under complex specifications. In this paper, we propose safety-aware-stl-mppi, a computationally efficient sampling-based receding-horizon planning framework designed to promote satisfaction of constraints expressed in Signal Temporal Logic (STL). Our approach encodes discrete-time STL formulas into candidate time-varying control barrier functions (CBF), which are integrated into a model predictive path integral (MPPI) controller. Our method inherits the benefits of low computational cost from an efficiently parallelizable sampling based planner and utilizes CBF for constraints expressed in STL. We compare against several MPPI baselines using four artificial Mars Rover planning case studies with a diverse environment and cost setups, where we show our method consistently achieving high safety and efficiency. We show a quadcopter planning experiment with NVIDIA Isaac Lab.

cs.RO

Logic-VLA: A Temporal Logic Conditioned Vision-Language-Action Model

Vision-language-action (VLA) models can follow natural-language (NL) task instructions, but such instructions may not precisely specify safety-critical or spatiotemporal requirements on the resulting behavior. We introduce Logic-VLA, a formal-requirement-aware VLA that conditions on Signal Temporal Logic (STL) specifications supplied at inference time. Logic-VLA uses a syntax-graph-based STL encoder pre-trained to capture temporal logic semantics. Policy adaptation proceeds in two stages: STL-conditioned supervised fine-tuning on satisfying demonstrations is followed by trajectory-level preference optimization over matched satisfying-violating rollout pairs using a flow-matching surrogate for Identity Preference Optimization. This formulation improves formal requirement satisfaction while preserving the nominal NL task. We evaluate Logic-VLA in closed-loop quadcopter navigation simulation across randomized photorealistic environments and test generalization to STL formulas unseen during training. Across the evaluation benchmarks, Logic-VLA improves STL satisfaction rate over an STL-blind base policy by 24.8 to 40.7 percentage points (pp) while reducing nominal NL task success by at most 1.8 pp, showing that a single VLA can adapt its behavior to varying formal requirements without requiring a separate policy for each specification.

cs.RO

Conformal Predictive Programming for Chance Constrained Optimization

We propose conformal predictive programming (CPP), a framework to solve chance constrained optimization problems, i.e., optimization problems with constraints that are functions of random variables. CPP utilizes samples from these random variables along with the quantile lemma - central to conformal prediction - to transform the chance constrained optimization problem into a deterministic problem with a quantile reformulation. CPP's main strength is an independent calibration step that provides a posteriori guarantees for the solution of this problem that are of conditional and marginal nature otherwise. These guarantees even apply in settings when assumptions required for obtaining standard a priori guarantees (e.g., in scenario optimization or sample average approximation) are unavailable, difficult to compute, or conservative. Another strength of CPP is that it can easily support different variants of conformal prediction which have been (or will be) proposed within the conformal prediction community. To illustrate this, we present robust CPP to deal with distribution shifts in the random variables and Mondrian CPP to deal with class conditional chance constraints. In a series of case studies, we show the validity of the aforementioned approaches, and illustrate the advantage of CPP as compared to scenario approach.

eess.SY

Duet: Dual-Robot Understanding via Efficient Teaching

Dual-robot collaboration enables tasks that exceed the reach and payload of a single robot, such as collaboratively transporting objects across environments and executing coordinated handovers. Data acquisition is the primary bottleneck for training these systems. To this end, we introduce DUET, a dual-robot learning framework for mobile manipulation. For efficient data collection, we create a unified dual-embodiment synchronized VR-based teleoperation system for in-domain heterogeneous robot data collection. We further develop a complementary tracking pipeline that records human-human coordination and collaborative mobile manipulation priors. To allow efficient learning, we introduce an Action Chunking Transformer based architecture that first pretrains collaborative policies on efficient human-human demonstrations, before finetuning them on a minimal set of real-robot teleoperation trajectories. We develop a benchmark of four collaborative tasks to evaluate our framework using a Unitree G1 humanoid and a Dexmate Vega1 mobile manipulator. The results demonstrate that harnessing human priors not only yields superior task performance compared to baselines trained only on robot data, but also reduces the total human effort required for data collection. Our human data collection pipeline achieves 5.4x acceleration on average from teleoperation, but we perform equally or better than robot-only data trained policies across all tasks. Our project page is available at https://zhaoy37.github.io/Duet/.

cs.RO

Compact self-matched gyrators using edge magnetoplasmons

Edge magnetoplasmons provide a natural platform for chiral electrodynamics, where broken time-reversal symmetry enforces unidirectional propagation. When probed at microwave frequencies, they offer a route to compact non-reciprocal devices. So far, implementations have suffered from large losses or required complicated matching networks. Here we show that the circulating modes coupled to capacitive gates give rise to a gyrator response, characterized by directional π phase difference between forward and reverse transmission. By engineering a three-terminal capacitive geometry, we realize a self-impedance matched gyrator in which the gyration points coincide with transmission maxima, enabling nearly lossless gyration without external matching networks. Our devices are implemented on a GaAs 2D gas, operate from 0.2 to 2 GHz, tuned by magnetic field, with sub-millimeter footprints and insertion loss as low as 2 dB. This is a factor of 100 smaller and less lossy than commercial and plasmon units, respectively. A dissipative model, in agreement with experiment, provides the fundamental physics and delivers the key materials parameters, leading the way to even less lossy devices approaching ideal operation by materials improvement. The self-impedance matched concept is broadly applicable to a variety of devices, thus providing a foundation for a new generation of high-quality microwave plasmon technology.

cond-mat.mes-hall

Formal Verification and Control with Conformal Prediction

We present recent advances in formal verification and control for autonomous systems with practical safety guarantees enabled by conformal prediction (CP), a statistical tool for uncertainty quantification. This survey is particularly motivated by learning-enabled autonomous systems (LEASs), where the complexity of learning-enabled components (LECs) poses a major bottleneck for applying traditional model-based verification and control techniques. To address this challenge, we advocate for CP as a lightweight alternative and demonstrate its use in formal verification, systems and control, and robotics. CP is appealing due to its simplicity (easy to understand, implement, and adapt), generality (requires no assumptions on learned models and underlying data distributions), and efficiency (real-time capable and accurate). This survey provides an accessible introduction to CP for non-experts interested in applying CP to autonomy problems. We particularly show how CP can be used for formal verification of LECs and the design of safe control as well as offline and online verification algorithms for LEASs. We present these techniques within a unifying framework that addresses the complexity of LEASs. Our exposition spans simple specifications, such as robot navigation tasks, to complex mission requirements expressed in temporal logic. Throughout the survey, we contrast CP with other statistical techniques, including scenario optimization and PAC-Bayes theory, highlighting advantages and limitations for verification and control. Finally, we outline open problems and promising directions for future research.

eess.SY

STL-GO: Spatio-Temporal Logic with Graph Operators for Distributed Systems with Multiple Network Topologies

Multi-agent systems (MASs) consisting of a number of autonomous agents that communicate, coordinate, and jointly sense the environment to achieve complex missions can be found in a variety of applications such as robotics, smart cities, and internet-of-things applications. Modeling and monitoring MAS requirements to guarantee overall mission objectives, safety, and reliability is an important problem. Such requirements implicitly require reasoning about diverse sensing and communication modalities between agents, analysis of the dependencies between agent tasks, and the spatial or virtual distance between agents. To capture such rich MAS requirements, we model agent interactions via multiple directed graphs, and introduce a new logic -- Spatio-Temporal Logic with Graph Operators (STL-GO). The key innovation in STL-GO are graph operators that enable us to reason about the number of agents along either the incoming or outgoing edges of the underlying interaction graph that satisfy a given property of interest; for example, the requirement that an agent should sense at least two neighboring agents whose task graphs indicate the ability to collaborate. We then propose novel distributed monitoring conditions for individual agents that use only local information to determine whether or not an STL-GO specification is satisfied. We compare the expressivity of STL-GO against existing spatio-temporal logic formalisms, and demonstrate the utility of STL-GO and our distributed monitors in a bike-sharing and a multi-drone case study.

cs.LO

Signal Temporal Logic Control Synthesis among Uncontrollable Dynamic Agents with Conformal Prediction

The control of dynamical systems under temporal logic specifications among uncontrollable dynamic agents is challenging due to the agents' a-priori unknown behavior. Existing works have considered the problem where either all agents are controllable, the agent models are deterministic and known, or no safety guarantees are provided. We propose a predictive control synthesis framework that guarantees, with high probability, the satisfaction of signal temporal logic (STL) tasks that are defined over a controllable system in the presence of uncontrollable stochastic agents. We use trajectory predictors and conformal prediction to construct probabilistic prediction regions for each uncontrollable agent that are valid over multiple future time steps. Specifically, we construct a normalized prediction region over all agents and time steps to reduce conservatism and increase data efficiency. We then formulate a worst-case bilevel mixed integer program (MIP) that accounts for all agent realizations within the prediction region to obtain an open-loop controller that provably guarantee task satisfaction with high probability. To efficiently solve this bilevel MIP, we propose an equivalent MIP program based on KKT conditions of the original bilevel formulation. Building upon this, we design a closed-loop controller, where both recursive feasibility and task satisfaction can be guaranteed with high probability. We illustrate our control synthesis framework on two case studies.

eess.SY

Distributionally Robust Predictive Runtime Verification under Spatio-Temporal Logic Specifications

Cyber-physical systems (CPS) designed in simulators, often consisting of multiple interacting agents (e.g. in multi-agent formations), behave differently in the real-world. We want to verify these systems during runtime when they are deployed. We thus propose robust predictive runtime verification (RPRV) algorithms for: (1) general stochastic CPS under signal temporal logic (STL) tasks, and (2) stochastic multi-agent systems (MAS) under spatio-temporal logic tasks. The RPRV problem presents the following challenges: (1) there may not be sufficient data on the behavior of the deployed CPS, (2) predictive models based on design phase system trajectories may encounter distribution shift during real-world deployment, and (3) the algorithms need to scale to the complexity of MAS and be applicable to spatio-temporal logic tasks. To address the challenges, we assume knowledge of an upper bound on the statistical distance between the trajectory distributions of the system at deployment and design time. We are motivated by our prior work [1, 2] where we proposed an accurate and an interpretable RPRV algorithm for general CPS, which we here extend to the MAS setting and spatio-temporal logic tasks. Specifically, we use a learned predictive model to estimate the system behavior at runtime and robust conformal prediction to obtain probabilistic guarantees by accounting for distribution shifts. Building on [1], we perform robust conformal prediction over the robust semantics of spatio-temporal reach and escape logic (STREL) to obtain centralized RPRV algorithms for MAS. We empirically validate our results in a drone swarm simulator, where we show the scalability of our RPRV algorithms to MAS and analyze the impact of different trajectory predictors on the verification result. To the best of our knowledge, these are the first statistically valid algorithms for MAS under distribution shift.

eess.SY

Programmable on-chip nonlinear photonics

Nonlinear photonics uses coherent interactions between optical waves to engineer functionality that is not possible with purely linear optics. Traditionally, the function of a nonlinear-optical device is determined during design and fixed during fabrication. In this paper, we present a photonic device with highly programmable nonlinear functionality: an optical slab waveguide with an arbitrarily reconfigurable two-dimensional distribution of $χ^{(2)}$ nonlinearity. The nonlinearity is realized using electric-field-induced $χ^{(2)}$ in a $χ^{(3)}$ material. The programmability is engineered by massively parallel control of the electric-field distribution within the device using a photoconductive layer and optical programming with a spatial light pattern. To showcase the versatility of our device, we demonstrated spectral, spatial, and spatio-spectral engineering of second-harmonic generation by tailoring arbitrary quasi-phase-matching (QPM) grating structures in two dimensions. Second-harmonic light was generated with programmable spectra, enabled by real-time in situ inverse design of QPM gratings. Flexible spatial control was also achieved, including the generation of complex waveforms such as Airy beams and the simultaneous engineering of spectral and spatial features. This allowed us to create distinct spatial light profiles across multiple wavelengths. The programmability also allowed us to demonstrate in situ, real-time compensation of fluctuations in pump laser wavelength. Our work shows that we can transcend the conventional one-device--one-function paradigm, expanding the potential applications of nonlinear optics in situations where fast device reconfigurability is not merely practically convenient but essential -- such as in programmable optical quantum gates and quantum light sources, all-optical signal processing, optical computation, and structured light for sensing.

physics.optics

Robust Conformal Prediction for STL Runtime Verification under Distribution Shift

Cyber-physical systems (CPS) designed in simulators behave differently in the real-world. Once they are deployed in the real-world, we would hence like to predict system failures during runtime. We propose robust predictive runtime verification (RPRV) algorithms under signal temporal logic (STL) tasks for general stochastic CPS. The RPRV problem faces several challenges: (1) there may not be sufficient data of the behavior of the deployed CPS, (2) predictive models are based on a distribution over system trajectories encountered during the design phase, i.e., there may be a distribution shift during deployment. To address these challenges, we assume to know an upper bound on the statistical distance (in terms of an f-divergence) between the distributions at deployment and design time, and we utilize techniques based on robust conformal prediction. Motivated by our results in [1], we construct an accurate and an interpretable RPRV algorithm. We use a trajectory prediction model to estimate the system behavior at runtime and robust conformal prediction to obtain probabilistic guarantees by accounting for distribution shifts. We precisely quantify the relationship between calibration data, desired confidence, and permissible distribution shift. To the best of our knowledge, these are the first statistically valid algorithms under distribution shift in this setting. We empirically validate our algorithms on a Franka manipulator within the NVIDIA Isaac sim environment.

eess.SY

Fairguard: Harness Logic-based Fairness Rules in Smart Cities

Smart cities operate on computational predictive frameworks that collect, aggregate, and utilize data from large-scale sensor networks. However, these frameworks are prone to multiple sources of data and algorithmic bias, which often lead to unfair prediction results. In this work, we first demonstrate that bias persists at a micro-level both temporally and spatially by studying real city data from Chattanooga, TN. To alleviate the issue of such bias, we introduce Fairguard, a micro-level temporal logic-based approach for fair smart city policy adjustment and generation in complex temporal-spatial domains. The Fairguard framework consists of two phases: first, we develop a static generator that is able to reduce data bias based on temporal logic conditions by minimizing correlations between selected attributes. Then, to ensure fairness in predictive algorithms, we design a dynamic component to regulate prediction results and generate future fair predictions by harnessing logic rules. Evaluations show that logic-enabled static Fairguard can effectively reduce the biased correlations while dynamic Fairguard can guarantee fairness on protected groups at run-time with minimal impact on overall performance.

cs.AI

EduSAT: A Pedagogical Tool for Theory and Applications of Boolean Satisfiability

Boolean Satisfiability (SAT) and Satisfiability Modulo Theories (SMT) are widely used in automated verification, but there is a lack of interactive tools designed for educational purposes in this field. To address this gap, we present EduSAT, a pedagogical tool specifically developed to support learning and understanding of SAT and SMT solving. EduSAT offers implementations of key algorithms such as the Davis-Putnam-Logemann-Loveland (DPLL) algorithm and the Reduced Order Binary Decision Diagram (ROBDD) for SAT solving. Additionally, EduSAT provides solver abstractions for five NP-complete problems beyond SAT and SMT. Users can benefit from EduSAT by experimenting, analyzing, and validating their understanding of SAT and SMT solving techniques. Our tool is accompanied by comprehensive documentation and tutorials, extensive testing, and practical features such as a natural language interface and SAT and SMT formula generators, which also serve as a valuable opportunity for learners to deepen their understanding. Our evaluation of EduSAT demonstrates its high accuracy, achieving 100% correctness across all the implemented SAT and SMT solvers. We release EduSAT as a python package in .whl file, and the source can be identified at https://github.com/zhaoy37/SAT_Solver.

cs.AI

Joint Design for Electric Fleet Operator an Charging Service Provider: Understanding the Non-Cooperative Nature

This work proposes a new modeling framework for jointly optimizing the charging network design and the logistic mobility planning for an electric vehicle fleet. Existing literature commonly assumes the existence of a single entity, the social planner, as a powerful decision maker who manages all resources. However, this is often not the case in practice. Instead of making this assumption, we specifically examine the innate noncooperative nature of two different entities involved in the planning problem. Namely, they are the charging service provider (CSP) and the fleet operator (FO). To address the strategic interaction between entities, a bilevel mixed integer program is formulated, with the CSP and FO problems expressed in the upper and lower levels respectively, in a joint decision making process. These decisions involve the CSP infrastructure siting, sizing, substation capacity upgrades, the FO fleet composition, vehicle routing, charging, and delivery assignment. To relieve computational burdens, we utilize a double loop solution architecture to iteratively reach optimality. We conduct detailed numerical studies on a synthesized small network and the simulation results reveal the unique aspects of this two entity framework. This modeling perspective can be generalized to other system design problems with two interacting agents planning and operating resources across networks.

math.OC

A Survey of Forex and Stock Price Prediction Using Deep Learning

The prediction of stock and foreign exchange (Forex) had always been a hot and profitable area of study. Deep learning application had proven to yields better accuracy and return in the field of financial prediction and forecasting. In this survey we selected papers from the DBLP database for comparison and analysis. We classified papers according to different deep learning methods, which included: Convolutional neural network (CNN), Long Short-Term Memory (LSTM), Deep neural network (DNN), Recurrent Neural Network (RNN), Reinforcement Learning, and other deep learning methods such as HAN, NLP, and Wavenet. Furthermore, this paper reviewed the dataset, variable, model, and results of each article. The survey presented the results through the most used performance metrics: RMSE, MAPE, MAE, MSE, accuracy, Sharpe ratio, and return rate. We identified that recent models that combined LSTM with other methods, for example, DNN, are widely researched. Reinforcement learning and other deep learning method yielded great returns and performances. We conclude that in recent years the trend of using deep-learning based method for financial modeling is exponentially rising.

q-fin.ST

Wavelet Denoised-ResNet CNN and LightGBM Method to Predict Forex Rate of Change

Foreign Exchange (Forex) is the largest financial market in the world. The daily trading volume of the Forex market is much higher than that of stock and futures markets. Therefore, it is of great significance for investors to establish a foreign exchange forecast model. In this paper, we propose a Wavelet Denoised-ResNet with LightGBM model to predict the rate of change of Forex price after five time intervals to allow enough time to execute trades. All the prices are denoised by wavelet transform, and a matrix of 30 time intervals is formed by calculating technical indicators. Image features are obtained by feeding the maxtrix into a ResNet. Finally, the technical indicators and image features are fed to LightGBM. Our experiments on 5-minutes USDJPY demonstrate that the model outperforms baseline modles with MAE: 0.240977x10EXP-3 MSE: 0.156x10EXP-6 and RMSE: 0.395185x10EXP-3. An accurate price prediction after 25 minutes in future provides a window of opportunity for hedge funds algorithm trading. The code is available from https://mkhushi.github.io/

q-fin.ST