OpenRaiser/Intern-Atlas huggingface dataset:
Cubical informal type theory: the higher groupoid structure
Venue: arXiv cs.LO 2018
Year: 2018

Following a project of developing conventions and notations for informal type theory carried out in the homotopy type theory book for a framework built out of an augmentation of constructive type theory with axioms governing higher-dimensional constructions via Voevodsky's univalance axiom and higher-inductive types, this paper proposes a way of doing informal type theory with a cubical type theory as the underlying foundation instead. To that end, we adopt a cubical type theory recently proposed by Angiuli, Hou (Favonia) and Harper, a framework with a cumulative hierarchy of univalent Kan universes, full univalence and instances of higher-inductive types. In the present paper we confine ourselves to some elementary theorems concerning the higher groupoid structure of types.
Global Semantic Consistency for Zero-Shot Learning
Venue: arXiv cs.CV 2018
Year: 2018

In image recognition, there are many cases where training samples cannot cover all target classes. Zero-shot learning (ZSL) utilizes the class semantic information to classify samples of the unseen categories that have no corresponding samples contained in the training set. In this paper, we propose an end-to-end framework, called Global Semantic Consistency Network (GSC-Net for short), which makes complete use of the semantic information of both seen and unseen classes, to support effective zero-shot learning. We also adopt a soft label embedding loss to further exploit the semantic relationships among classes. To adapt GSC-Net to a more practical setting, Generalized Zero-shot Learning (GZSL), we introduce a parametric novelty detection mechanism. Our approach achieves the state-of-the-art performance on both ZSL and GZSL tasks over three visual attribute datasets, which validates the effectiveness and advantage of the proposed framework.
Analysis of Evolutionary Algorithms in Dynamic and Stochastic Environments
Venue: arXiv cs.NE 2018
Year: 2018

Many real-world optimization problems occur in environments that change dynamically or involve stochastic components. Evolutionary algorithms and other bio-inspired algorithms have been widely applied to dynamic and stochastic problems. This survey gives an overview of major theoretical developments in the area of runtime analysis for these problems. We review recent theoretical studies of evolutionary algorithms and ant colony optimization for problems where the objective functions or the constraints change over time. Furthermore, we consider stochastic problems under various noise models and point out some directions for future research.
Real-time gait planner for human walking using a lower limb exoskeleton and its implementation on Exoped robot
Venue: arXiv cs.RO 2018
Year: 2018

Lower extremity exoskeleton has been developed as a motion assistive technology in recent years. Walking pattern generation is a fundamental topic in the design of these robots. The usual approach with most exoskeletons is to use a pre-recorded pattern as a look-up table. There are some deficiencies with this method, including data storage limitation and poor regulation relating to the walking parameters. Therefore modeling human walking patterns to use in exoskeletons is required. The few existing models provide piece by piece walking patterns, only generating at the beginning of each stride cycle in respect to fixed walking parameters. In this paper, we present a real-time walking pattern generation method which enables changing the walking parameters during the stride. For this purpose, two feedback controlled third order systems are proposed as optimal trajectory planners for generating the trajectory of the x and y components of each joints position. The boundary conditions of the trajectories are obtained according to some pre-considered walking constraints. In addition, a cost function is intended for each trajectory planner in order to increase the trajectories smoothness. We use the minimum principle of Pontryagin to design the feedback controller in order to track the boundary conditions in such a way that the cost functions are minimized. Finally, by using inverse kinematics equations, the proper joints angles are generated for and implemented on Exoped robot. The good performance of the gait planner is demonstrated by second derivative continuity of the trajectories being maintained as a result of a simulation, and user satisfaction being determined by experimental testing.
Towards an Active, Autonomous and Intelligent Cyber Defense of Military Systems: the NATO AICA Reference Architecture
Venue: arXiv cs.CR 2018
Year: 2018

