OpenRaiser/Intern-Atlas huggingface dataset:
The Power of Quantum Fourier Sampling
Venue: arXiv cs.CC 2015
Year: 2015

A line of work initiated by Terhal and DiVincenzo and Bremner, Jozsa, and Shepherd, shows that quantum computers can efficiently sample from probability distributions that cannot be exactly sampled efficiently on a classical computer, unless the PH collapses. Aaronson and Arkhipov take this further by considering a distribution that can be sampled efficiently by linear optical quantum computation, that under two feasible conjectures, cannot even be approximately sampled classically within bounded total variation distance, unless the PH collapses. In this work we use Quantum Fourier Sampling to construct a class of distributions that can be sampled by a quantum computer. We then argue that these distributions cannot be approximately sampled classically, unless the PH collapses, under variants of the Aaronson and Arkhipov conjectures. In particular, we show a general class of quantumly sampleable distributions each of which is based on an "Efficiently Specifiable" polynomial, for which a classical approximate sampler implies an average-case approximation. This class of polynomials contains the Permanent but also includes, for example, the Hamiltonian Cycle polynomial, and many other familiar #P-hard polynomials. Although our construction, unlike that proposed by Aaronson and Arkhipov, likely requires a universal quantum computer, we are able to use this additional power to weaken the conjectures needed to prove approximate sampling hardness results.
An Efficient Solver for Sparse Linear Systems Based on Rank-Structured Cholesky Factorization
Venue: arXiv cs.NA 2015
Year: 2015

Direct factorization methods for the solution of large, sparse linear systems that arise from PDE discretizations are robust, but typically show poor time and memory scalability for large systems. In this paper, we describe an efficient sparse, rank-structured Cholesky algorithm for solution of the positive definite linear system $A x = b$ when $A$ comes from a discretized partial-differential equation. Our approach combines the efficient memory access patterns of conventional supernodal Cholesky algorithms with the memory efficiency of rank-structured direct solvers. For several test problems arising from PDE discretizations, our method takes less memory than standard sparse Cholesky solvers and less wall-clock time than standard preconditioned iterations.
Marimba: A Tool for Verifying Properties of Hidden Markov Models
Venue: arXiv cs.LO 2015
Year: 2015

The formal verification of properties of Hidden Markov Models (HMMs) is highly desirable for gaining confidence in the correctness of the model and the corresponding system. A significant step towards HMM verification was the development by Zhang et al. of a family of logics for verifying HMMs, called POCTL*, and its model checking algorithm. As far as we know, the verification tool we present here is the first one based on Zhang et al.'s approach. As an example of its effective application, we verify properties of a handover task in the context of human-robot interaction. Our tool was implemented in Haskell, and the experimental evaluation was performed using the humanoid robot Bert2.
Building a Large-scale Multimodal Knowledge Base System for Answering Visual Queries
Venue: arXiv cs.CV 2015
Year: 2015

The complexity of the visual world creates significant challenges for comprehensive visual understanding. In spite of recent successes in visual recognition, today's vision systems would still struggle to deal with visual queries that require a deeper reasoning. We propose a knowledge base (KB) framework to handle an assortment of visual queries, without the need to train new classifiers for new tasks. Building such a large-scale multimodal KB presents a major challenge of scalability. We cast a large-scale MRF into a KB representation, incorporating visual, textual and structured data, as well as their diverse relations. We introduce a scalable knowledge base construction system that is capable of building a KB with half billion variables and millions of parameters in a few hours. Our system achieves competitive results compared to purpose-built models on standard recognition and retrieval tasks, while exhibiting greater flexibility in answering richer visual queries.
Rapid Co-optimization of Processing and Circuit Design to Overcome Carbon Nanotube Variations
Venue: arXiv cs.ET 2015
Year: 2015

Carbon nanotube field-effect transistors (CNFETs) are promising candidates for building energy-efficient digital systems at highly-scaled technology nodes. However, carbon nanotubes (CNTs) are inherently subject to variations that reduce circuit yield, increase susceptibility to noise, and severely degrade their anticipated energy and speed benefits. Joint exploration and optimization of CNT processing options and CNFET circuit design are required to overcome this outstanding challenge. Unfortunately, existing approaches for such exploration and optimization are computationally expensive, and mostly rely on trial-and-error-based ad hoc techniques. In this paper, we present a framework that quickly evaluates the impact of CNT variations on circuit delay and noise margin, and systematically explores the large space of CNT processing options to derive optimized CNT processing and CNFET circuit design guidelines. We demonstrate that our framework: 1) runs over 100x faster than existing approaches, and 2) accurately identifies the most important CNT processing parameters, together with CNFET circuit design parameters (e.g., for CNFET sizing and standard cell layouts), to minimize the impact of CNT variations on CNFET circuit speed with less than 5% energy cost, while simultaneously meeting circuit-level noise margin and yield constraints.
Structural Analysis of Criminal Network and Predicting Hidden Links using Machine Learning
Venue: arXiv cs.SI 2015
Year: 2015

