OpenRaiser/Intern-Atlas huggingface dataset:
Convolutional Recurrent Neural Networks for Dynamic MR Image Reconstruction
Venue: arXiv cs.CV 2018
Year: 2018

Accelerating the data acquisition of dynamic magnetic resonance imaging (MRI) leads to a challenging ill-posed inverse problem, which has received great interest from both the signal processing and machine learning community over the last decades. The key ingredient to the problem is how to exploit the temporal correlation of the MR sequence to resolve the aliasing artefact. Traditionally, such observation led to a formulation of a non-convex optimisation problem, which were solved using iterative algorithms. Recently, however, deep learning based-approaches have gained significant popularity due to its ability to solve general inversion problems. In this work, we propose a unique, novel convolutional recurrent neural network (CRNN) architecture which reconstructs high quality cardiac MR images from highly undersampled k-space data by jointly exploiting the dependencies of the temporal sequences as well as the iterative nature of the traditional optimisation algorithms. In particular, the proposed architecture embeds the structure of the traditional iterative algorithms, efficiently modelling the recurrence of the iterative reconstruction stages by using recurrent hidden connections over such iterations. In addition, spatiotemporal dependencies are simultaneously learnt by exploiting bidirectional recurrent hidden connections across time sequences. The proposed algorithm is able to learn both the temporal dependency and the iterative reconstruction process effectively with only a very small number of parameters, while outperforming current MR reconstruction methods in terms of computational complexity, reconstruction accuracy and speed.
Tech Report: A Fast Multiscale Spatial Regularization for Sparse Hyperspectral Unmixing
Venue: arXiv cs.CV 2018
Year: 2018

Sparse hyperspectral unmixing from large spectral libraries has been considered to circumvent limitations of endmember extraction algorithms in many applications. This strategy often leads to ill-posed inverse problems, which can benefit from spatial regularization strategies. While existing spatial regularization methods improve the problem conditioning and promote piecewise smooth solutions, they lead to large nonsmooth optimization problems. Thus, efficiently introducing spatial context in the unmixing problem remains a challenge, and a necessity for many real world applications. In this paper, a novel multiscale spatial regularization approach for sparse unmixing is proposed. The method uses a signal-adaptive spatial multiscale decomposition based on superpixels to decompose the unmixing problem into two simpler problems, one in the approximation domain and another in the original domain. Simulation results using both synthetic and real data indicate that the proposed method can outperform state-of-the-art Total Variation-based algorithms with a computation time comparable to that of their unregularized counterparts.
Accomplishing High-Level Tasks with Modular Robots
Venue: arXiv cs.RO 2018
Year: 2018

The advantage of modular self-reconfigurable robot systems is their flexibility, but this advantage can only be realized if appropriate configurations (shapes) and behaviors (controlling programs) can be selected for a given task. In this paper, we present an integrated system for addressing high-level tasks with modular robots, and demonstrate that it is capable of accomplishing challenging, multi-part tasks in hardware experiments. The system consists of four tightly integrated components: (1) A high-level mission planner, (2) A large design library spanning a wide set of functionality, (3) A design and simulation tool for populating the library with new configurations and behaviors, and (4) modular robot hardware. This paper builds on earlier work by the authors, extending the original system to include environmentally adaptive parametric behaviors, which integrate motion planners and feedback controllers with the system.
Mining Fix Patterns for FindBugs Violations
Venue: arXiv cs.SE 2018
Year: 2018

In this paper, we first collect and track a large number of fixed and unfixed violations across revisions of software. The empirical analyses reveal that there are discrepancies in the distributions of violations that are detected and those that are fixed, in terms of occurrences, spread and categories, which can provide insights into prioritizing violations. To automatically identify patterns in violations and their fixes, we propose an approach that utilizes convolutional neural networks to learn features and clustering to regroup similar instances. We then evaluate the usefulness of the identified fix patterns by applying them to unfixed violations. The results show that developers will accept and merge a majority (69/116) of fixes generated from the inferred fix patterns. It is also noteworthy that the yielded patterns are applicable to four real bugs in the Defects4J major benchmark for software testing and automated repair.
Visual aesthetic analysis using deep neural network: model and techniques to increase accuracy without transfer learning
Venue: arXiv cs.CV 2018
Year: 2018

