Trust snapshot

Quick read

Trust 21 - EmergingVerification L1Unclaimed author
24works
0followers
16topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

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

Published work

24 published item(s)

preprint2026arXiv

Are LLM Decisions Faithful to Verbal Confidence?

Large Language Models (LLMs) can produce surprisingly sophisticated estimates of their own uncertainty. However, it remains unclear to what extent this expressed confidence is tied to the reasoning, knowledge, or decision making of the model. To test this, we introduce $\textbf{RiskEval}$: a framework designed to evaluate whether models adjust their abstention policies in response to varying error penalties. Our evaluation of several frontier models reveals a critical dissociation: models are neither cost-aware when articulating their verbal confidence, nor strategically responsive when deciding whether to engage or abstain under high-penalty conditions. Even when extreme penalties render frequent abstention the mathematically optimal strategy, models almost never abstain, resulting in utility collapse. This indicates that calibrated verbal confidence scores may not be sufficient to create trustworthy and interpretable AI systems, as current models lack the strategic agency to convert uncertainty signals into optimal and risk-sensitive decisions.

preprint2026arXiv

DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning

General reasoning represents a long-standing and formidable challenge in artificial intelligence. Recent breakthroughs, exemplified by large language models (LLMs) and chain-of-thought prompting, have achieved considerable success on foundational reasoning tasks. However, this success is heavily contingent upon extensive human-annotated demonstrations, and models' capabilities are still insufficient for more complex problems. Here we show that the reasoning abilities of LLMs can be incentivized through pure reinforcement learning (RL), obviating the need for human-labeled reasoning trajectories. The proposed RL framework facilitates the emergent development of advanced reasoning patterns, such as self-reflection, verification, and dynamic strategy adaptation. Consequently, the trained model achieves superior performance on verifiable tasks such as mathematics, coding competitions, and STEM fields, surpassing its counterparts trained via conventional supervised learning on human demonstrations. Moreover, the emergent reasoning patterns exhibited by these large-scale models can be systematically harnessed to guide and enhance the reasoning capabilities of smaller models.

preprint2026arXiv

Graph-Based Financial Fraud Detection with Calibrated Risk Scoring and Structural Regularization

Financial transaction fraud prevention faces challenges such as complex relationship structures, concealed behavioral patterns, and dynamically changing data distribution. Discrimination models relying solely on independent sample features are insufficient to fully characterize the risks of group collaboration and chain transfers within transaction networks. This paper proposes a graph neural network representation learning and risk discrimination framework for financial transaction fraud prevention. It integrates transaction records and identity information into node attributes and constructs a transaction graph based on shared attributes and interaction consistency to explicitly model inter-transaction relationships. In model design, a multi-layer message passing mechanism is employed to aggregate neighborhood information, learn node embedding representations containing structural context semantics, and output transaction-level fraud probability and risk scores through a lightweight risk discrimination head. A weighted supervision objective is introduced to mitigate training bias caused by class imbalance, and structural consistency regularization constraints are combined to suppress the impact of noisy edges on representation drift, thereby improving the stability and usability of risk characterization. Experiments are conducted on a publicly available financial transaction dataset, comparing various methods in the same direction and comprehensively evaluating them under a unified evaluation protocol. The results show that the proposed method outperforms other methods in risk ranking and probability calibration quality, validating the effectiveness of graph structure modeling and representation learning collaboration in financial transaction fraud prevention.

preprint2026arXiv

InfiniDepth: Arbitrary-Resolution and Fine-Grained Depth Estimation with Neural Implicit Fields

Existing depth estimation methods are fundamentally limited to predicting depth on discrete image grids. Such representations restrict their scalability to arbitrary output resolutions and hinder the geometric detail recovery. This paper introduces InfiniDepth, which represents depth as neural implicit fields. Through a simple yet effective local implicit decoder, we can query depth at continuous 2D coordinates, enabling arbitrary-resolution and fine-grained depth estimation. To better assess our method's capabilities, we curate a high-quality 4K synthetic benchmark from five different games, spanning diverse scenes with rich geometric and appearance details. Extensive experiments demonstrate that InfiniDepth achieves state-of-the-art performance on both synthetic and real-world benchmarks across relative and metric depth estimation tasks, particularly excelling in fine-detail regions. It also benefits the task of novel view synthesis under large viewpoint shifts, producing high-quality results with fewer holes and artifacts.

preprint2026arXiv

