pwc-archive/papers-with-abstracts huggingface dataset:
dafny-annotator: AI-Assisted Verification of Dafny Programs
Authors: Gabriel Poesia, Chloe Loughridge, Nada Amin
Date: 2024-11-05 00:00:00
Tasks: Friction

Formal verification has the potential to drastically reduce software bugs, but its high additional cost has hindered large-scale adoption. While Dafny presents a promise to significantly reduce the effort to write verified programs, users are often required to provide logical annotations to aid the verifier. Here, we explore using a combination of Large Language Models and search to build dafny-annotator: a tool that adds logical annotations to a Dafny method until the verifier can prove it correct. On a test set from the DafnyBench collection of programs, greedy search guided by LLaMa 3.1 8B successfully annotates only 15.7% of the methods. Since this data-driven approach is hindered by the lack of large-scale training data, we propose a method for open-ended synthesis of new Dafny programs in a flexible pipeline where LLMs formulate high-level ideas, implement them, and incrementally propose changes to existing programs, which Dafny validates. This gives us a synthetic dataset, DafnySynth, which we use to augment DafnyBench for training. Fine-tuning on both datasets boosts LLaMa 8B's success rate to 50.6% -- significantly better than the base model, or training on either dataset alone. Our results suggest a path towards capable AI assistants for languages that don't yet have large-scale human-generated examples. In turn, such assistants might reduce friction for users and ultimately drive adoption.
Safety-Critical Controller Synthesis with Reduced-Order Models
Authors: Max H. Cohen, Noel Csomay-Shanklin, William D. Compton, Tamas G. Molnar, Aaron D. Ames
Date: 2024-11-25 00:00:00

Reduced-order models (ROMs) provide lower dimensional representations of complex systems, capturing their salient features while simplifying control design. Building on previous work, this paper presents an overarching framework for the integration of ROMs and control barrier functions, enabling the use of simplified models to construct safety-critical controllers while providing safety guarantees for complex full-order models. To achieve this, we formalize the connection between full and ROMs by defining projection mappings that relate the states and inputs of these models and leverage simulation functions to establish conditions under which safety guarantees may be transferred from a ROM to its corresponding full-order model. The efficacy of our framework is illustrated through simulation results on a drone and hardware demonstrations on ARCHER, a 3D hopping robot.
Rethinking the Intermediate Features in Adversarial Attacks: Misleading Robotic Models via Adversarial Distillation
Authors: Ke Zhao, Huayang Huang, Miao Li, Yu Wu
Date: 2024-11-21 00:00:00
Tasks: Robot Manipulation

Language-conditioned robotic learning has significantly enhanced robot adaptability by enabling a single model to execute diverse tasks in response to verbal commands. Despite these advancements, security vulnerabilities within this domain remain largely unexplored. This paper addresses this gap by proposing a novel adversarial prompt attack tailored to language-conditioned robotic models. Our approach involves crafting a universal adversarial prefix that induces the model to perform unintended actions when added to any original prompt. We demonstrate that existing adversarial techniques exhibit limited effectiveness when directly transferred to the robotic domain due to the inherent robustness of discretized robotic action spaces. To overcome this challenge, we propose to optimize adversarial prefixes based on continuous action representations, circumventing the discretization process. Additionally, we identify the beneficial impact of intermediate features on adversarial attacks and leverage the negative gradient of intermediate self-attention features to further enhance attack efficacy. Extensive experiments on VIMA models across 13 robot manipulation tasks validate the superiority of our method over existing approaches and demonstrate its transferability across different model variants.
Attention-guided Spectrogram Sequence Modeling with CNNs for Music Genre Classification
Authors: Aditya Sridhar
Date: 2024-11-18 00:00:00
Tasks: Classification, Genre classification, Music Genre Classification, Music Recommendation, Recommendation Systems

