OpenRaiser/Intern-Atlas huggingface dataset:
Selective Feature Connection Mechanism: Concatenating Multi-layer CNN Features with a Feature Selector
Venue: arXiv cs.CV 2019
Year: 2019

Different layers of deep convolutional neural networks(CNNs) can encode different-level information. High-layer features always contain more semantic information, and low-layer features contain more detail information. However, low-layer features suffer from the background clutter and semantic ambiguity. During visual recognition, the feature combination of the low-layer and high-level features plays an important role in context modulation. If directly combining the high-layer and low-layer features, the background clutter and semantic ambiguity may be caused due to the introduction of detailed information. In this paper, we propose a general network architecture to concatenate CNN features of different layers in a simple and effective way, called Selective Feature Connection Mechanism (SFCM). Low-level features are selectively linked to high-level features with a feature selector which is generated by high-level features. The proposed connection mechanism can effectively overcome the above-mentioned drawbacks. We demonstrate the effectiveness, superiority, and universal applicability of this method on multiple challenging computer vision tasks, including image classification, scene text detection, and image-to-image translation.
Cluster analysis of homicide rates in the Brazilian state of Goias from 2002 to 2014
Venue: arXiv cs.CY 2019
Year: 2019

Homicide mortality is a worldwide concern and has occupied the agenda of researchers and public managers. In Brazil, homicide is the third leading cause of death in the general population and the first in the 15-39 age group. In South America, Brazil has the third highest homicide mortality, behind Venezuela and Colombia. To measure the impacts of violence it is important to assess health systems and criminal justice, as well as other areas. In this paper, we analyze the spatial distribution of homicide mortality in the state of Goias, Center-West of Brazil, since the homicide rate increased from 24.5 per 100,000 in 2002 to 42.6 per 100,000 in 2014 in this location. Moreover, this state had the fifth position of homicides in Brazil in 2014. We considered socio-demographic variables for the state, performed analysis about correlation and employed three clustering algorithms: K-means, Density-based and Hierarchical. The results indicate the homicide rates are higher in cities neighbors of large urban centers, although these cities have the best socioeconomic indicators.
Verified Runtime Validation for Partially Observable Hybrid Systems
Venue: arXiv cs.LO 2019
Year: 2019

Formal verification provides strong safety guarantees but only for models of cyber-physical systems. Hybrid system models describe the required interplay of computation and physical dynamics, which is crucial to guarantee what computations lead to safe physical behavior (e.g., cars should not collide). Control computations that affect physical dynamics must act in advance to avoid possibly unsafe future circumstances. Formal verification then ensures that the controllers correctly identify and provably avoid unsafe future situations under a certain model of physics. But any model of physics necessarily deviates from reality and, moreover, any observation with real sensors and manipulation with real actuators is subject to uncertainty. This makes runtime validation a crucial step to monitor whether the model assumptions hold for the real system implementation. The key question is what property needs to be runtime-monitored and what a satisfied runtime monitor entails about the safety of the system: the observations of a runtime monitor only relate back to the safety of the system if they are themselves accompanied by a proof of correctness! For an unbroken chain of correctness guarantees, we, thus, synthesize runtime monitors in a provably correct way from provably safe hybrid system models. This paper addresses the inevitable challenge of making the synthesized monitoring conditions robust to partial observability of sensor uncertainty and partial controllability due to actuator disturbance. We show that the monitoring conditions result in provable safety guarantees with fallback controllers that react to monitor violation at runtime.
Tail Probabilities for Randomized Program Runtimes via Martingales for Higher Moments
Venue: arXiv cs.LO 2019
Year: 2019

Programs with randomization constructs is an active research topic, especially after the recent introduction of martingale-based analysis methods for their termination and runtimes. Unlike most of the existing works that focus on proving almost-sure termination or estimating the expected runtime, in this work we study the tail probabilities of runtimes-such as "the execution takes more than 100 steps with probability at most 1%." To this goal, we devise a theory of supermartingales that overapproximate higher moments of runtime. These higher moments, combined with a suitable concentration inequality, yield useful upper bounds of tail probabilities. Moreover, our vector-valued formulation enables automated template-based synthesis of those supermartingales. Our experiments suggest the method's practical use.
Symbolic Register Automata
Venue: arXiv cs.FL 2019
Year: 2019

Symbolic Finite Automata and Register Automata are two orthogonal extensions of finite automata motivated by real-world problems where data may have unbounded domains. These automata address a demand for a model over large or infinite alphabets, respectively. Both automata models have interesting applications and have been successful in their own right. In this paper, we introduce Symbolic Register Automata, a new model that combines features from both symbolic and register automata, with a view on applications that were previously out of reach. We study their properties and provide algorithms for emptiness, inclusion and equivalence checking, together with experimental results.
Towards Training Recurrent Neural Networks for Lifelong Learning
Venue: arXiv cs.LG 2019
Year: 2019

