OpenRaiser/Intern-Atlas huggingface dataset:
Two-Dimensional Pattern-Coupled Sparse Bayesian Learning via Generalized Approximate Message Passing
Venue: arXiv cs.IT 2015
Year: 2015

We consider the problem of recovering two-dimensional (2-D) block-sparse signals with \emph{unknown} cluster patterns. Two-dimensional block-sparse patterns arise naturally in many practical applications such as foreground detection and inverse synthetic aperture radar imaging. To exploit the block-sparse structure, we introduce a 2-D pattern-coupled hierarchical Gaussian prior model to characterize the statistical pattern dependencies among neighboring coefficients. Unlike the conventional hierarchical Gaussian prior model where each coefficient is associated independently with a unique hyperparameter, the pattern-coupled prior for each coefficient not only involves its own hyperparameter, but also its immediate neighboring hyperparameters. Thus the sparsity patterns of neighboring coefficients are related to each other and the hierarchical model has the potential to encourage 2-D structured-sparse solutions. An expectation-maximization (EM) strategy is employed to obtain the maximum a posterior (MAP) estimate of the hyperparameters, along with the posterior distribution of the sparse signal. In addition, the generalized approximate message passing (GAMP) algorithm is embedded into the EM framework to efficiently compute an approximation of the posterior distribution of hidden variables, which results in a significant reduction in computational complexity. Numerical results are provided to illustrate the effectiveness of the proposed algorithm.
Tracking Human Mobility using WiFi signals
Venue: arXiv cs.CY 2015
Year: 2015

We study six months of human mobility data, including WiFi and GPS traces recorded with high temporal resolution, and find that time series of WiFi scans contain a strong latent location signal. In fact, due to inherent stability and low entropy of human mobility, it is possible to assign location to WiFi access points based on a very small number of GPS samples and then use these access points as location beacons. Using just one GPS observation per day per person allows us to estimate the location of, and subsequently use, WiFi access points to account for 80\% of mobility across a population. These results reveal a great opportunity for using ubiquitous WiFi routers for high-resolution outdoor positioning, but also significant privacy implications of such side-channel location tracking.
Multi-beam 4 GHz Microwave Apertures Using Current-Mode DFT Approximation on 65 nm CMOS
Venue: arXiv cs.IT 2015
Year: 2015

A current-mode CMOS design is proposed for realizing receive mode multi-beams in the analog domain using a novel DFT approximation. High-bandwidth CMOS RF transistors are employed in low-voltage current mirrors to achieve bandwidths exceeding 4 GHz with good beam fidelity. Current mirrors realize the coefficients of the considered DFT approximation, which take simple values in $\{0, \pm1, \pm2\}$ only. This allows high bandwidths realizations using simple circuitry without needing phase-shifters or delays. The proposed design is used as a method to efficiently achieve spatial discrete Fourier transform operation across a ULA to obtain multiple simultaneous RF beams. An example using 1.2 V current-mode approximate DFT on 65 nm CMOS, with BSIM4 models from the RF kit, show potential operation up to 4 GHz with eight independent aperture beams.
Category Theory in Coq 8.5
Venue: arXiv cs.LO 2015
Year: 2015

We report on our experience implementing category theory in Coq 8.5. The repository of this development can be found at https://bitbucket.org/amintimany/categories/. This implementation most notably makes use of features, primitive projections for records and universe polymorphism that are new to Coq 8.5.
Asymptotic Error Free Partitioning over Noisy Boolean Multiaccess Channels
Venue: arXiv cs.IT 2015
Year: 2015