Sub-Doppler rubidium atom cooling using a programmable agile integrated PZT-on-SiN resonator

Programmability and precise control of laser frequency are essential for quantum experiments and applications such as atomic clocks, quantum computers, and cold-atom sensors. Current systems use bulky, power-hungry modulators and frequency shifters which are difficult to integrate and limit portability and scalability. We report an electrically controllable, agile optical frequency source based on a semiconductor laser stabilized to a photonic-integrated, lead zirconate titanate (PZT)-actuated resonator cavity. We demonstrate this approach with precision programmable frequency control of a 780-nm laser that can periodically reference to rubidium spectroscopy followed by fast, programmable, arbitrary frequency tuning sequences for quantum control. We use this approach to demonstrate sub-Doppler cooling of rubidium-87 without any external modulators, achieving atom-cloud temperatures as low as 16 $μ$K. The device achieves a tuning strength up to 1 GHz/V with 11 MHz modulation bandwidth while consuming only 10 nW of electrical power. This work establishes a route toward compact, low-power, and chip-scale laser systems for next-generation quantum and atomic sensing technologies.

preprint2026arXiv

Variational Theory and Parquet Diagrams for Nuclear Systems: A Comprehensive Study of Neutron Matter

To deal with the problem of realistic nuclear interactions we have combined techniques of the Jastrow-Feenberg variational method and the local parquet-diagram theory. In the language of diagrammatic perturbation theory, ``commutator diagrams'' can be identified with non-parquet diagrams. We examine the physical processes described by these terms and include the relevant diagrams in a way that is suggested by the Jastrow-Feenberg approach. We show that the corrections from non-parquet contributions are, at short distances, larger than all other many-body effects. We examine here neutron matter as a prototype of systems with state-dependent interactions. Calculations are carried out for neutrons interacting via the so-called $v_8$ version of four popular interactions. We determine the structure and effective interactions and apply the method to the calculation of the energetics, structure and dynamic properties such as the single-particle self-energy and the dynamic response functions as well as BCS pairing in both singlet and triplet states. We find that many-body correlations lead to a strong reduction of the spin-orbit interaction, and, therefore, to a suppression of the $^3P_2$ and $^3P_2$-$^3F_2$ gaps. We also find pairing in $^3P_0$ states; the strength of the pairing gap depends sensitively on the potential model employed.

preprint2025arXiv

BALI: Branch-Aware Loop Invariant Inference with Large Language Models

Loop invariants are fundamental for reasoning about the correctness of iterative algorithms. However, deriving suitable invariants remains a challenging and often manual task, particularly for complex programs. In this paper, we introduce BALI, a branch-aware framework that integrates large language models (LLMs) to enhance the inference and verification of loop invariants. Our approach combines automated reasoning with branch-aware static program analysis to improve both precision and scalability. Specifically, unlike prior LLM-only guess-and-check methods, BALI first verifies branch-sequence-level (path-level) clauses with SMT and then composes them into program-level invariants. We outline its key components, present preliminary results, and discuss future directions toward fully automated invariant discovery.

preprint2024arXiv

TypeEvalPy: A Micro-benchmarking Framework for Python Type Inference Tools

In light of the growing interest in type inference research for Python, both researchers and practitioners require a standardized process to assess the performance of various type inference techniques. This paper introduces TypeEvalPy, a comprehensive micro-benchmarking framework for evaluating type inference tools. TypeEvalPy contains 154 code snippets with 845 type annotations across 18 categories that target various Python features. The framework manages the execution of containerized tools, transforms inferred types into a standardized format, and produces meaningful metrics for assessment. Through our analysis, we compare the performance of six type inference tools, highlighting their strengths and limitations. Our findings provide a foundation for further research and optimization in the domain of Python type inference.

preprint2022arXiv

ArT: All-round Thinker for Unsupervised Commonsense Question-Answering

Without labeled question-answer pairs for necessary training, unsupervised commonsense question-answering (QA) appears to be extremely challenging due to its indispensable unique prerequisite on commonsense source like knowledge bases (KBs), which are usually highly resource consuming in construction. Recently pre-trained language models (PLMs) show effectiveness as an alternative for commonsense clues when they play a role of knowledge generator. However, existing work either relies on large-scale in-domain or out-of-domain labeled data, or fails to generate knowledge of high quality in a general way. Motivated by human thinking experience, we propose an approach of All-round Thinker (ArT) by fully taking association during knowledge generating. In detail, our model first focuses on key parts in the given context, and then generates highly related knowledge on such a basis in an association way like human thinking. Besides, for causal reasoning, a reverse thinking mechanism is especially added to further enhance bidirectional inferring between cause and effect. ArT is totally unsupervised and KBs-free. We evaluate it on three commonsense QA benchmarks: COPA, SocialIQA and SCT. On all scales of PLM backbones, ArT shows its brilliant performance and outperforms previous advanced unsupervised models. Our code is available at https://github.com/WangJW424/commonsenseQA-ArT.