Catastrophic forgetting and capacity saturation are the central challenges of any parametric lifelong learning system. In this work, we study these challenges in the context of sequential supervised learning with an emphasis on recurrent neural networks. To evaluate the models in the lifelong learning setting, we propose a curriculum-based, simple, and intuitive benchmark where the models are trained on tasks with increasing levels of difficulty. To measure the impact of catastrophic forgetting, the model is tested on all the previous tasks as it completes any task. As a step towards developing true lifelong learning systems, we unify Gradient Episodic Memory (a catastrophic forgetting alleviation approach) and Net2Net(a capacity expansion approach). Both these models are proposed in the context of feedforward networks and we evaluate the feasibility of using them for recurrent networks. Evaluation on the proposed benchmark shows that the unified model is more suitable than the constituent models for lifelong learning setting.
Bilingual Dictionary Induction for Bantu Languages
Venue: arXiv cs.CL 2019
Year: 2019

We present a method for learning bilingual translation dictionaries between English and Bantu languages. We show that exploiting the grammatical structure common to Bantu languages enables bilingual dictionary induction for languages where training data is unavailable.
Not just a matter of semantics: the relationship between visual similarity and semantic similarity
Venue: arXiv cs.CV 2019
Year: 2019

Knowledge transfer, zero-shot learning and semantic image retrieval are methods that aim at improving accuracy by utilizing semantic information, e.g. from WordNet. It is assumed that this information can augment or replace missing visual data in the form of labeled training images because semantic similarity correlates with visual similarity. This assumption may seem trivial, but is crucial for the application of such semantic methods. Any violation can cause mispredictions. Thus, it is important to examine the visual-semantic relationship for a certain target problem. In this paper, we use five different semantic and visual similarity measures each to thoroughly analyze the relationship without relying too much on any single definition. We postulate and verify three highly consequential hypotheses on the relationship. Our results show that it indeed exists and that WordNet semantic similarity carries more information about visual similarity than just the knowledge of "different classes look different". They suggest that classification is not the ideal application for semantic methods and that wrong semantic information is much worse than none.
Equilibria-based Probabilistic Model Checking for Concurrent Stochastic Games
Venue: arXiv cs.LO 2019
Year: 2019

Probabilistic model checking for stochastic games enables formal verification of systems that comprise competing or collaborating entities operating in a stochastic environment. Despite good progress in the area, existing approaches focus on zero-sum goals and cannot reason about scenarios where entities are endowed with different objectives. In this paper, we propose probabilistic model checking techniques for concurrent stochastic games based on Nash equilibria. We extend the temporal logic rPATL (probabilistic alternating-time temporal logic with rewards) to allow reasoning about players with distinct quantitative goals, which capture either the probability of an event occurring or a reward measure. We present algorithms to synthesise strategies that are subgame perfect social welfare optimal Nash equilibria, i.e., where there is no incentive for any players to unilaterally change their strategy in any state of the game, whilst the combined probabilities or rewards are maximised. We implement our techniques in the PRISM-games tool and apply them to several case studies, including network protocols and robot navigation, showing the benefits compared to existing approaches.
Recurrent Convolutions for Causal 3D CNNs
Venue: arXiv cs.CV 2019
Year: 2019

Recently, three dimensional (3D) convolutional neural networks (CNNs) have emerged as dominant methods to capture spatiotemporal representations in videos, by adding to pre-existing 2D CNNs a third, temporal dimension. Such 3D CNNs, however, are anti-causal (i.e., they exploit information from both the past and the future frames to produce feature representations, thus preventing their use in online settings), constrain the temporal reasoning horizon to the size of the temporal convolution kernel, and are not temporal resolution-preserving for video sequence-to-sequence modelling, as, for instance, in action detection. To address these serious limitations, here we present a new 3D CNN architecture for the causal/online processing of videos. Namely, we propose a novel Recurrent Convolutional Network (RCN), which relies on recurrence to capture the temporal context across frames at each network level. Our network decomposes 3D convolutions into (1) a 2D spatial convolution component, and (2) an additional hidden state $1\times 1$ convolution, applied across time. The hidden state at any time $t$ is assumed to depend on the hidden state at $t-1$ and on the current output of the spatial convolution component. As a result, the proposed network: (i) produces causal outputs, (ii) provides flexible temporal reasoning, (iii) preserves temporal resolution. Our experiments on the large-scale large Kinetics and MultiThumos datasets show that the proposed method performs comparably to anti-causal 3D CNNs, while being causal and using fewer parameters.
Attention-based Walking Gait and Direction Recognition in Wi-Fi Networks
Venue: arXiv cs.HC 2019
Year: 2019

