OpenRaiser/Intern-Atlas huggingface dataset:
Predicting Rankings of Software Verification Competitions
Venue: arXiv cs.LG 2017
Year: 2017

Software verification competitions, such as the annual SV-COMP, evaluate software verification tools with respect to their effectivity and efficiency. Typically, the outcome of a competition is a (possibly category-specific) ranking of the tools. For many applications, such as building portfolio solvers, it would be desirable to have an idea of the (relative) performance of verification tools on a given verification task beforehand, i.e., prior to actually running all tools on the task. In this paper, we present a machine learning approach to predicting rankings of tools on verification tasks. The method builds upon so-called label ranking algorithms, which we complement with appropriate kernels providing a similarity measure for verification tasks. Our kernels employ a graph representation for software source code that mixes elements of control flow and program dependence graphs with abstract syntax trees. Using data sets from SV-COMP, we demonstrate our rank prediction technique to generalize well and achieve a rather high predictive accuracy. In particular, our method outperforms a recently proposed feature-based approach of Demyanova et al. (when applied to rank predictions).
Robust Spatial Filtering with Graph Convolutional Neural Networks
Venue: arXiv cs.CV 2017
Year: 2017

Convolutional Neural Networks (CNNs) have recently led to incredible breakthroughs on a variety of pattern recognition problems. Banks of finite impulse response filters are learned on a hierarchy of layers, each contributing more abstract information than the previous layer. The simplicity and elegance of the convolutional filtering process makes them perfect for structured problems such as image, video, or voice, where vertices are homogeneous in the sense of number, location, and strength of neighbors. The vast majority of classification problems, for example in the pharmaceutical, homeland security, and financial domains are unstructured. As these problems are formulated into unstructured graphs, the heterogeneity of these problems, such as number of vertices, number of connections per vertex, and edge strength, cannot be tackled with standard convolutional techniques. We propose a novel neural learning framework that is capable of handling both homogeneous and heterogeneous data, while retaining the benefits of traditional CNN successes. Recently, researchers have proposed variations of CNNs that can handle graph data. In an effort to create learnable filter banks of graphs, these methods either induce constraints on the data or require preprocessing. As opposed to spectral methods, our framework, which we term Graph-CNNs, defines filters as polynomials of functions of the graph adjacency matrix. Graph-CNNs can handle both heterogeneous and homogeneous graph data, including graphs having entirely different vertex or edge sets. We perform experiments to validate the applicability of Graph-CNNs to a variety of structured and unstructured classification problems and demonstrate state-of-the-art results on document and molecule classification problems.
SLIM: Semi-Lazy Inference Mechanism for Plan Recognition
Venue: arXiv cs.AI 2017
Year: 2017

Plan Recognition algorithms require to recognize a complete hierarchy explaining the agent's actions and goals. While the output of such algorithms is informative to the recognizer, the cost of its calculation is high in run-time, space, and completeness. Moreover, performing plan recognition online requires the observing agent to reason about future actions that have not yet been seen and maintain a set of hypotheses to support all possible options. This paper presents a new and efficient algorithm for online plan recognition called SLIM (Semi-Lazy Inference Mechanism). It combines both a bottom-up and top-down parsing processes, which allow it to commit only to the minimum necessary actions in real-time, but still provide complete hypotheses post factum. We show both theoretically and empirically that although the computational cost of this process is still exponential, there is a significant improvement in run-time when compared to a state of the art of plan recognition algorithm.
An efficient algorithm for finding all possible input nodes for controlling complex networks
Venue: arXiv cs.DM 2017
Year: 2017

Understanding structural controllability of a complex network requires to identify a Minimum Input nodes Set (MIS) of the network. It has been suggested that finding an MIS is equivalent to computing a maximum matching of the network, where the unmatched nodes constitute an MIS. However, maximum matching of a network is often not unique, and finding all MISs may provide deep insights to the controllability of the network. Finding all possible input nodes, which form the union of all MISs, is computationally challenging for large networks. Here we present an efficient enumerative algorithm for the problem. The main idea is to modify a maximum matching algorithm to make it efficient for finding all possible input nodes by computing only one MIS. We rigorously proved the correctness of the new algorithm and evaluated its performance on synthetic and large real networks. The experimental results showed that the new algorithm ran several orders of magnitude faster than the existing method on large real networks.
Workload Analysis of Blue Waters
Venue: arXiv cs.DC 2017
Year: 2017

