OpenRaiser/Intern-Atlas huggingface dataset:
Analysis of One-Bit Quantized Precoding for the Multiuser Massive MIMO Downlink
Venue: arXiv cs.IT 2016
Year: 2016

We present a mathematical analysis of linear precoders for downlink massive MIMO multiuser systems that employ one-bit digital-to-analog converters at the basestation in order to reduce complexity and mitigate power usage. The analysis is based on the Bussgang theorem, and applies generally to any linear precoding scheme. We examine in detail the special case of the quantized zero-forcing (ZF) precoder, and derive a simple asymptotic expression for the resulting symbol error rate at each terminal. Our analysis illustrates that the performance of the quantized ZF precoder depends primarily on the ratio of the number of antennas to the number of users, and our simulations show that it can outperform the much more complicated maximum likelihood encoder for low-to-moderate signal to noise ratios, where massive MIMO systems are presumed to operate. We also use the Bussgang theorem to derive a new linear precoder optimized for the case of one-bit quantization, and illustrate its improved performance.
Multispectral image denoising with optimized vector non-local mean filter
Venue: arXiv cs.CV 2016
Year: 2016

Nowadays, many applications rely on images of high quality to ensure good performance in conducting their tasks. However, noise goes against this objective as it is an unavoidable issue in most applications. Therefore, it is essential to develop techniques to attenuate the impact of noise, while maintaining the integrity of relevant information in images. We propose in this work to extend the application of the Non-Local Means filter (NLM) to the vector case and apply it for denoising multispectral images. The objective is to benefit from the additional information brought by multispectral imaging systems. The NLM filter exploits the redundancy of information in an image to remove noise. A restored pixel is a weighted average of all pixels in the image. In our contribution, we propose an optimization framework where we dynamically fine tune the NLM filter parameters and attenuate its computational complexity by considering only pixels which are most similar to each other in computing a restored pixel. Filter parameters are optimized using Stein's Unbiased Risk Estimator (SURE) rather than using ad hoc means. Experiments have been conducted on multispectral images corrupted with additive white Gaussian noise and PSNR and similarity comparison with other approaches are provided to illustrate the efficiency of our approach in terms of both denoising performance and computation complexity.
End-to-End Training Approaches for Discriminative Segmental Models
Venue: arXiv cs.CL 2016
Year: 2016

Recent work on discriminative segmental models has shown that they can achieve competitive speech recognition performance, using features based on deep neural frame classifiers. However, segmental models can be more challenging to train than standard frame-based approaches. While some segmental models have been successfully trained end to end, there is a lack of understanding of their training under different settings and with different losses. We investigate a model class based on recent successful approaches, consisting of a linear model that combines segmental features based on an LSTM frame classifier. Similarly to hybrid HMM-neural network models, segmental models of this class can be trained in two stages (frame classifier training followed by linear segmental model weight training), end to end (joint training of both frame classifier and linear weights), or with end-to-end fine-tuning after two-stage training. We study segmental models trained end to end with hinge loss, log loss, latent hinge loss, and marginal log loss. We consider several losses for the case where training alignments are available as well as where they are not. We find that in general, marginal log loss provides the most consistent strong performance without requiring ground-truth alignments. We also find that training with dropout is very important in obtaining good performance with end-to-end training. Finally, the best results are typically obtained by a combination of two-stage training and fine-tuning.
Two Stage Optimization with Recourse and Revocation
Venue: arXiv cs.DS 2016
Year: 2016

Two-stage optimization with recourse model is an important and widely used model, which has been studied extensively these years. In this article, we will look at a new variant of it, called the two-stage optimization with recourse and revocation model. This new model differs from the traditional one in that one is allowed to revoke some of his earlier decisions and withdraw part of the earlier costs, which is not unlikely in many real applications, and is therefore considered to be more realistic under many situations. We will adopt several approaches to study this model. In fact, we will develop an LP rounding scheme for some cover problems and show that they can be solved using this scheme and an adaptation of the rounding approach for the deterministic counterpart, provided the polynomial scenario assumption. Stochastic uncapacitated facility location problem will also be studied to show that the approximation algorithm that worked for the two-stage with recourse model worked for this model as well. In addition, we will use other methods to study the model.
A New Simulation Approach to Performance Evaluation of Binary Linear Codes in the Extremely Low Error Rate Region
Venue: arXiv cs.IT 2016
Year: 2016