In this paper, we consider the problem of partitioning active users in a manner that facilitates multi-access without collision. The setting is of a noisy, synchronous, Boolean, multi-access channel where $K$ active users (out of a total of $N$ users) seek to access. A solution to the partition problem places each of the $N$ users in one of $K$ groups (or blocks) such that no two active nodes are in the same block. We consider a simple, but non-trivial and illustrative case of $K=2$ active users and study the number of steps $T$ used to solve the partition problem. By random coding and a suboptimal decoding scheme, we show that for any $T\geq (C_1 +ξ_1)\log N$, where $C_1$ and $ξ_1$ are positive constants (independent of $N$), and $ξ_1$ can be arbitrary small, the partition problem can be solved with error probability $P_e^{(N)} \to 0$, for large $N$. Under the same scheme, we also bound $T$ from the other direction, establishing that, for any $T \leq (C_2 - ξ_2) \log N$, the error probability $P_e^{(N)} \to 1$ for large $N$; again $C_2$ and $ξ_2$ are constants and $ξ_2$ can be arbitrarily small. These bounds on the number of steps are lower than the tight achievable lower-bound in terms of $T \geq (C_g +ξ)\log N $ for group testing (in which all active users are identified, rather than just partitioned). Thus, partitioning may prove to be a more efficient approach for multi-access than group testing.
A Proof of Correctness for the Tardis Cache Coherence Protocol
Venue: arXiv cs.DC 2015
Year: 2015

We prove the correctness of a recently-proposed cache coherence protocol, Tardis, which is simple, yet scalable to high processor counts, because it only requires O(logN) storage per cacheline for an N-processor system. We prove that Tardis follows the sequential consistency model and is both deadlock- and livelock-free. Our proof is based on simple and intuitive invariants of the system and thus applies to any system scale and many variants of Tardis.
A survey of SMS based Information Systems
Venue: arXiv cs.AI 2015
Year: 2015

Short Message Service (SMS) based Information Systems (SMSbIS) provide an excellent alternative to a traditional approach of obtaining specific information by direct (through phone) or indirect (IVRS, Web, Email) probing. Information and communication technology and far reaching mobile penetration has opened this new research trend Number of key players in Search industry including Microsoft and Google are attracted by the expected increase in volume of use of such applications. The wide range of applications and their public acceptance has motivated researchers to work in this research domain. Several applications such as SMS based information access using database management services, SMS based information retrieval through internet (search engine), SMS based information extraction, question answering, image retrieval etc. have been emerged. With the aim to understand the functionality involved in these systems, an extensive review of a few of these SMSbISs has been planned and executed by us. These systems are classified into four categories based on the objectives and domains of the applications. As a result of this study a well structured functional model is presented here. The model is evaluated in different dimensions, which is presented in this paper. In addition to this a chronological progress with respect to research and development in this upcoming field is compiled in this paper. Such an extensive review presented in this paper would definitely help the researchers and developers to understand the technical aspects of this field. The functional framework presented here would be useful to the system designers to design and develop an SMS based Information System of any specific domain.
Differentially Private Distributed Online Learning
Venue: arXiv cs.LG 2015
Year: 2015

Online learning has been in the spotlight from the machine learning society for a long time. To handle massive data in Big Data era, one single learner could never efficiently finish this heavy task. Hence, in this paper, we propose a novel distributed online learning algorithm to solve the problem. Comparing to typical centralized online learner, the distributed learners optimize their own learning parameters based on local data sources and timely communicate with neighbors. However, communication may lead to a privacy breach. Thus, we use differential privacy to preserve the privacy of learners, and study the influence of guaranteeing differential privacy on the utility of the distributed online learning algorithm. Furthermore, by using the results from Kakade and Tewari (2009), we use the regret bounds of online learning to achieve fast convergence rates for offline learning algorithms in distributed scenarios, which provides tighter utility performance than the existing state-of-the-art results. In simulation, we demonstrate that the differentially private offline learning algorithm has high variance, but we can use mini-batch to improve the performance. Finally, the simulations show that the analytical results of our proposed theorems are right and our private distributed online learning algorithm is a general framework.
New results on inconsistency indices and their relationship with the quality of priority vector estimation
Venue: arXiv cs.AI 2015
Year: 2015