Within the future Global Information Grid, complex massively interconnected systems, isolated defense vehicles, sensors and effectors, and infrastructures and systems demanding extremely low failure rates, to which human security operators cannot have an easy access and cannot deliver fast enough reactions to cyber-attacks, need an active, autonomous and intelligent cyber defense. Multi Agent Systems for Cyber Defense may provide an answer to this requirement. This paper presents the concept and architecture of an Autonomous Intelligent Cyber defense Agent (AICA). First, we describe the rationale of the AICA concept. Secondly, we explain the methodology and purpose that drive the definition of the AICA Reference Architecture (AICARA) by NATO's IST-152 Research and Technology Group. Thirdly, we review some of the main features and challenges of Multi Autonomous Intelligent Cyber defense Agent (MAICA). Fourthly, we depict the initially assumed AICA Reference Architecture. Then we present one of our preliminary research issues, assumptions and ideas. Finally, we present the future lines of research that will help develop and test the AICA / MAICA concept.
To Skip or to Switch? Minimizing Age of Information under Link Capacity Constraint
Venue: arXiv cs.IT 2018
Year: 2018

Consider a scenario where a source continuously monitors an object and sends time-stamped status updates to a destination through a rate-limited link. In order to measure the "freshness" of the status information available at the destination, we adopt the metric called Age of Information (AoI). We assume all updates are of the same size, and arrive randomly at the source according to a Bernoulli process. Due to the link capacity constraint, it takes $d$ ($d\geq 2$) time slots for the source to complete the transmission of an update. Therefore, when a new update when arrives at the source and it is transmitting another update, the source needs to decide whether to skip the new arrival or to switch to it, in order to minimize the expected average AoI at the destination. We prove that within a broadly defined class of online policies, the optimal policy should be a renewal policy, and has a sequential switching property. We then show that the optimal decision the source should take in any time slot has a multiple-threshold structure, and only depends on the age of the update being transmitted and the AoI in the system. The thresholds are then numerically identified by formulating the problem as a Markov Decision Process (MDP).
CVC4 at the SMT Competition 2018
Venue: arXiv cs.LO 2018
Year: 2018

This paper is a description of the CVC4 SMT solver as entered into the 2018 SMT Competition. We only list important differences from the 2017 SMT Competition version of CVC4. For further and more detailed information about CVC4, please refer to the original paper, the CVC4 website, or the source code on GitHub.
Age of Information and Throughput in a Shared Access Network with Heterogeneous Traffic
Venue: arXiv cs.NI 2018
Year: 2018

We consider a cognitive shared access scheme consisting of a high priority primary node and a low priority network with $N$ secondary nodes accessing the spectrum. Assuming bursty traffic at the primary node, saturated queues at the secondary nodes, and multipacket reception capabilities at the receivers, we derive analytical expressions of the time average age of information of the primary node and the throughput of the secondary nodes. We formulate two optimization problems, the first aiming to minimize the time average age of information of the primary node subject to an aggregate secondary throughput requirement. The second problem aims to maximize the aggregate secondary throughput of the network subject to a maximum time average staleness constraint. Our results provide guidelines for the design of a multiple access system with multipacket reception capabilities that fulfils both timeliness and throughput requirements.
Wireless Channel Dynamics and Robustness for Ultra-Reliable Low-Latency Communications
Venue: arXiv cs.IT 2018
Year: 2018

Interactive, immersive and critical applications demand ultra-reliable low-latency communication (URLLC). To build wireless communication systems that can support these applications, understanding the characteristics of the wireless medium is paramount. Although wireless channel characteristics and dynamics have been extensively studied, it is important to revisit these concepts in the context of the strict demands of low latency and ultra-reliability. In this paper, we bring a modeling approach from robust control to wireless communication -- the wireless channel characteristics are given a nominal model around which we allow for some quantified uncertainty. We propose certain key "directions" along which to bound model uncertainty that are relevant to URLLC. For the nominal model, we take an in-depth look at wireless channel characteristics such as spatial and temporal correlations based on Jakes' model. Contrary to what has been claimed in the literature, we find that standard Rayleigh fading processes are not bandlimited. This has significant implications on the predictability of channels. We also find that under reasonable conditions the spatial correlation of channels provide a fading distribution that is not too far off from an independent spatial fading model. Additionally, we look at the impact of these channel models on cooperative communication based systems. We find that while spatial-diversity-based techniques are necessary to combat the adverse effects of fading, time-diversity-based techniques are necessary to be robust against unmodeled errors. Robust URLLC systems need to operate with both an SNR margin and a time/repetition margin.
Finding Local Minima via Stochastic Nested Variance Reduction
Venue: arXiv cs.LG 2018
Year: 2018