Blue Waters is a Petascale-level supercomputer whose mission is to enable the national scientific and research community to solve "grand challenge" problems that are orders of magnitude more complex than can be carried out on other high performance computing systems. Given the important and unique role that Blue Waters plays in the U.S. research portfolio, it is important to have a detailed understanding of its workload in order to guide performance optimization both at the software and system configuration level as well as inform architectural balance tradeoffs. Furthermore, understanding the computing requirements of the Blue Water's workload (memory access, IO, communication, etc.), which is comprised of some of the most computationally demanding scientific problems, will help drive changes in future computing architectures, especially at the leading edge. With this objective in mind, the project team carried out a detailed workload analysis of Blue Waters.
Eliciting Private User Information for Residential Demand Response
Venue: arXiv cs.GT 2017
Year: 2017

Residential Demand Response has emerged as a viable tool to alleviate supply and demand imbalances of electricity, particularly during times when the electric grid is strained due a shortage of supply. Demand Response providers bid reduction capacity into the wholesale electricity market by asking their customers under contract to temporarily reduce their consumption in exchange for a monetary incentive. To contribute to the analysis of consumer behavior in response to such incentives, this paper formulates Demand Response as a Mechanism Design problem, where a Demand Response Provider elicits private information of its rational, profit-maximizing customers who derive positive expected utility by participating in reduction events. By designing an incentive compatible and individually rational mechanism to collect users' price elasticities of demand, the Demand Response provider can target the most susceptible users to incentives. We measure reductions by comparing the materialized consumption to the projected consumption, which we model as the "10-in-10"-baseline, the regulatory standard set by the California Independent System Operator. Due to the suboptimal performance of this baseline, we show, using consumption data of residential customers in California, that Demand Response Providers receive payments for "virtual reductions", which exist due to the inaccuracies of the baseline rather than actual reductions. Improving the accuracy of the baseline diminishes the contribution of these virtual reductions.
A Comparative Study of Word Embeddings for Reading Comprehension
Venue: arXiv cs.CL 2017
Year: 2017

The focus of past machine learning research for Reading Comprehension tasks has been primarily on the design of novel deep learning architectures. Here we show that seemingly minor choices made on (1) the use of pre-trained word embeddings, and (2) the representation of out-of-vocabulary tokens at test time, can turn out to have a larger impact than architectural choices on the final performance. We systematically explore several options for these choices, and provide recommendations to researchers working in this area.
Exponential Moving Average Model in Parallel Speech Recognition Training
Venue: arXiv cs.CL 2017
Year: 2017

As training data rapid growth, large-scale parallel training with multi-GPUs cluster is widely applied in the neural network model learning currently.We present a new approach that applies exponential moving average method in large-scale parallel training of neural network model. It is a non-interference strategy that the exponential moving average model is not broadcasted to distributed workers to update their local models after model synchronization in the training process, and it is implemented as the final model of the training system. Fully-connected feed-forward neural networks (DNNs) and deep unidirectional Long short-term memory (LSTM) recurrent neural networks (RNNs) are successfully trained with proposed method for large vocabulary continuous speech recognition on Shenma voice search data in Mandarin. The character error rate (CER) of Mandarin speech recognition further degrades than state-of-the-art approaches of parallel training.
Deconvolving Feedback Loops in Recommender Systems
Venue: arXiv cs.SI 2017
Year: 2017

Collaborative filtering is a popular technique to infer users' preferences on new content based on the collective information of all users preferences. Recommender systems then use this information to make personalized suggestions to users. When users accept these recommendations it creates a feedback loop in the recommender system, and these loops iteratively influence the collaborative filtering algorithm's predictions over time. We investigate whether it is possible to identify items affected by these feedback loops. We state sufficient assumptions to deconvolve the feedback loops while keeping the inverse solution tractable. We furthermore develop a metric to unravel the recommender system's influence on the entire user-item rating matrix. We use this metric on synthetic and real-world datasets to (1) identify the extent to which the recommender system affects the final rating matrix, (2) rank frequently recommended items, and (3) distinguish whether a user's rated item was recommended or an intrinsic preference. Our results indicate that it is possible to recover the ratings matrix of intrinsic user preferences using a single snapshot of the ratings matrix without any temporal information.
On the Presence of Green and Sustainable Software Engineering in Higher Education Curricula
Venue: arXiv cs.SE 2017
Year: 2017

Nowadays, software is pervasive in our everyday lives. Its sustainability and environmental impact have become major factors to be considered in the development of software systems. Millennials-the newer generation of university students-are particularly keen to learn about and contribute to a more sustainable and green society. The need for training on green and sustainable topics in software engineering has been reflected in a number of recent studies. The goal of this paper is to get a first understanding of what is the current state of teaching sustainability in the software engineering community, what are the motivations behind the current state of teaching, and what can be done to improve it. To this end, we report the findings from a targeted survey of 33 academics on the presence of green and sustainable software engineering in higher education. The major findings from the collected data suggest that sustainability is under-represented in the curricula, while the current focus of teaching is on energy efficiency delivered through a fact-based approach. The reasons vary from lack of awareness, teaching material and suitable technologies, to the high effort required to teach sustainability. Finally, we provide recommendations for educators willing to teach sustainability in software engineering that can help to suit millennial students needs.
Employing Spectral Domain Features for Efficient Collaborative Filtering
Venue: arXiv cs.IR 2017
Year: 2017

