OpenRaiser/Intern-Atlas huggingface dataset:
Early MFCC And HPCP Fusion for Robust Cover Song Identification
Venue: arXiv cs.IR 2017
Year: 2017

While most schemes for automatic cover song identification have focused on note-based features such as HPCP and chord profiles, a few recent papers surprisingly showed that local self-similarities of MFCC-based features also have classification power for this task. Since MFCC and HPCP capture complementary information, we design an unsupervised algorithm that combines normalized, beat-synchronous blocks of these features using cross-similarity fusion before attempting to locally align a pair of songs. As an added bonus, our scheme naturally incorporates structural information in each song to fill in alignment gaps where both feature sets fail. We show a striking jump in performance over MFCC and HPCP alone, achieving a state of the art mean reciprocal rank of 0.87 on the Covers80 dataset. We also introduce a new medium-sized hand designed benchmark dataset called "Covers 1000," which consists of 395 cliques of cover songs for a total of 1000 songs, and we show that our algorithm achieves an MRR of 0.9 on this dataset for the first correctly identified song in a clique. We provide the precomputed HPCP and MFCC features, as well as beat intervals, for all songs in the Covers 1000 dataset for use in further research.
Stochastic Spin-Orbit Torque Devices as Elements for Bayesian Inference
Venue: arXiv cs.ET 2017
Year: 2017

Probabilistic inference from real-time input data is becoming increasingly popular and may be one of the potential pathways at enabling cognitive intelligence. As a matter of fact, preliminary research has revealed that stochastic functionalities also underlie the spiking behavior of neurons in cortical microcircuits of the human brain. In tune with such observations, neuromorphic and other unconventional computing platforms have recently started adopting the usage of computational units that generate outputs probabilistically, depending on the magnitude of the input stimulus. In this work, we experimentally demonstrate a spintronic device that offers a direct mapping to the functionality of such a controllable stochastic switching element. We show that the probabilistic switching of Ta/CoFeB/MgO heterostructures in presence of spin-orbit torque and thermal noise can be harnessed to enable probabilistic inference in a plethora of unconventional computing scenarios. This work can potentially pave the way for hardware that directly mimics the computational units of Bayesian inference.
Forensic Investigation of P2P Cloud Storage: BitTorrent Sync as a Case Study
Venue: arXiv cs.CR 2017
Year: 2017

Cloud computing has been regarded as the technology enabler for the Internet of Things (IoT). To ensure the most effective collection of IoT-based evidence, it is vital for forensic practitioners to possess a contemporary understanding of the artefacts from different cloud services. In this paper, we seek to determine the data remnants from the use of BitTorrent Sync version 2.0. Findings from our research using mobile and computer devices running Windows 8.1, Mac OS X Mavericks 10.9.5, Ubuntu 14.04.1 LTS, iOS 7.1.2, and Android KitKat 4.4.4 suggested that artefacts relating to the installation, uninstallation, log-in, log-off, and file synchronisation could be recovered, which are potential sources of IoT forensics. We also present a forensically sound investigation methodology for BitTorrent Sync.
Formalization of the fundamental group in untyped set theory using auto2
Venue: arXiv cs.LO 2017
Year: 2017

We present a new framework for formalizing mathematics in untyped set theory using auto2. Using this framework, we formalize in Isabelle/FOL the entire chain of development from the axioms of set theory to the definition of the fundamental group for an arbitrary topological space. The auto2 prover is used as the sole automation tool, and enables succinct proof scripts throughout the project.
Clustering Algorithms for the Centralized and Local Models
Venue: arXiv cs.DS 2017
Year: 2017

We revisit the problem of finding a minimum enclosing ball with differential privacy: Given a set of $n$ points in the Euclidean space $\mathbb{R}^d$ and an integer $t\leq n$, the goal is to find a ball of the smallest radius $r_{opt}$ enclosing at least $t$ input points. The problem is motivated by its various applications to differential privacy, including the sample and aggregate technique, private data exploration, and clustering. Without privacy concerns, minimum enclosing ball has a polynomial time approximation scheme (PTAS), which computes a ball of radius almost $r_{opt}$ (the problem is NP-hard to solve exactly). In contrast, under differential privacy, until this work, only a $O(\sqrt{\log n})$-approximation algorithm was known. We provide new constructions of differentially private algorithms for minimum enclosing ball achieving constant factor approximation to $r_{opt}$ both in the centralized model (where a trusted curator collects the sensitive information and analyzes it with differential privacy) and in the local model (where each respondent randomizes her answers to the data curator to protect her privacy). We demonstrate how to use our algorithms as a building block for approximating $k$-means in both models.
Open-Set Language Identification
Venue: arXiv cs.CL 2017
Year: 2017