We propose two algorithms that can find local minima faster than the state-of-the-art algorithms in both finite-sum and general stochastic nonconvex optimization. At the core of the proposed algorithms is $\text{One-epoch-SNVRG}^+$ using stochastic nested variance reduction (Zhou et al., 2018a), which outperforms the state-of-the-art variance reduction algorithms such as SCSG (Lei et al., 2017). In particular, for finite-sum optimization problems, the proposed $\text{SNVRG}^{+}+\text{Neon2}^{\text{finite}}$ algorithm achieves $\tilde{O}(n^{1/2}ε^{-2}+nε_H^{-3}+n^{3/4}ε_H^{-7/2})$ gradient complexity to converge to an $(ε, ε_H)$-second-order stationary point, which outperforms $\text{SVRG}+\text{Neon2}^{\text{finite}}$ (Allen-Zhu and Li, 2017) , the best existing algorithm, in a wide regime. For general stochastic optimization problems, the proposed $\text{SNVRG}^{+}+\text{Neon2}^{\text{online}}$ achieves $\tilde{O}(ε^{-3}+ε_H^{-5}+ε^{-2}ε_H^{-3})$ gradient complexity, which is better than both $\text{SVRG}+\text{Neon2}^{\text{online}}$ (Allen-Zhu and Li, 2017) and Natasha2 (Allen-Zhu, 2017) in certain regimes. Furthermore, we explore the acceleration brought by third-order smoothness of the objective function.
Self-Driving Vehicle Verification Towards a Benchmark
Venue: arXiv cs.LO 2018
Year: 2018

Industrial cyber-physical systems are hybrid systems with strict safety requirements. Despite not having a formal semantics, most of these systems are modeled using Stateflow/Simulink for mainly two reasons: (1) it is easier to model, test, and simulate using these tools, and (2) dynamics of these systems are not supported by most other tools. Furthermore, with the ever growing complexity of cyber-physical systems, grows the gap between what can be modeled using an automatic formal verification tool and models of industrial cyber-physical systems. In this paper, we present a simple formal model for self-deriving cars. While after some simplification, safety of this system has already been proven manually, to the best of our knowledge, no automatic formal verification tool supports its dynamics. We hope this serves as a challenge problem for formal verification tools targeting industrial applications.
RUC+CMU: System Report for Dense Captioning Events in Videos
Venue: arXiv cs.CV 2018
Year: 2018

This notebook paper presents our system in the ActivityNet Dense Captioning in Video task (task 3). Temporal proposal generation and caption generation are both important to the dense captioning task. Therefore, we propose a proposal ranking model to employ a set of effective feature representations for proposal generation, and ensemble a series of caption models enhanced with context information to generate captions robustly on predicted proposals. Our approach achieves the state-of-the-art performance on the dense video captioning task with 8.529 METEOR score on the challenge testing set.
xGEMs: Generating Examplars to Explain Black-Box Models
Venue: arXiv cs.LG 2018
Year: 2018

This work proposes xGEMs or manifold guided exemplars, a framework to understand black-box classifier behavior by exploring the landscape of the underlying data manifold as data points cross decision boundaries. To do so, we train an unsupervised implicit generative model -- treated as a proxy to the data manifold. We summarize black-box model behavior quantitatively by perturbing data samples along the manifold. We demonstrate xGEMs' ability to detect and quantify bias in model learning and also for understanding the changes in model behavior as training progresses.
Deep Reinforcement Learning: An Overview
Venue: arXiv cs.LG 2018
Year: 2018