The study of human gait recognition has been becoming an active research field. In this paper, we propose to adopt the attention-based Recurrent Neural Network (RNN) encoder-decoder framework to implement a cycle-independent human gait and walking direction recognition system in Wi-Fi networks. For capturing more human walking dynamics, two receivers together with one transmitter are deployed in different spatial layouts. In the proposed system, the Channel State Information (CSI) measurements from different receivers are first gathered together and refined to form an integrated walking profile. Then, the RNN encoder reads and encodes the walking profile into primary feature vectors. Given a specific recognition task, the decoder computes a corresponding attention vector which is a weighted sum of the primary features assigned with different attentions, and is finally used to predict the target. The attention scheme motivates our system to learn to adaptively align with different critical clips of CSI data sequence for human walking gait and direction recognitions. We implement our system on commodity Wi-Fi devices in indoor environment, and the experimental results demonstrate that our system can achieve average F1 scores of 89.69% for gait recognition from a group of 8 subjects and 95.06% for direction recognition from 8 walking directions, in addition, the average accuracies of these two recognition tasks both exceed 97%.
Multiphase-Linear Ranking Functions and their Relation to Recurrent Sets
Venue: arXiv cs.PL 2019
Year: 2019

Multiphase ranking functions (M$Φ$RFs) are tuples $\langle f_1,\ldots,f_d \rangle$ of linear functions that are often used to prove termination of loops in which the computation progresses through a number of "phases". Our work provides new insights regarding such functions for loops described by a conjunction of linear constraints (Single-Path Constraint loops). The decision problem existence of a M$Φ$RF asks to determine whether a given SLC loop admits a M$Φ$RF, and the corresponding bounded decision problem restricts the search to M$Φ$RFs of depth $d$, where the parameter $d$ is part of the input. The algorithmic and complexity aspects of the bounded problem have been completely settled in a recent work. In this paper we make progress regarding the existence problem, without a given depth bound. In particular, we present an approach that reveals some important insights into the structure of these functions. Interestingly, it relates the problem of seeking M$Φ$RFs to that of seeking recurrent sets (used to prove non-termination). It also helps in identifying classes of loops for which M$Φ$RFs are sufficient. Our research has led to a new representation for single-path loops, the difference polyhedron replacing the customary transition polyhedron. This representation yields new insights on M$Φ$RFs and SLC loops in general. For example, a result on bounded SLC loops becomes straightforward.
Feature selection as Monte-Carlo Search in Growing Single Rooted Directed Acyclic Graph by Best Leaf Identification
Venue: arXiv cs.LG 2019
Year: 2019

Monte Carlo tree search (MCTS) has received considerable interest due to its spectacular success in the difficult problem of computer Go and also proved beneficial in a range of other domains. A major issue that has received little attention in the MCTS literature is the fact that, in most games, different actions can lead to the same state, that may lead to a high degree of redundancy in tree representation and unnecessary additional computational cost. We extend MCTS to single rooted directed acyclic graph (SR-DAG), and consider the Best Arm Identification (BAI) and the Best Leaf Identification (BLI) problem of an expanding SR-DAG of arbitrary depth. We propose algorithms that are (epsilon, delta)-correct in the fixed confidence setting, and prove an asymptotic upper bounds of sample complexity for our BAI algorithm. As a major application for our BLI algorithm, a novel approach for Feature Selection is proposed by representing the feature set space as a SR-DAG and repeatedly evaluating feature subsets until a candidate for the best leaf is returned, a proof of concept is shown on benchmark data sets.
SEIGAN: Towards Compositional Image Generation by Simultaneously Learning to Segment, Enhance, and Inpaint
Venue: arXiv cs.CV 2019
Year: 2019

We present a novel approach to image manipulation and understanding by simultaneously learning to segment object masks, paste objects to another background image, and remove them from original images. For this purpose, we develop a novel generative model for compositional image generation, SEIGAN (Segment-Enhance-Inpaint Generative Adversarial Network), which learns these three operations together in an adversarial architecture with additional cycle consistency losses. To train, SEIGAN needs only bounding box supervision and does not require pairing or ground truth masks. SEIGAN produces better generated images (evaluated by human assessors) than other approaches and produces high-quality segmentation masks, improving over other adversarially trained approaches and getting closer to the results of fully supervised training.
FD-GAN: Face-demorphing generative adversarial network for restoring accomplice's facial image
Venue: arXiv cs.CV 2019
Year: 2019