We present the first open-set language identification experiments using one-class classification. We first highlight the shortcomings of traditional feature extraction methods and propose a hashing-based feature vectorization approach as a solution. Using a dataset of 10 languages from different writing systems, we train a One- Class Support Vector Machine using only a monolingual corpus for each language. Each model is evaluated against a test set of data from all 10 languages and we achieve an average F-score of 0.99, highlighting the effectiveness of this approach for open-set language identification.
Geometric Jacobians Derivation and Kinematic Singularity Analysis for Smokie Robot Manipulator & the Barrett WAM
Venue: arXiv cs.RO 2017
Year: 2017

This paper discusses deriving geometric jacobians and identifying and analyzing the kinematic singularities for two 6 DOF arm robots. First we show the direct kinematics and D-H parameters derived for these two arms. The Geometric jacobian is computed for Barrett WAM and Smokie OUR. By analyzing the jacobian matrices we find the configurations at which J is rank deficient and derive the kinematic singularities through jacobian's determinent. Schematic are provided to show the singular configurations of both robots. Finally a survey is done on redundant kinematic allocation schemesfor 7 DoF Barrett WAM.
FML-based Dynamic Assessment Agent for Human-Machine Cooperative System on Game of Go
Venue: arXiv cs.AI 2017
Year: 2017

In this paper, we demonstrate the application of Fuzzy Markup Language (FML) to construct an FML-based Dynamic Assessment Agent (FDAA), and we present an FML-based Human-Machine Cooperative System (FHMCS) for the game of Go. The proposed FDAA comprises an intelligent decision-making and learning mechanism, an intelligent game bot, a proximal development agent, and an intelligent agent. The intelligent game bot is based on the open-source code of Facebook Darkforest, and it features a representational state transfer application programming interface mechanism. The proximal development agent contains a dynamic assessment mechanism, a GoSocket mechanism, and an FML engine with a fuzzy knowledge base and rule base. The intelligent agent contains a GoSocket engine and a summarization agent that is based on the estimated win rate, real-time simulation number, and matching degree of predicted moves. Additionally, the FML for player performance evaluation and linguistic descriptions for game results commentary are presented. We experimentally verify and validate the performance of the FDAA and variants of the FHMCS by testing five games in 2016 and 60 games of Google Master Go, a new version of the AlphaGo program, in January 2017. The experimental results demonstrate that the proposed FDAA can work effectively for Go applications.
Overcoming Catastrophic Interference by Conceptors
Venue: arXiv cs.NE 2017
Year: 2017

Catastrophic interference has been a major roadblock in the research of continual learning. Here we propose a variant of the back-propagation algorithm, "conceptor-aided back-prop" (CAB), in which gradients are shielded by conceptors against degradation of previously learned tasks. Conceptors have their origin in reservoir computing, where they have been previously shown to overcome catastrophic forgetting. CAB extends these results to deep feedforward networks. On the disjoint MNIST task CAB outperforms two other methods for coping with catastrophic interference that have recently been proposed in the deep learning field.
Near Optimal Sized Weight Tolerant Subgraph for Single Source Shortest Path
Venue: arXiv cs.DS 2017
Year: 2017