Analysis of criminal networks is inherently difficult because of the nature of the topic. Criminal networks are covert and most of the information is not publicly available. This leads to small datasets available for analysis. The available criminal network datasets consists of entities, i.e. individual or organizations, which are linked to each other. The links between entities indicates that there is a connection between these entities such as involvement in the same criminal event, having commercial ties, and/or memberships in the same criminal organization. Because of incognito criminal activities, there could be many hidden links from entities to entities, which makes the publicly available criminal networks incomplete. Revealing hidden links introduces new information, e.g. affiliation of a suspected individual with a criminal organization, which may not be known with public information. What will we be able to find if we can run analysis on a larger dataset and use link prediction to reveal the implicit connections? We plan to answer this question by using a dataset that is an order of magnitude more than what is used in most criminal networks analysis. And by using machine learning techniques, we will convert a link prediction problem to a binary classification problem. We plan to reveal hidden links and potentially hidden key attributes of the criminal network. With a more complete picture of the network, we can potentially use this data to thwart criminal organizations and/or take a Pareto approach in targeting key nodes. We conclude our analysis with an effective destruction strategy to weaken criminal networks and prove the effectiveness of revealing hidden links when attacking to criminal networks.
Horn Clauses as an Intermediate Representation for Program Analysis and Transformation
Venue: arXiv cs.PL 2015
Year: 2015

Many recent analyses for conventional imperative programs begin by transforming programs into logic programs, capitalising on existing LP analyses and simple LP semantics. We propose using logic programs as an intermediate program representation throughout the compilation process. With restrictions ensuring determinism and single-modedness, a logic program can easily be transformed to machine language or other low-level language, while maintaining the simple semantics that makes it suitable as a language for program analysis and transformation. We present a simple LP language that enforces determinism and single-modedness, and show that it makes a convenient program representation for analysis and transformation.
Promises and Challenges of Ambient Assisted Living Systems
Venue: arXiv cs.CY 2015
Year: 2015

The population of elderly people keeps increasing rapidly, which becomes a predominant aspect of our societies. As such, solutions both efficacious and cost-effective need to be sought. Ambient Assisted Living (AAL) is a new approach which promises to address the needs from elderly people. Ambient Intelligence technologies are widely developed in this domain aiming to construct safe environments around assisted peoples and help them maintain independent living. However, there are still many fundamental issues in AAL that remain open. Most of the current efforts still do not fully express the power of human being, and the importance of social connections and social activities is less noticed. Our conjecture is that such features are fundamental prerequisites towards truly effective AAL services. This paper reviews the current status of researches on AAL, discusses the promises and possible advantages of AAL, and also indicates the challenges we must meet in order to develop practical and efficient AAL systems for elderly people. In this paper, we also propose an approach to construct effective home-care system for the elderly people.
Proving Correctness of Imperative Programs by Linearizing Constrained Horn Clauses
Venue: arXiv cs.LO 2015
Year: 2015

We present a method for verifying the correctness of imperative programs which is based on the automated transformation of their specifications. Given a program prog, we consider a partial correctness specification of the form $\{φ\}$ prog $\{ψ\}$, where the assertions $φ$ and $ψ$ are predicates defined by a set Spec of possibly recursive Horn clauses with linear arithmetic (LA) constraints in their premise (also called constrained Horn clauses). The verification method consists in constructing a set PC of constrained Horn clauses whose satisfiability implies that $\{φ\}$ prog $\{ψ\}$ is valid. We highlight some limitations of state-of-the-art constrained Horn clause solving methods, here called LA-solving methods, which prove the satisfiability of the clauses by looking for linear arithmetic interpretations of the predicates. In particular, we prove that there exist some specifications that cannot be proved valid by any of those LA-solving methods. These specifications require the proof of satisfiability of a set PC of constrained Horn clauses that contain nonlinear clauses (that is, clauses with more than one atom in their premise). Then, we present a transformation, called linearization, that converts PC into a set of linear clauses (that is, clauses with at most one atom in their premise). We show that several specifications that could not be proved valid by LA-solving methods, can be proved valid after linearization. We also present a strategy for performing linearization in an automatic way and we report on some experimental results obtained by using a preliminary implementation of our method.
On Structural Parameterizations of Hitting Set: Hitting Paths in Graphs Using 2-SAT
Venue: arXiv cs.DS 2015
Year: 2015