We train a deep Convolutional Neural Network (CNN) from scratch for visual aesthetic analysis in images and discuss techniques we adopt to improve the accuracy. We avoid the prevalent best transfer learning approaches of using pretrained weights to perform the task and train a model from scratch to get accuracy of 78.7% on AVA2 Dataset close to the best models available (85.6%). We further show that accuracy increases to 81.48% on increasing the training set by incremental 10 percentile of entire AVA dataset showing our algorithm gets better with more data.
Uniqueness of Transformation based on Jacobian Determinant and curl-Vector
Venue: arXiv cs.CG 2018
Year: 2018

Numerical examples demonstrated that a prescribed positive Jacobian determinant alone can not uniquely determine a diffeomorphism. It is conjectured that the uniqueness of a transformation can be assured by its Jacobian determinant and the curl-vector. In this work, we study the uniqueness problem analytically and propose an approach to the proof of the uniqueness of a transformation with prescribed Jacobian determinant and curl-vector.
A Graph-theoretic Model to Steganography on Social Networks
Venue: arXiv cs.MM 2018
Year: 2018

Steganography aims to conceal the very fact that the communication takes place, by embedding a message into a digit object such as image without introducing noticeable artifacts. A number of steganographic systems have been developed in past years, most of which, however, are confined to the laboratory conditions where the real-world use of steganography are rarely concerned. In this paper, we introduce an alternative perspective to steganography. A graph-theoretic model to steganography on social networks is presented to analyze real-world steganographic scenarios. In the graph, steganographic participants are corresponding to the vertices with meaningless unique identifiers. Each edge allows the two vertices to communicate with each other by any steganographic algorithm. Meanwhile, the edges are associated with weights to quantize the corresponding communication risk (or say cost). The optimization task is to minimize the overall risk, which is modeled as additive over the social network. We analyze different scenarios on a social network, and provide the suited solutions to the corresponding optimization tasks. We prove that a multiplicative probabilistic graph is equivalent to an additive weighted graph. From the viewpoint of an attacker, he may hope to detect suspicious communication channels, the data encoder(s) and the data decoder(s). We present limited detection analysis to steganographic communication on a network.
Ultra-Large Repair Search Space with Automatically Mined Templates: the Cardumen Mode of Astor
Venue: arXiv cs.SE 2018
Year: 2018

Astor is a program repair library which has different modes. In this paper, we present the Cardumen mode of Astor, a repair approach based mined templates that has an ultra-large search space. We evaluate the capacity of Cardumen to discover test-suite adequate patches (aka plausible patches) over the 356 real bugs from Defects4J. Cardumen finds 8935 patches over 77 bugs of Defects4J. This is the largest number of automatically synthesized patches ever reported, all patches being available in an open-science repository. Moreover, Cardumen identifies 8 unique patches, that are patches for Defects4J bugs that were never repaired in the whole history of program repair.
Diversity Combining via Universal Orthogonal Space-Time Transformations
Venue: arXiv cs.IT 2018
Year: 2018

Receiver diversity combining methods play a key role in combating the detrimental effects of fadingin wireless communication and other applications. A novel diversity combining method is proposedwhere a universal, i.e., channel independent, orthogonal dimension-reducing space-time transformationis applied prior to quantization of the signals. The scheme may be considered as the counterpart ofAlamouti modulation, and more generally of orthogonal space-time block codes.
Ultra valuations
Venue: arXiv cs.GT 2018
Year: 2018

