OpenRaiser/Intern-Atlas huggingface dataset:
Zero-shot object prediction using semantic scene knowledge
Venue: arXiv cs.CV 2016
Year: 2016

This work focuses on the semantic relations between scenes and objects for visual object recognition. Semantic knowledge can be a powerful source of information especially in scenarios with few or no annotated training samples. These scenarios are referred to as zero-shot or few-shot recognition and often build on visual attributes. Here, instead of relying on various visual attributes, a more direct way is pursued: after recognizing the scene that is depicted in an image, semantic relations between scenes and objects are used for predicting the presence of objects in an unsupervised manner. Most importantly, relations between scenes and objects can easily be obtained from external sources such as large scale text corpora from the web and, therefore, do not require tremendous manual labeling efforts. It will be shown that in cluttered scenes, where visual recognition is difficult, scene knowledge is an important cue for predicting objects.
Lifting QBF Resolution Calculi to DQBF
Venue: arXiv cs.LO 2016
Year: 2016

We examine the existing Resolution systems for quantified Boolean formulas (QBF) and answer the question which of these calculi can be lifted to the more powerful Dependency QBFs (DQBF). An interesting picture emerges: While for QBF we have the strict chain of proof systems Q-Resolution < IR-calc < IRM-calc, the situation is quite different in DQBF. Q-Resolution and likewise universal Resolution are too weak: they are not complete. IR-calc has the right strength: it is sound and complete. IRM-calc is too strong: it is not sound any more, and the same applies to long-distance Resolution. Conceptually, we use the relation of DQBF to EPR and explain our new DQBF calculus based on IR-calc as a subsystem of FO-Resolution.
Balanced model order reduction for systems depending on a parameter
Venue: arXiv cs.SY 2016
Year: 2016

We provide an analytical framework for balanced realization model order reduction of linear control systems which depend on an unknown parameter. Besides recovering known results for the first order corrections, we obtain explicit novel expressions for the form of second order corrections for singular values and singular vectors. The final result of our procedure is an order reduced model which incorporates the uncertain parameter. We apply our algorithm to the model order reduction of a linear system of masses and springs with parameter dependent coefficients.
Consistent Map-based 3D Localization on Mobile Devices
Venue: arXiv cs.RO 2016
Year: 2016

The objective of this paper is to provide consistent, real-time 3D localization capabilities to mobile devices navigating within previously mapped areas. To this end, we introduce the Cholesky-Schmidt-Kalman filter (C-SKF), which explicitly considers the uncertainty of the prior map, by employing the sparse Cholesky factor of the map's Hessian, instead of its dense covariance--as is the case for the Schmidt-Kalman filter (SKF). By doing so, the C-SKF has memory requirements typically linear in the size of the map, as opposed to quadratic for storing the map's covariance. Moreover, and in order to bound the processing needs of the C-SKF (between linear and quadratic in the size of the map), we introduce a relaxation of the C-SKF algorithm, the sC-SKF, which operates on the Cholesky factors of independent sub-maps resulting from dividing the trajectory and observations used for constructing the map into overlapping segments. Lastly, we assess the processing and memory requirements of the proposed C-SKF and sC-SKF algorithms, and compare their positioning accuracy against other approximate map-based localization approaches that employ measurement-noise-covariance inflation to compensate for the map's uncertainty.
Accent Classification with Phonetic Vowel Representation
Venue: arXiv cs.SD 2016
Year: 2016

Previous accent classification research focused mainly on detecting accents with pure acoustic information without recognizing accented speech. This work combines phonetic knowledge such as vowels with acoustic information to build Guassian Mixture Model (GMM) classifier with Perceptual Linear Predictive (PLP) features, optimized by Hetroscedastic Linear Discriminant Analysis (HLDA). With input about 20-second accented speech, this system achieves classification rate of 51% on a 7-way classification system focusing on the major types of accents in English, which is competitive to the state-of-the-art results in this field.
Amodal Instance Segmentation
Venue: arXiv cs.CV 2016
Year: 2016

We consider the problem of amodal instance segmentation, the objective of which is to predict the region encompassing both visible and occluded parts of each object. Thus far, the lack of publicly available amodal segmentation annotations has stymied the development of amodal segmentation methods. In this paper, we sidestep this issue by relying solely on standard modal instance segmentation annotations to train our model. The result is a new method for amodal instance segmentation, which represents the first such method to the best of our knowledge. We demonstrate the proposed method's effectiveness both qualitatively and quantitatively.
Index Modulation Techniques for 5G Wireless Networks
Venue: arXiv cs.IT 2016
Year: 2016