Music genre classification is a critical component of music recommendation systems, generation algorithms, and cultural analytics. In this work, we present an innovative model for classifying music genres using attention-based temporal signature modeling. By processing spectrogram sequences through Convolutional Neural Networks (CNNs) and multi-head attention layers, our approach captures the most temporally significant moments within each piece, crafting a unique "signature" for genre identification. This temporal focus not only enhances classification accuracy but also reveals insights into genre-specific characteristics that can be intuitively mapped to listener perceptions. Our findings offer potential applications in personalized music recommendation systems by highlighting cross-genre similarities and distinctiveness, aligning closely with human musical intuition. This work bridges the gap between technical classification tasks and the nuanced, human experience of genre.
Direct Speech-to-Speech Neural Machine Translation: A Survey
Authors: Mahendra Gupta, Maitreyee Dutta, Chandresh Kumar Maurya
Date: 2024-11-13 00:00:00
Tasks: Machine Translation, Speech-to-Speech Translation, Survey, Text Generation, Translation

Speech-to-Speech Translation (S2ST) models transform speech from one language to another target language with the same linguistic information. S2ST is important for bridging the communication gap among communities and has diverse applications. In recent years, researchers have introduced direct S2ST models, which have the potential to translate speech without relying on intermediate text generation, have better decoding latency, and the ability to preserve paralinguistic and non-linguistic features. However, direct S2ST has yet to achieve quality performance for seamless communication and still lags behind the cascade models in terms of performance, especially in real-world translation. To the best of our knowledge, no comprehensive survey is available on the direct S2ST system, which beginners and advanced researchers can look upon for a quick survey. The present work provides a comprehensive review of direct S2ST models, data and application issues, and performance metrics. We critically analyze the models' performance over the benchmark datasets and provide research challenges and future directions.
Optimal MPPT Control of a Photovoltaic System Under Non-uniform Irradiation
Authors: Yehia Lalili, Meriem Halimi, Toufik Bouden
Date: 2024-11-25 00:00:00
Tasks: Evolutionary Algorithms

Under Partial shading conditions (PSC), traditional MPPT methods such as, P&O, IncCon and SMC, cannot track down the Global MPP. Thus, the energy conversion of the PV modules will decrease. To overcome this drawback, two evolutionary algorithms; PSO and CS, were presented. Also, the study introduces a hybrid optimization method to enhance the overall performance of the PV system under PSC. MATLAB simulations will be used in order to illustrate the efficiency of the proposed method.
Extensions of the Path-integral formula for computation of Koopman eigenfunctions
Authors: Shankar A. Deka, Umesh Vaidya
Date: 2024-11-25 00:00:00

Representing nonlinear dynamical systems using the Koopman Operator and its spectrum has distinct advantages in terms of linear interpretability of the model as well as in analysis and control synthesis through the use of well-studied techniques from linear systems theory. As such, efficient computation of Koopman eigenfunctions is of paramount importance towards enabling such Koopman-based constructions. To this end, several approaches have been proposed in literature, including data-driven, convex optimization, and Deep Learning-based methods. In our recent work, we proposed a novel approach based on path-integrals that allowed eigenfunction computations using a closed-form formula. In this paper, we present several important developments such as finite-time computations, relaxation of assumptions on the distribution of the principal Koopman eigenvalues, as well as extension towards saddle point systems, which greatly enhance the practical applicability of our method.
Dampening parameter distributional shifts under robust control and gain scheduling
Authors: Mohammad Ramadan, Mihai Anitescu
Date: 2024-11-25 00:00:00
Tasks: Scheduling

Many traditional robust control approaches assume linearity of the system and independence between the system state-input and the parameters of its approximant low-order model. This assumption implies that robust control design introduces no distributional shifts in the parameters of this low-order model. This is generally not true when the underlying actual system is nonlinear, which admits typically state-input coupling with the parameters of the approximating model. Therefore, a robust controller has to be robust under the parameter distribution that will be experienced in the future data, after applying this control, not the parameter distribution seen in the learning data or assumed in the design. In this paper we seek a solution to this problem by restricting the newly designed closed-loop system to be consistent with the learning data and slowing down any distributional shifts in the state-input and parameter spaces. In computational terms, these objectives are formulated as convex semi-definite programs that standard software packages can efficiently solve. We evaluate the proposed approaches on a simple yet telling gain-scheduling problem, which can be equivalently posed as a robust control problem.
USRP-Based Single Anchor Positioning: AoA with 5G Uplink Signals, and UWB Ranging
Authors: Thodoris Spanos, Fran Fabra, José A. López-Salcedo, Gonzalo Seco-Granados, Nikos Kanistras, Ivan Lapin, Vassilis Paliouras
Date: 2024-11-25 00:00:00

