1,721,007 research outputs found
Cloud-based quadratic optimization with partially homomorphic encryption
No full textThis article develops a cloud-based protocol for a constrained quadratic optimization problem involving multiple parties, each holding private data. The protocol is based on the projected gradient ascent on the Lagrange dual problem and exploits partially homomorphic encryption and secure communication techniques. Using formal cryptographic definitions of indistinguishability, the protocol is shown to achieve computational privacy. We show the implementation results of the protocol and discuss its computational and communication complexity. We conclude this article with a discussion on privacy notions
Recommended from our members
Formal Verification of AI-Controlled Cyber-Physical Systems Using Polynomial Approximations: Constraints Solver, Model Checkers, and Applications
Get PDFThe last decade's advancement in machine learning (ML) for controlling cyber-physical systems has heralded a new era in autonomous technology, driving innovations from self-driving cars to smart infrastructure. However, these systems often grapple with challenges related to safety, reliability, and the ability to generalize across different scenarios. This dissertation aims to bridge the gap between the scalability and flexibility of ML-based control systems and the rigorous safety and reliability guarantees provided by formal methods and control theory. It introduces novel methodologies that leverage machine learning to enhance the design, verification, and optimization of AI-controlled cyber-physical systems, ensuring they meet high-level specifications while managing such systems' inherent complexity and non-linearity. The contributions of this thesis are multi-fold. 1) We proposed a highly efficient and parallelizable solver called PolyAR, which aims to solve general multivariate polynomial inequality constraints. PolyAR uses convex polynomials as an abstraction for highly nonlinear polynomials. Such abstractions were previously shown to be powerful to prune the search space and restrict the usage of sound and complete solvers to small search space. We compared the scalability of PolyAR against state-of-the-art solvers such as Z3 8.9 and Yices 2.6 on complex design and verification problems. The experiment results show that the PolyAR solver drastically outperformed Z3 8.9 and Yices 2.6 regarding execution time. 2) We developed PolyARBerNN, an enhancement to PolyAR that employs neural networks (NN) to guide the abstraction refinement procedure that helps to select the right abstraction out of a set of pre-defined abstractions and a Bernstein polynomial-based search space pruning mechanism. These enhancements together made PolyARBerNN capable of solving complex instances and scaling more favorably compared to the state-of-the-art nonlinear real arithmetic solvers while maintaining the soundness and completeness of the resulting solver. In addition, we proposed an efficient optimizer called PolyAROpt that transforms polynomial objective functions into polynomial constraints (on the gradient of the objective function) whose solutions are guaranteed to be close to the global optima. PolyAROpt optimizer uses PolyARBerNN to solve constrained polynomial optimization problems. Numerical results show that PolyAROpt can solve high-dimensional and high-order polynomial optimization problems faster than the built-in optimizer in the Z3 8.9 solver. 3) We proposed an efficient algorithm called BERN-NN that employs polynomial interval arithmetic, where tight over/under approximations of the NN's activation functions are computed using Bernstein polynomials. These polynomials have several interesting mathematical proprieties. One particular property is called the sharpness propriety, which allows us to obtain extremely tight bounds that are tighter than those currently exist in the literature (e.g., interval arithmetic, crowns, linear programming, and many centered forms). Moreover, we exploited the mathematical proprieties of Bernstein polynomials to convert the proposed polynomial interval arithmetic operations into add-and-multiply operations, which are easily implemented using GPUs. Thanks to those GPUs, our tool's execution time is drastically reduced. Experimental results show that our method approximates NN's outputs tighter than state-of-the-art NN verification tools by several orders of magnitude. 4) We proposed BERN-NN-IBF, a significant enhancement of the Bernstein-polynomial-based bound propagation algorithms. BERN-NN-IBF offers three main contributions: (i) a memory-efficient encoding of Bernstein-polynomials to scale the bound propagation algorithms, (ii) optimized tensor operations for the new polynomial encoding to maintain the integrity of the bounds while enhancing computational efficiency, and (iii) tighter under-approximations of the ReLU activation function using quadratic polynomials tailored to minimize approximation errors. Through comprehensive testing, we demonstrate that BERN-NN-IBF achieves tighter bounds and higher computational efficiency than the original BERN-NN and state-of-the-art methods, including linear programming and convex used within the winner of the VNN-COMPETITION
Safe Learning and Verification of Neural Network Controllers for Autonomous Systems
Get PDFThe last decade has witnessed tremendous success in using machine learning (ML) to control physical systems, such as autonomous vehicles, drones, and smart cities. On the one hand, learning-based controller synthesis enjoys the scalability and flexibility benefits offered by purely data-driven architectures. Nevertheless, these end-to-end learning approaches suffer from the lack of safety, reliability, and generalization guarantees. On the other hand, control-theoretic and formal-methods techniques enjoy the guarantees of satisfying high-level specifications. Nevertheless, these algorithms need an explicit model of the dynamic systems and suffer from computational complexity whenever the dynamical models are highly nonlinear and complex. The objective of this dissertation is to develop learning algorithms and verification tools that bridge ideas from symbolic control/reasoning techniques to design ML-controlled autonomous systems with certifiable trust and assurance.
The contributions of this dissertation are multi-fold. (1) We propose a neurosymbolic framework that integrates machine learning and symbolic techniques in training neural network (NN) controllers for robotic systems to satisfy temporal logic specifications. In particular, the trained NN controllers enjoy strong correctness guarantees when applying to unseen tasks, i.e., the exact task (including the environment, specifications, and dynamic constraints of a robot) is unknown during the training of NNs. (2) We introduce the first framework to formally reason about the safety of autonomous systems equipped with a neural network controller that processes LiDAR images to produce control actions. Given a NN-controlled autonomous system that processes the environment with a LiDAR sensor, our framework computes a set of safe initial states such that the autonomous system is guaranteed to be safe when starting from these initial states. (3) We propose a novel approach called NNSynth that uses machine learning techniques to guide the design of abstraction-based controllers. Thanks to the use of ML, NNSynth achieves significant performance improvement compared to traditional controller synthesis while maintaining probabilistic guarantees in the meantime. (4) We consider the problem of automatically designing neural network architectures and exhibit a systematic methodology for choosing NN architectures that are guaranteed to implement a controller that satisfies the given high-level specification. (5) Finally, we present an efficient multi-robot motion planning algorithm for missions captured by temporal logic specifications in the presence of bounded disturbances and denial-of-service (DoS) attacks
Recommended from our members
Formal Verication of Neural Networks
Get PDFNeural networks(NNs) have been widely used over the past decade at the core of intelligentsystems from sensing modules to learning-based controllers. They've also been deployed in
dierent safety-critical domains including healthcare and transportation. However, recent
work has shown that NNs are fragile and can make dangerous mistakes that are either
unintentional or adversarial. As a consequence, formal verication of NNs holds the promise
of providing safety guarantees on the behaviour of such systems. We focus our work on
ReLU networks as it is the most widely used activation function. Exact formal verication
of ReLU NNs was proved to be NP-hard due to the combinatorial nature of the problem,
therefore all of the current verication methods use some relaxation of the problem. We
propose a novel framework for formal verication of ReLU neural networks that can ensure
that they satisfy some polytopic specications on the input and the output of the network.
Our approach uses a relaxed convex program to mitigate the combinatorial complexity of
the problem together with some optimization heuristics to eciently verify the satisfaction
of the specication on a given network. We have implemented our algorithm in a toolkit,
PeregriNN. To test PeregriNN, we run it on two test benches in dierent domains. First,
we achieve SOTA results on verifying the adversarial robustness of dierent networks on the
MNIST dataset. Second, we verify the safety of a neural network controlled autonomous
robot in a structured environment
Recommended from our members
Formal Verification of Vision-Based AI-Controlled Cyber-Physical Vehicles
Get PDFThe autonomous landing of small airplanes remains a significant challenge in aviation safety,with the Federal Aviation Administration (FAA) reporting an average of three crashes per
day in the United States. While autonomous landing systems for large commercial airplanes
exist, accessible technology for small airplanes is lacking, necessitating alternative solutions.
Vision-based perception using cameras, coupled with artificial neural networks (NN), of-
fers a promising approach by leveraging structural information to infer the vehicle’s pose
and surrounding environment, enabling safe and reliable landings. This research addresses
key challenges in ensuring the safety and reliability of vision-based closed-loop systems for
autonomous landings.A central issue is the absence of robust mathematical models that accurately capture therelationship between system states, camera images, and the NN controller. Existing NN
model checkers also fall short in verifying complex closed-loop systems. This Ph.D. thesis
proposes NNLander-VeriF, a specialized framework for model-checking vision-based NN con-
trollers in autonomous landing scenarios. The framework re-models the camera’s physical
model as a perception network, augmenting it with the NN controller to simplify closed-loop
dynamics. This approach enables encoding closed-loop verification as robustness queries,
leveraging state-of-the-art NN model checkers.The research also focuses on designing certified vision-based state estimators using a gen-erative NN model to enhance scene feature representation and aircraft state estimation.
This model’s mixed-monotonicity property aids in performing reachability analysis, provid-
ing guarantees on estimation accuracy and certifiable error bounds. Experimental results
using real-world images from event-based cameras demonstrate significant improvements in
state estimation accuracy and reliability.Lastly, the research introduces a repair algorithm for NN controllers to address unsafe closed-loop behavior in certain states. By formulating the repair problem as convex optimization
problems, the algorithm effectively repairs unsafe behavior while preserving safety for other
states. The proposed framework enhances trust in autonomous landing systems through
closed-loop verification, certified state estimation, and safe-by-repair techniques. This work
aims to reduce crash rates in small airplanes, paving the way for safer autonomous landings
and broader operational opportunities in aviation
Recommended from our members
Model Extraction Attack Against Reinforcement Learning Based Controllers
Get PDFWe introduce the problem of model-extraction attacks in cyber-physical systems in which an attacker attempts to estimate (or extract) the feedback controller of the system. Extracting (or estimating) the controller provides an unmatched edge to attackers since it allows them to predict the future control actions of the system and plan their attack accordingly. Hence, it is important to understand the ability of the attackers to perform such an attack. In this paper, we focus on the setting when a Deep Neural Network (DNN) controller is trained using Reinforcement Learning (RL) algorithms and is used to control a stochastic system. We play the role of the attacker that aims to estimate such an unknown DNN controller, and we propose a two-phase algorithm. In the first phase, also called the offline phase, the attacker uses side-channel information about the RL-reward function and the system dynamics to identify a set of candidate estimates of the unknown DNN. In the second phase, also called the online phase, the attacker observes the behavior of the unknown DNN and uses these observations to shortlist the set of final policy estimates. We provide theoretical analysis of the error between the unknown DNN and the estimated one. We also provide numerical results showing the effectiveness of the proposed algorithm
Recommended from our members
Formal Verification of Neural Networks: Algorithms and Applications
Get PDFNeural networks (NNs) have become the backbone of intelligent systems, with applications ranging from sensing modules to learning-based controllers. Their deployment in safety-critical domains such as healthcare and transportation underscores their significance. However, the fragility of NNs and their potential for dangerous mistakes, whether unintentional or adversarial, necessitates rigorous checks on their behavior. This thesis delves into the Formal Verification of NNs, a process that can provides formal guarantees on their behavior and ensures the reliability and robustness of these systems.The cornerstone of this work is a novel algorithm, PeregriNN, that has advanced the Formal Verification of NNs. This algorithm has been used to verify various NN properties such as Adversarial Robustness, safety of autonomous systems, and in demonstrating the fairness of NNs by innovatively formulating the fairness property into a Formal Verification problem. Further, this thesis explores a new type of activation function that simplifies the formal verification process, albeit at the cost of increased training time. This exploration, coupled with a collaborative effort that led to the proposal of a polynomial approximation method for ReLU NNs to formally verify them, provides valuable insights into the balance between verification ease and computational efficiency. These methods offer promising approaches to the formal verification of neural networks, further enhancing the robustness and reliability of these systems. The thesis also extends the application of these theories and algorithms to the safety of autonomous systems with neural network controllers. This practical application underscores the real-world implications of formal verification in ensuring the safety and reliability of autonomous systems. In summary, this thesis provides a comprehensive understanding of the formal verification of neural networks, underscoring the importance of algorithm development and its real-world applications. The findings from this study contribute significantly to this critical field of study, with implications for the fairness, safety, and robustness of NNs
Recommended from our members
Hierarchical Reinforcement Learning with Model-Based Planning for Finding Sparse Rewards
Get PDFReinforcement learning (RL) has proven useful for a wide variety of important applications, including robotics, autonomous vehicles, healthcare, finance, gaming, recommendation systems, and advertising, among many others. In general, RL involves training an agent to make decisions based on a reward signal. One of the major challenges in the field is the sparse reward problem, which occurs when the agent receives rewards only occasionally during the training process. This can make conventional RL algorithms difficult to train since the agent does not receive enough feedback to learn the optimal policy. Model-based planning is one potential solution to the sparse reward problem since it enables an agent to simulate their actions and predict the outcome far into the future. However, planning can be computationally expensive or even intractable when too many time steps are required to be internally simulated, due to combinatorial explosion.To address these challenges, this thesis presents a new RL algorithm that uses a hierarchy of model-based (manager) and model-free (worker) policies to take advantage of the unique advantages of both. The worker takes guidance from the manager in the form of a goal or selected policy. The worker is computationally efficient and can respond to changes or uncertainty in the environment to carry out its task. From the manager’s perspective, this abstracts away the trivially small state transitions, reducing the depth needed for tree search, and greatly improving the efficiency of planning. Two different applications were used for evaluation of the hierarchical agent. The first is a maze navigation environment, with continuous-state dynamics and unique episodes. This makes the environment extremely challenging for both model-based and model-free algorithms. The performance of the agent was evaluated on multiple platforms for the random maze task, including DeepMind Lab. For the second demonstration, the proposed algorithm was compared against other algorithms with the Arcade Learning Environment, which is a popular RL benchmark. In comparison with state-of-the-art algorithms, the proposed hierarchical algorithm is shown to have a faster convergence and greater sample efficiency on several tasks. Overall, the proposed hierarchical approach is a potential solution to the sparse rewards problem, and may enable RL algorithms to be applied to a wider range of tasks, ultimately leading to better outcomes in various applications
Going Beyond Counting First Authors in Author Co-citation Analysis
Get PDFThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
- …
