OpenRaiser/Intern-Atlas huggingface dataset:
A Rational Agent Controlling an Autonomous Vehicle: Implementation and Formal Verification
Venue: arXiv cs.LO 2017
Year: 2017

The development and deployment of Autonomous Vehicles (AVs) on our roads is not only realistic in the near future but can also bring significant benefits. In particular, it can potentially solve several problems relating to vehicles and traffic, for instance: (i) possible reduction of traffic congestion, with the consequence of improved fuel economy and reduced driver inactivity; (ii) possible reduction in the number of accidents, assuming that an AV can minimise the human errors that often cause traffic accidents; and (iii) increased ease of parking, especially when one considers the potential for shared AVs. In order to deploy an AV there are significant steps that must be completed in terms of hardware and software. As expected, software components play a key role in the complex AV system and so, at least for safety, we should assess the correctness of these components. In this paper, we are concerned with the high-level software component(s) responsible for the decisions in an AV. We intend to model an AV capable of navigation; obstacle avoidance; obstacle selection (when a crash is unavoidable) and vehicle recovery, etc, using a rational agent. To achieve this, we have established the following stages. First, the agent plans and actions have been implemented within the Gwendolen agent programming language. Second, we have built a simulated automotive environment in the Java language. Third, we have formally specified some of the required agent properties through LTL formulae, which are then formally verified with the AJPF verification tool. Finally, within the MCAPL framework (which comprises all the tools used in previous stages) we have obtained formal verification of our AV agent in terms of its specific behaviours. For example, the agent plans responsible for selecting an obstacle with low potential damage, instead of a higher damage obstacle (when possible) can be formally verified within MCAPL. We must emphasise that the major goal (of our present approach) lies in the formal verification of agent plans, rather than evaluating real-world applications. For this reason we utilised a simple matrix representation concerning the environment used by our agent.
Formal Verification of Station Keeping Maneuvers for a Planar Autonomous Hybrid System
Venue: arXiv cs.SY 2017
Year: 2017

We formally verify a hybrid control law designed to perform a station keeping maneuver for a planar vehicle. Such maneuver requires that the vehicle reaches a neighborhood of its station in finite time and remains in it while waiting for further instructions. We model the dynamics as well as the control law as a hybrid program and formally verify both the reachability and safety properties involved. We highlight in particular the automated generation of invariant regions which turns out to be crucial in performing such verification. We use the theorem prover Keymaera X to discharge some of the generated proof obligations.
Best Practices in Convolutional Networks for Forward-Looking Sonar Image Recognition
Venue: arXiv cs.CV 2017
Year: 2017

Convolutional Neural Networks (CNN) have revolutionized perception for color images, and their application to sonar images has also obtained good results. But in general CNNs are difficult to train without a large dataset, need manual tuning of a considerable number of hyperparameters, and require many careful decisions by a designer. In this work, we evaluate three common decisions that need to be made by a CNN designer, namely the performance of transfer learning, the effect of object/image size and the relation between training set size. We evaluate three CNN models, namely one based on LeNet, and two based on the Fire module from SqueezeNet. Our findings are: Transfer learning with an SVM works very well, even when the train and transfer sets have no classes in common, and high classification performance can be obtained even when the target dataset is small. The ADAM optimizer combined with Batch Normalization can make a high accuracy CNN classifier, even with small image sizes (16 pixels). At least 50 samples per class are required to obtain $90\%$ test accuracy, and using Dropout with a small dataset helps improve performance, but Batch Normalization is better when a large dataset is available.
Efficient Logging in Non-Volatile Memory by Exploiting Coherency Protocols
Venue: arXiv cs.DC 2017
Year: 2017

Non-volatile memory (NVM) technologies such as PCM, ReRAM and STT-RAM allow processors to directly write values to persistent storage at speeds that are significantly faster than previous durable media such as hard drives or SSDs. Many applications of NVM are constructed on a logging subsystem, which enables operations to appear to execute atomically and facilitates recovery from failures. Writes to NVM, however, pass through a processor's memory system, which can delay and reorder them and can impair the correctness and cost of logging algorithms. Reordering arises because of out-of-order execution in a CPU and the inter-processor cache coherence protocol. By carefully considering the properties of these reorderings, this paper develops a logging protocol that requires only one round trip to non-volatile memory while avoiding expensive computations. We show how to extend the logging protocol to building a persistent set (hash map) that also requires only a single round trip to non-volatile memory for insertion, updating, or deletion.
An On-chip Trainable and Clock-less Spiking Neural Network with 1R Memristive Synapses
Venue: arXiv cs.NE 2017
Year: 2017