The article is devoted to the problem of inconsistency in the pairwise comparisons based prioritization methodology. The issue of "inconsistency" in this context has gained much attention in recent years. The literature provides us with a number of different "inconsistency" indices suggested for measuring the inconsistency of the pairwise comparison matrix (PCM). The latter is understood as a deviation of the PCM from the "consistent case" - a notion that is formally well-defined in this theory. However the usage of the indices is justified only by some heuristics. It is still unclear what they really "measure". What is even more important and still not known is the relationship between their values and the "consistency" of the decision maker's judgments on one hand, and the prioritization results upon the other. We provide examples showing that it is necessary to distinguish between these three following tasks: the "measuring" of the "PCM inconsistency" and the PCM-based "measuring" of the consistency of decision maker's judgments and, finally, the "measuring" of the usefulness of the PCM as a source of information for estimation of the priority vector (PV). Next we focus on the third task, which seems to be the most important one in Multi-Criteria Decision Making. With the help of Monte Carlo experiments, we study the performance of various inconsistency indices as indicators of the final PV estimation quality. The presented results allow a deeper understanding of the information contained in these indices and help in choosing a proper one in a given situation. They also enable us to develop a new inconsistency characteristic and, based on it, to propose the PCM acceptance approach that is supported by the classical statistical methodology.
Towards Realistic Team Formation in Social Networks based on Densest Subgraphs
Venue: arXiv cs.SI 2015
Year: 2015

Given a task $\mathcal{T}$, a set of experts $V$ with multiple skills and a social network $G(V, W)$ reflecting the compatibility among the experts, team formation is the problem of identifying a team $C \subseteq V$ that is both competent in performing the task $\mathcal{T}$ and compatible in working together. Existing methods for this problem make too restrictive assumptions and thus cannot model practical scenarios. The goal of this paper is to consider the team formation problem in a realistic setting and present a novel formulation based on densest subgraphs. Our formulation allows modeling of many natural requirements such as (i) inclusion of a designated team leader and/or a group of given experts, (ii) restriction of the size or more generally cost of the team (iii) enforcing locality of the team, e.g., in a geographical sense or social sense, etc. The proposed formulation leads to a generalized version of the classical densest subgraph problem with cardinality constraints (DSP), which is an NP hard problem and has many applications in social network analysis. In this paper, we present a new method for (approximately) solving the generalized DSP (GDSP). Our method, FORTE, is based on solving an equivalent continuous relaxation of GDSP. The solution found by our method has a quality guarantee and always satisfies the constraints of GDSP. Experiments show that the proposed formulation (GDSP) is useful in modeling a broader range of team formation problems and that our method produces more coherent and compact teams of high quality. We also show, with the help of an LP relaxation of GDSP, that our method gives close to optimal solutions to GDSP.
VeinPLUS: A Transillumination and Reflection-based Hand Vein Database
Venue: arXiv cs.CV 2015
Year: 2015

This paper gives a short summary of work related to the creation of a department-hosted hand vein database. After the introducing section, special properties of the hand vein acquisition are explained, followed by a comparison table, which shows key differences to existing well-known hand vein databases. At the end, the ROI extraction process is described and sample images and ROIs are presented.
Unauthorized Cross-App Resource Access on MAC OS X and iOS
Venue: arXiv cs.CR 2015
Year: 2015

