OpenRaiser/Intern-Atlas huggingface dataset:
Succinct Hitting Sets and Barriers to Proving Algebraic Circuits Lower Bounds
Venue: arXiv cs.CC 2018
Year: 2018

We formalize a framework of algebraically natural lower bounds for algebraic circuits. Just as with the natural proofs notion of Razborov and Rudich for boolean circuit lower bounds, our notion of algebraically natural lower bounds captures nearly all lower bound techniques known. However, unlike the boolean setting, there has been no concrete evidence demonstrating that this is a barrier to obtaining super-polynomial lower bounds for general algebraic circuits, as there is little understanding whether algebraic circuits are expressive enough to support "cryptography" secure against algebraic circuits. Following a similar result of Williams in the boolean setting, we show that the existence of an algebraic natural proofs barrier is equivalent to the existence of succinct derandomization of the polynomial identity testing problem. That is, whether the coefficient vectors of polylog(N)-degree polylog(N)-size circuits is a hitting set for the class of poly(N)-degree poly(N)-size circuits. Further, we give an explicit universal construction showing that if such a succinct hitting set exists, then our universal construction suffices. Further, we assess the existing literature constructing hitting sets for restricted classes of algebraic circuits and observe that none of them are succinct as given. Yet, we show how to modify some of these constructions to obtain succinct hitting sets. This constitutes the first evidence supporting the existence of an algebraic natural proofs barrier. Our framework is similar to the Geometric Complexity Theory (GCT) program of Mulmuley and Sohoni, except that here we emphasize constructiveness of the proofs while the GCT program emphasizes symmetry. Nevertheless, our succinct hitting sets have relevance to the GCT program as they imply lower bounds for the complexity of the defining equations of polynomials computed by small circuits.
A Pliable Index Coding Approach to Data Shuffling
Venue: arXiv cs.IT 2018
Year: 2018

A promising research area that has recently emerged, is on how to use index coding to improve the communication efficiency in distributed computing systems, especially for data shuffling in iterative computations. In this paper, we posit that pliable index coding can offer a more efficient framework for data shuffling, as it can better leverage the many possible shuffling choices to reduce the number of transmissions. We theoretically analyze pliable index coding under data shuffling constraints, and design a hierarchical data-shuffling scheme that uses pliable coding as a component. We find benefits up to $O(ns/m)$ over index coding, where $ns/m$ is the average number of workers caching a message, and $m$, $n$, and $s$ are the numbers of messages, workers, and cache size, respectively.
Pseudo-Wigner Matrices
Venue: arXiv cs.IT 2018
Year: 2018

We consider the problem of generating pseudo-random matrices based on the similarity of their spectra to Wigner's semicircular law. We introduce the notion of an r-independent pseudo-Wigner matrix ensemble and prove closeness of the spectra of its matrices to the semicircular density in the Kolmogorov distance. We give an explicit construction of a family of N by N pseudo-Wigner ensembles using dual BCH codes and show that the Kolmogorov complexity of the obtained matrices is of the order of log(N) bits for a fixed designed Kolmogorov distance precision. We compare our construction to the quasi-random graphs introduced by Chung, Graham and Wilson and demonstrate that the pseudo-Wigner matrices pass stronger randomness tests than the adjacency matrices of these graphs (lifted by the mapping 0 -> 1 and 1 -> -1) do. Finally, we provide numerical simulations verifying our theoretical results.
Algorithm for an arbitrary-order cumulant tensor calculation in a sliding window of data streams
Venue: arXiv cs.DS 2018
Year: 2018

High order cumulant tensors carry information about statistics of non-normally distributed multivariate data. In this work we present a new efficient algorithm for calculation of cumulants of arbitrary order in a sliding window for data streams. We showed that this algorithms enables speedups of cumulants updates compared to current algorithms. This algorithm can be used for processing on-line high-frequency multivariate data and can find applications in, e.g., on-line signal filtering and classification of data streams. To present an application of this algorithm, we propose an estimator of non-Gaussianity of a data stream based on the norms of high-order cumulant tensors. We show how to detect the transition from Gaussian distributed data to non-Gaussian ones in a~data stream. In order to achieve high implementation efficiency of operations on super-symmetric tensors, such as cumulant tensors, we employ the block structure to store and calculate only one hyper-pyramid part of such tensors.
Speech Map: A Statistical Multimodal Atlas of 4D Tongue Motion During Speech from Tagged and Cine MR Images
Venue: arXiv cs.CV 2018
Year: 2018

