OpenRaiser/Intern-Atlas huggingface dataset:
Broadband DOA estimation using Convolutional neural networks trained with noise signals
Venue: arXiv cs.SD 2017
Year: 2017

A convolution neural network (CNN) based classification method for broadband DOA estimation is proposed, where the phase component of the short-time Fourier transform coefficients of the received microphone signals are directly fed into the CNN and the features required for DOA estimation are learnt during training. Since only the phase component of the input is used, the CNN can be trained with synthesized noise signals, thereby making the preparation of the training data set easier compared to using speech signals. Through experimental evaluation, the ability of the proposed noise trained CNN framework to generalize to speech sources is demonstrated. In addition, the robustness of the system to noise, small perturbations in microphone positions, as well as its ability to adapt to different acoustic conditions is investigated using experiments with simulated and real data.
Adaptive Noise Cancellation Using Deep Cerebellar Model Articulation Controller
Venue: arXiv cs.SY 2017
Year: 2017

This paper proposes a deep cerebellar model articulation controller (DCMAC) for adaptive noise cancellation (ANC). We expand upon the conventional CMAC by stacking sin-gle-layer CMAC models into multiple layers to form a DCMAC model and derive a modified backpropagation training algorithm to learn the DCMAC parameters. Com-pared with conventional CMAC, the DCMAC can characterize nonlinear transformations more effectively because of its deep structure. Experimental results confirm that the pro-posed DCMAC model outperforms the CMAC in terms of residual noise in an ANC task, showing that DCMAC provides enhanced modeling capability based on channel characteristics.
Robust reputation-based ranking on multipartite rating networks
Venue: arXiv cs.IR 2017
Year: 2017

The spread of online reviews, ratings and opinions and its growing influence on people's behavior and decisions boosted the interest to extract meaningful information from this data deluge. Hence, crowdsourced ratings of products and services gained a critical role in business, governments, and others. We propose a new reputation-based ranking system utilizing multipartite rating subnetworks, that clusters users by their similarities, using Kolmogorov complexity. Our system is novel in that it reflects a diversity of opinions/preferences by assigning possibly distinct rankings, for the same item, for different groups of users. We prove the convergence and efficiency of the system and show that it copes better with spamming/spurious users, and it is more robust to attacks than state-of-the-art approaches.
Stochastic Geometric Coverage Analysis in mmWave Cellular Networks with a Realistic Channel Model
Venue: arXiv cs.NI 2017
Year: 2017

Millimeter-wave (mmWave) bands have been attracting growing attention as a possible candidate for next-generation cellular networks, since the available spectrum is orders of magnitude larger than in current cellular allocations. To precisely design mmWave systems, it is important to examine mmWave interference and SIR coverage under large-scale deployments. For this purpose, we apply an accurate mmWave channel model, derived from experiments, into an analytical framework based on stochastic geometry. In this way we obtain a closed-form SIR coverage probability in large-scale mmWave cellular networks.
Robust Location-Aided Beam Alignment in Millimeter Wave Massive MIMO
Venue: arXiv cs.IT 2017
Year: 2017

Location-aided beam alignment has been proposed recently as a potential approach for fast link establishment in millimeter wave (mmWave) massive MIMO (mMIMO) communications. However, due to mobility and other imperfections in the estimation process, the spatial information obtained at the base station (BS) and the user (UE) is likely to be noisy, degrading beam alignment performance. In this paper, we introduce a robust beam alignment framework in order to exhibit resilience with respect to this problem. We first recast beam alignment as a decentralized coordination problem where BS and UE seek coordination on the basis of correlated yet individual position information. We formulate the optimum beam alignment solution as the solution of a Bayesian team decision problem. We then propose a suite of algorithms to approach optimality with reduced complexity. The effectiveness of the robust beam alignment procedure, compared with classical designs, is then verified on simulation settings with varying location information accuracies.
Visual Attribute Transfer through Deep Image Analogy
Venue: arXiv cs.CV 2017
Year: 2017

