OpenRaiser/Intern-Atlas huggingface dataset:
Supervised Saliency Map Driven Segmentation of the Lesions in Dermoscopic Images
Venue: arXiv cs.CV 2018
Year: 2018

Lesion segmentation is the first step in most automatic melanoma recognition systems. Deficiencies and difficulties in dermoscopic images such as color inconstancy, hair occlusion, dark corners and color charts make lesion segmentation an intricate task. In order to detect the lesion in the presence of these problems, we propose a supervised saliency detection method tailored for dermoscopic images based on the discriminative regional feature integration (DRFI). DRFI method incorporates multi-level segmentation, regional contrast, property, background descriptors, and a random forest regressor to create saliency scores for each region in the image. In our improved saliency detection method, mDRFI, we have added some new features to regional property descriptors. Also, in order to achieve more robust regional background descriptors, a thresholding algorithm is proposed to obtain a new pseudo-background region. Findings reveal that mDRFI is superior to DRFI in detecting the lesion as the salient object in dermoscopic images. The proposed overall lesion segmentation framework uses detected saliency map to construct an initial mask of the lesion through thresholding and post-processing operations. The initial mask is then evolving in a level set framework to fit better on the lesion's boundaries. The results of evaluation tests on three public datasets show that our proposed segmentation method outperforms the other conventional state-of-the-art segmentation algorithms and its performance is comparable with most recent approaches that are based on deep convolutional neural networks.
Dynamic Word Embeddings for Evolving Semantic Discovery
Venue: arXiv cs.CL 2018
Year: 2018

Word evolution refers to the changing meanings and associations of words throughout time, as a byproduct of human language evolution. By studying word evolution, we can infer social trends and language constructs over different periods of human history. However, traditional techniques such as word representation learning do not adequately capture the evolving language structure and vocabulary. In this paper, we develop a dynamic statistical model to learn time-aware word vector representation. We propose a model that simultaneously learns time-aware embeddings and solves the resulting "alignment problem". This model is trained on a crawled NYTimes dataset. Additionally, we develop multiple intuitive evaluation strategies of temporal word embeddings. Our qualitative and quantitative tests indicate that our method not only reliably captures this evolution over time, but also consistently outperforms state-of-the-art temporal embedding approaches on both semantic accuracy and alignment quality.
Learning Mixtures of Sparse Linear Regressions Using Sparse Graph Codes
Venue: arXiv cs.IT 2018
Year: 2018

In this paper, we consider the mixture of sparse linear regressions model. Let $β^{(1)},\ldots,β^{(L)}\in\mathbb{C}^n$ be $ L $ unknown sparse parameter vectors with a total of $ K $ non-zero coefficients. Noisy linear measurements are obtained in the form $y_i={x}_i^H β^{(\ell_i)} + w_i$, each of which is generated randomly from one of the sparse vectors with the label $ \ell_i $ unknown. The goal is to estimate the parameter vectors efficiently with low sample and computational costs. This problem presents significant challenges as one needs to simultaneously solve the demixing problem of recovering the labels $ \ell_i $ as well as the estimation problem of recovering the sparse vectors $ β^{(\ell)} $. Our solution to the problem leverages the connection between modern coding theory and statistical inference. We introduce a new algorithm, Mixed-Coloring, which samples the mixture strategically using query vectors $ {x}_i $ constructed based on ideas from sparse graph codes. Our novel code design allows for both efficient demixing and parameter estimation. In the noiseless setting, for a constant number of sparse parameter vectors, our algorithm achieves the order-optimal sample and time complexities of $Θ(K)$. In the presence of Gaussian noise, for the problem with two parameter vectors (i.e., $L=2$), we show that the Robust Mixed-Coloring algorithm achieves near-optimal $Θ(K polylog(n))$ sample and time complexities. When $K=O(n^α)$ for some constant $α\in(0,1)$ (i.e., $K$ is sublinear in $n$), we can achieve sample and time complexities both sublinear in the ambient dimension. In one of our experiments, to recover a mixture of two regressions with dimension $n=500$ and sparsity $K=50$, our algorithm is more than $300$ times faster than EM algorithm, with about one third of its sample cost.
Deep Learning with Domain Adaptation for Accelerated Projection-Reconstruction MR
Venue: arXiv cs.CV 2018
Year: 2018