Quantitative measurement of functional and anatomical traits of 4D tongue motion in the course of speech or other lingual behaviors remains a major challenge in scientific research and clinical applications. Here, we introduce a statistical multimodal atlas of 4D tongue motion using healthy subjects, which enables a combined quantitative characterization of tongue motion in a reference anatomical configuration. This atlas framework, termed Speech Map, combines cine- and tagged-MRI in order to provide both the anatomic reference and motion information during speech. Our approach involves a series of steps including (1) construction of a common reference anatomical configuration from cine-MRI, (2) motion estimation from tagged-MRI, (3) transformation of the motion estimations to the reference anatomical configuration, and (4) computation of motion quantities such as Lagrangian strain. Using this framework, the anatomic configuration of the tongue appears motionless, while the motion fields and associated strain measurements change over the time course of speech. In addition, to form a succinct representation of the high-dimensional and complex motion fields, principal component analysis is carried out to characterize the central tendencies and variations of motion fields of our speech tasks. Our proposed method provides a platform to quantitatively and objectively explain the differences and variability of tongue motion by illuminating internal motion and strain that have so far been intractable. The findings are used to understand how tongue function for speech is limited by abnormal internal motion and strain in glossectomy patients.
Large Scale Novel Object Discovery in 3D
Venue: arXiv cs.CV 2018
Year: 2018

We present a method for discovering never-seen-before objects in 3D point clouds obtained from sensors like Microsoft Kinect. We generate supervoxels directly from the point cloud data and use them with a Siamese network, built on a recently proposed 3D convolutional neural network architecture. We use known objects to train a non-linear embedding of supervoxels, by optimizing the criteria that supervoxels which fall on the same object should be closer than those which fall on different objects, in the embedding space. We test on unknown objects, which were not seen during training, and perform clustering in the learned embedding space of supervoxels to effectively perform novel object discovery. We validate the method with extensive experiments, quantitatively showing that it can discover numerous unseen objects while being trained on only a few dense 3D models. We also show very good qualitative results of object discovery in point cloud data when the test objects, either specific instances or even categories, were never seen during training.
DroidStar: Callback Typestates for Android Classes
Venue: arXiv cs.LO 2018
Year: 2018

Event-driven programming frameworks, such as Android, are based on components with asynchronous interfaces. The protocols for interacting with these components can often be described by finite-state machines we dub *callback typestates*. Callback typestates are akin to classical typestates, with the difference that their outputs (callbacks) are produced asynchronously. While useful, these specifications are not commonly available, because writing them is difficult and error-prone. Our goal is to make the task of producing callback typestates significantly easier. We present a callback typestate assistant tool, DroidStar, that requires only limited user interaction to produce a callback typestate. Our approach is based on an active learning algorithm, L*. We improved the scalability of equivalence queries (a key component of L*), thus making active learning tractable on the Android system. We use DroidStar to learn callback typestates for Android classes both for cases where one is already provided by the documentation, and for cases where the documentation is unclear. The results show that DroidStar learns callback typestates accurately and efficiently. Moreover, in several cases, the synthesized callback typestates uncovered surprising and undocumented behaviors.
Double-sided probing by map of Asplund's distances using Logarithmic Image Processing in the framework of Mathematical Morphology
Venue: arXiv cs.CV 2018
Year: 2018

We establish the link between Mathematical Morphology and the map of Asplund's distances between a probe and a grey scale function, using the Logarithmic Image Processing scalar multiplication. We demonstrate that the map is the logarithm of the ratio between a dilation and an erosion of the function by a structuring function: the probe. The dilations and erosions are mappings from the lattice of the images into the lattice of the positive functions. Using a flat structuring element, the expression of the map of Asplund's distances can be simplified with a dilation and an erosion of the image; these mappings stays in the lattice of the images. We illustrate our approach by an example of pattern matching with a non-flat structuring function.
Deconvolution and Restoration of Optical Endomicroscopy Images
Venue: arXiv cs.CV 2018
Year: 2018

Optical endomicroscopy (OEM) is an emerging technology platform with preclinical and clinical imaging applications. Pulmonary OEM via fibre bundles has the potential to provide in vivo, in situ molecular signatures of disease such as infection and inflammation. However, enhancing the quality of data acquired by this technique for better visualization and subsequent analysis remains a challenging problem. Cross coupling between fiber cores and sparse sampling by imaging fiber bundles are the main reasons for image degradation, and poor detection performance (i.e., inflammation, bacteria, etc.). In this work, we address the problem of deconvolution and restoration of OEM data. We propose a hierarchical Bayesian model to solve this problem and compare three estimation algorithms to exploit the resulting joint posterior distribution. The first method is based on Markov chain Monte Carlo (MCMC) methods, however, it exhibits a relatively long computational time. The second and third algorithms deal with this issue and are based on a variational Bayes (VB) approach and an alternating direction method of multipliers (ADMM) algorithm respectively. Results on both synthetic and real datasets illustrate the effectiveness of the proposed methods for restoration of OEM images.
A homotopy-theoretic model of function extensionality in the effective topos
Venue: arXiv cs.LO 2018
Year: 2018