preprint2022arXiv

CODE-MVP: Learning to Represent Source Code from Multiple Views with Contrastive Pre-Training

Recent years have witnessed increasing interest in code representation learning, which aims to represent the semantics of source code into distributed vectors. Currently, various works have been proposed to represent the complex semantics of source code from different views, including plain text, Abstract Syntax Tree (AST), and several kinds of code graphs (e.g., Control/Data Flow Graph). However, most of them only consider a single view of source code independently, ignoring the correspondences among different views. In this paper, we propose to integrate different views with the natural-language description of source code into a unified framework with Multi-View contrastive Pre-training, and name our model as CODE-MVP. Specifically, we first extract multiple code views using compiler tools, and learn the complementary information among them under a contrastive learning framework. Inspired by the type checking in compilation, we also design a fine-grained type inference objective in the pre-training. Experiments on three downstream tasks over five datasets demonstrate the superiority of CODE-MVP when compared with several state-of-the-art baselines. For example, we achieve 2.4/2.3/1.1 gain in terms of MRR/MAP/Accuracy metrics on natural language code retrieval, code similarity, and code defect detection tasks, respectively.

preprint2022arXiv

Conflict-free Cooperation Method for Connected and Automated Vehicles at Unsignalized Intersections: Graph-based Modeling and Optimality Analysis

Connected and automated vehicles have shown great potential in improving traffic mobility and reducing emissions, especially at unsignalized intersections. Previous research has shown that vehicle passing order is the key influencing factor in improving intersection traffic mobility. In this paper, we propose a graph-based cooperation method to formalize the conflict-free scheduling problem at an unsignalized intersection. Based on graphical analysis, a vehicle's trajectory conflict relationship is modeled as a conflict directed graph and a coexisting undirected graph. Then, two graph-based methods are proposed to find the vehicle passing order. The first is an improved depth-first spanning tree algorithm, which aims to find the local optimal passing order vehicle by vehicle. The other novel method is a minimum clique cover algorithm, which identifies the global optimal solution. Finally, a distributed control framework and communication topology are presented to realize the conflict-free cooperation of vehicles. Extensive numerical simulations are conducted for various numbers of vehicles and traffic volumes, and the simulation results prove the effectiveness of the proposed algorithms.

preprint2022arXiv

Cooperative Formation of Autonomous Vehicles in Mixed Traffic Flow: Beyond Platooning

Cooperative formation and control of autonomous vehicles (AVs) promise increased efficiency and safety on public roads. In mixed traffic flow consisting of AVs and human-driven vehicles (HDVs), the prevailing platooning of multiple AVs is not the only choice for cooperative formation. In this paper, we investigate how different formations of AVs impact traffic performance from a set-function optimization perspective. We first reveal a stability invariance property and a diminishing improvement property of noncooperative formation when AVs adopt typical Adaptive Cruise Control (ACC) strategies. Then, we focus on the case of cooperative formation where the AV controllers are cooperatively designed %redesign the control strategies of AVs in different formations and investigate the optimal formation of multiple AVs using set-function optimization. Two predominant optimal formations, i.e., uniform distribution and platoon formation, emerge from extensive numerical experiments. Interestingly, platooning might have the least potential to improve traffic performance when HDVs have poor string stability behavior. These results suggest more opportunities for cooperative formation of AVs, beyond platooning, in practical mixed traffic flow.

preprint2022arXiv

Data-Driven Predictive Control for Connected and Autonomous Vehicles in Mixed Traffic