This paper presents a novel testbed designed for 5th-Generation (5G) positioning using Universal Software Radio Peripherals (USRPs). The testbed integrates multiple units: an Operation Unit for test management, a User Unit equipped with an Ettus E312 USRP, and a Station Unit featuring an Ettus N310 USRP equipped with a three-element Uniform Linear Array for Angle of Arrival estimation. Alongside ultra wideband ranging, the testbed estimates the user's position relative to the base station. Signal processing algorithms are executed in a dedicated processing unit. Key challenges addressed include phase misalignment between RX channel pairs due to different Local Oscillators in the Ettus N310, necessitating real-time calibration for precise signal alignment. High sampling rates (up to 61.44 MSps) result in large IQ sample files, managed efficiently using a snapshot technique to optimize storage without compromising testbed positioning capabilities. The testbed synchronizes angular measurements with ranging estimates allowing consistent performance evaluation for real-life cases of dynamic users (e.g. pedestrian). Experimental results demonstrate the testbed's effectiveness in achieving accurate pedestrian user localization.
Goal-oriented Semantic Communications for Metaverse Construction via Generative AI and Optimal Transport
Authors: Zhe Wang, Nan Li, Yansha Deng, A. Hamid Aghvami
Date: 2024-11-25 00:00:00
Tasks: Decoder, Semantic Communication

The emergence of the metaverse has boosted productivity and creativity, driving real-time updates and personalized content, which will substantially increase data traffic. However, current bit-oriented communication networks struggle to manage this high volume of dynamic information, restricting metaverse applications interactivity. To address this research gap, we propose a goal-oriented semantic communication (GSC) framework for metaverse. Building on an existing metaverse wireless construction task, our proposed GSC framework includes an hourglass network-based (HgNet) encoder to extract semantic information of objects in the metaverse; and a semantic decoder that uses this extracted information to reconstruct the metaverse content after wireless transmission, enabling efficient communication and real-time object behaviour updates to the scenery for metaverse construction task. To overcome the wireless channel noise at the receiver, we design an optimal transport (OT)-enabled semantic denoiser, which enhances the accuracy of metaverse scenery through wireless communication. Experimental results show that compared to the conventional metaverse construction, our proposed GSC framework significantly reduces wireless metaverse construction latency by 92.6\%, while improving metaverse object status accuracy and viewing experience by 45.6\% and 44.7\%, respectively.
Comparative Analysis of Machine Learning Models for Short-Term Distribution System Load Forecasting
Authors: Elias Raffoul, Mingjian Tuo, Cunzhi Zhao, Tianxia Zhao, Meng Ling, Xingpeng Li
Date: 2024-11-25 00:00:00
Tasks: Load Forecasting

Accurate electrical load forecasting is crucial for optimizing power system operations, planning, and management. As power systems become increasingly complex, traditional forecasting methods may fail to capture the intricate patterns and dependencies within load data. Machine learning (ML) techniques have emerged as powerful alternatives, offering superior prediction accuracy and the ability to model non-linear and complex temporal relationships. This study presents a comprehensive comparison of prominent ML models: feedforward neural networks, recurrent neural networks, long short-term memory networks, gated recurrent units, and the attention temporal graph convolutional network; for short-term load forecasting of the Energy Corridor distribution system in Houston, Texas. Using a 24-hour look-back window, we train the models on datasets spanning one and five years, to predict the load demand for the next hour and assess performance. Our findings aim to identify the most effective ML approach for accurate load forecasting, contributing to improved grid reliability and system optimization.
A Differentially Private Quantum Neural Network for Probabilistic Optimal Power Flow
Authors: Yuji Cao, Yue Chen, Yan Xu
Date: 2024-11-25 00:00:00
Tasks: Privacy Preserving