This paper proposes an original exchange property of valuations.This property is shown to be equivalent to a property described by Dress and Terhalle in the context of discrete optimization and matroids and shown there to characterize the valuations for which the demand oracle can be implemented by a greedy algorithm. The same exchange property is also equivalent to a property described independently by Reijnierse, van Gellekom and Potters and by Lehmann, Lehmann and Nisan and shown there to be satisfied by substitutes valuations. It studies the family of valuations that satisfy this exchange property, the ultra valuations. Any substitutes valuation is an ultra valuation, but ultra valuations may exhibit complementarities. Any symmetric valuation is an ultra valuation. Substitutes valuations are exactly the submodular ultra valuations. Ultra valuations define ultrametrics on the set of items. The maximum of an ultra valuation on $n$ items can be found in $O(n^2)$ steps. Finding an efficient allocation among ultra valuations is NP-hard.
Fundamental Limits of Cloud and Cache-Aided Interference Management with Multi-Antenna Edge Nodes
Venue: arXiv cs.IT 2018
Year: 2018

In fog-aided cellular systems, content delivery latency can be minimized by jointly optimizing edge caching and transmission strategies. In order to account for the cache capacity limitations at the Edge Nodes (ENs), transmission generally involves both fronthaul transfer from a cloud processor with access to the content library to the ENs, as well as wireless delivery from the ENs to the users. In this paper, the resulting problem is studied from an information-theoretic viewpoint by making the following practically relevant assumptions: 1) the ENs have multiple antennas; 2) only uncoded fractional caching is allowed; 3) the fronthaul links are used to send fractions of contents; and 4) the ENs are constrained to use one-shot linear precoding on the wireless channel. Assuming offline proactive caching and focusing on a high signal-to-noise ratio (SNR) latency metric, the optimal information-theoretic performance is investigated under both serial and pipelined fronthaul-edge transmission modes. The analysis characterizes the minimum high-SNR latency in terms of Normalized Delivery Time (NDT) for worst-case users' demands. The characterization is exact for a subset of system parameters, and is generally optimal within a multiplicative factor of 3/2 for the serial case and of 2 for the pipelined case. The results bring insights into the optimal interplay between edge and cloud processing in fog-aided wireless networks as a function of system resources, including the number of antennas at the ENs, the ENs' cache capacity and the fronthaul capacity.
Music Generation by Deep Learning - Challenges and Directions
Venue: arXiv cs.SD 2018
Year: 2018

In addition to traditional tasks such as prediction, classification and translation, deep learning is receiving growing attention as an approach for music generation, as witnessed by recent research groups such as Magenta at Google and CTRL (Creator Technology Research Lab) at Spotify. The motivation is in using the capacity of deep learning architectures and training techniques to automatically learn musical styles from arbitrary musical corpora and then to generate samples from the estimated distribution. However, a direct application of deep learning to generate content rapidly reaches limits as the generated content tends to mimic the training set without exhibiting true creativity. Moreover, deep learning architectures do not offer direct ways for controlling generation (e.g., imposing some tonality or other arbitrary constraints). Furthermore, deep learning architectures alone are autistic automata which generate music autonomously without human user interaction, far from the objective of interactively assisting musicians to compose and refine music. Issues such as: control, structure, creativity and interactivity are the focus of our analysis. In this paper, we select some limitations of a direct application of deep learning to music generation, analyze why the issues are not fulfilled and how to address them by possible approaches. Various examples of recent systems are cited as examples of promising directions.
Computational Logic: Its Origins and Applications
Venue: arXiv cs.LO 2018
Year: 2018

Computational Logic is the use of computers to establish facts in a logical formalism. Originating in 19th-century attempts to understand the nature of mathematical reasoning, the subject now comprises a wide variety of formalisms, techniques and technologies. One strand of work follows the "LCF approach" pioneered by Robin Milner FRS, where proofs can be constructed interactively or with the help of users' code (which does not compromise correctness). A refinement of LCF, called Isabelle, retains these advantages while providing flexibility in the choice of logical formalism and much stronger automation. The main application of these techniques has been to prove the correctness of hardware and software systems, but increasingly researchers have been applying them to mathematics itself.
Keyword-Based Delegable Proofs of Storage
Venue: arXiv cs.CR 2018
Year: 2018