Cooperative control of Connected and Autonomous Vehicles (CAVs) promises great benefits for mixed traffic. Most existing research focuses on model-based control strategies, assuming that car-following dynamics of human-driven vehicles are explicitly known. In this paper, instead of relying on a parametric car-following model, we introduce a data-driven predictive control strategy to achieve safe and optimal control for CAVs in mixed traffic. We first present a linearized dynamical model for mixed traffic systems, and investigate its controllability and observability. Based on these control-theoretic properties, we then propose a novel DeeP-LCC (Data-EnablEd Predictive Leading Cruise Control) strategy for CAVs based on measurable driving data to smooth mixed traffic. Our method is implemented in a receding horizon manner, in which input/output constraints are incorporated to achieve collision-free guarantees. Nonlinear traffic simulations reveal its saving of up to 24.96% fuel consumption during a braking scenario of Extra-Urban Driving Cycle while ensuring safety.

preprint2022arXiv

Scalpel: The Python Static Analysis Framework

Despite being the most popular programming language, Python has not yet received enough attention from the community. To the best of our knowledge, there is no general static analysis framework proposed to facilitate the implementation of dedicated Python static analyzers. To fill this gap, we design and implement such a framework (named Scalpel) and make it publicly available as an open-source project. The Scalpel framework has already integrated a number of fundamental static analysis functions (e.g., call graph constructions, control-flow graph constructions, alias analysis, etc.) that are ready to be reused by developers to implement client applications focusing on statically resolving dedicated Python problems such as detecting bugs or fixing vulnerabilities.

preprint2022arXiv

Silicon nitride stress-optic microresonator modulator for optical control applications

The silicon nitride integration platform has been successful at realizing extremely low waveguide losses across the visible to infrared and components including high performance lasers, filters, resonators, stabilization cavities, and optical frequency combs. Yet, progress towards implementing low loss, low power modulators in the silicon nitride platform, while maintaining the planar, wafer-scale process compatibility has been limited. Here we report a significant advance in integration of a piezo-electric (PZT) actuated micro-ring modulation in a fully-planar, wafer-scale silicon nitride platform, that maintains low optical loss (0.03 dB/cm in a 625 um resonator) at 1550 nm, with an order of magnitude increase in bandwidth (DC to 20 MHz 3-dB) and order of magnitude lower power consumption of 20 nW improvement over prior PZT modulators. The modulator provides a >14 dB ER and 7.1 million Q over the entire 4 GHz tuning range, a tuning efficiency of 200 MHz/V, and delivers the linearity required for control applications with 65.1 dBHz2/3 and 73.8 dBHz2/3 IMD3 SFDR at 1 MHz and 10 MHz respectively. We demonstrate two control applications, laser stabilization in a PDH lock loop, reducing laser frequency noise by 40 dB, and as a laser carrier tracking filter. This PZT modulator design can be extended to the visible in the ultra-low loss silicon nitride platform with minor waveguide design changes. This integration of PZT modulation in the ultra-low loss silicon nitride waveguide platform enables modulator control functions in a wide range of visible to IR applications such as atomic and molecular transition locking for cooling, controllable optical frequency combs, low-power external cavity tunable lasers, atomic clocks, and tunable ultra-low linewidth lasers and ultra-low phase noise microwave synthesizers.

preprint2022arXiv

TSRFormer: Table Structure Recognition with Transformers

We present a new table structure recognition (TSR) approach, called TSRFormer, to robustly recognizing the structures of complex tables with geometrical distortions from various table images. Unlike previous methods, we formulate table separation line prediction as a line regression problem instead of an image segmentation problem and propose a new two-stage DETR based separator prediction approach, dubbed \textbf{Sep}arator \textbf{RE}gression \textbf{TR}ansformer (SepRETR), to predict separation lines from table images directly. To make the two-stage DETR framework work efficiently and effectively for the separation line prediction task, we propose two improvements: 1) A prior-enhanced matching strategy to solve the slow convergence issue of DETR; 2) A new cross attention module to sample features from a high-resolution convolutional feature map directly so that high localization accuracy is achieved with low computational cost. After separation line prediction, a simple relation network based cell merging module is used to recover spanning cells. With these new techniques, our TSRFormer achieves state-of-the-art performance on several benchmark datasets, including SciTSR, PubTabNet and WTW. Furthermore, we have validated the robustness of our approach to tables with complex structures, borderless cells, large blank spaces, empty or spanning cells as well as distorted or even curved shapes on a more challenging real-world in-house dataset.

preprint2021arXiv

36 Hz integral linewidth laser based on a photonic integrated 4.0-meter coil resonator