On modern operating systems, applications under the same user are separated from each other, for the purpose of protecting them against malware and compromised programs. Given the complexity of today's OSes, less clear is whether such isolation is effective against different kind of cross-app resource access attacks (called XARA in our research). To better understand the problem, on the less-studied Apple platforms, we conducted a systematic security analysis on MAC OS~X and iOS. Our research leads to the discovery of a series of high-impact security weaknesses, which enable a sandboxed malicious app, approved by the Apple Stores, to gain unauthorized access to other apps' sensitive data. More specifically, we found that the inter-app interaction services, including the keychain, WebSocket and NSConnection on OS~X and URL Scheme on the MAC OS and iOS, can all be exploited by the malware to steal such confidential information as the passwords for iCloud, email and bank, and the secret token of Evernote. Further, the design of the app sandbox on OS~X was found to be vulnerable, exposing an app's private directory to the sandboxed malware that hijacks its Apple Bundle ID. As a result, sensitive user data, like the notes and user contacts under Evernote and photos under WeChat, have all been disclosed. Fundamentally, these problems are caused by the lack of app-to-app and app-to-OS authentications. To better understand their impacts, we developed a scanner that automatically analyzes the binaries of MAC OS and iOS apps to determine whether proper protection is missing in their code. Running it on hundreds of binaries, we confirmed the pervasiveness of the weaknesses among high-impact Apple apps. Since the issues may not be easily fixed, we built a simple program that detects exploit attempts on OS~X, helping protect vulnerable apps before the problems can be fully addressed.
Detecting Unrealizability of Distributed Fault-tolerant Systems
Venue: arXiv cs.LO 2015
Year: 2015

Writing formal specifications for distributed systems is difficult. Even simple consistency requirements often turn out to be unrealizable because of the complicated information flow in the distributed system: not all information is available in every component, and information transmitted from other components may arrive with a delay or not at all, especially in the presence of faults. The problem of checking the distributed realizability of a temporal specification is, in general, undecidable. Semi-algorithms for synthesis, such as bounded synthesis, are only useful in the positive case, where they construct an implementation for a realizable specification, but not in the negative case: if the specification is unrealizable, the search for the implementation never terminates. In this paper, we introduce counterexamples to distributed realizability and present a method for the detection of such counterexamples for specifications given in linear-time temporal logic (LTL). A counterexample consists of a set of paths, each representing a different sequence of inputs from the environment, such that, no matter how the components are implemented, the specification is violated on at least one of these paths. We present a method for finding such counterexamples both for the classic distributed realizability problem and for the fault-tolerant realizability problem. Our method considers, incrementally, larger and larger sets of paths until a counterexample is found. For safety specifications in weakly ordered architectures we obtain a decision procedure, while counterexamples for full LTL and arbitrary architectures may consist of infinitely many paths. Experimental results, obtained with a QBF-based prototype implementation, show that our method finds simple errors very quickly, and even problems with high combinatorial complexity, like the Byzantine Generals' Problem, are tractable.
On Nested Sequents for Constructive Modal Logics
Venue: arXiv cs.LO 2015
Year: 2015

We present deductive systems for various modal logics that can be obtained from the constructive variant of the normal modal logic CK by adding combinations of the axioms d, t, b, 4, and 5. This includes the constructive variants of the standard modal logics K4, S4, and S5. We use for our presentation the formalism of nested sequents and give a syntactic proof of cut elimination.
Times series averaging from a probabilistic interpretation of time-elastic kernel
Venue: arXiv cs.LG 2015
Year: 2015

At the light of regularized dynamic time warping kernels, this paper reconsider the concept of time elastic centroid (TEC) for a set of time series. From this perspective, we show first how TEC can easily be addressed as a preimage problem. Unfortunately this preimage problem is ill-posed, may suffer from over-fitting especially for long time series and getting a sub-optimal solution involves heavy computational costs. We then derive two new algorithms based on a probabilistic interpretation of kernel alignment matrices that expresses in terms of probabilistic distributions over sets of alignment paths. The first algorithm is an iterative agglomerative heuristics inspired from the state of the art DTW barycenter averaging (DBA) algorithm proposed specifically for the Dynamic Time Warping measure. The second proposed algorithm achieves a classical averaging of the aligned samples but also implements an averaging of the time of occurrences of the aligned samples. It exploits a straightforward progressive agglomerative heuristics. An experimentation that compares for 45 time series datasets classification error rates obtained by first near neighbors classifiers exploiting a single medoid or centroid estimate to represent each categories show that: i) centroids based approaches significantly outperform medoids based approaches, ii) on the considered experience, the two proposed algorithms outperform the state of the art DBA algorithm, and iii) the second proposed algorithm that implements an averaging jointly in the sample space and along the time axes emerges as the most significantly robust time elastic averaging heuristic with an interesting noise reduction capability. Index Terms-Time series averaging Time elastic kernel Dynamic Time Warping Time series clustering and classification.
Fantasy Football Prediction
Venue: arXiv cs.LG 2015
Year: 2015