The stochastic nature of renewable energy and load demand requires efficient and accurate solutions for probabilistic optimal power flow (OPF). Quantum neural networks (QNNs), which combine quantum computing and machine learning, offer computational advantages in approximating OPF by effectively handling high-dimensional data. However, adversaries with access to non-private OPF solutions can potentially infer sensitive load demand patterns, raising significant privacy concerns. To address this issue, we propose a privacy-preserving QNN model for probabilistic OPF approximation. By incorporating Gaussian noise into the training process, the learning algorithm achieves ($\varepsilon, \delta$)-differential privacy with theoretical guarantees. Moreover, we develop a strongly entangled quantum state to enhance the nonlinearity expressiveness of the QNN. Experimental results demonstrate that the proposed method successfully prevents privacy leakage without compromising the statistical properties of probabilistic OPF. Moreover, compared to classical private neural networks, the QNN reduces the number of parameters by 90% while achieving significantly higher accuracy and greater stability.
Stealth Attacks Against Moving Target Defense for Smart Grid
Authors: Ke Sun, Iñaki Esnaola, H. Vincent Poor
Date: 2024-11-25 00:00:00

Data injection attacks (DIAs) pose a significant cybersecurity threat to the Smart Grid by enabling an attacker to compromise the integrity of data acquisition and manipulate estimated states without triggering bad data detection procedures. To mitigate this vulnerability, the moving target defense (MTD) alters branch admittances to mismatch the system information that is available to an attacker, thereby inducing an imperfect DIA construction that results in degradation of attack performance. In this paper, we first analyze the existence of stealth attacks for the case in which the MTD strategy only changes the admittance of a single branch. Equipped with this initial insight, we then extend the results to the case in which multiple branches are protected by the MTD strategy. Remarkably, we show that stealth attacks can be constructed with information only about which branches are protected, without knowledge about the particular admittance value changes. Furthermore, we provide a sufficient protection condition for the MTD strategy via graph-theoretic tools that guarantee that the system is not vulnerable to DIAs. Numerical simulations are implemented on IEEE test systems to validate the obtained results.
Nonlinear Model Predictive Control of a Hybrid Thermal Management System
Authors: Demetrius Gulewicz, Uduak Inyang-Udoh, Trevor Bird, Neera Jain
Date: 2024-11-24 00:00:00
Tasks: Management, Model Predictive Control

Model predictive control has gained popularity for its ability to satisfy constraints and guarantee robustness for certain classes of systems. However, for systems whose dynamics are characterized by a high state dimension, substantial nonlinearities, and stiffness, suitable methods for online nonlinear MPC are lacking. One example of such a system is a vehicle thermal management system (TMS) with integrated thermal energy storage (TES), also referred to as a hybrid TMS. Here, hybrid refers to the ability to achieve cooling through a conventional heat exchanger or via melting of a phase change material, or both. Given increased electrification in vehicle platforms, more stringent performance specifications are being placed on TMS, in turn requiring more advanced control methods. In this paper, we present the design and real-time implementation of a nonlinear model predictive controller with 77 states on an experimental hybrid TMS testbed. We show how, in spite of high-dimension and stiff dynamics, an explicit integration method can be obtained by linearizing the dynamics at each time step within the MPC horizon. This integration method further allows the first-order gradients to be calculated with minimal additional computational cost. Through simulated and experimental results, we demonstrate the utility of the proposed solution method and the benefits of TES for mitigating highly transient heat loads achieved by actively controlling its charging and discharging behavior.
Finding Thermodynamically Favorable Pathways in Chemical Reaction Networks Using Flows in Hypergraphs and Mixed-Integer Linear Programming
Authors: Adittya Pal, Rolf Fagerberg, Jakob Lykke Andersen, Christoph Flamm, Peter Dittrich, Daniel Merkle
Date: 2024-11-24 00:00:00