Laser stabilization sits at the heart of many precision scientific experiments and applications, including quantum information science, metrology and atomic timekeeping. These systems narrow the laser linewidth and stabilize the carrier by use of Pound-Drever-Hall (PDH) locking to a table-scale, ultra-high quality factor (Q), vacuum spaced Fabry-Perot reference cavity. Integrating these cavities, to bring characteristics of PDH stabilization to the chip-scale, is critical to reduce their size, cost, and weight, and enable a wide range of portable and system-on-chip applications. We report a significant advance in integrated laser linewidth narrowing, stabilization and noise reduction, by use of a photonic integrated 4.0-meter-long coil resonator to stabilize a semiconductor laser. We achieve a 36 Hz 1/π-integral linewidth, an Allan deviation (ADEV) of 1.8x10^{-13} at 10 ms measurement time, and a 2.3 kHz/sec drift, to the best of our knowledge the lowest integral linewidth and highest stability demonstrated for an integrated reference cavity. Two coil designs, stabilizing lasers operating at 1550 nm and 1319 nm are demonstrated. The resonator is bus coupled to a 4.0-meter-long coil, with a 49 MHz free spectral range (FSR), a mode volume of 1.0x10^{10} μm^3 and a 142 million intrinsic Q, fabricated in a CMOS compatible, ultra-low loss silicon nitride waveguide platform. Our measurements and simulations show that the thermorefractive noise floor for this particular cavity is reached for frequencies down to 20 Hz in an ambient environment with simple passive vibration isolation and without vacuum or thermal isolation. The TRN limited performance is estimated to be an 8 Hz 1/π integral linewidth and ADEV of 5x10^{-14} at 10 ms, opening a stability regime that heretofore has only been available in fundamentally un-integrated systems.

preprint2021arXiv

Leading Cruise Control in Mixed Traffic Flow: System Modeling, Controllability, and String Stability

Connected and autonomous vehicles (CAVs) have great potential to improve road transportation systems. Most existing strategies for CAVs' longitudinal control focus on downstream traffic conditions, but neglect the impact of CAVs' behaviors on upstream traffic flow. In this paper, we introduce a notion of Leading Cruise Control (LCC), in which the CAV maintains car-following operations adapting to the states of its preceding vehicles, and also aims to lead the motion of its following vehicles. Specifically, by controlling the CAV, LCC aims to attenuate downstream traffic perturbations and smooth upstream traffic flow actively. We first present the dynamical modeling of LCC, with a focus on three fundamental scenarios: car-following, free-driving, and Connected Cruise Control. Then, the analysis of controllability, observability, and head-to-tail string stability reveals the feasibility and potential of LCC in improving mixed traffic flow performance. Extensive numerical studies validate that the capability of CAVs in dissipating traffic perturbations is further strengthened when incorporating the information of the vehicles behind into the CAV's control.

preprint2021arXiv

Restoring Execution Environments of Jupyter Notebooks

More than ninety percent of published Jupyter notebooks do not state dependencies on external packages. This makes them non-executable and thus hinders reproducibility of scientific results. We present SnifferDog, an approach that 1) collects the APIs of Python packages and versions, creating a database of APIs; 2) analyzes notebooks to determine candidates for required packages and versions; and 3) checks which packages are required to make the notebook executable (and ideally, reproduce its stored results). In its evaluation, we show that SnifferDog precisely restores execution environments for the largest majority of notebooks, making them immediately executable for end users.

preprint2021arXiv

Robust Dynamic Bus Control: A Distributional Multi-agent Reinforcement Learning Approach

Bus system is a critical component of sustainable urban transportation. However, the operation of a bus fleet is unstable in nature, and bus bunching has become a common phenomenon that undermines the efficiency and reliability of bus systems. Recently research has demonstrated the promising application of multi-agent reinforcement learning (MARL) to achieve efficient vehicle holding control to avoid bus bunching. However, existing studies essentially overlook the robustness issue resulting from various events, perturbations and anomalies in a transit system, which is of utmost importance when transferring the models for real-world deployment/application. In this study, we integrate implicit quantile network and meta-learning to develop a distributional MARL framework -- IQNC-M -- to learn continuous control. The proposed IQNC-M framework achieves efficient and reliable control decisions through better handling various uncertainties/events in real-time transit operations. Specifically, we introduce an interpretable meta-learning module to incorporate global information into the distributional MARL framework, which is an effective solution to circumvent the credit assignment issue in the transit system. In addition, we design a specific learning procedure to train each agent within the framework to pursue a robust control policy. We develop simulation environments based on real-world bus services and passenger demand data and evaluate the proposed framework against both traditional holding control models and state-of-the-art MARL models. Our results show that the proposed IQNC-M framework can effectively handle the various extreme events, such as traffic state perturbations, service interruptions, and demand surges, thus improving both efficiency and reliability of the system.