Spiking neural networks (SNNs) are being explored in an attempt to mimic brain's capability to learn and recognize at low power. Crossbar architecture with highly scalable Resistive RAM or RRAM array serving as synaptic weights and neuronal drivers in the periphery is an attractive option for SNN. Recognition (akin to reading the synaptic weight) requires small amplitude bias applied across the RRAM to minimize conductance change. Learning (akin to writing or updating the synaptic weight) requires large amplitude bias pulses to produce a conductance change. The contradictory bias amplitude requirement to perform reading and writing simultaneously and asynchronously, akin to biology, is a major challenge. Solutions suggested in the literature rely on time-division-multiplexing of read and write operations based on clocks, or approximations ignoring the reading when coincidental with writing. In this work, we overcome this challenge and present a clock-less approach wherein reading and writing are performed in different frequency domains. This enables learning and recognition simultaneously on an SNN. We validate our scheme in SPICE circuit simulator by translating a two-layered feed-forward Iris classifying SNN to demonstrate software-equivalent performance. The system performance is not adversely affected by a voltage dependence of conductance in realistic RRAMs, despite departing from linearity. Overall, our approach enables direct implementation of biological SNN algorithms in hardware.
Crowdsourcing Predictors of Residential Electric Energy Usage
Venue: arXiv cs.HC 2017
Year: 2017

Crowdsourcing has been successfully applied in many domains including astronomy, cryptography and biology. In order to test its potential for useful application in a Smart Grid context, this paper investigates the extent to which a crowd can contribute predictive hypotheses to a model of residential electric energy consumption. In this experiment, the crowd generated hypotheses about factors that make one home different from another in terms of monthly energy usage. To implement this concept, we deployed a web-based system within which 627 residential electricity customers posed 632 questions that they thought predictive of energy usage. While this occurred, the same group provided 110,573 answers to these questions as they accumulated. Thus users both suggested the hypotheses that drive a predictive model and provided the data upon which the model is built. We used the resulting question and answer data to build a predictive model of monthly electric energy consumption, using random forest regression. Because of the sparse nature of the answer data, careful statistical work was needed to ensure that these models are valid. The results indicate that the crowd can generate useful hypotheses, despite the sparse nature of the dataset.
Towards Proving the Adversarial Robustness of Deep Neural Networks
Venue: arXiv cs.LG 2017
Year: 2017

Autonomous vehicles are highly complex systems, required to function reliably in a wide variety of situations. Manually crafting software controllers for these vehicles is difficult, but there has been some success in using deep neural networks generated using machine-learning. However, deep neural networks are opaque to human engineers, rendering their correctness very difficult to prove manually; and existing automated techniques, which were not designed to operate on neural networks, fail to scale to large systems. This paper focuses on proving the adversarial robustness of deep neural networks, i.e. proving that small perturbations to a correctly-classified input to the network cannot cause it to be misclassified. We describe some of our recent and ongoing work on verifying the adversarial robustness of networks, and discuss some of the open questions we have encountered and how they might be addressed.
Mixed Integer Programming with Convex/Concave Constraints: Fixed-Parameter Tractability and Applications to Multicovering and Voting
Venue: arXiv cs.DS 2017
Year: 2017

A classic result of Lenstra [Math.~Oper.~Res.~1983] says that an integer linear program can be solved in fixed-parameter tractable (FPT) time for the parameter being the number of variables. We extend this result by incorporating non-decreasing piecewise linear convex or concave functions to our (mixed) integer programs. This general technique allows us to establish parameterized complexity of a number of classic computational problems. In particular, we prove that Weighted Set Multicover is in FPT when parameterized by the number of elements to cover, and that there exists an FPT-time approximation scheme for Multiset Multicover for the same parameter. Further, we use our general technique to prove that a number of problems from computational social choice (e.g., problems related to bribery and control in elections) are in FPT when parameterized by the number of candidates. For bribery, this resolves a nearly 10-year old family of open problems, and for weighted electoral control of Approval voting, this improves some previously known XP-memberships to FPT-memberships.
Variable Annealing Length and Parallelism in Simulated Annealing
Venue: arXiv cs.NE 2017
Year: 2017

In this paper, we propose: (a) a restart schedule for an adaptive simulated annealer, and (b) parallel simulated annealing, with an adaptive and parameter-free annealing schedule. The foundation of our approach is the Modified Lam annealing schedule, which adaptively controls the temperature parameter to track a theoretically ideal rate of acceptance of neighboring states. A sequential implementation of Modified Lam simulated annealing is almost parameter-free. However, it requires prior knowledge of the annealing length. We eliminate this parameter using restarts, with an exponentially increasing schedule of annealing lengths. We then extend this restart schedule to parallel implementation, executing several Modified Lam simulated annealers in parallel, with varying initial annealing lengths, and our proposed parallel annealing length schedule. To validate our approach, we conduct experiments on an NP-Hard scheduling problem with sequence-dependent setup constraints. We compare our approach to fixed length restarts, both sequentially and in parallel. Our results show that our approach can achieve substantial performance gains, throughout the course of the run, demonstrating our approach to be an effective anytime algorithm.
Network of Nano-Landers for In-Situ Characterization of Asteroid Impact Studies
Venue: arXiv cs.RO 2017
Year: 2017