Hitting Set is a classic problem in combinatorial optimization. Its input consists of a set system F over a finite universe U and an integer t; the question is whether there is a set of t elements that intersects every set in F. The Hitting Set problem parameterized by the size of the solution is a well-known W[2]-complete problem in parameterized complexity theory. In this paper we investigate the complexity of Hitting Set under various structural parameterizations of the input. Our starting point is the folklore result that Hitting Set is polynomial-time solvable if there is a tree T on vertex set U such that the sets in F induce connected subtrees of T. We consider the case that there is a treelike graph with vertex set U such that the sets in F induce connected subgraphs; the parameter of the problem is a measure of how treelike the graph is. Our main positive result is an algorithm that, given a graph G with cyclomatic number k, a collection P of simple paths in G, and an integer t, determines in time 2^{5k} (|G| +|P|)^O(1) whether there is a vertex set of size t that hits all paths in P. It is based on a connection to the 2-SAT problem in multiple valued logic. For other parameterizations we derive W[1]-hardness and para-NP-completeness results.
The Budget-Constrained Functional Dependency
Venue: arXiv cs.LO 2015
Year: 2015

Armstrong's axioms of functional dependency form a well-known logical system that captures properties of functional dependencies between sets of database attributes. This article assumes that there are costs associated with attributes and proposes an extension of Armstrong's system for reasoning about budget-constrained functional dependencies in such a setting. The main technical result of this article is the completeness theorem for the proposed logical system. Although the proposed axioms are obtained by just adding cost subscript to the original Armstrong's axioms, the proof of the completeness for the proposed system is significantly more complicated than that for the Armstrong's system.
Incorporating Belief Function in SVM for Phoneme Recognition
Venue: arXiv cs.CL 2015
Year: 2015

The Support Vector Machine (SVM) method has been widely used in numerous classification tasks. The main idea of this algorithm is based on the principle of the margin maximization to find an hyperplane which separates the data into two different classes.In this paper, SVM is applied to phoneme recognition task. However, in many real-world problems, each phoneme in the data set for recognition problems may differ in the degree of significance due to noise, inaccuracies, or abnormal characteristics; All those problems can lead to the inaccuracies in the prediction phase. Unfortunately, the standard formulation of SVM does not take into account all those problems and, in particular, the variation in the speech input. This paper presents a new formulation of SVM (B-SVM) that attributes to each phoneme a confidence degree computed based on its geometric position in the space. Then, this degree is used in order to strengthen the class membership of the tested phoneme. Hence, we introduce a reformulation of the standard SVM that incorporates the degree of belief. Experimental performance on TIMIT database shows the effectiveness of the proposed method B-SVM on a phoneme recognition problem.
Parameterized lower bound and NP-completeness of some $H$-free Edge Deletion problems
Venue: arXiv cs.DS 2015
Year: 2015

For a graph $H$, the $H$-free Edge Deletion problem asks whether there exist at most $k$ edges whose deletion from the input graph $G$ results in a graph without any induced copy of $H$. We prove that $H$-free Edge Deletion is NP-complete if $H$ is a graph with at least two edges and $H$ has a component with maximum number of vertices which is a tree or a regular graph. Furthermore, we obtain that these NP-complete problems cannot be solved in parameterized subexponential time, i.e., in time $2^{o(k)}\cdot |G|^{O(1)}$, unless Exponential Time Hypothesis fails.
Deep Fishing: Gradient Features from Deep Nets
Venue: arXiv cs.CV 2015
Year: 2015

Convolutional Networks (ConvNets) have recently improved image recognition performance thanks to end-to-end learning of deep feed-forward models from raw pixels. Deep learning is a marked departure from the previous state of the art, the Fisher Vector (FV), which relied on gradient-based encoding of local hand-crafted features. In this paper, we discuss a novel connection between these two approaches. First, we show that one can derive gradient representations from ConvNets in a similar fashion to the FV. Second, we show that this gradient representation actually corresponds to a structured matrix that allows for efficient similarity computation. We experimentally study the benefits of transferring this representation over the outputs of ConvNet layers, and find consistent improvements on the Pascal VOC 2007 and 2012 datasets.
Algorithmization, requirements analysis and architectural challenges of TraConDa
Venue: arXiv cs.NI 2015
Year: 2015

Globally, there are so much information security threats on Internet that even when data is encrypted, there is no guarantee that copy would not be available to third-party, and eventually be decrypted. Thus, trusted routing mechanism that inhibits availability of (encrypted or not) data being transferred to third-party is proposed in this paper. Algorithmization, requirements analysis and architectural challenges for its development are presented.
Alexandria: Extensible Framework for Rapid Exploration of Social Media
Venue: arXiv cs.IR 2015
Year: 2015