preprint2020arXiv

Controllability Analysis and Optimal Control of Mixed Traffic Flow with Human-driven and Autonomous Vehicles

Connected and automated vehicles (CAVs) have a great potential to improve traffic efficiency in mixed traffic systems, which has been demonstrated by multiple numerical simulations and field experiments. However, some fundamental properties of mixed traffic flow, including controllability and stabilizability, have not been well understood. This paper analyzes the controllability of mixed traffic systems and designs a system-level optimal control strategy. Using the Popov-Belevitch-Hautus (PBH) criterion, we prove for the first time that a ring-road mixed traffic system with one CAV and multiple heterogeneous human-driven vehicles is not completely controllable, but is stabilizable under a very mild condition. Then, we formulate the design of a system-level control strategy for the CAV as a structured optimal control problem, where the CAV's communication ability is explicitly considered. Finally, we derive an upper bound for reachable traffic velocity via controlling the CAV. Extensive numerical experiments verify the effectiveness of our analytical results and the proposed control strategy. Our results validate the possibility of utilizing CAVs as mobile actuators to smooth traffic flow actively.

preprint2020arXiv

Domain Confusion with Self Ensembling for Unsupervised Adaptation

Data collection and annotation are time-consuming in machine learning, expecially for large scale problem. A common approach for this problem is to transfer knowledge from a related labeled domain to a target one. There are two popular ways to achieve this goal: adversarial learning and self training. In this article, we first analyze the training unstablity problem and the mistaken confusion issue in adversarial learning process. Then, inspired by domain confusion and self-ensembling methods, we propose a combined model to learn feature and class jointly invariant representation, namely Domain Confusion with Self Ensembling (DCSE). The experiments verified that our proposed approach can offer better performance than empirical art in a variety of unsupervised domain adaptation benchmarks.

preprint2020arXiv

NeuroDiff: Scalable Differential Verification of Neural Networks using Fine-Grained Approximation

As neural networks make their way into safety-critical systems, where misbehavior can lead to catastrophes, there is a growing interest in certifying the equivalence of two structurally similar neural networks. For example, compression techniques are often used in practice for deploying trained neural networks on computationally- and energy-constrained devices, which raises the question of how faithfully the compressed network mimics the original network. Unfortunately, existing methods either focus on verifying a single network or rely on loose approximations to prove the equivalence of two networks. Due to overly conservative approximation, differential verification lacks scalability in terms of both accuracy and computational cost. To overcome these problems, we propose NeuroDiff, a symbolic and fine-grained approximation technique that drastically increases the accuracy of differential verification while achieving many orders-of-magnitude speedup. NeuroDiff has two key contributions. The first one is new convex approximations that more accurately bound the difference neurons of two networks under all possible inputs. The second one is judicious use of symbolic variables to represent neurons whose difference bounds have accumulated significant error. We also find that these two techniques are complementary, i.e., when combined, the benefit is greater than the sum of their individual benefits. We have evaluated NeuroDiff on a variety of differential verification tasks. Our results show that NeuroDiff is up to 1000X faster and 5X more accurate than the state-of-the-art tool.

preprint2020arXiv

Smoothing Traffic Flow via Control of Autonomous Vehicles

The emergence of autonomous vehicles is expected to revolutionize road transportation in the near future. Although large-scale numerical simulations and small-scale experiments have shown promising results, a comprehensive theoretical understanding to smooth traffic flow via autonomous vehicles is lacking. In this paper, from a control-theoretic perspective, we establish analytical results on the controllability, stabilizability, and reachability of a mixed traffic system consisting of human-driven vehicles and autonomous vehicles in a ring road. We show that the mixed traffic system is not completely controllable, but is stabilizable, indicating that autonomous vehicles can not only suppress unstable traffic waves but also guide the traffic flow to a higher speed. Accordingly, we establish the maximum traffic speed achievable via controlling autonomous vehicles. Numerical results show that the traffic speed can be increased by over 6% when there are only 5% autonomous vehicles. We also design an optimal control strategy for autonomous vehicles to actively dampen undesirable perturbations. These theoretical findings validate the high potential of autonomous vehicles to smooth traffic flow.