Exploration of asteroids and comets can give insight into the origins of the solar system and can be instrumental in planetary defence and in-situ resource utilization (ISRU). Asteroids, due to their low gravity are a challenging target for surface exploration. Current missions envision performing touch-and-go operations over an asteroid surface. In this work, we analyse the feasibility of sending scores of nano-landers, each 1 kg in mass and volume of 1U, or 1000 cm3. These landers would hop, roll and fly over the asteroid surface. The landers would include science instruments such as stereo cameras, hand-lens imagers and spectrometers to characterize rock composition. A network of nano-landers situated on the surface of an asteroid can provide unique and very detailed measurements of a spacecraft impacting onto an asteroid surface. A full-scale, artificial impact experiment onto an asteroid can help characterize its composition and geology and help in the development of asteroid deflection techniques intended for planetary defence. Scores of nano-landers could provide multiple complementary views of the impact, resultant seismic activity and trajectory of the ejecta. The nano-landers can analyse the pristine, unearthed regolith shielded from effects of UV and cosmic rays and that may be millions of years old. Our approach to formulating this mission concepts utilizes automated machine learning techniques in the planning and design of space systems. We use a form of Darwinian selection to select and identify suitable number of nano-landers, the on-board instruments and control system to explore and navigate the asteroid environment. Scenarios are generated in simulation and evaluated against quantifiable mission goals such as area explored on the asteroid and amount of data recorded from the impact event.
A First Look at Ad Blocking Apps on Google Play
Venue: arXiv cs.CR 2017
Year: 2017

Online advertisers and analytics services (or trackers), are constantly tracking users activities as they access web services either through browsers or a mobile apps. Numerous tools such as browser plugins and specialized mobile apps have been proposed to limit intrusive advertisements and prevent tracking on desktop computing and mobile phones. For desktop computing, browser plugins are heavily studied for their usability and efficiency issues, however, tools that block ads and prevent trackers in mobile platforms, have received the least or no attention. In this paper, we present a first look at 97 Android adblocking apps (or adblockers), extracted from more than 1.5 million apps from Google Play, that promise to block advertisements and analytics services. With our data collection and analysis pipeline of the Android adblockers, we reveal the presences of third-party tracking libraries and sensitive permissions for critical resources on user mobile devices as well as have malware in the source codes. We analyze users' reviews for the in-effectiveness of adblockers in terms of not blocking ads and trackers. We found that a significant fraction of adblockers are not fulfilling their advertised functionality.
A New Approximation Guarantee for Monotone Submodular Function Maximization via Discrete Convexity
Venue: arXiv cs.DS 2017
Year: 2017

In monotone submodular function maximization, approximation guarantees based on the curvature of the objective function have been extensively studied in the literature. However, the notion of curvature is often pessimistic, and we rarely obtain improved approximation guarantees, even for very simple objective functions. In this paper, we provide a novel approximation guarantee by extracting an M$^\natural$-concave function $h:2^E \to \mathbb R_+$, a notion in discrete convex analysis, from the objective function $f:2^E \to \mathbb R_+$. We introduce the notion of $h$-curvature, which measures how much $f$ deviates from $h$, and show that we can obtain a $(1-γ/e-ε)$-approximation to the problem of maximizing $f$ under a cardinality constraint in polynomial time for any constant $ε> 0$. Then, we show that we can obtain nontrivial approximation guarantees for various problems by applying the proposed algorithm.
How to Train Triplet Networks with 100K Identities?
Venue: arXiv cs.CV 2017
Year: 2017

Training triplet networks with large-scale data is challenging in face recognition. Due to the number of possible triplets explodes with the number of samples, previous studies adopt the online hard negative mining(OHNM) to handle it. However, as the number of identities becomes extremely large, the training will suffer from bad local minima because effective hard triplets are difficult to be found. To solve the problem, in this paper, we propose training triplet networks with subspace learning, which splits the space of all identities into subspaces consisting of only similar identities. Combined with the batch OHNM, hard triplets can be found much easier. Experiments on the large-scale MS-Celeb-1M challenge with 100K identities demonstrate that the proposed method can largely improve the performance. In addition, to deal with heavy noise and large-scale retrieval, we also make some efforts on robust noise removing and efficient image retrieval, which are used jointly with the subspace learning to obtain the state-of-the-art performance on the MS-Celeb-1M competition (without external data in Challenge1).
Sequential 3D U-Nets for Biologically-Informed Brain Tumor Segmentation
Venue: arXiv cs.CV 2017
Year: 2017