Purpose: The radial k-space trajectory is a well-established sampling trajectory used in conjunction with magnetic resonance imaging. However, the radial k-space trajectory requires a large number of radial lines for high-resolution reconstruction. Increasing the number of radial lines causes longer acquisition time, making it more difficult for routine clinical use. On the other hand, if we reduce the number of radial lines, streaking artifact patterns are unavoidable. To solve this problem, we propose a novel deep learning approach with domain adaptation to restore high-resolution MR images from under-sampled k-space data. Methods: The proposed deep network removes the streaking artifacts from the artifact corrupted images. To address the situation given the limited available data, we propose a domain adaptation scheme that employs a pre-trained network using a large number of x-ray computed tomography (CT) or synthesized radial MR datasets, which is then fine-tuned with only a few radial MR datasets. Results: The proposed method outperforms existing compressed sensing algorithms, such as the total variation and PR-FOCUSS methods. In addition, the calculation time is several orders of magnitude faster than the total variation and PR-FOCUSS methods.Moreover, we found that pre-training using CT or MR data from similar organ data is more important than pre-training using data from the same modality for different organ. Conclusion: We demonstrate the possibility of a domain-adaptation when only a limited amount of MR data is available. The proposed method surpasses the existing compressed sensing algorithms in terms of the image quality and computation time.
Why Smart Appliances May Result in a Stupid Energy Grid?
Venue: arXiv cs.SY 2018
Year: 2018

This article discusses unexpected consequences of idealistic conceptions about the modernization of power grids. We will focus our analysis on demand-response policies based on automatic decisions by the so-called smart home appliances. Following the usual design approach, each individual appliance has access to a universal signal (e.g. grid frequency or electricity price) that is believed to indicate the system state. Such information is then used as the basis of the appliances' individual decisions. While each single device has a negligible impact in the system, the aggregate effect of the distributed appliances' reactions is expect to bring improvements in the system efficiency; this effect is the demand-response policy goal. The smartness of such an ideal system, composed by isolated appliances with their individual decisions, but connected in the same physical grid, may worsen the system stability. This first-sight undesirable outcome comes as a consequence of synchronization among agents that are subject to the same signal. We argue that this effect is in fact byproduct of methodological choices, which are many times implicit. To support this claim, we employ a different approach that understands the electricity system as constituted by physical, informational and regulatory (networked and structured) layers that cannot be reduced to only one or two of them, but have to be viewed as an organic whole. By classifying its structure under this lens, more appropriate management tools can be designed by looking at the system totality in action. Two examples are provided to illustrate the strength of this modeling.
On squares of cyclic codes
Venue: arXiv cs.IT 2018
Year: 2018

The square $C^{*2}$ of a linear error correcting code $C$ is the linear code spanned by the component-wise products of every pair of (non-necessarily distinct) words in $C$. Squares of codes have gained attention for several applications mainly in the area of cryptography, and typically in those applications one is concerned about some of the parameters (dimension, minimum distance) of both $C^{*2}$ and $C$. In this paper, motivated mostly by the study of this problem in the case of linear codes defined over the binary field, squares of cyclic codes are considered. General results on the minimum distance of the squares of cyclic codes are obtained and constructions of cyclic codes $C$ with relatively large dimension of $C$ and minimum distance of the square $C^{*2}$ are discussed. In some cases, the constructions lead to codes $C$ such that both $C$ and $C^{*2}$ simultaneously have the largest possible minimum distances for their length and dimensions.
Inducing syntactic cut-elimination for indexed nested sequents
Venue: arXiv cs.LO 2018
Year: 2018