Face morphing attack is proved to be a serious threat to the existing face recognition systems. Although a few face morphing detection methods have been put forward, the face morphing accomplice's facial restoration remains a challenging problem. In this paper, a face de-morphing generative adversarial network (FD-GAN) is proposed to restore the accomplice's facial image. It utilizes a symmetric dual network architecture and two levels of restoration losses to separate the identity feature of the morphing accomplice. By exploiting the captured facial image (containing the criminal's identity) from the face recognition system and the morphed image stored in the e-passport system (containing both criminal and accomplice's identities), the FD-GAN can effectively restore the accomplice's facial image. Experimental results and analysis demonstrate the effectiveness of the proposed scheme. It has great potential to be implemented for detecting the face morphing accomplice in a real identity verification scenario.
Electric vehicle charging during the day or at night: a perspective on carbon emissions
Venue: arXiv cs.SY 2019
Year: 2019

We propose an emission-oriented charging scheme to evaluate the emissions of electric vehicle (EV) charging from the electricity sector at the region of Electric Reliability Council of Texas (ERCOT). We investigate both day- and night-charging scenarios combined with realistic system load demand under the emission-oriented vs direct charging schemes. Our emission-oriented charging scheme reduces carbon emissions in the day by 13.8% on average. We also find that emission-oriented charging results in a significant CO2 reduction in 30% of the days in a year compared with direct charging. Apart from offering a flat rebate for EV owners, our analysis reveals that certain policy incentives (e.g. pricing) regarding EV charging should be taken into account in order to reflect the benefits of emissions reduction that haven't been incorporated in the current market of electricity transactions.
Synthetic Lung Nodule 3D Image Generation Using Autoencoders
Venue: arXiv cs.CV 2019
Year: 2019

One of the challenges of using machine learning techniques with medical data is the frequent dearth of source image data on which to train. A representative example is automated lung cancer diagnosis, where nodule images need to be classified as suspicious or benign. In this work we propose an automatic synthetic lung nodule image generator. Our 3D shape generator is designed to augment the variety of 3D images. Our proposed system takes root in autoencoder techniques, and we provide extensive experimental characterization that demonstrates its ability to produce quality synthetic images.
Tracking Control by the Newton-Raphson Flow: Applications to Autonomous Vehicles
Venue: arXiv cs.SY 2019
Year: 2019

This paper concerns applications of a recently-developed output-tracking technique to trajectory control of autonomous vehicles. The technique is based on three principles: Newton-Raphson flow for solving algebraic equations,output prediction, and controller speedup. Early applications of the technique, made to simple systems of an academic nature,were implemented by simple algorithms requiring modest computational efforts. In contrast, this paper tests it on commonly-used dynamic models to see if it can handle more complex control scenarios. Results are derived from simulations as well as a laboratory setting, and they indicate effective tracking convergence despite the simplicity of the control algorithm.
Coupled Recurrent Models for Polyphonic Music Composition
Venue: arXiv cs.SD 2019
Year: 2019

This paper introduces a novel recurrent model for music composition that is tailored to the structure of polyphonic music. We propose an efficient new conditional probabilistic factorization of musical scores, viewing a score as a collection of concurrent, coupled sequences: i.e. voices. To model the conditional distributions, we borrow ideas from both convolutional and recurrent neural models; we argue that these ideas are natural for capturing music's pitch invariances, temporal structure, and polyphony. We train models for single-voice and multi-voice composition on 2,300 scores from the KernScores dataset.
Improved Quantum Multicollision-Finding Algorithm
Venue: arXiv cs.CR 2019
Year: 2019

The current paper improves the number of queries of the previous quantum multi-collision finding algorithms presented by Hosoyamada et al. at Asiacrypt 2017. Let an $l$-collision be a tuple of $l$ distinct inputs that result in the same output of a target function. In cryptology, it is important to study how many queries are required to find $l$-collisions for random functions of which domains are larger than ranges. The previous algorithm finds an $l$-collision for a random function by recursively calling the algorithm for finding $(l-1)$-collisions, and it achieves the average quantum query complexity of $O(N^{(3^{l-1}-1) / (2 \cdot 3^{l-1})})$, where $N$ is the range size of target functions. The new algorithm removes the redundancy of the previous recursive algorithm so that different recursive calls can share a part of computations. The new algorithm finds an $l$-collision for random functions with the average quantum query complexity of $O(N^{(2^{l-1}-1) / (2^{l}-1)})$, which improves the previous bound for all $l\ge 3$ (the new and previous algorithms achieve the optimal bound for $l=2$). More generally, the new algorithm achieves the average quantum query complexity of $O\left(c^{3/2}_N N^{\frac{2^{l-1}-1}{ 2^{l}-1}}\right)$ for a random function $f\colon X\to Y$ such that $|X| \geq l \cdot |Y| / c_N$ for any $1\le c_N \in o(N^{\frac{1}{2^l - 1}})$. With the same query complexity, it also finds a multiclaw for random functions, which is harder to find than a multicollision.