In this paper, the sphere bound (SB) is revisited within a general bounding framework based on nested Gallager regions. The equivalence is revealed between the SB proposed by Herzberg and Poltyrev and the SB proposed by Kasami et al., whereas the latter was rarely cited in the literatures. Interestingly and importantly, the derivation of the SB based on nested Gallager regions suggests us a new simulation approach to performance evaluation of binary linear codes over additive white Gaussian noise (AWGN) channels. In order for the performance evaluation, the proposed approach decouples the geometrical structure of the code from the noise statistics. The former specifies the conditional error probabilities, which are independent of signal-to-noise ratios (SNRs) and can be simulated and estimated efficiently, while the latter determines the probabilities of those conditions, which involve SNRs and can be calculated numerically. Numerical results show that the proposed simulation approach matches well with the traditional simulation approach in the high error rate region but is able to evaluate efficiently the performance in the extremely low error rate region.
Automating Induction for Solving Horn Clauses
Venue: arXiv cs.PL 2016
Year: 2016

Verification problems of programs written in various paradigms (such as imperative, logic, concurrent, functional, and object-oriented ones) can be reduced to problems of solving Horn clause constraints on predicate variables that represent unknown inductive invariants. This paper presents a novel Horn constraint solving method based on inductive theorem proving: the method reduces Horn constraint solving to validity checking of first-order formulas with inductively defined predicates, which are then checked by induction on the derivation of the predicates. To automate inductive proofs, we introduce a novel proof system tailored to Horn constraint solving and use an SMT solver to discharge proof obligations arising in the proof search. The main advantage of the proposed method is that it can verify relational specifications across programs in various paradigms where multiple function calls need to be analyzed simultaneously. The class of specifications includes practically important ones such as functional equivalence, associativity, commutativity, distributivity, monotonicity, idempotency, and non-interference. Furthermore, our novel combination of Horn clause constraints with inductive theorem proving enables us to naturally and automatically axiomatize recursive functions that are possibly non-terminating, non-deterministic, higher-order, exception-raising, and over non-inductively defined data types. We have implemented a relational verification tool for the OCaml functional language based on the proposed method and obtained promising results in preliminary experiments.
Spark Level Sparsity and the $\ell_1$ Tail Minimization
Venue: arXiv cs.IT 2016
Year: 2016

Solving compressed sensing problems relies on the properties of sparse signals. It is commonly assumed that the sparsity s needs to be less than one half of the spark of the sensing matrix A, and then the unique sparsest solution exists, and recoverable by $\ell_1$-minimization or related procedures. We discover, however, a measure theoretical uniqueness exists for nearly spark-level sparsity from compressed measurements Ax = b. Specifically, suppose A is of full spark with m rows, and suppose $\frac{m}{2}$ < s < m. Then the solution to Ax = b is unique for x with $\|x\|_0 \leq s$ up to a set of measure 0 in every s-sparse plane. This phenomenon is observed and confirmed by an $\ell_1$-tail minimization procedure, which recovers sparse signals uniquely with s > $\frac{m}{2}$ in thousands and thousands of random tests. We further show instead that the mere $\ell_1$-minimization would actually fail if s > $\frac{m}{2}$ even from the same measure theoretical point of view.
Population estimation from mobile network traffic metadata
Venue: arXiv cs.NI 2016
Year: 2016

Smartphones and other mobile devices are today pervasive across the globe. As an interesting side effect of the surge in mobile communications, mobile network operators can now easily collect a wealth of high-resolution data on the habits of large user populations. The information extracted from mobile network traffic data is very relevant in the context of population mapping: it provides a tool for the automatic and live estimation of population densities, overcoming the limitations of traditional data sources such as censuses and surveys. In this paper, we propose a new approach to infer population densities at urban scales, based on aggregated mobile network traffic metadata. Our approach allows estimating both static and dynamic populations, achieves a significant improvement in terms of accuracy with respect to state-of-the-art solutions in the literature, and is validated on different city scenarios.
Multitask Learning of Vegetation Biochemistry from Hyperspectral Data
Venue: arXiv cs.CV 2016
Year: 2016

Statistical models have been successful in accurately estimating the biochemical contents of vegetation from the reflectance spectra. However, their performance deteriorates when there is a scarcity of sizable amount of ground truth data for modeling the complex non-linear relationship occurring between the spectrum and the biochemical quantity. We propose a novel Gaussian process based multitask learning method for improving the prediction of a biochemical through the transfer of knowledge from the learned models for predicting related biochemicals. This method is most advantageous when there are few ground truth data for the biochemical of interest, but plenty of ground truth data for related biochemicals. The proposed multitask Gaussian process hypothesizes that the inter-relationship between the biochemical quantities is better modeled by using a combination of two or more covariance functions and inter-task correlation matrices. In the experiments, our method outperformed the current methods on two real-world datasets.
Local Maxima and Improved Exact Algorithm for MAX-2-SAT
Venue: arXiv cs.DS 2016
Year: 2016