The ubiquity of professional sports and specifically the NFL have lead to an increase in popularity for Fantasy Football. Users have many tools at their disposal: statistics, predictions, rankings of experts and even recommendations of peers. There are issues with all of these, though. Especially since many people pay money to play, the prediction tools should be enhanced as they provide unbiased and easy-to-use assistance for users. This paper provides and discusses approaches to predict Fantasy Football scores of Quarterbacks with relatively limited data. In addition to that, it includes several suggestions on how the data could be enhanced to achieve better results. The dataset consists only of game data from the last six NFL seasons. I used two different methods to predict the Fantasy Football scores of NFL players: Support Vector Regression (SVR) and Neural Networks. The results of both are promising given the limited data that was used.
Automatic Repair of Real Bugs: An Experience Report on the Defects4J Dataset
Venue: arXiv cs.SE 2015
Year: 2015

Defects4J is a large, peer-reviewed, structured dataset of real-world Java bugs. Each bug in Defects4J is provided with a test suite and at least one failing test case that triggers the bug. In this paper, we report on an experiment to explore the effectiveness of automatic repair on Defects4J. The result of our experiment shows that 47 bugs of the Defects4J dataset can be automatically repaired by state-of- the-art repair. This sets a baseline for future research on automatic repair for Java. We have manually analyzed 84 different patches to assess their real correctness. In total, 9 real Java bugs can be correctly fixed with test-suite based repair. This analysis shows that test-suite based repair suffers from under-specified bugs, for which trivial and incorrect patches still pass the test suite. With respect to practical applicability, it takes in average 14.8 minutes to find a patch. The experiment was done on a scientific grid, totaling 17.6 days of computation time. All their systems and experimental results are publicly available on Github in order to facilitate future research on automatic repair.
A U.S. Research Roadmap for Human Computation
Venue: arXiv cs.HC 2015
Year: 2015

The Web has made it possible to harness human cognition en masse to achieve new capabilities. Some of these successes are well known; for example Wikipedia has become the go-to place for basic information on all things; Duolingo engages millions of people in real-life translation of text, while simultaneously teaching them to speak foreign languages; and fold.it has enabled public-driven scientific discoveries by recasting complex biomedical challenges into popular online puzzle games. These and other early successes hint at the tremendous potential for future crowd-powered capabilities for the benefit of health, education, science, and society. In the process, a new field called Human Computation has emerged to better understand, replicate, and improve upon these successes through scientific research. Human Computation refers to the science that underlies online crowd-powered systems and was the topic of a recent visioning activity in which a representative cross-section of researchers, industry practitioners, visionaries, funding agency representatives, and policy makers came together to understand what makes crowd-powered systems successful. Teams of experts considered past, present, and future human computation systems to explore which kinds of crowd-powered systems have the greatest potential for societal impact and which kinds of research will best enable the efficient development of new crowd-powered systems to achieve this impact. This report summarize the products and findings of those activities as well as the unconventional process and activities employed by the workshop, which were informed by human computation research.
Intelligent escalation and the principle of relativity
Venue: arXiv cs.GT 2015
Year: 2015

Escalation is the fact that in a game (for instance in an auction), the agents play forever. The $0,1$-game is an extremely simple infinite game with intelligent agents in which escalation arises. It shows at the light of research on cognitive psychology the difference between intelligence (algorithmic mind) and rationality (algorithmic and reflective mind) in decision processes. It also shows that depending on the point of view (inside or outside) the rationality of the agent may change which is proposed to be called the principle of relativity.