The increasing demand for higher data rates, better quality of service, fully mobile and connected wireless networks lead the researchers to seek new solutions beyond 4G wireless systems. It is anticipated that 5G wireless networks, which are expected to be introduced around 2020, will achieve ten times higher spectral and energy efficiency than current 4G wireless networks and will support data rates up to 10 Gbps for low mobility users. The ambitious goals set for 5G wireless networks require dramatic changes in the design of different layers for next generation communications systems. Massive multiple-input multiple-output (MIMO) systems, filter bank multi-carrier (FBMC) modulation, relaying technologies, and millimeter-wave communications have been considered as some of the strong candidates for the physical layer design of 5G networks. In this article, we shed light on the potential and implementation of index modulation (IM) techniques for MIMO and multi-carrier communications systems which are expected to be two of the key technologies for 5G systems. Specifically, we focus on two promising applications of IM: spatial modulation (SM) and orthogonal frequency division multiplexing with IM (OFDM-IM), and we discuss the recent advances and future research directions in IM technologies towards spectral and energy-efficient 5G wireless networks.
Semantic Reasoning for Context-aware Internet of Things Applications
Venue: arXiv cs.AI 2016
Year: 2016

Advances in ICT are bringing into reality the vision of a large number of uniquely identifiable, interconnected objects and things that gather information from diverse physical environments and deliver the information to a variety of innovative applications and services. These sensing objects and things form the Internet of Things (IoT) that can improve energy and cost efficiency and automation in many different industry fields such as transportation and logistics, health care and manufacturing, and facilitate our everyday lives as well. IoT applications rely on real-time context data and allow sending information for driving the behaviors of users in intelligent environments.
Convolutional Neural Networks For Automatic State-Time Feature Extraction in Reinforcement Learning Applied to Residential Load Control
Venue: arXiv cs.LG 2016
Year: 2016

Direct load control of a heterogeneous cluster of residential demand flexibility sources is a high-dimensional control problem with partial observability. This work proposes a novel approach that uses a convolutional neural network to extract hidden state-time features to mitigate the curse of partial observability. More specific, a convolutional neural network is used as a function approximator to estimate the state-action value function or Q-function in the supervised learning step of fitted Q-iteration. The approach is evaluated in a qualitative simulation, comprising a cluster of thermostatically controlled loads that only share their air temperature, whilst their envelope temperature remains hidden. The simulation results show that the presented approach is able to capture the underlying hidden features and successfully reduce the electricity cost the cluster.
Polynomial-time kernel reductions
Venue: arXiv cs.CC 2016
Year: 2016

In the framework of computational complexity and in an effort to define a more natural reduction for problems of equivalence, we investigate the recently introduced kernel reduction, a reduction that operates on each element of a pair independently. This paper details the limitations and uses of kernel reductions. We show that kernel reductions are weaker than many-one reductions and provide conditions under which complete problems exist. Ultimately, the number and size of equivalence classes can dictate the existence of a kernel reduction. We leave unsolved the unconditional existence of a complete problem under polynomial-time kernel reductions for the standard complexity classes.
Stringer: Balancing Latency and Resource Usage in Service Function Chain Provisioning
Venue: arXiv cs.NI 2016
Year: 2016

Network Functions Virtualization, or NFV, enables telecommunications infrastructure providers to replace special-purpose networking equipment with commodity servers running virtualized network functions (VNFs). A service provider utilizing NFV technology faces the SFC provisioning problem of assigning VNF instances to nodes in the physical infrastructure (e.g., a datacenter), and routing Service Function Chains (sequences of functions required by customers, a.k.a. SFCs) in the physical network. In doing so, the provider must balance between various competing goals of performance and resource usage. We present an approach for SFC provisioning, consisting of three elements. The first element is a fast, scalable round-robin heuristic. The second element is a Mixed Integer Programming (MIP) based approach. The third element is a queueing-theoretic model to estimate the average latency associated with any SFC provisioning solution. Combined, these elements create an approach that generates a set of SFC provisioning solutions, reflecting different tradeoffs between resource usage and performance.
Hilbert Exclusion: Improved Metric Search through Finite Isometric Embeddings
Venue: arXiv cs.IR 2016
Year: 2016