Collaborative filtering (CF) is a powerful recommender system that generates a list of recommended items for an active user based on the ratings of similar users. This paper presents a novel approach to CF by first finding the set of users similar to the active user by adopting self-organizing maps (SOM), followed by k-means clustering. Then, the ratings for each item in the cluster closest to the active user are mapped to the frequency domain using the Discrete Fourier Transform (DFT). The power spectra of the mapped ratings are generated, and a new similarity measure based on the coherence of these power spectra is calculated. The proposed similarity measure is more time efficient than current state-of-the-art measures. Moreover, it can capture the global similarity between the profiles of users. Experimental results show that the proposed approach overcomes the major problems in existing CF algorithms as follows: First, it mitigates the scalability problem by creating clusters of similar users and applying the time-efficient similarity measure. Second, its frequency-based similarity measure is less sensitive to sparsity problems because the DFT performs efficiently even with sparse data. Third, it outperforms standard similarity measures in terms of accuracy.
On Parameterized Complexity of Group Activity Selection Problems on Social Networks
Venue: arXiv cs.GT 2017
Year: 2017

In Group Activity Selection Problem (GASP), players form coalitions to participate in activities and have preferences over pairs of the form (activity, group size). Recently, Igarashi et al. have initiated the study of group activity selection problems on social networks (gGASP): a group of players can engage in the same activity if the members of the group form a connected subset of the underlying communication structure. Igarashi et al. have primarily focused on Nash stable outcomes, and showed that many associated algorithmic questions are computationally hard even for very simple networks. In this paper we study the parameterized complexity of gGASP with respect to the number of activities as well as with respect to the number of players, for several solution concepts such as Nash stability, individual stability and core stability. The first parameter we consider in the number of activities. For this parameter, we propose an FPT algorithm for Nash stability for the case where the social network is acyclic and obtain a W[1]-hardness result for cliques (i.e., for classic GASP); similar results hold for individual stability. In contrast, finding a core stable outcome is hard even if the number of activities is bounded by a small constant, both for classic GASP and when the social network is a star. Another parameter we study is the number of players. While all solution concepts we consider become polynomial-time computable when this parameter is bounded by a constant, we prove W[1]-hardness results for cliques (i.e., for classic GASP).
First-Order Logic with Counting: At Least, Weak Hanf Normal Forms Always Exist and Can Be Computed!
Venue: arXiv cs.LO 2017
Year: 2017

We introduce the logic FOCN(P) which extends first-order logic by counting and by numerical predicates from a set P, and which can be viewed as a natural generalisation of various counting logics that have been studied in the literature. We obtain a locality result showing that every FOCN(P)-formula can be transformed into a formula in Hanf normal form that is equivalent on all finite structures of degree at most d. A formula is in Hanf normal form if it is a Boolean combination of formulas describing the neighbourhood around its tuple of free variables and arithmetic sentences with predicates from P over atomic statements describing the number of realisations of a type with a single centre. The transformation into Hanf normal form can be achieved in time elementary in $d$ and the size of the input formula. From this locality result, we infer the following applications: (*) The Hanf-locality rank of first-order formulas of bounded quantifier alternation depth only grows polynomially with the formula size. (*) The model checking problem for the fragment FOC(P) of FOCN(P) on structures of bounded degree is fixed-parameter tractable (with elementary parameter dependence). (*) The query evaluation problem for fixed queries from FOC(P) over fully dynamic databases of degree at most d can be solved efficiently: there is a dynamic algorithm that can enumerate the tuples in the query result with constant delay, and that allows to compute the size of the query result and to test if a given tuple belongs to the query result within constant time after every database update.
Symmetric Laplacians, Quantum Density Matrices and their Von-Neumann Entropy
Venue: arXiv cs.IT 2017
Year: 2017