We present a way of constructing a Quillen model structure on a full subcategory of an elementary topos, starting with an interval object with connections and a certain dominance. The advantage of this method is that it does not require the underlying topos to be cocomplete. The resulting model category structure gives rise to a model of homotopy type theory with identity types, $Σ$- and $Π$-types, and functional extensionality. We apply the method to the effective topos with the interval object $\nabla 2$. In the resulting model structure we identify uniform inhabited objects as contractible objects, and show that discrete objects are fibrant. Moreover, we show that the unit of the discrete reflection is a homotopy equivalence and the homotopy category of fibrant assemblies is equivalent to the category of modest sets. We compare our work with the path object category construction on the effective topos by Jaap van Oosten.
Extensional Semantics for Higher-Order Logic Programs with Negation
Venue: arXiv cs.LO 2018
Year: 2018

We develop an extensional semantics for higher-order logic programs with negation, generalizing the technique that was introduced in [Bezem99,Bezem01] for positive higher-order programs. In this way we provide an alternative extensional semantics for higher-order logic programs with negation to the one proposed in [CharalambidisER14]. As an immediate useful consequence of our developments, we define for the language we consider the notions of stratification and local stratification, which generalize the familiar such notions from classical logic programming. We demonstrate that for stratified and locally stratified higher-order logic programs, the proposed semantics never assigns the unknown truth value. We conclude the paper by providing a negative result: we demonstrate that the well-known stable model semantics of classical logic programming, if extended according to the technique of [Bezem99,Bezem01] to higher-order logic programs, does not in general lead to extensional stable models.
Weighted omega-Restricted One Counter Automata
Venue: arXiv cs.FL 2018
Year: 2018

Let $S$ be a complete star-omega semiring and $Σ$ be an alphabet. For a weighted $ω$-restricted one-counter automaton $\mathcal{C}$ with set of states $\{1, \dots, n\}$, $n \geq 1$, we show that there exists a mixed algebraic system over a complete semiring-semimodule pair ${((S \ll Σ^* \gg)^{n\times n}, (S \ll Σ^ω\gg)^n)}$ such that the behavior $\Vert\mathcal{C} \Vert$ of $\mathcal{C}$ is a component of a solution of this system. In case the basic semiring is $\mathbb{B}$ or $\mathbb{N}^{\infty}$ we show that there exists a mixed context-free grammar that generates $\Vert\mathcal{C} \Vert$. The construction of the mixed context-free grammar from $\mathcal{C}$ is a generalization of the well-known triple construction in case of restricted one-counter automata and is called now triple-pair construction for $ω$-restricted one-counter automata.
Pushing for weighted tree automata
Venue: arXiv cs.FL 2018
Year: 2018

