arXiv subjects

Pengfei Yang

Publications and source records attributed to Pengfei Yang.

At least 37 records · Page 2Linked to original sources

arXiv2024

Patch Synthesis for Property Repair of Deep Neural Networks

Deep neural networks (DNNs) are prone to various dependability issues, such as adversarial attacks, which hinder their adoption in safety-critical domains. Recently, NN repair techniques have been proposed to address these issues while preserving original performance by locating and modifying guilty neurons and their parameters. However, existing repair approaches are often limited to specific data sets and do not provide theoretical guarantees for the effectiveness of the repairs. To address these limitations, we introduce PatchPro, a novel patch-based approach for property-level repair of DNNs, focusing on local robustness. The key idea behind PatchPro is to construct patch modules that, when integrated with the original network, provide specialized repairs for all samples within the robustness neighborhood while maintaining the network's original performance. Our method incorporates formal verification and a heuristic mechanism for allocating patch modules, enabling it to defend against adversarial attacks and generalize to other inputs. PatchPro demonstrates superior efficiency, scalability, and repair success rates compared to existing DNN repair methods, i.e., realizing provable property-level repair for 100% cases across multiple high-dimensional datasets.

cs.LG↗

arXiv2024

DeepCDCL: An CDCL-based Neural Network Verification Framework

Neural networks in safety-critical applications face increasing safety and security concerns due to their susceptibility to little disturbance. In this paper, we propose DeepCDCL, a novel neural network verification framework based on the Conflict-Driven Clause Learning (CDCL) algorithm. We introduce an asynchronous clause learning and management structure, reducing redundant time consumption compared to the direct application of the CDCL framework. Furthermore, we also provide a detailed evaluation of the performance of our approach on the ACAS Xu and MNIST datasets, showing that a significant speed-up is achieved in most cases.

cs.LG↗

arXiv2023

Extending the coherence time limit of a single-alkali-atom qubit by suppressing phonon-jumping-induced decoherence

In the fields of quantum metrology and quantum information processing with the system of optically trapped single neutral atoms, the coherence time of qubit encoded in the electronic states is regarded as one of the most important parameters. Longer coherence time is always pursued for higher precision of measurement and quantum manipulation. The coherence time is usually assumed to be merely determined by relative stability of the energy between the electronic states, and the analysis of the decoherence was conducted by treating the atom motion classically. We proposed a complete description of the decoherence of a qubit encoded in two ground electronic states of an optically trapped alkali atom by adopting a full description of the atomic wavefunction. The motional state, i.e., the phonon state, is taken into account. In addition to decoherence due to the variance of differential light shift (DLS), a new decoherence mechanism, phonon-jumping-induced decoherence (PJID), was discovered and verified experimentally. The coherence time of a single-cesium-atom qubit can be extended to $T_2\approx 20$ s by suppressing both the variances of DLS and PJID by trapping the atom in a blue-detuned bottle beam trap (BBT) and preparing the atom in its three-dimensional motional ground states. The coherence time is the longest for a qubit encoded in an optically trapped single alkali atom. Our work provides a deep understanding of the decoherence mechanism for single atom qubits and thus provides a new way to extend the coherence time limit. The method can be applied for other atoms and molecules, opening up new prospects for high-precision control the quantum states of optically trapped atoms or molecules.

quant-ph↗

arXiv2023

Resolved Raman sideband cooling of a single optically trapped cesium atom

We developed a resolved Raman sideband cooling scheme that can efficiently prepare a single optically trapped cesium (Cs) atom in its motional ground states. A two-photon Raman process between two outermost Zeeman sublevels in a single hyperfine state is applied to reduce the phonon number. Our scheme is less sensitive to the variation in the magnetic field than the commonly used scheme where the two outermost Zeeman sublevels belonging to the two separate ground hyperfine states are taken. Fast optical pumping with less spontaneous emission guarantees the efficiency of the cooling process. After cooling for 50 ms, 82% of the Cs atoms populate their three-dimensional ground states. Our scheme improves the long-term stability of Raman sideband cooling in the presence of magnetic field drift and is thus suitable for cooling other trapped atoms or ions with abundant magnetic sublevels.

quant-ph↗

arXiv2023

TrajPAC: Towards Robustness Verification of Pedestrian Trajectory Prediction Models