We show that the (normalized) symmetric Laplacian of a simple graph can be obtained from the partial trace over a pure bipartite quantum state that resides in a bipartite Hilbert space (one part corresponding to the vertices, the other corresponding to the edges). This suggests an interpretation of the symmetric Laplacian's Von Neumann entropy as a measure of bipartite entanglement present between the two parts of the state. We then study extreme values for a connected graph's generalized Rényi-$p$ entropy. Specifically, we show that (1) the complete graph achieves maximum entropy, (2) the $2$-regular graph: a) achieves minimum Rényi-$2$ entropy among all $k$-regular graphs, b) is within $\log 4/3$ of the minimum Rényi-$2$ entropy and $\log4\sqrt{2}/3$ of the minimum Von Neumann entropy among all connected graphs, c) achieves a Von Neumann entropy less than the star graph. Point $(2)$ contrasts sharply with similar work applied to (normalized) combinatorial Laplacians, where it has been shown that the star graph almost always achieves minimum Von Neumann entropy. In this work we find that the star graph achieves maximum entropy in the limit as the number of vertices grows without bound. Keywords: Symmetric; Laplacian; Quantum; Entropy; Bounds; Rényi.
Augmented Reality for Depth Cues in Monocular Minimally Invasive Surgery
Venue: arXiv cs.CV 2017
Year: 2017

One of the major challenges in Minimally Invasive Surgery (MIS) such as laparoscopy is the lack of depth perception. In recent years, laparoscopic scene tracking and surface reconstruction has been a focus of investigation to provide rich additional information to aid the surgical process and compensate for the depth perception issue. However, robust 3D surface reconstruction and augmented reality with depth perception on the reconstructed scene are yet to be reported. This paper presents our work in this area. First, we adopt a state-of-the-art visual simultaneous localization and mapping (SLAM) framework - ORB-SLAM - and extend the algorithm for use in MIS scenes for reliable endoscopic camera tracking and salient point mapping. We then develop a robust global 3D surface reconstruction frame- work based on the sparse point clouds extracted from the SLAM framework. Our approach is to combine an outlier removal filter within a Moving Least Squares smoothing algorithm and then employ Poisson surface reconstruction to obtain smooth surfaces from the unstructured sparse point cloud. Our proposed method has been quantitatively evaluated compared with ground-truth camera trajectories and the organ model surface we used to render the synthetic simulation videos. In vivo laparoscopic videos used in the tests have demonstrated the robustness and accuracy of our proposed framework on both camera tracking and surface reconstruction, illustrating the potential of our algorithm for depth augmentation and depth-corrected augmented reality in MIS with monocular endoscopes.
Downlink Cellular Network Analysis with LOS/NLOS Propagation and Elevated Base Stations
Venue: arXiv cs.IT 2017
Year: 2017

In this paper, we investigate the downlink performance of dense cellular networks with elevated base stations (BSs) using a channel model that incorporates line-of-sight (LOS)/non-line-of-sight (NLOS) propagation in both small-scale and large-scale fading. Modeling LOS fading with Nakagami-$m$ fading, we provide a unified framework based on stochastic geometry that encompasses both closest and strongest BS association. Our study is particularized to two distance-dependent LOS/NLOS models of practical interest. Considering the effect of LOS propagation alone, we derive closed-form expressions for the coverage probability with Nakagami-$m$ fading, showing that the performance for strongest BS association is the same as in the case of Rayleigh fading, whereas for closest BS association it monotonically increases with the shape parameter $m$. Then, focusing on the effect of elevated BSs, we show that network densification eventually leads to near-universal outage even for moderately low BS densities: in particular, the maximum area spectral efficiency is proportional to the inverse of the squared BS height.
A Layered Architecture for Erasure-Coded Consistent Distributed Storage
Venue: arXiv cs.DC 2017
Year: 2017

Motivated by emerging applications to the edge computing paradigm, we introduce a two-layer erasure-coded fault-tolerant distributed storage system offering atomic access for read and write operations. In edge computing, clients interact with an edge-layer of servers that is geographically near; the edge-layer in turn interacts with a back-end layer of servers. The edge-layer provides low latency access and temporary storage for client operations, and uses the back-end layer for persistent storage. Our algorithm, termed Layered Data Storage (LDS) algorithm, offers several features suitable for edge-computing systems, works under asynchronous message-passing environments, supports multiple readers and writers, and can tolerate $f_1 < n_1/2$ and $f_2 < n_2/3$ crash failures in the two layers having $n_1$ and $n_2$ servers, respectively. We use a class of erasure codes known as regenerating codes for storage of data in the back-end layer. The choice of regenerating codes, instead of popular choices like Reed-Solomon codes, not only optimizes the cost of back-end storage, but also helps in optimizing communication cost of read operations, when the value needs to be recreated all the way from the back-end. The two-layer architecture permits a modular implementation of atomicity and erasure-code protocols; the implementation of erasure-codes is mostly limited to interaction between the two layers. We prove liveness and atomicity of LDS, and also compute performance costs associated with read and write operations. Further, in a multi-object system running $N$ independent instances of LDS, where only a small fraction of the objects undergo concurrent accesses at any point during the execution, the overall storage cost is dominated by that of persistent storage in the back-end layer, and is given by $Θ(N)$.