Deep learning has quickly become the weapon of choice for brain lesion segmentation. However, few existing algorithms pre-configure any biological context of their chosen segmentation tissues, and instead rely on the neural network's optimizer to develop such associations de novo. We present a novel method for applying deep neural networks to the problem of glioma tissue segmentation that takes into account the structured nature of gliomas - edematous tissue surrounding mutually-exclusive regions of enhancing and non-enhancing tumor. We trained multiple deep neural networks with a 3D U-Net architecture in a tree structure to create segmentations for edema, non-enhancing tumor, and enhancing tumor regions. Specifically, training was configured such that the whole tumor region including edema was predicted first, and its output segmentation was fed as input into separate models to predict enhancing and non-enhancing tumor. Our method was trained and evaluated on the publicly available BraTS dataset, achieving Dice scores of 0.882, 0.732, and 0.730 for whole tumor, enhancing tumor and tumor core respectively.
Energy Trade-off in Ground-to-UAV Communication via Trajectory Design
Venue: arXiv cs.IT 2017
Year: 2017

Unmanned aerial vehicles (UAVs) have a great potential for improving the performance of wireless communication systems due to their wide coverage and high mobility. In this paper, we study a UAV-enabled data collection system, where a UAV is dispatched to collect a given amount of data from a ground terminals (GT) at fixed location. Intuitively, if the UAV flies closer to the GT, the uplink transmission energy of the GT required to send the target data can be more reduced. However, such UAV movement may consume more propulsion energy of the UAV, which needs to be properly controlled to save its limited on-board energy. As a result, the transmission energy reduction of the GT is generally at the cost of higher propulsion energy consumption of the UAV, which leads to a new fundamental energy trade-off in Ground-to-UAV (G2U) wireless communication. To characterize this trade-off, we consider two practical UAV trajectories, namely circular flight and straight flight. In each case, we first derive the energy consumption expressions of the UAV and GT, and then find the optimal GT transmit power and UAV trajectory that achieve different Pareto optimal trade-off between them. Numerical results are provided to corroborate our study.
RDeepSense: Reliable Deep Mobile Computing Models with Uncertainty Estimations
Venue: arXiv cs.LG 2017
Year: 2017

Recent advances in deep learning have led various applications to unprecedented achievements, which could potentially bring higher intelligence to a broad spectrum of mobile and ubiquitous applications. Although existing studies have demonstrated the effectiveness and feasibility of running deep neural network inference operations on mobile and embedded devices, they overlooked the reliability of mobile computing models. Reliability measurements such as predictive uncertainty estimations are key factors for improving the decision accuracy and user experience. In this work, we propose RDeepSense, the first deep learning model that provides well-calibrated uncertainty estimations for resource-constrained mobile and embedded devices. RDeepSense enables the predictive uncertainty by adopting a tunable proper scoring rule as the training criterion and dropout as the implicit Bayesian approximation, which theoretically proves its correctness.To reduce the computational complexity, RDeepSense employs efficient dropout and predictive distribution estimation instead of model ensemble or sampling-based method for inference operations. We evaluate RDeepSense with four mobile sensing applications using Intel Edison devices. Results show that RDeepSense can reduce around 90% of the energy consumption while producing superior uncertainty estimations and preserving at least the same model accuracy compared with other state-of-the-art methods.
Optimal Transport for Deep Joint Transfer Learning
Venue: arXiv cs.CV 2017
Year: 2017

Training a Deep Neural Network (DNN) from scratch requires a large amount of labeled data. For a classification task where only small amount of training data is available, a common solution is to perform fine-tuning on a DNN which is pre-trained with related source data. This consecutive training process is time consuming and does not consider explicitly the relatedness between different source and target tasks. In this paper, we propose a novel method to jointly fine-tune a Deep Neural Network with source data and target data. By adding an Optimal Transport loss (OT loss) between source and target classifier predictions as a constraint on the source classifier, the proposed Joint Transfer Learning Network (JTLN) can effectively learn useful knowledge for target classification from source data. Furthermore, by using different kind of metric as cost matrix for the OT loss, JTLN can incorporate different prior knowledge about the relatedness between target categories and source categories. We carried out experiments with JTLN based on Alexnet on image classification datasets and the results verify the effectiveness of the proposed JTLN in comparison with standard consecutive fine-tuning. This Joint Transfer Learning with OT loss is general and can also be applied to other kind of Neural Networks.