Robust pedestrian trajectory forecasting is crucial to developing safe autonomous vehicles. Although previous works have studied adversarial robustness in the context of trajectory forecasting, some significant issues remain unaddressed. In this work, we try to tackle these crucial problems. Firstly, the previous definitions of robustness in trajectory prediction are ambiguous. We thus provide formal definitions for two kinds of robustness, namely label robustness and pure robustness. Secondly, as previous works fail to consider robustness about all points in a disturbance interval, we utilise a probably approximately correct (PAC) framework for robustness verification. Additionally, this framework can not only identify potential counterexamples, but also provides interpretable analyses of the original methods. Our approach is applied using a prototype tool named TrajPAC. With TrajPAC, we evaluate the robustness of four state-of-the-art trajectory prediction models -- Trajectron++, MemoNet, AgentFormer, and MID -- on trajectories from five scenes of the ETH/UCY dataset and scenes of the Stanford Drone Dataset. Using our framework, we also experimentally study various factors that could influence robustness performance.

cs.AI↗

arXiv2023

Incremental Satisfiability Modulo Theory for Verification of Deep Neural Networks

Constraint solving is an elementary way for verification of deep neural networks (DNN). In the domain of AI safety, a DNN might be modified in its structure and parameters for its repair or attack. For such situations, we propose the incremental DNN verification problem, which asks whether a safety property still holds after the DNN is modified. To solve the problem, we present an incremental satisfiability modulo theory (SMT) algorithm based on the Reluplex framework. We simulate the most important features of the configurations that infers the verification result of the searching branches in the old solving procedure (with respect to the original network), and heuristically check whether the proofs are still valid for the modified DNN. We implement our algorithm as an incremental solver called DeepInc, and exerimental results show that DeepInc is more efficient in most cases. For the cases that the property holds both before and after modification, the acceleration can be faster by several orders of magnitude, showing that DeepInc is outstanding in incrementally searching for counterexamples. Moreover, based on the framework, we propose the multi-objective DNN repair problem and give an algorithm based on our incremental SMT solving algorithm. Our repair method preserves more potential safety properties on the repaired DNNs compared with state-of-the-art.

cs.AI↗

arXiv2022

Safety Analysis of Autonomous Driving Systems Based on Model Learning

We present a practical verification method for safety analysis of the autonomous driving system (ADS). The main idea is to build a surrogate model that quantitatively depicts the behaviour of an ADS in the specified traffic scenario. The safety properties proved in the resulting surrogate model apply to the original ADS with a probabilistic guarantee. Furthermore, we explore the safe and the unsafe parameter space of the traffic scenario for driving hazards. We demonstrate the utility of the proposed approach by evaluating safety properties on the state-of-the-art ADS in literature, with a variety of simulated traffic scenarios.

cs.AI↗

arXiv2022

10-Hertz quantum light source generation on the cesium D2 line using single photon modulation

Generation of quantum light source is a promising technique to overcome the standard quantum limit in precision measurement. Here, we demonstrate an experimental generation of quadrature squeezing resonating on the cesium D2 line down to 10 Hz for the first time. The maximum squeezing in audio frequency band is 5.57 dB. Moreover, we have presented a single-photon modulation locking to control the squeezing angle, while effectively suppressing the influence of laser noise on low-frequency squeezing. The whole system operates steadily for hours. The generated low-frequency quantum light source can be applied in quantum metrology,light-matter interaction investigation and quantum memory in the audio frequency band and even below.

quant-ph↗

arXiv2022

Gate fidelity, dephasing, and "magic" trapping of optically trapped neutral atom

The fidelity of the gate operation and the coherence time of neutral atoms trapped in an optical dipole trap are figures of merit for the applications. The motion of the trapped atom is one of the key factors which influence the gate fidelity and coherence time. The motion has been considered as a classical oscillator in analyzing the influence. Here we treat the motion of the atom as a quantum oscillator. The population on the vibrational states of the atom are considered in analyzing the gate fidelity and decoherence. We show that the fidelity of a coherent rotation gate is dramatically limited by the temperature of a thermally trapped atom. We also show that the dephasing between the two hyperfine states due to the thermal motion of the atom could rephase naturally if the differential frequency shift is stable and the vibrational states do not change. The decoherence due to the fluctuations of the trap laser intensity is also discussed. Both the gate fidelity and coherence time can be dramatically enhanced by cooling the atom into vibrational ground states and/or by using a blue-detuned trap. More importantly, we propose a "magic" trapping condition by preparing the atom into specific vibrational states.

quant-ph↗

arXiv2022

Realization of strong coupling between deterministic single-atom arrays and a high-finesse miniature optical cavity