The search for pathways that optimize the formation of a particular target molecule in a reaction network is a key problem in many settings, including reactor systems. Chemical reaction networks are mathematically well represented as hypergraphs, modeling that facilitates the search for pathways by computational means. We propose to enrich an existing search method for pathways by including thermodynamic principles. In more detail, we give a mixed-integer linear programming (mixed ILP) formulation of the search problem into which we integrate chemical potentials and concentrations for individual molecules, enabling us to constrain the search to return pathways containing only thermodynamically favorable reactions. Moreover, if multiple possible pathways are found, we can rank these by objective functions based on thermodynamics. As an example of use, we apply the framework to a reaction network representing the HCN-formamide chemistry. Alternative pathways to the one currently hypothesized in the literature are queried and enumerated, including some that score better according to our chosen objective function.
A Human-optimized Model Predictive Control Scheme and Extremum Seeking Parameter Estimator for Slip Control of Electric Race Cars
Authors: Wytze de Vries, Jorn van Kampen, Mauro Salazar
Date: 2024-11-24 00:00:00
Tasks: Model Predictive Control

This paper presents a longitudinal slip control system for a rear-wheel-driven electric endurance race car. The control system integrates Model Predictive Control (MPC) with Extremum Seeking Control (ESC) to optimize the traction and regenerative braking performance of the powertrain. The MPC contains an analytical solution which results in a negligible computation time, whilst providing an optimal solution to a multi-objective optimization problem. The ESC algorithm allows continuous estimation of the optimal slip reference without assuming any prior knowledge of the tire dynamics. Finally, the control parameters are determined using a human-driven preference-based optimization algorithm in order to obtain the desired response. Simulation results and comparisons with other methods demonstrate the system's capability to automatically determine and track the optimal slip values, showing stability and performance under varying conditions.
Analysis of Hierarchical AoII over unreliable channel: A Stochastic Hybrid System Approach
Authors: Han Xu, Jiaqi Li, Jixiang Zhang, Tiecheng Song, Yinfei Xu
Date: 2024-11-24 00:00:00

In this work, we generalize the Stochastic Hybrid Systems (SHSs) analysis of traditional AoI to the AoII metric. Hierarchical ageing processes are adopted using the continuous AoII for the first time, where two different hierarchy schemes, i.e., a hybrid of linear ageing processes with different slopes and a hybrid of linear and quadratic ageing processes, are considered. We first modify the main result in \cite[Theorem 1]{yates_age_2020b} to provide a systematic way to analyze the continuous hierarchical AoII over unslotted real-time systems. The closed-form expressions of average hierarchical AoII are obtained based on our Theorem \ref{theorem1} in two typical scenarios with different channel conditions, i.e., an M/M/1/1 queue over noisy channel and two M/M/1/1 queues over collision channel. Moreover, we analyze the stability conditions for two scenarios given that the quadratic ageing process may lead to the absence of stationary solutions. Finally, we compare the average age performance between the classic AoI results and our AoII results in the M/M/1/1 queue, and the effects of different channel parameters on AoII are also evaluated.
Distributionally Robust Safety Verification for Markov Decision Processes
Authors: Abhijit Mazumdar, Yuting Hou, Rafal Wisniewski
Date: 2024-11-23 00:00:00

In this paper, we propose a distributionally robust safety verification method for Markov decision processes where only an ambiguous transition kernel is available instead of the precise transition kernel. We define the ambiguity set around the nominal distribution by considering a Wasserstein distance. To this end, we introduce a robust safety function to characterize probabilistic safety in the face of uncertain transition probability. First, we obtain an upper bound on the robust safety function in terms of a distributionally robust Q-function. Then, we present a convex program-based distributionally robust Q-iteration algorithm to compute the robust Q-function. By considering a numerical example, we demonstrate our theoretical results.