Most research into similarity search in metric spaces relies upon the triangle inequality property. This property allows the space to be arranged according to relative distances to avoid searching some subspaces. We show that many common metric spaces, notably including those using Euclidean and Jensen-Shannon distances, also have a stronger property, sometimes called the four-point property: in essence, these spaces allow an isometric embedding of any four points in three-dimensional Euclidean space, as well as any three points in two-dimensional Euclidean space. In fact, we show that any space which is isometrically embeddable in Hilbert space has the stronger property. This property gives stronger geometric guarantees, and one in particular, which we name the Hilbert Exclusion property, allows any indexing mechanism which uses hyperplane partitioning to perform better. One outcome of this observation is that a number of state-of-the-art indexing mechanisms over high dimensional spaces can be easily extended to give a significant increase in performance; furthermore, the improvement given is greater in higher dimensions. This therefore leads to a significant improvement in the cost of metric search in these spaces.
Crowd Counting via Weighted VLAD on Dense Attribute Feature Maps
Venue: arXiv cs.CV 2016
Year: 2016

Crowd counting is an important task in computer vision, which has many applications in video surveillance. Although the regression-based framework has achieved great improvements for crowd counting, how to improve the discriminative power of image representation is still an open problem. Conventional holistic features used in crowd counting often fail to capture semantic attributes and spatial cues of the image. In this paper, we propose integrating semantic information into learning locality-aware feature sets for accurate crowd counting. First, with the help of convolutional neural network (CNN), the original pixel space is mapped onto a dense attribute feature map, where each dimension of the pixel-wise feature indicates the probabilistic strength of a certain semantic class. Then, locality-aware features (LAF) built on the idea of spatial pyramids on neighboring patches are proposed to explore more spatial context and local information. Finally, the traditional VLAD encoding method is extended to a more generalized form in which diverse coefficient weights are taken into consideration. Experimental results validate the effectiveness of our presented method.
LMS Moodle: Distance international education in cooperation of higher education institutions of different countries
Venue: arXiv cs.CY 2016
Year: 2016

The development of international cooperation requires cooperation in the sphere of education. An enhanced sharing of experience in the sphere of practical teaching activities implies the increase of the quality of teaching process and of scientific cooperation. Sharing of experience in educational activities implies understanding among representatives of different nations anywhere in the world. It means that through LSM teaching the principle of social constructivism is realized, when participants together create a narrow culture of common objects and senses. The article presents an example of practical application of electronic media to the process of a real lesson. The article describes the process of teaching students from different countries using the system of LMS MOODLE, beginning with preparing study materials, giving lectures by foreign lecturers, practical tasks and ending with passing an examination. Training has included some full-time students from the Slovak Republic, the Republic of Dagestan and the Republic of Kazakhstan, and has been realized by applying the method of distance learning (LMS).
System Level Performance Evaluation of LTE-V2X Network
Venue: arXiv cs.NI 2016
Year: 2016

Vehicles are among the fastest growing type of connected devices. Therefore, there is a need for Vehicle-to-Everything (V2X) communication i.e. passing of information from a Vehicle-to-Vehicle (V2V) or Vehicle-to-Infrastructure (V2I) and vice versa. In this paper, the main focus is on the communication between vehicles and road side units (RSUs) commonly referred to as V2I communication in a multi-lane freeway scenario. Moreover, we analyze network related bottlenecks such as the maximum number of vehicles that can be supported when coverage is provided by the Long Term Evolution Advanced (LTE-A) network. The performance evaluation is assessed through extensive system-level simulations. Results show that new resource allocation and interference mitigation techniques are needed in order to achieve the required high reliability requirements, especially when network load is high.
Verifying Buchberger's Algorithm in Reduction Rings
Venue: arXiv cs.SC 2016
Year: 2016

In this paper we present the formal, computer-supported verification of a functional implementation of Buchberger's critical-pair/completion algorithm for computing Gröbner bases in reduction rings. We describe how the algorithm can be implemented and verified within one single software system, which in our case is the Theorema system. In contrast to existing formal correctness proofs of Buchberger's algorithm in other systems, e. g. Coq and ACL2, our work is not confined to the classical setting of polynomial rings over fields, but considers the much more general setting of reduction rings; this, naturally, makes the algorithm more complicated and the verification more difficult. The correctness proof is essentially based on some non-trivial results from the theory of reduction rings, which we formalized and formally proved as well. This formalization already consists of more than 800 interactively proved lemmas and theorems, making the elaboration an extensive example of higher-order theory exploration in Theorema.
Deriving approximation tolerance constraints from verification runs
Venue: arXiv cs.SE 2016
Year: 2016