Cloud users (clients) with limited storage capacity at their end can outsource bulk data to the cloud storage server. A client can later access her data by downloading the required data files. However, a large fraction of the data files the client outsources to the server is often archival in nature that the client uses for backup purposes and accesses less frequently. An untrusted server can thus delete some of these archival data files in order to save some space (and allocate the same to other clients) without being detected by the client (data owner). Proofs of storage enable the client to audit her data files uploaded to the server in order to ensure the integrity of those files. In this work, we introduce one type of (selective) proofs of storage that we call keyword-based delegable proofs of storage, where the client wants to audit all her data files containing a specific keyword (e.g., "important"). Moreover, it satisfies the notion of public verifiability where the client can delegate the auditing task to a third-party auditor who audits the set of files corresponding to the keyword on behalf of the client. We formally define the security of a keyword-based delegable proof-of-storage protocol. We construct such a protocol based on an existing proof-of-storage scheme and analyze the security of our protocol. We argue that the techniques we use can be applied atop any existing publicly verifiable proof-of-storage scheme for static data. Finally, we discuss the efficiency of our construction.
Axioms for Modelling Cubical Type Theory in a Topos
Venue: arXiv cs.LO 2018
Year: 2018

The homotopical approach to intensional type theory views proofs of equality as paths. We explore what is required of an object $I$ in a topos to give such a path-based model of type theory in which paths are just functions with domain $I$. Cohen, Coquand, Huber and Mörtberg give such a model using a particular category of presheaves. We investigate the extent to which their model construction can be expressed in the internal type theory of any topos and identify a collection of quite weak axioms for this purpose. This clarifies the definition and properties of the notion of uniform Kan filling that lies at the heart of their constructive interpretation of Voevodsky's univalence axiom. (This paper is a revised and expanded version of a paper of the same name that appeared in the proceedings of the 25th EACSL Annual Conference on Computer Science Logic, CSL 2016.)
Robust Estimation of Similarity Transformation for Visual Object Tracking
Venue: arXiv cs.CV 2018
Year: 2018

Most of existing correlation filter-based tracking approaches only estimate simple axis-aligned bounding boxes, and very few of them is capable of recovering the underlying similarity transformation. To tackle this challenging problem, in this paper, we propose a new correlation filter-based tracker with a novel robust estimation of similarity transformation on the large displacements. In order to efficiently search in such a large 4-DoF space in real-time, we formulate the problem into two 2-DoF sub-problems and apply an efficient Block Coordinates Descent solver to optimize the estimation result. Specifically, we employ an efficient phase correlation scheme to deal with both scale and rotation changes simultaneously in log-polar coordinates. Moreover, a variant of correlation filter is used to predict the translational motion individually. Our experimental results demonstrate that the proposed tracker achieves very promising prediction performance compared with the state-of-the-art visual object tracking methods while still retaining the advantages of high efficiency and simplicity in conventional correlation filter-based tracking methods.
Taylor expansion in linear logic is invertible
Venue: arXiv cs.LO 2018
Year: 2018

Each Multiplicative Exponential Linear Logic (MELL) proof-net can be expanded into a differential net, which is its Taylor expansion. We prove that two different MELL proof-nets have two different Taylor expansions. As a corollary, we prove a completeness result for MELL: We show that the relational model is injective for MELL proof-nets, i.e. the equality between MELL proof-nets in the relational model is exactly axiomatized by cut-elimination.
Semantic Visual Localization
Venue: arXiv cs.CV 2018
Year: 2018