We propose a new technique for visual attribute transfer across images that may have very different appearance but have perceptually similar semantic structure. By visual attribute transfer, we mean transfer of visual information (such as color, tone, texture, and style) from one image to another. For example, one image could be that of a painting or a sketch while the other is a photo of a real scene, and both depict the same type of scene. Our technique finds semantically-meaningful dense correspondences between two input images. To accomplish this, it adapts the notion of "image analogy" with features extracted from a Deep Convolutional Neutral Network for matching; we call our technique Deep Image Analogy. A coarse-to-fine strategy is used to compute the nearest-neighbor field for generating the results. We validate the effectiveness of our proposed method in a variety of cases, including style/texture transfer, color/style swap, sketch/painting to photo, and time lapse.
Influence of Reviewer Interaction Network on Long-term Citations: A Case Study of the Scientific Peer-Review System of the Journal of High Energy Physics
Venue: arXiv cs.DL 2017
Year: 2017

A `peer-review system' in the context of judging research contributions, is one of the prime steps undertaken to ensure the quality of the submissions received, a significant portion of the publishing budget is spent towards successful completion of the peer-review by the publication houses. Nevertheless, the scientific community is largely reaching a consensus that peer-review system, although indispensable, is nonetheless flawed. A very pertinent question therefore is "could this system be improved?". In this paper, we attempt to present an answer to this question by considering a massive dataset of around $29k$ papers with roughly $70k$ distinct review reports together consisting of $12m$ lines of review text from the Journal of High Energy Physics (JHEP) between 1997 and 2015. In specific, we introduce a novel \textit{reviewer-reviewer interaction network} (an edge exists between two reviewers if they were assigned by the same editor) and show that surprisingly the simple structural properties of this network such as degree, clustering coefficient, centrality (closeness, betweenness etc.) serve as strong predictors of the long-term citations (i.e., the overall scientific impact) of a submitted paper. These features, when plugged in a regression model, alone achieves a high $R^2$ of \0.79 and a low $RMSE$ of 0.496 in predicting the long-term citations. In addition, we also design a set of supporting features built from the basic characteristics of the submitted papers, the authors and the referees (e.g., the popularity of the submitting author, the acceptance rate history of a referee, the linguistic properties laden in the text of the review reports etc.), which further results in overall improvement with $R^2$ of 0.81 and $RMSE$ of 0.46.
Summarized Network Behavior Prediction
Venue: arXiv cs.LG 2017
Year: 2017

This work studies the entity-wise topical behavior from massive network logs. Both the temporal and the spatial relationships of the behavior are explored with the learning architectures combing the recurrent neural network (RNN) and the convolutional neural network (CNN). To make the behavioral data appropriate for the spatial learning in CNN, several reduction steps are taken to form the topical metrics and place them homogeneously like pixels in the images. The experimental result shows both the temporal- and the spatial- gains when compared to a multilayer perceptron (MLP) network. A new learning framework called spatially connected convolutional networks (SCCN) is introduced to more efficiently predict the behavior.
Revisiting Parametricity: Inductives and Uniformity of Propositions
Venue: arXiv cs.LO 2017
Year: 2017

Reynold's parametricity theory captures the property that parametrically polymorphic functions behave uniformly: they produce related results on related instantiations. In dependently-typed programming languages, such relations and uniformity proofs can be expressed internally, and generated as a program translation. We present a new parametricity translation for a significant fragment of Coq. Previous translations of parametrically polymorphic propositions allowed non-uniformity. For example, on related instantiations, a function may return propositions that are logically inequivalent (e.g. True and False). We show that uniformity of polymorphic propositions is not achievable in general. Nevertheless, our translation produces proofs that the two propositions are logically equivalent and also that any two proofs of those propositions are related. This is achieved at the cost of potentially requiring more assumptions on the instantiations, requiring them to be isomorphic in the worst case. Our translation augments the previous one for Coq by carrying and compositionally building extra proofs about parametricity relations. It is made easier by a new method for translating inductive types and pattern matching. The new method builds upon and generalizes previous such translations for dependently-typed programming languages. Using reification and reflection, we have implemented our translation as Coq programs. We obtain several stronger free theorems applicable to an ongoing compiler-correctness project. Previously, proofs of some of these theorems took several hours to finish.
Resource Allocation for Elastic Optical Networks using Geometric Optimization
Venue: arXiv cs.IT 2017
Year: 2017

Resource allocation with quality of service constraints is one of the most challenging problems in elastic optical networks which is normally formulated as an MINLP optimization program. In this paper, we focus on novel properties of geometric optimization and provide a heuristic approach for resource allocation which is very faster than its MINLP counterpart. Our heuristic consists of two main parts for routing/traffic ordering and power/spectrum assignment. It aims at minimization of transmitted optical power and spectrum usage constrained to quality of service and physical requirements. We consider three routing/traffic ordering procedures and compare them in terms of total transmitted optical power, total received noise power and total nonlinear interference including self- and cross-channel interferences. We propose a posynomial expression for optical signal to noise ratio in which fiber nonlinearities and spontaneous emission noise have been addressed. We also propose posynomial expressions that relate modulation spectral efficiency to its corresponding minimum required optical signal to noise ratio. We then use the posynomial expressions to develop six geometric formulations for power/spectrum assignment part of the heuristic which are different in run time, complexity and accuracy. Simulation results demonstrate that the proposed solution has a very good accuracy and much lower computational complexity in comparison with MINLP formulation. As example for European Cost239 optical network with 46 transmit transponders, the geometric formulations can be more than 59 times faster than its MINLP counterpart. Numerical results also reveal that in long-haul elastic optical networks, considering the product of the number of common fiber spans and the transmission bit rate is a better goal function for routing/traffic ordering sub-problem.
The Lovász Theta Function for Random Regular Graphs and Community Detection in the Hard Regime
Venue: arXiv cs.CC 2017
Year: 2017

We derive upper and lower bounds on the degree $d$ for which the Lovász $\vartheta$ function, or equivalently sum-of-squares proofs with degree two, can refute the existence of a $k$-coloring in random regular graphs $G_{n,d}$. We show that this type of refutation fails well above the $k$-colorability transition, and in particular everywhere below the Kesten-Stigum threshold. This is consistent with the conjecture that refuting $k$-colorability, or distinguishing $G_{n,d}$ from the planted coloring model, is hard in this region. Our results also apply to the disassortative case of the stochastic block model, adding evidence to the conjecture that there is a regime where community detection is computationally hard even though it is information-theoretically possible. Using orthogonal polynomials, we also provide explicit upper bounds on $\vartheta(\overline{G})$ for regular graphs of a given girth, which may be of independent interest.
A Versatile, Sound Tool for Simplifying Definitions
Venue: arXiv cs.PL 2017
Year: 2017

We present a tool, simplify-defun, that transforms the definition of a given function into a simplified definition of a new function, providing a proof checked by ACL2 that the old and new functions are equivalent. When appropriate it also generates termination and guard proofs for the new function. We explain how the tool is engineered so that these proofs will succeed. Examples illustrate its utility, in particular for program transformation in synthesis and verification.
Term-Level Reasoning in Support of Bit-blasting
Venue: arXiv cs.LO 2017
Year: 2017

GL is a verified tool for proving ACL2 theorems using Boolean methods such as BDD reasoning and satisfiability checking. In its typical operation, GL recursively traverses a term, computing a symbolic object representing the value of each subterm. In older versions of GL, such a symbolic object could use Boolean functions to compactly represent many possible values for integer and Boolean subfields, but otherwise needed to reflect the concrete structure of all possiblealues that its term might take. When a term has many possible values that can't share such a representation, this can easily cause blowups because GL must then case-split. To address this problem, we have added several features to GL that allow it to reason about term-like symbolic objects using various forms of rewriting. These features allow GL to be programmed with rules much like the ACL2 rewriter, so that users may choose a better normal form for terms for which the default, value-like representation would otherwise cause case explosions. In this paper we describe these new features; as a motivating example, we show how to program the rewriter to reason effectively about the theory of records.
Super-Resolution of Wavelet-Encoded Images
Venue: arXiv cs.CV 2017
Year: 2017

Multiview super-resolution image reconstruction (SRIR) is often cast as a resampling problem by merging non-redundant data from multiple low-resolution (LR) images on a finer high-resolution (HR) grid, while inverting the effect of the camera point spread function (PSF). One main problem with multiview methods is that resampling from nonuniform samples (provided by LR images) and the inversion of the PSF are highly nonlinear and ill-posed problems. Non-linearity and ill-posedness are typically overcome by linearization and regularization, often through an iterative optimization process, which essentially trade off the very same information (i.e. high frequency) that we want to recover. We propose a novel point of view for multiview SRIR: Unlike existing multiview methods that reconstruct the entire spectrum of the HR image from the multiple given LR images, we derive explicit expressions that show how the high-frequency spectra of the unknown HR image are related to the spectra of the LR images. Therefore, by taking any of the LR images as the reference to represent the low-frequency spectra of the HR image, one can reconstruct the super-resolution image by focusing only on the reconstruction of the high-frequency spectra. This is very much like single-image methods, which extrapolate the spectrum of one image, except that we rely on information provided by all other views, rather than by prior constraints as in single-image methods (which may not be an accurate source of information). This is made possible by deriving and applying explicit closed-form expressions that define how the local high frequency information that we aim to recover for the reference high resolution image is related to the local low frequency information in the sequence of views. Results and comparisons with recently published state-of-the-art methods show the superiority of the proposed solution.
Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks
Venue: arXiv cs.LO 2017
Year: 2017

We present an approach for the verification of feed-forward neural networks in which all nodes have a piece-wise linear activation function. Such networks are often used in deep learning and have been shown to be hard to verify for modern satisfiability modulo theory (SMT) and integer linear programming (ILP) solvers. The starting point of our approach is the addition of a global linear approximation of the overall network behavior to the verification problem that helps with SMT-like reasoning over the network behavior. We present a specialized verification algorithm that employs this approximation in a search process in which it infers additional node phases for the non-linear nodes in the network from partial node phase assignments, similar to unit propagation in classical SAT solving. We also show how to infer additional conflict clauses and safe node fixtures from the results of the analysis steps performed during the search. The resulting approach is evaluated on collision avoidance and handwritten digit recognition case studies.
Linear complexity of Legendre-polynomial quotients
Venue: arXiv cs.CR 2017
Year: 2017

We continue to investigate binary sequence $(f_u)$ over $\{0,1\}$ defined by $(-1)^{f_u}=\left(\frac{(u^w-u^{wp})/p}{p}\right)$ for integers $u\ge 0$, where $\left(\frac{\cdot}{p}\right)$ is the Legendre symbol and we restrict $\left(\frac{0}{p}\right)=1$. In an earlier work, the linear complexity of $(f_u)$ was determined for $w=p-1$ under the assumption of $2^{p-1}\not\equiv 1 \pmod {p^2}$. In this work, we give possible values on the linear complexity of $(f_u)$ for all $1\le w<p-1$ under the same conditions. We also state that the case of larger $w(\geq p)$ can be reduced to that of $0\leq w\leq p-1$.
Covering Small Independent Sets and Separators with Applications to Parameterized Algorithms
Venue: arXiv cs.DS 2017
Year: 2017

We present two new combinatorial tools for the design of parameterized algorithms. The first is a simple linear time randomized algorithm that given as input a $d$-degenerate graph $G$ and an integer $k$, outputs an independent set $Y$, such that for every independent set $X$ in $G$ of size at most $k$, the probability that $X$ is a subset of $Y$ is at least $\left({(d+1)k \choose k} \cdot k(d+1)\right)^{-1}$.The second is a new (deterministic) polynomial time graph sparsification procedure that given a graph $G$, a set $T = \{\{s_1, t_1\}, \{s_2, t_2\}, \ldots, \{s_\ell, t_\ell\}\}$ of terminal pairs and an integer $k$, returns an induced subgraph $G^\star$ of $G$ that maintains all the inclusion minimal multicuts of $G$ of size at most $k$, and does not contain any $(k+2)$-vertex connected set of size $2^{{\cal O}(k)}$. In particular, $G^\star$ excludes a clique of size $2^{{\cal O}(k)}$ as a topological minor. Put together, our new tools yield new randomized fixed parameter tractable (FPT) algorithms for Stable $s$-$t$ Separator, Stable Odd Cycle Transversal and Stable Multicut on general graphs, and for Stable Directed Feedback Vertex Set on $d$-degenerate graphs, resolving two problems left open by Marx et al. [ACM Transactions on Algorithms, 2013]. All of our algorithms can be derandomized at the cost of a small overhead in the running time.
A Nonlinear Model Predictive Control Scheme for Cooperative Manipulation with Singularity and Collision Avoidance
Venue: arXiv cs.RO 2017
Year: 2017

This paper addresses the problem of cooperative transportation of an object rigidly grasped by $N$ robotic agents. In particular, we propose a Nonlinear Model Predictive Control (NMPC) scheme that guarantees the navigation of the object to a desired pose in a bounded workspace with obstacles, while complying with certain input saturations of the agents. Moreover, the proposed methodology ensures that the agents do not collide with each other or with the workspace obstacles as well as that they do not pass through singular configurations. The feasibility and convergence analysis of the NMPC are explicitly provided. Finally, simulation results illustrate the validity and efficiency of the proposed method.
Distributed Proportional-Fairness Control in MicroGrids via Blockchain Smart Contracts
Venue: arXiv cs.MA 2017
Year: 2017

Residential microgrids (MGs) may host a large number of Distributed Energy Resources (DERs). The strategy that maximizes the revenue for each individual DER is the one in which the DER operates at capacity, injecting all available power into the grid. However, when the DER penetration is high and the consumption low, this strategy may lead to power surplus that causes voltage increase over recommended limits. In order to create incentives for the DER to operate below capacity, we propose a proportional-fairness control strategy in which (i) a subset of DERs decrease their own power output, sacrificing the individual revenue, and (ii) the DERs in the subset are dynamically selected based on the record of their control history. The trustworthy implementation of the scheme is carried out through a custom-designed blockchain mechanism that maintains a distributed database trusted by all DERs. In particular, the blockchain is used to stipulate and store a smart contract that enforces proportional fairness. The simulation results verify the potential of the proposed framework.
On Tackling the Limits of Resolution in SAT Solving
Venue: arXiv cs.LO 2017
Year: 2017

The practical success of Boolean Satisfiability (SAT) solvers stems from the CDCL (Conflict-Driven Clause Learning) approach to SAT solving. However, from a propositional proof complexity perspective, CDCL is no more powerful than the resolution proof system, for which many hard examples exist. This paper proposes a new problem transformation, which enables reducing the decision problem for formulas in conjunctive normal form (CNF) to the problem of solving maximum satisfiability over Horn formulas. Given the new transformation, the paper proves a polynomial bound on the number of MaxSAT resolution steps for pigeonhole formulas. This result is in clear contrast with earlier results on the length of proofs of MaxSAT resolution for pigeonhole formulas. The paper also establishes the same polynomial bound in the case of modern core-guided MaxSAT solvers. Experimental results, obtained on CNF formulas known to be hard for CDCL SAT solvers, show that these can be efficiently solved with modern MaxSAT solvers.