Given a MAX-2-SAT instance, we define a local maximum to be an assignment such that changing any single variable reduces the number of satisfied clauses. We consider the question of the number of local maxima that an instance of MAX-2-SAT can have. We give upper bounds in both the sparse and nonsparse case, where the sparse case means that there is a bound $d$ on the average number of clauses involving any given variable. The bounds in the nonsparse case are tight up to polylogarithmic factors, while in the sparse case the bounds are tight up to a multiplicative factor in $d$ for large $d$. Additionally, we generalize to the question of assignments which are maxima up to changing $k> 1$ variables simultaneously; in this case, we give explicit constructions with large (in a sense explained below) numbers of such maxima in the sparse case. The basic idea of the upper bound proof is to consider a random assignment to some subset of the variables and determine the probability that some fraction of the remaining variables can be fixed without considering interactions between them. The bounded results hold in the case of weighted MAX-2-SAT as well. Using this technique and combining with ideas from Ref. 6, we find an algorithm for weighted MAX-2-SAT which is faster for large $d$ than previous algorithms which use polynomial space; this algorithm does require an additional bounds on maximum weights and degree.
Developing and Assessing MATLAB Exercises for Active Concept Learning
Venue: arXiv cs.CY 2016
Year: 2016

New technologies, such as MOOCs, provide innovative methods to tackle new challenges in teaching and learning, such as globalization and changing contemporary culture and to remove the limits of conventional classrooms. However, they also bring challenges in course delivery and assessment, due to factors such as less direct student-instructor interaction. These challenges are especially severe in engineering education, which relies heavily on experiential learning, such as computer simulations and laboratory exercises, to assist students in understanding concepts. As a result, effective design of experiential learning components is extremely critical for engineering MOOCs. In this paper, we will share our experience gained through developing and offering a MOOC on communication systems, with special focus on the development and assessment of MATLAB exercises for active concept learning. Our approach introduced students to concepts using learning components commonly provided by many MOOC platforms (e.g., online lectures and quizzes), and augmented the student experience with MATLAB based computer simulations and exercises to enable more concrete and detailed understanding of the material. We describe here a systematic approach to MATLAB problem design and assessment, based on our experience with the MATLAB server provided by MathWorks and integrated with the edX MOOC platform. We discuss the effectiveness of the instructional methods as evaluated through students' learning performance. We analyze the impact of the course design tools from both the instructor and the student perspective.
Bounded embeddings of graphs in the plane
Venue: arXiv cs.CG 2016
Year: 2016

A drawing in the plane ($\mathbb{R}^2$) of a graph $G=(V,E)$ equipped with a function $γ: V \rightarrow \mathbb{N}$ is \emph{$x$-bounded} if (i) $x(u) <x(v)$ whenever $γ(u)<γ(v)$ and (ii) $γ(u)\leqγ(w)\leq γ(v)$, where $uv\in E$ and $γ(u)\leq γ(v)$, whenever $x(w)\in x(uv)$, where $x(.)$ denotes the projection to the $x$-axis. We prove a characterization of isotopy classes of graph embeddings in the plane containing an $x$-bounded embedding. Then we present an efficient algorithm, that relies on our result, for testing the existence of an $x$-bounded embedding if the given graph is a tree or generalized $Θ$-graph. This partially answers a question raised recently by Angelini et al. and Chang et al., and proves that c-planarity testing of flat clustered graphs with three clusters is tractable if each connected component of the underlying abstract graph is a tree.
Two are Better than One: An Ensemble of Retrieval- and Generation-Based Dialog Systems
Venue: arXiv cs.CL 2016
Year: 2016

Open-domain human-computer conversation has attracted much attention in the field of NLP. Contrary to rule- or template-based domain-specific dialog systems, open-domain conversation usually requires data-driven approaches, which can be roughly divided into two categories: retrieval-based and generation-based systems. Retrieval systems search a user-issued utterance (called a query) in a large database, and return a reply that best matches the query. Generative approaches, typically based on recurrent neural networks (RNNs), can synthesize new replies, but they suffer from the problem of generating short, meaningless utterances. In this paper, we propose a novel ensemble of retrieval-based and generation-based dialog systems in the open domain. In our approach, the retrieved candidate, in addition to the original query, is fed to an RNN-based reply generator, so that the neural model is aware of more information. The generated reply is then fed back as a new candidate for post-reranking. Experimental results show that such ensemble outperforms each single part of it by a large margin.
3D Hand Pose Tracking and Estimation Using Stereo Matching
Venue: arXiv cs.CV 2016
Year: 2016