The Alexandria system under development at IBM Research provides an extensible framework and platform for supporting a variety of big-data analytics and visualizations. The system is currently focused on enabling rapid exploration of text-based social media data. The system provides tools to help with constructing "domain models" (i.e., families of keywords and extractors to enable focus on tweets and other social media documents relevant to a project), to rapidly extract and segment the relevant social media and its authors, to apply further analytics (such as finding trends and anomalous terms), and visualizing the results. The system architecture is centered around a variety of REST-based service APIs to enable flexible orchestration of the system capabilities; these are especially useful to support knowledge-worker driven iterative exploration of social phenomena. The architecture also enables rapid integration of Alexandria capabilities with other social media analytics system, as has been demonstrated through an integration with IBM Research's SystemG. This paper describes a prototypical usage scenario for Alexandria, along with the architecture and key underlying analytics.
2001-2013: Survey and Analysis of Major Cyberattacks
Venue: arXiv cs.CY 2015
Year: 2015

Widespread and extensive use of computers and their interconnections in almost all sectors like communications, finance, transportation, military, governance, education, energy etc., have made them attractive targets for adversaries to spy, disrupt or steal information by pressing of few keystrokes from any part of the world. This paper presents a survey of major cyberattacks from 2001 to 2013 and analyzes these attacks to understand the motivation, targets and technique(s) employed by the attackers. Observed trends in cyberattacks have also been discussed in the paper.
The Anatomy of Large-Scale Distributed Graph Algorithms
Venue: arXiv cs.DC 2015
Year: 2015

The increasing complexity of the software/hardware stack of modern supercomputers results in explosion of parameters. The performance analysis becomes a truly experimental science, even more challenging in the presence of massive irregularity and data dependency. We analyze how the existing body of research handles the experimental aspect in the context of distributed graph algorithms (DGAs). We distinguish algorithm-level contributions, often prioritized by authors, from runtime-level concerns that are harder to place. We show that the runtime is such an integral part of DGAs that experimental results are difficult to interpret and extrapolate without understanding the properties of the runtime used. We argue that in order to gain understanding about the impact of runtimes, more information needs to be gathered. To begin this process, we provide an initial set of recommendations for describing DGA results based on our analysis of the current state of the field.
Probabilistic Self-Stabilization
Venue: arXiv cs.DC 2015
Year: 2015

By using concrete scenarios, we present and discuss a new concept of probabilistic Self-Stabilization in Distributed Systems.
D-DEMOS: A distributed, end-to-end verifiable, internet voting system
Venue: arXiv cs.CR 2015
Year: 2015

E-voting systems have emerged as a powerful technology for improving democracy by reducing election cost, increasing voter participation, and even allowing voters to directly verify the entire election procedure. Prior internet voting systems have single points of failure, which may result in the compromise of availability, voter secrecy, or integrity of the election results. In this paper, we present the design, implementation, security analysis, and evaluation of D-DEMOS, a complete e-voting system that is distributed, privacy-preserving and end-to-end verifiable. Our system includes a fully asynchronous vote collection subsystem that provides immediate assurance to the voter her vote was recorded as cast, without requiring cryptographic operations on behalf of the voter. We also include a distributed, replicated and fault-tolerant Bulletin Board component, that stores all necessary election-related information, and allows any party to read and verify the complete election process. Finally, we also incorporate trustees, i.e., individuals who control election result production while guaranteeing privacy and end-to-end-verifiability as long as their strong majority is honest. Our system is the first e-voting system whose voting operation is human verifiable, i.e., a voter can vote over the web, even when her web client stack is potentially unsafe, without sacrificing her privacy, and still be assured her vote was recorded as cast. Additionally, a voter can outsource election auditing to third parties, still without sacrificing privacy. Finally, as the number of auditors increases, the probability of election fraud going undetected is diminished exponentially. We provide a model and security analysis of the system. We implement a prototype of the complete system, we measure its performance experimentally, and we demonstrate its ability to handle large-scale elections.
Organizational Chart Inference
Venue: arXiv cs.SI 2015
Year: 2015

Nowadays, to facilitate the communication and cooperation among employees, a new family of online social networks has been adopted in many companies, which are called the "enterprise social networks" (ESNs). ESNs can provide employees with various professional services to help them deal with daily work issues. Meanwhile, employees in companies are usually organized into different hierarchies according to the relative ranks of their positions. The company internal management structure can be outlined with the organizational chart visually, which is normally confidential to the public out of the privacy and security concerns. In this paper, we want to study the IOC (Inference of Organizational Chart) problem to identify company internal organizational chart based on the heterogeneous online ESN launched in it. IOC is very challenging to address as, to guarantee smooth operations, the internal organizational charts of companies need to meet certain structural requirements (about its depth and width). To solve the IOC problem, a novel unsupervised method Create (ChArT REcovEr) is proposed in this paper, which consists of 3 steps: (1) social stratification of ESN users into different social classes, (2) supervision link inference from managers to subordinates, and (3) consecutive social classes matching to prune the redundant supervision links. Extensive experiments conducted on real-world online ESN dataset demonstrate that Create can perform very well in addressing the IOC problem.