OpenRaiser/Intern-Atlas huggingface dataset:
Sequences of Rewrites: A Categorical Interpretation
Venue: arXiv cs.LO 2015
Year: 2015

In Martin-Löf's Intensional Type Theory, identity type is a heavily used and studied concept. The reason for that is the fact that it's responsible for the recently discovered connection between Type Theory and Homotopy Theory. The main problem with identity types, as originally formulated, is that they are complex to understand and use. Using that fact as motivation, a much simpler formulation for the identity type was proposed by Queiroz & Gabbay (1994) and further developed by de Queiroz & de Oliveira (2013). In this formulation, an element of an identity type is seen as a sequence of rewrites (or computational paths). Together with the logical rules of this new entity, there exists a system of reduction rules between sequence of rewrites called LND_{EQS}-RWS. This system is constructed using the labelled natural deduction (i.e. Prawitz' Natural Deduction plus derivations-as-terms) and is responsible for establishing how a sequence of rewrites can be rewritten, resulting in a new sequence of rewrites. In this context, we propose a categorical interpretation for this new entity, using the types as objects and the rules of rewrites as morphisms. Moreover, we show that our interpretation is in accordance with some known results, like that types have a groupoidal structure. We also interpret more complicated structures, like the one formed by a rewrite of a sequence of rewrites.
An Intuitionistic Set-theoretical Model of the Extended Calculus of Constructions
Venue: arXiv cs.LO 2015
Year: 2015

Werner's set-theoretical model is one of the most intuitive models of ECC. It combines a functional view of predicative universes with a collapsed view of the impredicative sort Prop. However this model of Prop is so coarse that the principle of excluded middle holds. In this paper, we interpret Prop into a topological space (a special case of Heyting algebra) to make it more intuitionistic without sacrificing simplicity. We prove soundness and show some applications of our model.
Rethinking serializable multiversion concurrency control
Venue: arXiv cs.DB 2015
Year: 2015

Multi-versioned database systems have the potential to significantly increase the amount of concurrency in transaction processing because they can avoid read-write conflicts. Unfortunately, the increase in concurrency usually comes at the cost of transaction serializability. If a database user requests full serializability, modern multi-versioned systems significantly constrain read-write concurrency among conflicting transactions and employ expensive synchronization patterns in their design. In main-memory multi-core settings, these additional constraints are so burdensome that multi-versioned systems are often significantly outperformed by single-version systems. We propose Bohm, a new concurrency control protocol for main-memory multi-versioned database systems. Bohm guarantees serializable execution while ensuring that reads never block writes. In addition, Bohm does not require reads to perform any book-keeping whatsoever, thereby avoiding the overhead of tracking reads via contended writes to shared memory. This leads to excellent scalability and performance in multi-core settings. Bohm has all the above characteristics without performing validation based concurrency control. Instead, it is pessimistic, and is therefore not prone to excessive aborts in the presence of contention. An experimental evaluation shows that Bohm performs well in both high contention and low contention settings, and is able to dramatically outperform state-of-the-art multi-versioned systems despite maintaining the full set of serializability guarantees.
MLitB: Machine Learning in the Browser
Venue: arXiv cs.DC 2015
Year: 2015

With few exceptions, the field of Machine Learning (ML) research has largely ignored the browser as a computational engine. Beyond an educational resource for ML, the browser has vast potential to not only improve the state-of-the-art in ML research, but also, inexpensively and on a massive scale, to bring sophisticated ML learning and prediction to the public at large. This paper introduces MLitB, a prototype ML framework written entirely in JavaScript, capable of performing large-scale distributed computing with heterogeneous classes of devices. The development of MLitB has been driven by several underlying objectives whose aim is to make ML learning and usage ubiquitous (by using ubiquitous compute devices), cheap and effortlessly distributed, and collaborative. This is achieved by allowing every internet capable device to run training algorithms and predictive models with no software installation and by saving models in universally readable formats. Our prototype library is capable of training deep neural networks with synchronized, distributed stochastic gradient descent. MLitB offers several important opportunities for novel ML research, including: development of distributed learning algorithms, advancement of web GPU algorithms, novel field and mobile applications, privacy preserving computing, and green grid-computing. MLitB is available as open source software.
Interference Mitigation In Wireless Mesh Networks Through Radio Co-location Aware Conflict Graphs
Venue: arXiv cs.NI 2015
Year: 2015

Wireless Mesh Networks (WMNs) have evolved into a wireless communication technology of immense interest. But technological advancements in WMNs have inadvertently spawned a plethora of network performance bottlenecks, caused primarily by the rise in prevalent interference. Conflict Graphs are indispensable tools used to theoretically represent and estimate the interference in wireless networks. We propose a generic algorithm to generate conflict graphs which is independent of the underlying interference model. Further, we propose the notion of radio co-location interference, which is caused and experienced by spatially co-located radios in multi-radio multi-channel (MRMC) WMNs. We experimentally validate the concept, and propose a new all-encompassing algorithm to create a radio co-location aware conflict graph. Our novel conflict graph generation algorithm is demonstrated to be significantly superior and more efficient than the conventional approach, through theoretical interference estimates and comprehensive experiments. The results of an extensive set of ns-3 simulations run on the IEEE 802.11g platform strongly indicate that the radio co-location aware conflict graphs are a marked improvement over their conventional counterparts. We also question the use of total interference degree as a reliable metric to predict the performance of a Channel Assignment scheme in a given WMN deployment.
Generalization of Clustering Agreements and Distances for Overlapping Clusters and Network Communities
Venue: arXiv cs.SI 2015
Year: 2015

A measure of distance between two clusterings has important applications, including clustering validation and ensemble clustering. Generally, such distance measure provides navigation through the space of possible clusterings. Mostly used in cluster validation, a normalized clustering distance, a.k.a. agreement measure, compares a given clustering result against the ground-truth clustering. Clustering agreement measures are often classified into two families of pair-counting and information theoretic measures, with the widely-used representatives of Adjusted Rand Index (ARI) and Normalized Mutual Information (NMI), respectively. This paper sheds light on the relation between these two families through a generalization. It further presents an alternative algebraic formulation for these agreement measures which incorporates an intuitive clustering distance, which is defined based on the analogous between cluster overlaps and co-memberships of nodes in clusters. Unlike the original measures, it is easily extendable for different cases, including overlapping clusters and clusters of inter-related data for complex networks. These two extensions are, in particular, important in the context of finding clusters in social and information networks, a.k.a communities.
A multi-protocol framework for the development of collaborative virtual environments
Venue: arXiv cs.SE 2015
Year: 2015

Collaborative virtual environments (CVEs) are used for collaboration and interaction of possibly many participants that may be spread over large distances. Both commercial and freely available CVEs exist today. Currently, CVEs are used already in a variety of different fields: gaming, business, education, social communication, and cooperative development. In this paper, a general framework is proposed for the development of a cooperative environment which is able to exploit a multi protocol network infrastructure. The framework offers support to concerns such as communication security and inter-protocol interoperability and let software engineers to focus on the specific business of the CVE under development. To show the framework effectiveness we consider, as a case of study, the design of a reusable software layer for the development of distributed card games built on top of it. This layer is, in turn, used for the implementation of a specific card game.
Numeric certified algorithm for the topology of resultant and discriminant curves
Venue: arXiv cs.CG 2015
Year: 2015

Let $\mathcal C$ be a real plane algebraic curve defined by the resultant of two polynomials (resp. by the discriminant of a polynomial). Geometrically such a curve is the projection of the intersection of the surfaces $P(x,y,z)=Q(x,y,z)=0$ (resp. $P(x,y,z)=\frac{\partial P}{\partial z}(x,y,z)=0$), and generically its singularities are nodes (resp. nodes and ordinary cusps). State-of-the-art numerical algorithms compute the topology of smooth curves but usually fail to certify the topology of singular ones. The main challenge is to find practical numerical criteria that guarantee the existence and the uniqueness of a singularity inside a given box $B$, while ensuring that $B$ does not contain any closed loop of $\mathcal{C}$. We solve this problem by first providing a square deflation system, based on subresultants, that can be used to certify numerically whether $B$ contains a unique singularity $p$ or not. Then we introduce a numeric adaptive separation criterion based on interval arithmetic to ensure that the topology of $\mathcal C$ in $B$ is homeomorphic to the local topology at $p$. Our algorithms are implemented and experiments show their efficiency compared to state-of-the-art symbolic or homotopic methods.
On DDoS Attack Related Minimum Cut Problems
Venue: arXiv cs.CC 2015
Year: 2015

In this paper, we study two important extensions of the classical minimum cut problem, called {\em Connectivity Preserving Minimum Cut (CPMC)} problem and {\em Threshold Minimum Cut (TMC)} problem, which have important applications in large-scale DDoS attacks. In CPMC problem, a minimum cut is sought to separate a of source from a destination node and meanwhile preserve the connectivity between the source and its partner node(s). The CPMC problem also has important applications in many other areas such as emergency responding, image processing, pattern recognition, and medical sciences. In TMC problem, a minimum cut is sought to isolate a target node from a threshold number of partner nodes. TMC problem is an important special case of network inhibition problem and has important applications in network security. We show that the general CPMC problem cannot be approximated within $logn$ unless $NP=P$ has quasi-polynomial algorithms. We also show that a special case of two group CPMC problem in planar graphs can be solved in polynomial time. The corollary of this result is that the network diversion problem in planar graphs is in $P$, a previously open problem. We show that the threshold minimum node cut (TMNC) problem can be approximated within ratio $O(\sqrt{n})$ and the threshold minimum edge cut problem (TMEC) can be approximated within ratio $O(\log^2{n})$. \emph{We also answer another long standing open problem: the hardness of the network inhibition problem and network interdiction problem. We show that both of them cannot be approximated within any constant ratio. unless $NP \nsubseteq \cap_{δ>0} BPTIME(2^{n^δ})$.
Teaching Deep Convolutional Neural Networks to Play Go
Venue: arXiv cs.AI 2015
Year: 2015

Mastering the game of Go has remained a long standing challenge to the field of AI. Modern computer Go systems rely on processing millions of possible future positions to play well, but intuitively a stronger and more 'humanlike' way to play the game would be to rely on pattern recognition abilities rather then brute force computation. Following this sentiment, we train deep convolutional neural networks to play Go by training them to predict the moves made by expert Go players. To solve this problem we introduce a number of novel techniques, including a method of tying weights in the network to 'hard code' symmetries that are expect to exist in the target function, and demonstrate in an ablation study they considerably improve performance. Our final networks are able to achieve move prediction accuracies of 41.1% and 44.4% on two different Go datasets, surpassing previous state of the art on this task by significant margins. Additionally, while previous move prediction programs have not yielded strong Go playing programs, we show that the networks trained in this work acquired high levels of skill. Our convolutional neural networks can consistently defeat the well known Go program GNU Go, indicating it is state of the art among programs that do not use Monte Carlo Tree Search. It is also able to win some games against state of the art Go playing program Fuego while using a fraction of the play time. This success at playing Go indicates high level principles of the game were learned.
Multi-Atlas Segmentation of Biomedical Images: A Survey
Venue: arXiv cs.CV 2015
Year: 2015

Multi-atlas segmentation (MAS), first introduced and popularized by the pioneering work of Rohlfing, Brandt, Menzel and Maurer Jr (2004), Klein, Mensh, Ghosh, Tourville and Hirsch (2005), and Heckemann, Hajnal, Aljabar, Rueckert and Hammers (2006), is becoming one of the most widely-used and successful image segmentation techniques in biomedical applications. By manipulating and utilizing the entire dataset of "atlases" (training images that have been previously labeled, e.g., manually by an expert), rather than some model-based average representation, MAS has the flexibility to better capture anatomical variation, thus offering superior segmentation accuracy. This benefit, however, typically comes at a high computational cost. Recent advancements in computer hardware and image processing software have been instrumental in addressing this challenge and facilitated the wide adoption of MAS. Today, MAS has come a long way and the approach includes a wide array of sophisticated algorithms that employ ideas from machine learning, probabilistic modeling, optimization, and computer vision, among other fields. This paper presents a survey of published MAS algorithms and studies that have applied these methods to various biomedical problems. In writing this survey, we have three distinct aims. Our primary goal is to document how MAS was originally conceived, later evolved, and now relates to alternative methods. Second, this paper is intended to be a detailed reference of past research activity in MAS, which now spans over a decade (2003 - 2014) and entails novel methodological developments and application-specific solutions. Finally, our goal is to also present a perspective on the future of MAS, which, we believe, will be one of the dominant approaches in biomedical image segmentation.
Logic programming beyond Prolog
Venue: arXiv cs.PL 2015
Year: 2015

A logic program is an executable specification. For example, merge sort in pure Prolog is a logical formula, yet shows creditable performance on long linked lists. But such executable specifications are a compromise: the logic is distorted by algorithmic considerations, yet only indirectly executable via an abstract machine. This paper introduces relational programming, a method that solves the difficulty with logic programming by a separation of concerns. It requires three texts: (1) the axioms, a logical formula that specifies the problem and is not compromised by algorithmic considerations, (2) the theorem, a logical formula that expresses the idea of the algorithm and follows from the axioms, and (3) the code, a transcription of the theorem to a procedural language. Correctness of the code relies on the logical relationship of the theorem with the axioms and relies on an accurate transcription of the theorem to the procedural language. Sorting is an example where relational programming has the advantage of a higher degree of abstractness: the data to be sorted can be any data type in C++ (the procedural language we use in our examples) that satisfies the axioms of linear order, while the pure-Prolog version is limited to data structures in the form of linked cells. We show another advantage of relational programs: they have a model-theoretic and fixpoint semantics equivalent to each other and analogous to those of pure Prolog programs.
Logic of temporal attribute implications
Venue: arXiv cs.LO 2015
Year: 2015

We study logic for reasoning with if-then formulas describing dependencies between attributes of objects which are observed in consecutive points in time. We introduce semantic entailment of the formulas, show its fixed-point characterization, investigate closure properties of model classes, present an axiomatization and prove its completeness, and investigate alternative axiomatizations and normalized proofs. We investigate decidability and complexity issues of the logic and prove that the entailment problem is NP-hard and belongs to EXPSPACE. We show that by restricting to predictive formulas, the entailment problem is decidable in pseudo-linear time.
Unsupervised Neural Architecture for Saliency Detection: Extended Version
Venue: arXiv cs.CV 2015
Year: 2015

We propose a novel neural network architecture for visual saliency detections, which utilizes neurophysiologically plausible mechanisms for extraction of salient regions. The model has been significantly inspired by recent findings from neurophysiology and aimed to simulate the bottom-up processes of human selective attention. Two types of features were analyzed: color and direction of maximum variance. The mechanism we employ for processing those features is PCA, implemented by means of normalized Hebbian learning and the waves of spikes. To evaluate performance of our model we have conducted psychological experiment. Comparison of simulation results with those of experiment indicates good performance of our model.
Distinguishing cause from effect using observational data: methods and benchmarks
Venue: arXiv cs.LG 2015
Year: 2015

The discovery of causal relationships from purely observational data is a fundamental problem in science. The most elementary form of such a causal discovery problem is to decide whether X causes Y or, alternatively, Y causes X, given joint observations of two variables X, Y. An example is to decide whether altitude causes temperature, or vice versa, given only joint measurements of both variables. Even under the simplifying assumptions of no confounding, no feedback loops, and no selection bias, such bivariate causal discovery problems are challenging. Nevertheless, several approaches for addressing those problems have been proposed in recent years. We review two families of such methods: Additive Noise Methods (ANM) and Information Geometric Causal Inference (IGCI). We present the benchmark CauseEffectPairs that consists of data for 100 different cause-effect pairs selected from 37 datasets from various domains (e.g., meteorology, biology, medicine, engineering, economy, etc.) and motivate our decisions regarding the "ground truth" causal directions of all pairs. We evaluate the performance of several bivariate causal discovery methods on these real-world benchmark data and in addition on artificially simulated data. Our empirical results on real-world data indicate that certain methods are indeed able to distinguish cause from effect using only purely observational data, although more benchmark data would be needed to obtain statistically significant conclusions. One of the best performing methods overall is the additive-noise method originally proposed by Hoyer et al. (2009), which obtains an accuracy of 63+-10 % and an AUC of 0.74+-0.05 on the real-world benchmark. As the main theoretical contribution of this work we prove the consistency of that method.
Delay Games with WMSO+U Winning Conditions
Venue: arXiv cs.GT 2015
Year: 2015

Delay games are two-player games of infinite duration in which one player may delay her moves to obtain a lookahead on her opponent's moves. We consider delay games with winning conditions expressed in weak monadic second order logic with the unbounding quantifier, which is able to express (un)boundedness properties. We show that it is decidable whether the delaying player has a winning strategy using bounded lookahead and give a doubly-exponential upper bound on the necessary lookahead. In contrast, we show that bounded lookahead is not always sufficient to win such a game.
Decoding of Projective Reed-Muller Codes by Dividing a Projective Space into Affine Spaces
Venue: arXiv cs.IT 2015
Year: 2015

A projective Reed-Muller (PRM) code, obtained by modifying a (classical) Reed-Muller code with respect to a projective space, is a doubly extended Reed-Solomon code when the dimension of the related projective space is equal to 1. The minimum distance and dual code of a PRM code are known, and some decoding examples have been represented for low-dimensional projective space. In this study, we construct a decoding algorithm for all PRM codes by dividing a projective space into a union of affine spaces. In addition, we determine the computational complexity and the number of errors correctable of our algorithm. Finally, we compare the codeword error rate of our algorithm with that of minimum distance decoding.
Inexact Alternating Direction Method Based on Newton descent algorithm with Application to Poisson Image Deblurring
Venue: arXiv cs.CV 2015
Year: 2015

The recovery of images from the observations that are degraded by a linear operator and further corrupted by Poisson noise is an important task in modern imaging applications such as astronomical and biomedical ones. Gradient-based regularizers involve the popular total variation semi-norm have become standard techniques for Poisson image restoration due to its edge-preserving ability. Various efficient algorithms have been developed for solving the corresponding minimization problem with non-smooth regularization terms. In this paper, motivated by the idea of the alternating direction minimization algorithm and the Newton's method with upper convergent rate, we further propose inexact alternating direction methods utilizing the proximal Hessian matrix information of the objective function, in a way reminiscent of Newton descent methods. Besides, we also investigate the global convergence of the proposed algorithms under certain conditions. Finally, we illustrate that the proposed algorithms outperform the current state-of-the-art algorithms through numerical experiments on Poisson image deblurring.