OpenRaiser/Intern-Atlas huggingface dataset:
A Parameterized Algorithm for Mixed Cut
Venue: arXiv cs.DS 2015
Year: 2015

The classical Menger's theorem states that in any undirected (or directed) graph $G$, given a pair of vertices $s$ and $t$, the maximum number of vertex (edge) disjoint paths is equal to the minimum number of vertices (edges) needed to disconnect from $s$ and $t$. This min-max result can be turned into a polynomial time algorithm to find the maximum number of vertex (edge) disjoint paths as well as the minimum number of vertices (edges) needed to disconnect $s$ from $t$. In this paper we study a mixed version of this problem, called Mixed-Cut, where we are given an undirected graph $G$, vertices $s$ and $t$, positive integers $k$ and $l$ and the objective is to test whether there exist a $k$ sized vertex set $S \subseteq V(G)$ and an $l$ sized edge set $F \subseteq E(G)$ such that deletion of $S$ and $F$ from $G$ disconnects from $s$ and $t$. We start with a small observation that this problem is NP-complete and then study this problem, in fact a much stronger generalization of this, in the realm of parameterized complexity. In particular we study the Mixed-Multiway Cut-Uncut problem where along with a set of terminals $T$, we are also given an equivalence relation $\mathcal{R}$ on $T$, and the question is whether we can delete at most $k$ vertices and at most $l$ edges such that connectivity of the terminals in the resulting graph respects $\mathcal{R}$. Our main results is a fixed parameter algorithm for Mixed-Multiway Cut-Uncut using the method of recursive understanding introduced by Chitnis et al. (FOCS 2012).
Type-based Self-stabilisation for Computational Fields
Venue: arXiv cs.LO 2015
Year: 2015

Emerging network scenarios require the development of solid large-scale situated systems. Unfortunately, the diffusion/aggregation computational processes therein often introduce a source of complexity that hampers predictability of the overall system behaviour. Computational fields have been introduced to help engineering such systems: they are spatially distributed data structures designed to adapt their shape to the topology of the underlying (mobile) network and to the events occurring in it, with notable applications to pervasive computing, sensor networks, and mobile robots. To assure behavioural correctness, namely, correspondence of micro-level specification (single device behaviour) with macro-level behaviour (resulting global spatial pattern), we investigate the issue of self-stabilisation for computational fields. We present a tiny, expressive, and type-sound calculus of computational fields, and define sufficient conditions for self-stabilisation, defined as the ability to react to changes in the environment finding a new stable state in finite time. A type-based approach is used to provide a correct checking procedure for self-stabilisation.
User-Curated Image Collections: Modeling and Recommendation
Venue: arXiv cs.MM 2015
Year: 2015

Most state-of-the-art image retrieval and recommendation systems predominantly focus on individual images. In contrast, socially curated image collections, condensing distinctive yet coherent images into one set, are largely overlooked by the research communities. In this paper, we aim to design a novel recommendation system that can provide users with image collections relevant to individual personal preferences and interests. To this end, two key issues need to be addressed, i.e., image collection modeling and similarity measurement. For image collection modeling, we consider each image collection as a whole in a group sparse reconstruction framework and extract concise collection descriptors given the pretrained dictionaries. We then consider image collection recommendation as a dynamic similarity measurement problem in response to user's clicked image set, and employ a metric learner to measure the similarity between the image collection and the clicked image set. As there is no previous work directly comparable to this study, we implement several competitive baselines and related methods for comparison. The evaluations on a large scale Pinterest data set have validated the effectiveness of our proposed methods for modeling and recommending image collections.
Low-Coherence Frames from Group Fourier Matrices
Venue: arXiv cs.IT 2015
Year: 2015