A weight normalization procedure, commonly called pushing, is introduced for weighted tree automata (wta) over commutative semifields. The normalization preserves the recognized weighted tree language even for nondeterministic wta, but it is most useful for bottom-up deterministic wta, where it can be used for minimization and equivalence testing. In both applications a careful selection of the weights to be redistributed followed by normalization allows a reduction of the general problem to the corresponding problem for bottom-up deterministic unweighted tree automata. This approach was already successfully used by Mohri and Eisner for the minimization of deterministic weighted string automata. Moreover, the new equivalence test for two wta $M$ and $M'$ runs in time $\mathcal O((\lvert M \rvert + \lvert M'\rvert) \cdot \log {(\lvert Q\rvert + \lvert Q'\rvert)})$, where $Q$ and $Q'$ are the states of $M$ and $M'$, respectively, which improves the previously best run-time $\mathcal O(\lvert M \rvert \cdot \lvert M'\rvert)$.
Chromatic bounds for some classes of $2K_2$-free graphs
Venue: arXiv cs.DM 2018
Year: 2018

A hereditary class $\mathcal{G}$ of graphs is $χ$-bounded if there is a $χ$-binding function, say $f$ such that $χ(G) \leq f(ω(G))$, for every $G \in \cal{G}$, where $χ(G)$ ($ω(G)$) denote the chromatic (clique) number of $G$. It is known that for every $2K_2$-free graph $G$, $χ(G) \leq \binom{ω(G)+1}{2}$, and the class of ($2K_2, 3K_1$)-free graphs does not admit a linear $χ$-binding function. In this paper, we are interested in classes of $2K_2$-free graphs that admit a linear $χ$-binding function. We show that the class of ($2K_2, H$)-free graphs, where $H\in \{K_1+P_4, K_1+C_4, \overline{P_2\cup P_3}, HVN, K_5-e, K_5\}$ admits a linear $χ$-binding function. Also, we show that some superclasses of $2K_2$-free graphs are $χ$-bounded.
Eye-Movement behavior identification for AD diagnosis
Venue: arXiv cs.NE 2018
Year: 2018

In the present work, we develop a deep-learning approach for differentiating the eye-movement behavior of people with neurodegenerative diseases over healthy control subjects during reading well-defined sentences. We define an information compaction of the eye-tracking data of subjects without and with probable Alzheimer's disease when reading a set of well-defined, previously validated, sentences including high-, low-predictable sentences, and proverbs. Using this information we train a set of denoising sparse-autoencoders and build a deep neural network with these and a softmax classifier. Our results are very promising and show that these models may help to understand the dynamics of eye movement behavior and its relationship with underlying neuropsychological correlates.
Primitivity, Uniform Minimality and State Complexity of Boolean Operations
Venue: arXiv cs.FL 2018
Year: 2018

A minimal deterministic finite automaton (DFA) is uniformly minimal if it always remains minimal when the final state set is replaced by a non-empty proper subset of the state set. We prove that a permutation DFA is uniformly minimal if and only if its transition monoid is a primitive group. We use this to study boolean operations on group languages, which are recognized by direct products of permutation DFAs. A direct product cannot be uniformly minimal, except in the trivial case where one of the DFAs in the product is a one-state DFA. However, non-trivial direct products can satisfy a weaker condition we call uniform boolean minimality, where only final state sets used to recognize boolean operations are considered. We give sufficient conditions for a direct product of two DFAs to be uniformly boolean minimal, which in turn gives sufficient conditions for pairs of group languages to have maximal state complexity under all binary boolean operations ("maximal boolean complexity"). In the case of permutation DFAs with one final state, we give necessary and sufficient conditions for pairs of group languages to have maximal boolean complexity. Our results demonstrate a connection between primitive groups and automata with strong minimality properties.
Ray tracing method for stereo image synthesis using CUDA
Venue: arXiv cs.GR 2018
Year: 2018

This paper presents a realization of the approach to spatial 3D stereo of visualization of 3D images with use parallel Graphics processing unit (GPU). The experiments of realization of synthesis of images of a 3D stage by a method of trace of beams on GPU with Compute Unified Device Architecture (CUDA) have shown that 60 % of the time is spent for the decision of a computing problem approximately, the major part of time (40 %) is spent for transfer of data between the central processing unit and GPU for computations and the organization process of visualization. The study of the influence of increase in the size of the GPU network at the speed of computations showed importance of the correct task of structure of formation of the parallel computer network and general mechanism of parallelization. Keywords: Volumetric 3D visualization, stereo 3D visualization, ray tracing, parallel computing on GPU, CUDA
Self-Sustainability of Energy Harvesting Systems: Concept, Analysis, and Design
Venue: arXiv cs.IT 2018
Year: 2018

Ambient energy harvesting is touted as a low cost solution to prolong the life of low-powered devices, reduce the carbon footprint, and make the system self-sustainable. Most research to date have focused either on the physical aspects of energy conversion process or on optimal consumption policy of the harvested energy at the system level. However, although intuitively understood, to the best of our knowledge, the idea of self-sustainability is yet to be made precise and studied as a performance metric. In this paper, we provide a mathematical definition of the concept of self-sustainability of an energy harvesting system, based on the complementary idea of eventual outage. In particular, we analyze the harvest-store-consume system with infinite battery capacity, stochastic energy arrivals, and fixed energy consumption rate. Using the random walk theory, we identify the necessary condition for the system to be self-sustainable. General formulas are given for the self-sustainability probability in the form of integral equations. Since these integral equations are difficult to solve analytically, an exponential upper bound for eventual outage probability is given using martingales. This bound guarantees that the eventual outage probability can be made arbitrarily small simply by increasing the initial battery energy. We also give an asymptotic formula for eventual outage. For the special case when the energy arrival follows a Poisson process, we are able to find the exact formulas for the eventual outage probability. We also show that the harvest-store-consume system is mathematically equivalent to a $GI/G/1$ queueing system, which allows us to easily find the outage probability, in case the necessary condition for self-sustainability is violated. Monte-Carlo simulations verify our analysis.
A Structural and Nominal Syntax for Diagrams
Venue: arXiv cs.PL 2018
Year: 2018

The correspondence between monoidal categories and graphical languages of diagrams has been studied extensively, leading to applications in quantum computing and communication, systems theory, circuit design and more. From the categorical perspective, diagrams can be specified using (name-free) combinators which enjoy elegant equational properties. However, conventional notations for diagrammatic structures, such as hardware description languages (VHDL, Verilog) or graph languages (Dot), use a different style, which is flat, relational, and reliant on extensive use of names (labels). Such languages are not known to enjoy nice syntactic equational properties. However, since they make it relatively easy to specify (and modify) arbitrary diagrammatic structures they are more popular than the combinator style. In this paper we show how the two approaches to diagram syntax can be reconciled and unified in a way that does not change the semantics and the existing equational theory. Additionally, we give sound and complete equational theories for the combined syntax.