Approximate computing (AC) is an emerging paradigm for energy-efficient computation. The basic idea of AC is to sacrifice high precision for low energy by allowing for hardware which only carries out "approximately correct" calculations. For software verification, this challenges the validity of verification results for programs run on approximate hardware. In this paper, we present a novel approach to examine program correctness in the context of approximate computing. In contrast to all existing approaches, we start with a standard program verification and compute the allowed tolerances for AC hardware from that verification run. More precisely, we derive a set of constraints which - when met by the AC hardware - guarantees the verification result to carry over to AC. Our approach is based on the framework of abstract interpretation. On the practical side, we furthermore (1) show how to extract tolerance constraints from verification runs employing predicate abstraction as an instance of abstract interpretation, and (2) show how to check such constraints on hardware designs. We exemplify our technique on example C programs and a number of recently proposed approximate adders.
Improved IKE Key Exchange Protocol Combined with Computer Security USB Key Device
Venue: arXiv cs.CR 2016
Year: 2016

: In this paper we suggest improved IKE key exchange protocol combined with the Computer Security USB Key device to solve the problems in using IKE and IKE v2 protocol.
Computational Higher Type Theory I: Abstract Cubical Realizability
Venue: arXiv cs.LO 2016
Year: 2016

Brouwer's constructivist foundations of mathematics is based on an intuitively meaningful notion of computation shared by all mathematicians. Martin-Löf's meaning explanations for constructive type theory define the concept of a type in terms of computation. Briefly, a type is a complete (closed) program that evaluates to a canonical type whose members are complete programs that evaluate to canonical elements of that type. The explanation is extended to incomplete (open) programs by functionality: types and elements must respect equality in their free variables. Equality is evidence-free---two types or elements are at most equal---and equal things are implicitly interchangeable in all contexts. Higher-dimensional type theory extends type theory to account for identifications of types and elements. An identification witnesses that two types or elements are explicitly interchangeable in all contexts by an explicit transport, or coercion, operation. There must be sufficiently many identifications, which is ensured by imposing a generalized form of the Kan condition from homotopy theory. Here we provide a Martin-Löf-style meaning explanation of simple higher-dimensional type theory based on a programming language that includes Kan-like constructs witnessing the computational meaning of the higher structure of types. The treatment includes an example of a higher inductive type (namely, the 1-dimensional sphere) and an example of Voevodsky's univalence principle, which identifies equivalent types. The main result is a computational canonicity theorem that validates the computational interpretation: a closed boolean expression must always evaluate to a boolean value, even in the presence of higher-dimensional structure. This provides the first fully computational formulation of higher-dimensional type theory.
Stack and register complexity of radix conversions
Venue: arXiv cs.FL 2016
Year: 2016

We investigate the question of computational resources (such as stacks and counters) necessary to perform radix conversions. To this end it is shown that no PDA can compute the significand of the best $n$-digit floating point approximation of a power of an incommensurable radix. This extends the results of W.~Clinger. We also prove that a two counter machine with input is capable of such conversions. On the other hand we note a curious asymmetry with respect to the order in which the digits are input by showing that a two counter machine can decode its input online if the digits are presented in the most-to-least significant order while no such machine can decode its input in this manner if the digits are presented in the least-to-most significant order. Some structural results about two counter machines (with input) are also established.
Higher Order Recurrent Neural Networks
Venue: arXiv cs.NE 2016
Year: 2016

In this paper, we study novel neural network structures to better model long term dependency in sequential data. We propose to use more memory units to keep track of more preceding states in recurrent neural networks (RNNs), which are all recurrently fed to the hidden layers as feedback through different weighted paths. By extending the popular recurrent structure in RNNs, we provide the models with better short-term memory mechanism to learn long term dependency in sequences. Analogous to digital filters in signal processing, we call these structures as higher order RNNs (HORNNs). Similar to RNNs, HORNNs can also be learned using the back-propagation through time method. HORNNs are generally applicable to a variety of sequence modelling tasks. In this work, we have examined HORNNs for the language modeling task using two popular data sets, namely the Penn Treebank (PTB) and English text8 data sets. Experimental results have shown that the proposed HORNNs yield the state-of-the-art performance on both data sets, significantly outperforming the regular RNNs as well as the popular LSTMs.
An Improved System for Sentence-level Novelty Detection in Textual Streams
Venue: arXiv cs.IR 2016
Year: 2016

Novelty detection in news events has long been a difficult problem. A number of models performed well on specific data streams but certain issues are far from being solved, particularly in large data streams from the WWW where unpredictability of new terms requires adaptation in the vector space model. We present a novel event detection system based on the Incremental Term Frequency-Inverse Document Frequency (TF-IDF) weighting incorporated with Locality Sensitive Hashing (LSH). Our system could efficiently and effectively adapt to the changes within the data streams of any new terms with continual updates to the vector space model. Regarding miss probability, our proposed novelty detection framework outperforms a recognised baseline system by approximately 16% when evaluating a benchmark dataset from Google News.