In this paper we address the problem of computing a sparse subgraph of a weighted directed graph such that the exact distances from a designated source vertex to all other vertices are preserved under bounded weight increment. Finding a small sized subgraph that preserves distances between any pair of vertices is a well studied problem. Since in the real world any network is prone to failures, it is natural to study the fault tolerant version of the above problem. Unfortunately, it turns out that there may not always exist such a sparse subgraph even under single edge failure [Demetrescu \emph{et al.} '08]. However in real applications it is not always the case that a link (edge) in a network becomes completely faulty. Instead, it can happen that some links become more congested which can easily be captured by increasing weight on the corresponding edges. Thus it makes sense to try to construct a sparse distance preserving subgraph under the above weight increment model. To the best of our knowledge this problem has not been studied so far. In this paper we show that given any weighted directed graph with $n$ vertices and a source vertex, one can construct a subgraph that contains at most $e \cdot (k-1)!2^kn$ many edges such that it preserves distances between the source and all other vertices as long as the total weight increment is bounded by $k$ and we are allowed to have only integer valued (can be negative) weight on each edge and also weight of an edge can only be increased by some positive integer. Next we show a lower bound of $c\cdot 2^kn$, for some constant $c \ge 5/4$, on the size of the subgraph. We also argue that restriction of integer valued weight and integer valued weight increment are actually essential by showing that if we remove any one of these two restrictions we may need to store $Ω(n^2)$ edges to preserve distances.
Further Formalization of the Process Algebra CCS in HOL4
Venue: arXiv cs.LO 2017
Year: 2017

In this project, we have extended previous work on the formalization of the process algebra CCS in HOL4. We have added full supports on weak bisimulation equivalence and observation congruence (rooted weak equivalence), with related definitions, theorems and algebraic laws. Some deep lemmas were also formally proved in this project, including Deng Lemma, Hennessy Lemma and several versions of the "Coarsest congruence contained in weak equivalence". For the last theorem, we have proved the full version (without any assumption) based on ordinals.
Coalition formation for Multi-agent Pursuit based on Neural Network and AGRMF Model
Venue: arXiv cs.AI 2017
Year: 2017

An approach for coalition formation of multi-agent pursuit based on neural network and AGRMF model is proposed.This paper constructs a novel neural work called AGRMF-ANN which consists of feature extraction part and group generation part. On one hand,The convolutional layers of feature extraction part can abstract the features of agent group role membership function(AGRMF) for all of the groups,on the other hand,those features will be fed to the group generation part based on self-organizing map(SOM) layer which is used to group the pursuers with similar features in the same group. Besides, we also come up the group attractiveness function(GAF) to evaluate the quality of groups and the pursuers contribution in order to adjust the main ability indicators of AGRMF and other weight of all neural network. The simulation experiment showed that this proposal can improve the effectiveness of coalition formation for multi-agent pursuit and ability to adopt pursuit-evasion problem with the scale of pursuer team growing.
Energy Conservation in Optical Fibers with Distributed Brick-Walls Filters
Venue: arXiv cs.IT 2017
Year: 2017

A band-pass filtering scheme is proposed to mitigate spectral broadening and channel coupling in the Nonlinear Schrödinger (NLS) fiber optic channel. The scheme is modeled by modifying the NLS Equation to include an attenuation profile with multiple brick-wall filters centered at different frequencies. It is shown that this brick-walls profile conserves the total in-band energy of the launch signal. Furthermore, energy fluctuations between the filtered channels are characterized, and conditions on the channel spacings are derived that ensure energy conservation in each channel. The maximum spectral efficiency of such a system is derived, and a constructive rule for achieving it using Sidon sequences is provided.
Economic MPC of Nonlinear Systems with Non-Monotonic Lyapunov Functions and Its Application to HVAC Control
Venue: arXiv cs.SY 2017
Year: 2017

This paper proposes a Lyapunov-based economic MPC scheme for nonlinear sytems with non-monotonic Lyapunov functions. Relaxed Lyapunov-based constraints are used in the MPC formulation to improve the economic performance. These constraints will enforce a Lyapunov decrease after every few steps. Recursive feasibility and asymptotical convergence to the steady state can be achieved using Lyapunov-like stability analysis. The proposed economic MPC can be applied to minimize energy consumption in HVAC control of commercial buildings. The Lyapunov-based constraints in the online MPC problem enable the tracking of the desired set-point temperature. The performance is demonstrated by a virtual building composed of two adjacent zones.
Downgrade Attack on TrustZone
Venue: arXiv cs.CR 2017
Year: 2017

Security-critical tasks require proper isolation from untrusted software. Chip manufacturers design and include trusted execution environments (TEEs) in their processors to secure these tasks. The integrity and security of the software in the trusted environment depend on the verification process of the system. We find a form of attack that can be performed on the current implementations of the widely deployed ARM TrustZone technology. The attack exploits the fact that the trustlet (TA) or TrustZone OS loading verification procedure may use the same verification key and may lack proper rollback prevention across versions. If an exploit works on an out-of-date version, but the vulnerability is patched on the latest version, an attacker can still use the same exploit to compromise the latest system by downgrading the software to an older and exploitable version. We did experiments on popular devices on the market including those from Google, Samsung and Huawei, and found that all of them have the risk of being attacked. Also, we show a real-world example to exploit Qualcomm's QSEE. In addition, in order to find out which device images share the same verification key, pattern matching schemes for different vendors are analyzed and summarized.
Truly Sub-cubic Algorithms for Language Edit Distance and RNA Folding via Fast Bounded-Difference Min-Plus Product
Venue: arXiv cs.DS 2017
Year: 2017

It is a major open problem whether the $(\min,+)$-product of two $n\times n$ matrices has a truly sub-cubic (i.e. $O(n^{3-ε})$ for $ε>0$) time algorithm, in particular since it is equivalent to the famous All-Pairs-Shortest-Paths problem (APSP) in $n$-vertex graphs. Some restrictions of the $(\min,+)$-product to special types of matrices are known to admit truly sub-cubic algorithms, each giving rise to a special case of APSP that can be solved faster. In this paper we consider a new, different and powerful restriction in which all matrix entries are integers and one matrix can be arbitrary, as long as the other matrix has "bounded differences" in either its columns or rows, i.e. any two consecutive entries differ by only a small amount. We obtain the first truly sub-cubic algorithm for this bounded-difference $(\min,+)$-product (answering an open problem of Chan and Lewenstein). Our new algorithm, combined with a strengthening of an approach of L.~Valiant for solving context-free grammar parsing with matrix multiplication, yields the first truly sub-cubic algorithms for the following problems: Language Edit Distance (a major problem in the parsing community), RNA-folding (a major problem in bioinformatics) and Optimum Stack Generation (answering an open problem of Tarjan).
The Power of Constraint Grammars Revisited
Venue: arXiv cs.FL 2017
Year: 2017

Sequential Constraint Grammar (SCG) (Karlsson, 1990) and its extensions have lacked clear connections to formal language theory. The purpose of this article is to lay a foundation for these connections by simplifying the definition of strings processed by the grammar and by showing that Nonmonotonic SCG is undecidable and that derivations similar to the Generative Phonology exist. The current investigations propose resource bounds that restrict the generative power of SCG to a subset of context sensitive languages and present a strong finite-state condition for grammars as wholes. We show that a grammar is equivalent to a finite-state transducer if it is implemented with a Turing machine that runs in o(n log n) time. This condition opens new finite-state hypotheses and avenues for deeper analysis of SCG instances in the way inspired by Finite-State Phonology.
Neural Reranking for Named Entity Recognition
Venue: arXiv cs.CL 2017
Year: 2017

We propose a neural reranking system for named entity recognition (NER). The basic idea is to leverage recurrent neural network models to learn sentence-level patterns that involve named entity mentions. In particular, given an output sentence produced by a baseline NER model, we replace all entity mentions, such as \textit{Barack Obama}, into their entity types, such as \textit{PER}. The resulting sentence patterns contain direct output information, yet is less sparse without specific named entities. For example, "PER was born in LOC" can be such a pattern. LSTM and CNN structures are utilised for learning deep representations of such sentences for reranking. Results show that our system can significantly improve the NER accuracies over two different baselines, giving the best reported results on a standard benchmark.
Detection, Recognition and Tracking of Moving Objects from Real-time Video via Visual Vocabulary Model and Species Inspired PSO
Venue: arXiv cs.CV 2017
Year: 2017

In this paper, we address the basic problem of recognizing moving objects in video images using Visual Vocabulary model and Bag of Words and track our object of interest in the subsequent video frames using species inspired PSO. Initially, the shadow free images are obtained by background modelling followed by foreground modeling to extract the blobs of our object of interest. Subsequently, we train a cubic SVM with human body datasets in accordance with our domain of interest for recognition and tracking. During training, using the principle of Bag of Words we extract necessary features of certain domains and objects for classification. Subsequently, matching these feature sets with those of the extracted object blobs that are obtained by subtracting the shadow free background from the foreground, we detect successfully our object of interest from the test domain. The performance of the classification by cubic SVM is satisfactorily represented by confusion matrix and ROC curve reflecting the accuracy of each module. After classification, our object of interest is tracked in the test domain using species inspired PSO. By combining the adaptive learning tools with the efficient classification of description, we achieve optimum accuracy in recognition of the moving objects. We evaluate our algorithm benchmark datasets: iLIDS, VIVID, Walking2, Woman. Comparative analysis of our algorithm against the existing state-of-the-art trackers shows very satisfactory and competitive results.
Object Tracking based on Quantum Particle Swarm Optimization
Venue: arXiv cs.CV 2017
Year: 2017

In Computer Vision domain, moving Object Tracking considered as one of the toughest problem.As there so many factors associated like illumination of light, noise, occlusion, sudden start and stop of moving object, shading which makes tracking even harder problem not only for dynamic background but also for static background.In this paper we present a new object tracking algorithm based on Dominant points on tracked object using Quantum particle swarm optimization (QPSO) which is a new different version of PSO based on Quantum theory. The novelty in our approach is that it can be successfully applicable in variable background as well as static background and application of quantum PSO makes the algorithm runs lot faster where other basic PSO algorithm failed to do so due to heavy computation.In our approach firstly dominants points of tracked objects detected, then a group of particles form a swarm are initialized randomly over the image search space and then start searching the curvature connected between two consecutive dominant points until they satisfy fitness criteria. Obviously it is a Multi-Swarm approach as there are multiple dominant points, as they moves, the curvature moves and the curvature movement is tracked by the swarm throughout the video and eventually when the swarm reaches optimal solution , a bounding box drawn based on particles final position.Experimental results demonstrate this proposed QPSO based method work efficiently and effectively in visual object tracking in both dynamic and static environments and run time shows that it runs closely 90% faster than basic PSO.in our approach we also apply parallelism using MatLab Parfor command to show how very less number of iteration and swarm size will enable us to successfully track object.