Many problems in areas such as compressive sensing and coding theory seek to design a set of equal-norm vectors with large angular separation. This idea is essentially equivalent to constructing a frame with low coherence. The elements of such frames can in turn be used to build high-performance spherical codes, quantum measurement operators, and compressive sensing measurement matrices, to name a few applications. In this work, we allude to the group-frame construction first described by Slepian and further explored in the works of Vale and Waldron. We present a method for selecting representations of a finite group to construct a group frame that achieves low coherence. Our technique produces a tight frame with a small number of distinct inner product values between the frame elements, in a sense approximating a Grassmanian frame. We identify special cases in which our construction yields some previously-known frames with optimal coherence meeting the Welch lower bound, and other cases in which the entries of our frame vectors come from small alphabets. In particular, we apply our technique to the problem choosing a subset of rows of a Hadamard matrix so that the resulting columns form a low-coherence frame. Finally, we give an explicit calculation of the average coherence of our frames, and find regimes in which they satisfy the Strong Coherence Property described by Mixon, Bajwa, and Calderbank.
Lower bounds for approximation schemes for Closest String
Venue: arXiv cs.DS 2015
Year: 2015

In the Closest String problem one is given a family $\mathcal S$ of equal-length strings over some fixed alphabet, and the task is to find a string $y$ that minimizes the maximum Hamming distance between $y$ and a string from $\mathcal S$. While polynomial-time approximation schemes (PTASes) for this problem are known for a long time [Li et al., J. ACM'02], no efficient polynomial-time approximation scheme (EPTAS) has been proposed so far. In this paper, we prove that the existence of an EPTAS for Closest String is in fact unlikely, as it would imply that $\mathrm{FPT}=\mathrm{W}[1]$, a highly unexpected collapse in the hierarchy of parameterized complexity classes. Our proof also shows that the existence of a PTAS for Closest String with running time $f(\varepsilon)\cdot n^{o(1/\varepsilon)}$, for any computable function $f$, would contradict the Exponential Time Hypothesis.
Face Photo Sketch Synthesis via Larger Patch and Multiresolution Spline
Venue: arXiv cs.CV 2015
Year: 2015

Face photo sketch synthesis has got some researchers' attention in recent years because of its potential applications in digital entertainment and law enforcement. Some patches based methods have been proposed to solve this problem. These methods usually focus more on how to get a sketch patch for a given photo patch than how to blend these generated patches. However, without appropriately blending method, some jagged parts and mottled points will appear in the entire face sketch. In order to get a smoother sketch, we propose a new method to reduce such jagged parts and mottled points. In our system, we resort to an existed method, which is Markov Random Fields (MRF), to train a crude face sketch firstly. Then this crude sketch face sketch will be divided into some larger patches again and retrained by Non-Negative Matrix Factorization (NMF). At last, we use Multiresolution Spline and a blend trick named full-coverage trick to blend these retrained patches. The experiment results show that compared with some previous method, we can get a smoother face sketch.
Distributed Filter Design for Cooperative H-Infinity-Type Estimation
Venue: arXiv cs.SY 2015
Year: 2015

In this paper, we consider the distributed robust filtering problem, where estimator design is based on a set of coupled linear matrix inequalities (LMIs). We separate the problem and show that the method of multipliers can be applied to obtain a solution efficiently and in a decentralized fashion, i.e. all local estimators can compute their filter gains locally and iteratively, with communications restricted to their neighbours. The convergence properties of the iterative algorithm are analyzed and interpreted.
Image Set Querying Based Localization
Venue: arXiv cs.CV 2015
Year: 2015

Conventional single image based localization methods usually fail to localize a querying image when there exist large variations between the querying image and the pre-built scene. To address this, we propose an image-set querying based localization approach. When the localization by a single image fails to work, the system will ask the user to capture more auxiliary images. First, a local 3D model is established for the querying image set. Then, the pose of the querying image set is estimated by solving a nonlinear optimization problem, which aims to match the local 3D model against the pre-built scene. Experiments have shown the effectiveness and feasibility of the proposed approach.
LT Codes Combined with Network Coding for Multihop Powerline Smart Grid Networks
Venue: arXiv cs.IT 2015
Year: 2015

This paper describes a novel approach for combining Luby Transform (LT) codes and Network Coding (NC) in the context of PowerLine Communications (PLC) smart grid networks. Multihop transmissions of LT-encoded data on PLC networks are considered and algorithms to combine data at relay nodes are proposed. Without the need to decode and then re-encode the total received data stream, the relay nodes can forward the received data stream while adding at the same time their own data. Simulation results are provided confirming the good performance of the proposed algorithms.
Stateman: Using Metafunctions to Manage Large Terms Representing Machine States
Venue: arXiv cs.LO 2015
Year: 2015

When ACL2 is used to model the operational semantics of computing machines, machine states are typically represented by terms recording the contents of the state components. When models are realistic and are stepped through thousands of machine cycles, these terms can grow quite large and the cost of simplifying them on each step grows. In this paper we describe an ACL2 book that uses HIDE and metafunctions to facilitate the management of large terms representing such states. Because the metafunctions for each state component updater are solely responsible for creating state expressions (i.e., "writing") and the metafunctions for each state component accessor are solely responsible for extracting values (i.e., "reading") from such state expressions, they can maintain their own normal form, use HIDE to prevent other parts of ACL2 from inspecting them, and use honsing to uniquely represent state expressions. The last feature makes it possible to memoize the metafunctions, which can improve proof performance in some machine models. This paper describes a general-purpose ACL2 book modeling a byte-addressed memory supporting "mixed" reads and writes. By "mixed" we mean that reads need not correspond (in address or number of bytes) with writes. Verified metafunctions simplify such "read-over-write" expressions while hiding the potentially large state expression. A key utility is a function that determines an upper bound on the value of a symbolic arithmetic expression, which plays a role in resolving writes to addresses given by symbolic expressions. We also report on a preliminary experiment with the book, which involves the production of states containing several million function calls.
Multilayer bootstrap network for unsupervised speaker recognition
Venue: arXiv cs.LG 2015
Year: 2015

We apply multilayer bootstrap network (MBN), a recent proposed unsupervised learning method, to unsupervised speaker recognition. The proposed method first extracts supervectors from an unsupervised universal background model, then reduces the dimension of the high-dimensional supervectors by multilayer bootstrap network, and finally conducts unsupervised speaker recognition by clustering the low-dimensional data. The comparison results with 2 unsupervised and 1 supervised speaker recognition techniques demonstrate the effectiveness and robustness of the proposed method.
Vision System and Depth Processing for DRC-HUBO+
Venue: arXiv cs.CV 2015
Year: 2015

This paper presents a vision system and a depth processing algorithm for DRC-HUBO+, the winner of the DRC finals 2015. Our system is designed to reliably capture 3D information of a scene and objects robust to challenging environment conditions. We also propose a depth-map upsampling method that produces an outliers-free depth map by explicitly handling depth outliers. Our system is suitable for an interactive robot with real-world that requires accurate object detection and pose estimation. We evaluate our depth processing algorithm over state-of-the-art algorithms on several synthetic and real-world datasets.
Transaction Remote Release (TRR): A New Anonymization Technology for Bitcoin
Venue: arXiv cs.CR 2015
Year: 2015

The anonymity of the Bitcoin system has some shortcomings. Analysis of Transaction Chain (ATC) and Analysis of Bitcoin Protocol and Network (ABPN) are two important methods of deanonymizing bitcoin transactions. Nowadays, there are some anonymization methods to combat ATC but there has been little research into ways to counter ABPN. This paper proposes a new anonymization technology called Transaction Remote Release (TRR). Inspired by The Onion Router (TOR), TRR is able to render several typical attacking methods of ABPN ineffective. Furthermore, the performance of encryption and decryption of TRR is good and the growth rate of the cipher is very limited. Hence, TRR is suited for practical applications.
Strong converses for group testing in the finite blocklength regime
Venue: arXiv cs.IT 2015
Year: 2015

We prove new strong converse results in a variety of group testing settings, generalizing a result of Baldassini, Johnson and Aldridge. These results are proved by two distinct approaches, corresponding to the non-adaptive and adaptive cases. In the non-adaptive case, we mimic the hypothesis testing argument introduced in the finite blocklength channel coding regime by Polyanskiy, Poor and Verdú. In the adaptive case, we combine a formulation based on directed information theory with ideas of Kemperman, Kesten and Wolfowitz from the problem of channel coding with feedback. In both cases, we prove results which are valid for finite sized problems, and imply capacity results in the asymptotic regime. These results are illustrated graphically for a range of models.
Efficient Algorithms for Morphisms over Omega-Regular Languages
Venue: arXiv cs.FL 2015
Year: 2015

Morphisms to finite semigroups can be used for recognizing omega-regular languages. The so-called strongly recognizing morphisms can be seen as a deterministic computation model which provides minimal objects (known as the syntactic morphism) and a trivial complementation procedure. We give a quadratic-time algorithm for computing the syntactic morphism from any given strongly recognizing morphism, thereby showing that minimization is easy as well. In addition, we give algorithms for efficiently solving various decision problems for weakly recognizing morphisms. Weakly recognizing morphism are often smaller than their strongly recognizing counterparts. Finally, we describe the language operations needed for converting formulas in monadic second-order logic (MSO) into strongly recognizing morphisms, and we give some experimental results.
Communication Complexity (for Algorithm Designers)
Venue: arXiv cs.CC 2015
Year: 2015

This document collects the lecture notes from my course "Communication Complexity (for Algorithm Designers),'' taught at Stanford in the winter quarter of 2015. The two primary goals of the course are: 1. Learn several canonical problems that have proved the most useful for proving lower bounds (Disjointness, Index, Gap-Hamming, etc.). 2. Learn how to reduce lower bounds for fundamental algorithmic problems to communication complexity lower bounds. Along the way, we'll also: 3. Get exposure to lots of cool computational models and some famous results about them --- data streams and linear sketches, compressive sensing, space-query time trade-offs in data structures, sublinear-time algorithms, and the extension complexity of linear programs. 4. Scratch the surface of techniques for proving communication complexity lower bounds (fooling sets, corruption bounds, etc.).
On Computational Paths and the Fundamental Groupoid of a Type
Venue: arXiv cs.LO 2015
Year: 2015

The main objective of this work is to study mathematical properties of computational paths. Originally proposed by de Queiroz \& Gabbay (1994) as `sequences of rewrites', computational paths can be seen as the grounds on which the propositional equality between two computational objects stand. Using computational paths and categorical semantics, we take any type $A$ of type theory and construct a groupoid for this type. We call this groupoid the fundamental groupoid of a type $A$, since it is similar to the one obtained using the homotopical interpretation of the identity type. The main difference is that instead of being just a semantical interpretation, computational paths are entities of the syntax of type theory. We also expand our results, using computational paths to construct fundamental groupoids of higher levels.
Deep Reinforcement Learning with Double Q-learning
Venue: arXiv cs.LG 2015
Year: 2015

The popular Q-learning algorithm is known to overestimate action values under certain conditions. It was not previously known whether, in practice, such overestimations are common, whether they harm performance, and whether they can generally be prevented. In this paper, we answer all these questions affirmatively. In particular, we first show that the recent DQN algorithm, which combines Q-learning with a deep neural network, suffers from substantial overestimations in some games in the Atari 2600 domain. We then show that the idea behind the Double Q-learning algorithm, which was introduced in a tabular setting, can be generalized to work with large-scale function approximation. We propose a specific adaptation to the DQN algorithm and show that the resulting algorithm not only reduces the observed overestimations, as hypothesized, but that this also leads to much better performance on several games.
Latency Analysis of an Aerial Video Tracking System Using Fiacre and Tina
Venue: arXiv cs.PF 2015
Year: 2015

We describe our experience with modeling a video tracking system used to detect and follow moving targets from an airplane. We provide a formal model that takes into account the real-time properties of the system and use it to compute the worst and best-case end to end latency. We also compute a lower bound on the delay between the loss of two frames. Our approach is based on the model-checking tool Tina, that provides state-space generation and model-checking algorithms for an extension of Time Petri Nets with data and priorities. We propose several models divided in two main categories: first Time Petri Net models, which are used to study the behavior of the system in the most basic way; then models based on the Fiacre specification language, where we take benefit of richer data structures to directly model the buffering of video information and the use of an unbounded number of frame identifiers.
Graph Kernels exploiting Weisfeiler-Lehman Graph Isomorphism Test Extensions
Venue: arXiv cs.LG 2015
Year: 2015

In this paper we present a novel graph kernel framework inspired the by the Weisfeiler-Lehman (WL) isomorphism tests. Any WL test comprises a relabelling phase of the nodes based on test-specific information extracted from the graph, for example the set of neighbours of a node. We defined a novel relabelling and derived two kernels of the framework from it. The novel kernels are very fast to compute and achieve state-of-the-art results on five real-world datasets.
Preprint: Bringing immersive enjoyment to hyperbaric oxygen chamber users using virtual reality glasses
Venue: arXiv cs.HC 2015
Year: 2015

This is the preprint version of our paper on REHAB2015. This paper proposed a novel immersive entertainment system for the users of hyperbaric oxygen therapy chamber. The system is a hybrid of hardware and software, the scheme is described in this paper. The hardware is combined by a HMD (i.e. virtual reality glasses shell), a smartphone and a waterproof bag. The software is able to transfer the stereoscopic images of the 3D game to the screen of the smartphone synchronously. The comparison and selection of the hardware are discussed according to the practical running scene of the clinical hyperbaric oxygen treatment. Finally, a preliminary guideline for designing this kind of system is raised accordingly.
Preprint: Comparing Kinect2 based Balance Measurement Software to Wii Balance Board
Venue: arXiv cs.HC 2015
Year: 2015

This is the preprint version of our paper on REHAB2015. A balance measurement software based on Kinect2 sensor is evaluated by comparing to Wii balance board in numerical analysis level, and further improved according to the consideration of BFP (Body fat percentage) values of the user. Several person with different body types are involved into the test. The algorithm is improved by comparing the body type of the user to the 'golden- standard' body type. The evaluation results of the optimized algorithm preliminarily prove the reliability of the software.
Bandit Label Inference for Weakly Supervised Learning
Venue: arXiv cs.LG 2015
Year: 2015

The scarcity of data annotated at the desired level of granularity is a recurring issue in many applications. Significant amounts of effort have been devoted to developing weakly supervised methods tailored to each individual setting, which are often carefully designed to take advantage of the particular properties of weak supervision regimes, form of available data and prior knowledge of the task at hand. Unfortunately, it is difficult to adapt these methods to new tasks and/or forms of data, which often require different weak supervision regimes or models. We present a general-purpose method that can solve any weakly supervised learning problem irrespective of the weak supervision regime or the model. The proposed method turns any off-the-shelf strongly supervised classifier into a weakly supervised classifier and allows the user to specify any arbitrary weakly supervision regime via a loss function. We apply the method to several different weak supervision regimes and demonstrate competitive results compared to methods specifically engineered for those settings.
A Forensically Sound Adversary Model for Mobile Devices
Venue: arXiv cs.CR 2015
Year: 2015

In this paper, we propose an adversary model to facilitate forensic investigations of mobile devices (e.g. Android, iOS and Windows smartphones) that can be readily adapted to the latest mobile device technologies. This is essential given the ongoing and rapidly changing nature of mobile device technologies. An integral principle and significant constraint upon forensic practitioners is that of forensic soundness. Our adversary model specifically considers and integrates the constraints of forensic soundness on the adversary, in our case, a forensic practitioner. One construction of the adversary model is an evidence collection and analysis methodology for Android devices. Using the methodology with six popular cloud apps, we were successful in extracting various information of forensic interest in both the external and internal storage of the mobile device.