The key to the proof-theoretic study of a logic is a proof calculus with a subformula property. Many different proof formalisms have been introduced (e.g. sequent, nested sequent, labelled sequent formalisms) in order to provide such calculi for the many logics of interest. The nested sequent formalism was recently generalised to indexed nested sequents in order to yield proof calculi with the subformula property for extensions of the modal logic K by (Lemmon-Scott) Geach axioms. The proofs of completeness and cut-elimination therein were semantic and intricate. Here we show that derivations in the labelled sequent formalism whose sequents are `almost treelike' correspond exactly to indexed nested sequents. This correspondence is exploited to induce syntactic proofs for indexed nested sequent calculi making use of the elegant proofs that exist for the labelled sequent calculi. A larger goal of this work is to demonstrate how specialising existing proof-theoretic transformations alleviate the need for independent proofs in each formalism. Such coercion can also be used to induce new cutfree calculi. We employ this to present the first indexed nested sequent calculi for intermediate logics.
On the VC-Dimension of Binary Codes
Venue: arXiv cs.IT 2018
Year: 2018

We investigate the asymptotic rates of length-$n$ binary codes with VC-dimension at most $dn$ and minimum distance at least $δn$. Two upper bounds are obtained, one as a simple corollary of a result by Haussler and the other via a shortening approach combining Sauer-Shelah lemma and the linear programming bound. Two lower bounds are given using Gilbert-Varshamov type arguments over constant-weight and Markov-type sets.
Reducing Guesswork via an Unreliable Oracle
Venue: arXiv cs.IT 2018
Year: 2018

Alice holds an random variable $X$, and Bob is trying to guess its value by asking questions of the form "is $X=x$?". Alice answers truthfully and the game terminates once Bob guesses correctly. Before the game begins, Bob is allowed to reach out to an oracle, Carole, and ask her any yes/no question, i.e., a question of the form "is $X\in A$?". Carole is known to lie with a given probability $p$. What should Bob ask Carole if he would like to minimize his expected guessing time? When Carole is always truthful ($p=0$), it is not difficult to check that Bob should order the symbol probabilities in descending order, and ask Carole whether the index of $X$ w.r.t this order is even or odd. We show that this strategy is almost optimal for any lying probability $p$, up to a small additive constant upper bounded by a $1/4$. We discuss a connection to the cutoff rate of the BSC with feedback.
Drawing Planar Graphs with Few Geometric Primitives
Venue: arXiv cs.CG 2018
Year: 2018

We define the \emph{visual complexity} of a plane graph drawing to be the number of basic geometric objects needed to represent all its edges. In particular, one object may represent multiple edges (e.g., one needs only one line segment to draw a path with an arbitrary number of edges). Let $n$ denote the number of vertices of a graph. We show that trees can be drawn with $3n/4$ straight-line segments on a polynomial grid, and with $n/2$ straight-line segments on a quasi-polynomial grid. Further, we present an algorithm for drawing planar 3-trees with $(8n-17)/3$ segments on an $O(n)\times O(n^2)$ grid. This algorithm can also be used with a small modification to draw maximal outerplanar graphs with $3n/2$ edges on an $O(n)\times O(n^2)$ grid. We also study the problem of drawing maximal planar graphs with circular arcs and provide an algorithm to draw such graphs using only $(5n - 11)/3$ arcs. This is significantly smaller than the lower bound of $2n$ for line segments for a nontrivial graph class.
A lattice formulation of the F4 completion procedure
Venue: arXiv cs.SC 2018
Year: 2018

We write a procedure for constructing noncommutative Groebner bases. Reductions are done by particular linear projectors, called reduction operators. The operators enable us to use a lattice construction to reduce simultaneously each S-polynomial into a unique normal form. We write an implementation as well as an example to illustrate our procedure. Moreover, the lattice construction is done by Gaussian elimination, which relates our procedure to the F4 algorithm for constructing commutative Groebner bases.
Using Off-the-Shelf Exception Support Components in C++ Verification
Venue: arXiv cs.SE 2018
Year: 2018

An important step toward adoption of formal methods in software development is support for mainstream programming languages. Unfortunately, these languages are often rather complex and come with substantial standard libraries. However, by choosing a suitable intermediate language, most of the complexity can be delegated to existing execution-oriented (as opposed to verification-oriented) compiler frontends and standard library implementations. In this paper, we describe how support for C++ exceptions can take advantage of the same principle. Our work is based on DiVM, an LLVM-derived, verification-friendly intermediate language. Our implementation consists of 2 parts: an implementation of the `libunwind` platform API which is linked to the program under test and consists of 9 C functions. The other part is a preprocessor for LLVM bitcode which prepares exception-related metadata and replaces associated special-purpose LLVM instructions.
Higher order mobile coverage control with application to localization
Venue: arXiv cs.SY 2018
Year: 2018

Most current results on coverage control using mobile sensors require that one partitioned cell is associated with precisely one sensor. In this paper, we consider a class of coverage control problems involving higher order Voronoi partitions, motivated by applications where more than one sensor is required to monitor and cover one cell. Such applications are frequent in scenarios requiring the sensors to localize targets. We introduce a framework depending on a coverage performance function incorporating higher order Voronoi cells and then design a gradient-based controller which allows the multi-sensor system to achieve a local equilibrium in a distributed manner. The convergence properties are studied and related to Lloyd algorithm. We study also the extension to coverage of a discrete set of points. In addition, we provide a number of real world scenarios where our framework can be applied. Simulation results are also provided to show the controller performance.
Efficient computational strategies to learn the structure of probabilistic graphical models of cumulative phenomena
Venue: arXiv cs.LG 2018
Year: 2018

Structural learning of Bayesian Networks (BNs) is a NP-hard problem, which is further complicated by many theoretical issues, such as the I-equivalence among different structures. In this work, we focus on a specific subclass of BNs, named Suppes-Bayes Causal Networks (SBCNs), which include specific structural constraints based on Suppes' probabilistic causation to efficiently model cumulative phenomena. Here we compare the performance, via extensive simulations, of various state-of-the-art search strategies, such as local search techniques and Genetic Algorithms, as well as of distinct regularization methods. The assessment is performed on a large number of simulated datasets from topologies with distinct levels of complexity, various sample size and different rates of errors in the data. Among the main results, we show that the introduction of Suppes' constraints dramatically improve the inference accuracy, by reducing the solution space and providing a temporal ordering on the variables. We also report on trade-offs among different search techniques that can be efficiently employed in distinct experimental settings. This manuscript is an extended version of the paper "Structural Learning of Probabilistic Graphical Models of Cumulative Phenomena" presented at the 2018 International Conference on Computational Science.
The cognitive roots of regularization in language
Venue: arXiv cs.CL 2018
Year: 2018

Regularization occurs when the output a learner produces is less variable than the linguistic data they observed. In an artificial language learning experiment, we show that there exist at least two independent sources of regularization bias in cognition: a domain-general source based on cognitive load and a domain-specific source triggered by linguistic stimuli. Both of these factors modulate how frequency information is encoded and produced, but only the production-side modulations result in regularization (i.e. cause learners to eliminate variation from the observed input). We formalize the definition of regularization as the reduction of entropy and find that entropy measures are better at identifying regularization behavior than frequency-based analyses. Using our experimental data and a model of cultural transmission, we generate predictions for the amount of regularity that would develop in each experimental condition if the artificial language were transmitted over several generations of learners. Here we find that the effect of cognitive constraints can become more complex when put into the context of cultural evolution: although learning biases certainly carry information about the course of language evolution, we should not expect a one-to-one correspondence between the micro-level processes that regularize linguistic datasets and the macro-level evolution of linguistic regularity.
Towards Efficient Verification of Population Protocols
Venue: arXiv cs.LO 2018
Year: 2018

Population protocols are a well established model of computation by anonymous, identical finite state agents. A protocol is well-specified if from every initial configuration, all fair executions reach a common consensus. The central verification question for population protocols is the well-specification problem: deciding if a given protocol is well-specified. Esparza et al. have recently shown that this problem is decidable, but with very high complexity: it is at least as hard as the Petri net reachability problem, which is EXPSPACE-hard, and for which only algorithms of non-primitive recursive complexity are currently known. In this paper we introduce the class WS3 of well-specified strongly-silent protocols and we prove that it is suitable for automatic verification. More precisely, we show that WS3 has the same computational power as general well-specified protocols, and captures standard protocols from the literature. Moreover, we show that the membership problem for WS3 reduces to solving boolean combinations of linear constraints over N. This allowed us to develop the first software able to automatically prove well-specification for all of the infinitely many possible inputs.
Algorithms for outerplanar graph roots and graph roots of pathwidth at most 2
Venue: arXiv cs.DS 2018
Year: 2018

Deciding whether a given graph has a square root is a classical problem that has been studied extensively both from graph theoretic and from algorithmic perspectives. The problem is NP-complete in general, and consequently substantial effort has been dedicated to deciding whether a given graph has a square root that belongs to a particular graph class. There are both polynomial-time solvable and NP-complete cases, depending on the graph class. We contribute with new results in this direction. Given an arbitrary input graph G, we give polynomial-time algorithms to decide whether G has an outerplanar square root, and whether G has a square root that is of pathwidth at most 2.
Accelerated and Inexact Soft-Impute for Large-Scale Matrix and Tensor Completion
Venue: arXiv cs.NA 2018
Year: 2018

Matrix and tensor completion aim to recover a low-rank matrix / tensor from limited observations and have been commonly used in applications such as recommender systems and multi-relational data mining. A state-of-the-art matrix completion algorithm is Soft-Impute, which exploits the special "sparse plus low-rank" structure of the matrix iterates to allow efficient SVD in each iteration. Though Soft-Impute is a proximal algorithm, it is generally believed that acceleration destroys the special structure and is thus not useful. In this paper, we show that Soft-Impute can indeed be accelerated without comprising this structure. To further reduce the iteration time complexity, we propose an approximate singular value thresholding scheme based on the power method. Theoretical analysis shows that the proposed algorithm still enjoys the fast $O(1/T^2)$ convergence rate of accelerated proximal algorithms. We further extend the proposed algorithm to tensor completion with the scaled latent nuclear norm regularizer. We show that a similar "sparse plus low-rank" structure also exists, leading to low iteration complexity and fast $O(1/T^2)$ convergence rate. Extensive experiments demonstrate that the proposed algorithm is much faster than Soft-Impute and other state-of-the-art matrix and tensor completion algorithms.
Robust Transceiver Design for Reciprocal M*N Interference Channel Based on Statistical Linearization Approximation
Venue: arXiv cs.IT 2018
Year: 2018

This paper focuses on robust transceiver design for throughput enhancement on the interference channel (IC), under imperfect channel state information (CSI). In this paper, two algorithms are proposed to improve the throughput of the multi-input multi-output (MIMO) IC. Each transmitter and receiver has respectively M and N antennas and IC operates in a time division duplex mode. In the first proposed algorithm, each transceiver adjusts its filter to maximize the expected value of signal-to-interference-plus-noise ratio (SINR). On the other hand, the second algorithm tries to minimize the variances of the SINRs to hedge against the variability due to CSI error. Taylor expansion is exploited to approximate the effect of CSI imperfection on mean and variance. The proposed robust algorithms utilize the reciprocity of wireless networks to optimize the estimated statistical properties in two different working modes. Monte Carlo simulations are employed to investigate sum rate performance of the proposed algorithms and the advantage of incorporating variation minimization into the transceiver design.