In recent years, a specific machine learning method called deep learning has gained huge attraction, as it has obtained astonishing results in broad applications such as pattern recognition, speech recognition, computer vision, and natural language processing. Recent research has also been shown that deep learning techniques can be combined with reinforcement learning methods to learn useful representations for the problems with high dimensional raw data input. This chapter reviews the recent advances in deep reinforcement learning with a focus on the most used deep architectures such as autoencoders, convolutional neural networks and recurrent neural networks which have successfully been come together with the reinforcement learning framework.
Temporal Activity Path Based Character Correction in Social Networks
Venue: arXiv cs.SI 2018
Year: 2018

Vast amount of multimedia data contains massive and multifarious social information which is used to construct large-scale social networks. In a complex social network, a character should be ideally denoted by one and only one vertex. However, it is pervasive that a character is denoted by two or more vertices with different names, thus it is usually considered as multiple, different characters. This problem causes incorrectness of results in network analysis and mining. The factual challenge is that character uniqueness is hard to correctly confirm due to lots of complicated factors, e.g. name changing and anonymization, leading to character duplication. Early, limited research has shown that previous methods depended overly upon supplementary attribute information from databases. In this paper, we propose a novel method to merge the character vertices which refer to as the same entity but are denoted with different names. With this method, we firstly build the relationship network among characters based on records of social activities participated, which are extracted from multimedia sources. Then define temporal activity paths (TAPs) for each character over time. After that, we measure similarity of the TAPs for any two characters. If the similarity is high enough, the two vertices should be considered to the same character. Based on TAPs, we can determine whether to merge the two character vertices. Our experiments shown that this solution can accurately confirm character uniqueness in large-scale social network.
Search Rank Fraud De-Anonymization in Online Systems
Venue: arXiv cs.SI 2018
Year: 2018

We introduce the fraud de-anonymization problem, that goes beyond fraud detection, to unmask the human masterminds responsible for posting search rank fraud in online systems. We collect and study search rank fraud data from Upwork, and survey the capabilities and behaviors of 58 search rank fraudsters recruited from 6 crowdsourcing sites. We propose Dolos, a fraud de-anonymization system that leverages traits and behaviors extracted from these studies, to attribute detected fraud to crowdsourcing site fraudsters, thus to real identities and bank accounts. We introduce MCDense, a min-cut dense component detection algorithm to uncover groups of user accounts controlled by different fraudsters, and leverage stylometry and deep learning to attribute them to crowdsourcing site profiles. Dolos correctly identified the owners of 95% of fraudster-controlled communities, and uncovered fraudsters who promoted as many as 97.5% of fraud apps we collected from Google Play. When evaluated on 13,087 apps (820,760 reviews), which we monitored over more than 6 months, Dolos identified 1,056 apps with suspicious reviewer groups. We report orthogonal evidence of their fraud, including fraud duplicates and fraud re-posts.
Communications, Caching and Computing for Mobile Virtual Reality: Modeling and Tradeoff
Venue: arXiv cs.IT 2018
Year: 2018

Virtual reality (VR) over wireless is emerging as an important use case of 5G networks. Immersive VR experience requires the delivery of huge data at ultra-low latency, thus demanding ultra-high transmission rate. This challenge can be largely addressed by the recent network architecture known as mobile edge computing (MEC), which enables caching and computing capabilities at the edge of wireless networks. This paper presents a novel MEC-based mobile VR delivery framework that is able to cache parts of the field of views (FOVs) in advance and run certain post-processing procedures at the mobile VR device. To optimize resource allocation at the mobile VR device, we formulate a joint caching and computing decision problem to minimize the average required transmission rate while meeting a given latency constraint. When FOVs are homogeneous, we obtain a closed-form expression for the optimal joint policy which reveals interesting communications-caching-computing tradeoffs. When FOVs are heterogeneous, we obtain a local optima of the problem by transforming it into a linearly constrained indefinite quadratic problem then applying concave convex procedure. Numerical results demonstrate great promises of the proposed mobile VR delivery framework in saving communication bandwidth while meeting low latency requirement.
A Recursive PLS (Partial Least Squares) based Approach for Enterprise Threat Management
Venue: arXiv cs.CR 2018
Year: 2018