We experimentally demonstrate strong coupling between a one-dimensional (1D) single-atom array and a high-finesse miniature cavity. The atom array is obtained by loading single atoms into a 1D optical tweezer array with dimensions of 1$\times$11. Therefore, a deterministic number of atoms is obtained, and the atom number is determined by imaging the atom array on a CCD camera in real time. By precisely controlling the position and spacing of the atom array in the high finesse Fabry--Perot cavity, all the atoms in the array are strongly coupled to the cavity simultaneously. The vacuum Rabi splitting spectra are discriminated for deterministic atom numbers from 1 to 8, and the $\sqrt{N}$ dependence of the collective enhancement of the coupling strength on atom number $N$ is validated at the single-atom level.

quant-ph↗

arXiv2022

Pre-stressed Bi-stable Hair Clip Mechanism for Faster Swimming Robots

Structural instability is a hazard that leads to catastrophic failure and is generally avoided through special designs. A trend, however, has emerged over the past decades pointing to the harnessing of mechanisms with instability. Inspired by the snapping of a hair clip, we are finessing the unique characteristics of the lateral-torsional buckling of beams and the snap-through of pre-buckled dome-like thin-wall structures in a new field: the in-plane prestressed mechanism. Analyses reveal how the 2D-3D assembly of an in-plane prestressed actuator (IPA) is achieved and how the post-buckling energy landscape is pictured. Combining them with soft robotics, we show that the inclusion of a bistable IPA can enormously enhance the performance of an underwater fish robot as well as inspire a finger-like soft gripper.

cs.RO↗

arXiv2022

Defensive Design of Saturating Counters Based on Differential Privacy

The saturating counter is the basic module of the dynamic branch predictor, which involves the core technique to improve instruction level parallelism performance in modern processors. However, most studies focus on the performance improvement and hardware consumption of saturating counters, while ignoring the security problems they may cause. In this paper, we creatively propose to study and design saturating counters from the defense perspective of differential privacy, so that attackers cannot distinguish the states that saturating counters are in and further infer sensitive information. To obtain theoretical guarantees, we use Markov chain to formalize the attack algorithm applied to the saturating counter, investigate into the optimal attack strategy and calculate the probability of successful attack. Furthermore, we find that the attacker is able to accurately guess the branch execution of the victim's process in the existing saturating counters. To avoid this, we design a new probabilistic saturating counter, which generalizes the existing conventional and probabilistic saturating counters. The guarantee of differential privacy is applied to deduce parameters of the new saturating counters so that the security requirement can be satisfied. We also theoretically calculate the misprediction rate when the saturating counter reaches the steady state. The experimental results on testing programs show that the calculated theoretical results agree with the experimental performances. Compared with the existing conventional and probabilistic saturating counters, when the parameters of our designed models are selected appropriately, the new saturating counters can not only ensure similar operational performance, but also establish strict security guarantee.

cs.CR↗

arXiv2022

QCD sum rule study for hidden-strange pentaquarks

Inspired by the LHCb's observations of hidden-charm $P_{c(s)}$ states, we study their hidden-strange analogues $P_s$ states in both $[udu][\bar ss]$ and $[uds][\bar su]$ configurations. We investigate the $P_s$ pentaquark states in $p\eta^\prime$, $p\phi$, $\Lambda K$, $\Sigma K$ and $\Sigma^\ast K^\ast$ structures with $J^P = \frac{1}{2}^-$ and $\Sigma ^\ast K$ and $\Sigma K^\ast$ with $J^P = \frac{3}{2}^-$, and calculate their masses in the framework of QCD sum rules. Our numerical results show that the extracted hadron masses for all the $p\eta^\prime$, $p\phi$, $\Lambda K$, $\Sigma K$ and $\Sigma^\ast K^\ast$ structures are much higher than $\Sigma K$ mass threshold and masses for $\Sigma ^\ast K$ and $\Sigma K^\ast$ also higher than threshold of corresponding hadron, so that no bound state exists in such channels, which is consistent with the experimental status to date.

hep-ph↗

arXiv2022

Weight Expansion: A New Perspective on Dropout and Generalization

While dropout is known to be a successful regularization technique, insights into the mechanisms that lead to this success are still lacking. We introduce the concept of \emph{weight expansion}, an increase in the signed volume of a parallelotope spanned by the column or row vectors of the weight covariance matrix, and show that weight expansion is an effective means of increasing the generalization in a PAC-Bayesian setting. We provide a theoretical argument that dropout leads to weight expansion and extensive empirical support for the correlation between dropout and weight expansion. To support our hypothesis that weight expansion can be regarded as an \emph{indicator} of the enhanced generalization capability endowed by dropout, and not just as a mere by-product, we have studied other methods that achieve weight expansion (resp.\ contraction), and found that they generally lead to an increased (resp.\ decreased) generalization ability. This suggests that dropout is an attractive regularizer, because it is a computationally cheap method for obtaining weight expansion. This insight justifies the role of dropout as a regularizer, while paving the way for identifying regularizers that promise improved generalization through weight expansion.