Robust visual localization under a wide range of viewing conditions is a fundamental problem in computer vision. Handling the difficult cases of this problem is not only very challenging but also of high practical relevance, e.g., in the context of life-long localization for augmented reality or autonomous robots. In this paper, we propose a novel approach based on a joint 3D geometric and semantic understanding of the world, enabling it to succeed under conditions where previous approaches failed. Our method leverages a novel generative model for descriptor learning, trained on semantic scene completion as an auxiliary task. The resulting 3D descriptors are robust to missing observations by encoding high-level 3D geometric and semantic information. Experiments on several challenging large-scale localization datasets demonstrate reliable localization under extreme viewpoint, illumination, and geometry changes.
Unifying Sparsest Cut, Cluster Deletion, and Modularity Clustering Objectives with Correlation Clustering
Venue: arXiv cs.DS 2018
Year: 2018

Graph clustering, or community detection, is the task of identifying groups of closely related objects in a large network. In this paper we introduce a new community-detection framework called LambdaCC that is based on a specially weighted version of correlation clustering. A key component in our methodology is a clustering resolution parameter, $λ$, which implicitly controls the size and structure of clusters formed by our framework. We show that, by increasing this parameter, our objective effectively interpolates between two different strategies in graph clustering: finding a sparse cut and forming dense subgraphs. Our methodology unifies and generalizes a number of other important clustering quality functions including modularity, sparsest cut, and cluster deletion, and places them all within the context of an optimization problem that has been well studied from the perspective of approximation algorithms. Our approach is particularly relevant in the regime of finding dense clusters, as it leads to a 2-approximation for the cluster deletion problem. We use our approach to cluster several graphs, including large collaboration networks and social networks.
Ray: A Distributed Framework for Emerging AI Applications
Venue: arXiv cs.DC 2018
Year: 2018

The next generation of AI applications will continuously interact with the environment and learn from these interactions. These applications impose new and demanding systems requirements, both in terms of performance and flexibility. In this paper, we consider these requirements and present Ray---a distributed system to address them. Ray implements a unified interface that can express both task-parallel and actor-based computations, supported by a single dynamic execution engine. To meet the performance requirements, Ray employs a distributed scheduler and a distributed and fault-tolerant store to manage the system's control state. In our experiments, we demonstrate scaling beyond 1.8 million tasks per second and better performance than existing specialized systems for several challenging reinforcement learning applications.
Efficient B-mode Ultrasound Image Reconstruction from Sub-sampled RF Data using Deep Learning
Venue: arXiv cs.CV 2018
Year: 2018

In portable, three dimensional, and ultra-fast ultrasound imaging systems, there is an increasing demand for the reconstruction of high quality images from a limited number of radio-frequency (RF) measurements due to receiver (Rx) or transmit (Xmit) event sub-sampling. However, due to the presence of side lobe artifacts from RF sub-sampling, the standard beamformer often produces blurry images with less contrast, which are unsuitable for diagnostic purposes. Existing compressed sensing approaches often require either hardware changes or computationally expensive algorithms, but their quality improvements are limited. To address this problem, here we propose a novel deep learning approach that directly interpolates the missing RF data by utilizing redundancy in the Rx-Xmit plane. Our extensive experimental results using sub-sampled RF data from a multi-line acquisition B-mode system confirm that the proposed method can effectively reduce the data rate without sacrificing image quality.
Inductive $k$-independent graphs and $c$-colorable subgraphs in scheduling: A review
Venue: arXiv cs.DM 2018
Year: 2018

Inductive $k$-independent graphs generalize chordal graphs and have recently been advocated in the context of interference-avoiding wireless communication scheduling. The NP-hard problem of finding maximum-weight induced $c$-colorable subgraphs, which is a generalization of finding maximum independent sets, naturally occurs when selecting $c$ sets of pairwise non-conflicting jobs (modeled as graph vertices). We investigate the parameterized complexity of this problem on inductive $k$-independent graphs. We show that the Independent Set problem is W[1]-hard even on 2-simplicial 3-minoes---a subclass of inductive 2-independent graphs. In contrast, we prove that the more general Maximum $c$-Colorable Subgraph problem is fixed-parameter tractable on edge-wise unions of cluster and chordal graphs, which are 2-simplicial. In both cases, the parameter is the solution size. Aside from this, we survey other graph classes between inductive 1-inductive and inductive 2-inductive graphs with applications in scheduling.