Most of the existing solutions to enterprise threat management are preventive approaches prescribing means to prevent policy violations with varying degrees of success. In this paper we consider the complementary scenario where a number of security violations have already occurred, or security threats, or vulnerabilities have been reported and a security administrator needs to generate optimal response to these security events. We present a principled approach to study and model the human expertise in responding to the emergent threats owing to these security events. A recursive Partial Least Squares based adaptive learning model is defined using a factorial analysis of the security events together with a method for estimating the effect of global context dependent semantic information used by the security administrators. Presented model is theoretically optimal and operationally recursive in nature to deal with the set of security events being generated continuously. We discuss the underlying challenges and ways in which the model could be operationalized in centralized versus decentralized, and real-time versus batch processing modes.
Social Centrality using Network Hierarchy and Community Structure
Venue: arXiv cs.SI 2018
Year: 2018

Several centrality measures have been formulated to quantify the notion of 'importance' of actors in social networks. Current measures scrutinize either local or global connectivity of the nodes and have been found to be inadequate for social networks. Ignoring hierarchy and community structure, which are inherent in all human social networks, is the primary cause of this inadequacy. Positional hierarchy and embeddedness of an actor in the community are intuitively crucial determinants of his importance. The theory of social capital asserts that an actor's importance is derived from his position in network hierarchy as well as from the potential to mobilize resources through intra-community (bonding) and inter-community (bridging) ties. Inspired by this idea, we propose a novel centrality measure SC (Social Centrality) for actors in social networks. Our measure accounts for - i) an individual's propensity to socialize, and ii) his connections within and outside the community. These two factors are suitably aggregated to produce social centrality score. Comparative analysis of SC measure with classical and recent centrality measures using large public networks shows that it consistently produces a more realistic ranking of nodes. The inference is based on the available ground truth for each tested networks. Extensive analysis of rankings delivered by SC measure and mapping with known facts in well-studied networks justifies its effectiveness in diverse social networks. Scalability evaluation of SC measure justifies its efficacy for real-world large networks.
Evaluation of Momentum Diverse Input Iterative Fast Gradient Sign Method (M-DI2-FGSM) Based Attack Method on MCS 2018 Adversarial Attacks on Black Box Face Recognition System
Venue: arXiv cs.CV 2018
Year: 2018

The convolutional neural network is the crucial tool for the recent success of deep learning based methods on various computer vision tasks like classification, segmentation, and detection. Convolutional neural networks achieved state-of-the-art performance in these tasks and every day pushing the limit of computer vision and AI. However, adversarial attack on computer vision systems is threatening their application in the real life and in safety-critical applications. Necessarily, Finding adversarial examples are important to detect susceptible models to attack and take safeguard measures to overcome the adversarial attacks. In this regard, MCS 2018 Adversarial Attacks on Black Box Face Recognition challenge aims to facilitate the research of finding new adversarial attack techniques and their effectiveness in generating adversarial examples. In this challenge, the attack"s nature is targeted-attack on the black-box neural network where we have no knowledge about black-block"s inner structure. The attacker must modify a set of five images of a single person so that the neural network miss-classify them as target image which is a set of five images of another person. In this competition, we applied Momentum Diverse Input Iterative Fast Gradient Sign Method (M-DI2-FGSM) to make an adversarial attack on black-box face recognition system. We tested our method on MCS 2018 Adversarial Attacks on Black Box Face Recognition challenge and found competitive result. Our solution got validation score 1.404 which better than baseline score 1.407 and stood 14 place among 132 teams in the leader-board. Further improvement can be achieved by finding improved feature extraction from source image, carefully chosen hyper-parameters, finding improved substitute model of the black-box and better optimization method.