cs.LG↗

arXiv2021

Numerical analysis of electrohydrodynamic (EHD) instability in dielectric liquid-gas flows subjected to unipolar injection

In this work, the electrohydrodynamic (EHD) instability induced by a unipolar charge injection is extended from a single-phase dielectric liquid to a two-phase system that consists of a liquid-air interface. A volume of fluid (VOF) model based two-phase solver was developed with simplified Maxwell equations implemented in the open-source platform OpenFOAM\textsuperscript. The numerically obtained critical value for the linear stability matches well with the theoretical values. To highlight the effect of the slip boundary at interface, the deformation of the interface is ignored. A bifurcation diagram with hysteresis loop linking the linear and finite amplitude criteria, which is Uf = 0.059, was obtained in this situation. It is concluded that the lack of viscous effect at interface leads to a significant increase in the flow intensity, which is the reason for the smaller instability threshold in two-phase system. The presence of interface also changes the flow structure and makes the flow vortices shift closer to the interface.

physics.flu-dyn↗

arXiv2021

Ensemble Defense with Data Diversity: Weak Correlation Implies Strong Robustness

In this paper, we propose a framework of filter-based ensemble of deep neuralnetworks (DNNs) to defend against adversarial attacks. The framework builds an ensemble of sub-models -- DNNs with differentiated preprocessing filters. From the theoretical perspective of DNN robustness, we argue that under the assumption of high quality of the filters, the weaker the correlations of the sensitivity of the filters are, the more robust the ensemble model tends to be, and this is corroborated by the experiments of transfer-based attacks. Correspondingly, we propose a principle that chooses the specific filters with smaller Pearson correlation coefficients, which ensures the diversity of the inputs received by DNNs, as well as the effectiveness of the entire framework against attacks. Our ensemble models are more robust than those constructed by previous defense methods like adversarial training, and even competitive with the classical ensemble of adversarial trained DNNs under adversarial attacks when the attacking radius is large.

cs.LG↗

arXiv2021

Reconstructing shock front of unstable detonations based on multi-layer perceptron

The dynamics of frontal and transverse shocks in gaseous detonation waves is a complex phenomenon bringing many difficulties to both numerical and experimental research. Advanced laser-optical visualization of detonation structure may provide certain information of its reactive front, but the corresponding lead shock needs to be reconstructed building the complete flow field. Using the Multi-Layer Perceptron (MLP) approach, we propose in this study a shock front reconstruction method which can predict evolution of the lead shock wavefront from the state of the reactive front. The method is verified through the numerical results of one- and two-dimensional unstable detonations based on the reactive Euler equations with a one-step irreversible chemical reaction model. Results show that the accuracy of the proposed method depends on the activation energy of the reactive mixture, which influences prominently the cellular detonation instability and hence, the distortion of the lead shock surface. To select the input variables for training and evaluate their influence on the effectiveness of the proposed method, five groups, one with six variables and the other with four variables, are tested and analyzed in the MLP model. The trained MLP is tested in the cases with different activation energies, demonstrates the inspiring generalization capability. This paper offers a universal framework for predicting detonation frontal evolution and provides a novel way to interpret numerical and experimental results of detonation waves.

physics.flu-dyn↗

arXiv2021

Towards Practical Robustness Analysis for DNNs based on PAC-Model Learning

To analyse local robustness properties of deep neural networks (DNNs), we present a practical framework from a model learning perspective. Based on black-box model learning with scenario optimisation, we abstract the local behaviour of a DNN via an affine model with the probably approximately correct (PAC) guarantee. From the learned model, we can infer the corresponding PAC-model robustness property. The innovation of our work is the integration of model learning into PAC robustness analysis: that is, we construct a PAC guarantee on the model level instead of sample distribution, which induces a more faithful and accurate robustness evaluation. This is in contrast to existing statistical methods without model learning. We implement our method in a prototypical tool named DeepPAC. As a black-box method, DeepPAC is scalable and efficient, especially when DNNs have complex structures or high-dimensional inputs. We extensively evaluate DeepPAC, with 4 baselines (using formal verification, statistical methods, testing and adversarial attack) and 20 DNN models across 3 datasets, including MNIST, CIFAR-10, and ImageNet. It is shown that DeepPAC outperforms the state-of-the-art statistical method PROVERO, and it achieves more practical robustness analysis than the formal verification tool ERAN. Also, its results are consistent with existing DNN testing work like DeepGini.

cs.LG↗