3D hand pose tracking/estimation will be very important in the next generation of human-computer interaction. Most of the currently available algorithms rely on low-cost active depth sensors. However, these sensors can be easily interfered by other active sources and require relatively high power consumption. As a result, they are currently not suitable for outdoor environments and mobile devices. This paper aims at tracking/estimating hand poses using passive stereo which avoids these limitations. A benchmark with 18,000 stereo image pairs and 18,000 depth images captured from different scenarios and the ground-truth 3D positions of palm and finger joints (obtained from the manual label) is thus proposed. This paper demonstrates that the performance of the state-of-the art tracking/estimation algorithms can be maintained with most stereo matching algorithms on the proposed benchmark, as long as the hand segmentation is correct. As a result, a novel stereo-based hand segmentation algorithm specially designed for hand tracking/estimation is proposed. The quantitative evaluation demonstrates that the proposed algorithm is suitable for the state-of-the-art hand pose tracking/estimation algorithms and the tracking quality is comparable to the use of active depth sensors under different challenging scenarios.
Are mmWave Low-Complexity Beamforming Structures Energy-Efficient? Analysis of the Downlink MU-MIMO
Venue: arXiv cs.IT 2016
Year: 2016

Future cellular systems based on the use of above-6 GHz frequencies, the so-called millimeter wave (mmWave) bandwidths, will heavily rely on the use of antenna arrays both at the transmitter and at the receiver, possibly with a large number of elements. For complexity reasons, fully digital precoding and postcoding structures may turn out to be unfeasible, and thus suboptimal structures, making use of simplified hardware and a limited number of RF chains, have been investigated. This paper considers and makes a comparative assessment, both from a spectral efficiency and energy efficiency point of view, of several suboptimal precoding and postcoding beamforming structures for the downlink of a cellular multiuser MIMO (MU-MIMO) system. Based on the most recently available data for the energy consumption of phase shifters and switches, we show that there are cases where fully-digital beamformers may achieve a larger energy efficiency than lower-complexity solutions, as well as that structures based on the exclusive use of switches achieve quite unsatisfactory performance in realistic scenarios.
A Rate-Distortion Approach to Caching
Venue: arXiv cs.IT 2016
Year: 2016

This paper takes a rate-distortion approach to understanding the information-theoretic laws governing cache-aided communications systems. Specifically, we characterise the optimal tradeoffs between the delivery rate, cache capacity and reconstruction distortions for a single-user problem and some special cases of a two-user problem. Our analysis considers discrete memoryless sources, expected- and excess-distortion constraints, and separable and f-separable distortion functions. We also establish a strong converse for separable-distortion functions, and we show that lossy versions of common information (Gács-Körner and Wyner) play an important role in caching. Finally, we illustrate and explicitly evaluate these laws for multivariate Gaussian sources and binary symmetric sources.
Introduction: Cognitive Issues in Natural Language Processing
Venue: arXiv cs.CL 2016
Year: 2016

This special issue is dedicated to get a better picture of the relationships between computational linguistics and cognitive science. It specifically raises two questions: "what is the potential contribution of computational language modeling to cognitive science?" and conversely: "what is the influence of cognitive science in contemporary computational linguistics?"
Simplification of Multi-Scale Geometry using Adaptive Curvature Fields
Venue: arXiv cs.GR 2016
Year: 2016

We present a novel algorithm to compute multi-scale curvature fields on triangle meshes. Our algorithm is based on finding robust mean curvatures using the ball neighborhood, where the radius of a ball corresponds to the scale of the features. The essential problem is to find a good radius for each ball to obtain a reliable curvature estimation. We propose an algorithm that finds suitable radii in an automatic way. In particular, our algorithm is applicable to meshes produced by image-based reconstruction systems. These meshes often contain geometric features at various scales, for example if certain regions have been captured in greater detail. We also show how such a multi-scale curvature field can be converted to a density field and used to guide applications like mesh simplification.
Record Counting in Historical Handwritten Documents with Convolutional Neural Networks
Venue: arXiv cs.CV 2016
Year: 2016

In this paper, we investigate the use of Convolutional Neural Networks for counting the number of records in historical handwritten documents. With this work we demonstrate that training the networks only with synthetic images allows us to perform a near perfect evaluation of the number of records printed on historical documents. The experiments have been performed on a benchmark dataset composed by marriage records and outperform previous results on this dataset.
From Event-B to Verified C via HLL
Venue: arXiv cs.SE 2016
Year: 2016

This work addresses the correct translation of an Event-B model to C code via an intermediate formal language, HLL. The proof of correctness follows two main steps. First, the final refinement of the Event-B model, including invariants, is translated to HLL. At that point, additional properties (e.g., deadlock-freeness, liveness properties, etc.) are added to the HLL model. The proof of the invariants and additional properties at the HLL level guarantees the correctness of the translation. Second, the C code is automatically generated from the HLL model for most of the system functions and manually for the remaining ones; in this case, the HLL model provides formal contracts to the software developer. An equivalence proof between the C code and the HLL model guarantees the correctness of the code.