OpenRaiser/Intern-Atlas huggingface dataset:
Functional Synthesis via Input-Output Separation
Venue: arXiv cs.LO 2018
Year: 2018

Boolean functional synthesis is the process of constructing a Boolean function from a Boolean specification that relates input and output variables. Despite significant recent developments in synthesis algorithms, Boolean functional synthesis remains a challenging problem even when state-of-the-art methods are used for decomposing the specification. In this work we bring a fresh decomposition approach, orthogonal to existing methods, that explores the decomposition of the specification into separate input and output components. We make use of an input-output decomposition of a given specification described as a CNF formula, by alternatingly analyzing the separate input and output components. We exploit well-defined properties of these components to ultimately synthesize a solution for the entire specification. We first provide a theoretical result that, for input components with specific structures, synthesis for CNF formulas via this framework can be performed more efficiently than in the general case. We then show by experimental evaluations that our algorithm performs well also in practice on instances which are challenging for existing state-of-the-art tools, serving as a good complement to modern synthesis techniques.
Congruence based proofs of the recognizability theorems for free many-sorted algebras
Venue: arXiv cs.FL 2018
Year: 2018

We generalize several recognizability theorems for free single-sorted algebras to the field of many-sorted algebras and provide, in a uniform way and without using neither regular tree grammars nor tree automata, purely algebraic proofs of them based on the concept of congruence.
LMI-Based Reset Unknown Input Observer for State Estimation of Linear Uncertain Systems
Venue: arXiv cs.SY 2018
Year: 2018

This paper proposes a novel kind of Unknown Input Observer (UIO) called Reset Unknown Input Observer (R-UIO) for state estimation of linear systems in the presence of disturbance using Linear Matrix Inequality (LMI) techniques. In R-UIO, the states of the observer are reset to the after-reset value based on an appropriate reset law in order to decrease the $L_2$ norm and settling time of estimation error. It is shown that the application of the reset theory to the UIOs in the LTI framework can significantly improve the transient response of the observer. Moreover, the devised approach can be applied to both SISO and MIMO systems. Furthermore, the stability and convergence analysis of the devised R-UIO is addressed. Finally, the efficiency of the proposed method is demonstrated by simulation results.
Adaptive Grey-Box Fuzz-Testing with Thompson Sampling
Venue: arXiv cs.AI 2018
Year: 2018

Fuzz testing, or "fuzzing," refers to a widely deployed class of techniques for testing programs by generating a set of inputs for the express purpose of finding bugs and identifying security flaws. Grey-box fuzzing, the most popular fuzzing strategy, combines light program instrumentation with a data driven process to generate new program inputs. In this work, we present a machine learning approach that builds on AFL, the preeminent grey-box fuzzer, by adaptively learning a probability distribution over its mutation operators on a program-specific basis. These operators, which are selected uniformly at random in AFL and mutational fuzzers in general, dictate how new inputs are generated, a core part of the fuzzer's efficacy. Our main contributions are two-fold: First, we show that a sampling distribution over mutation operators estimated from training programs can significantly improve performance of AFL. Second, we introduce a Thompson Sampling, bandit-based optimization approach that fine-tunes the mutator distribution adaptively, during the course of fuzzing an individual program. A set of experiments across complex programs demonstrates that tuning the mutational operator distribution generates sets of inputs that yield significantly higher code coverage and finds more crashes faster and more reliably than both baseline versions of AFL as well as other AFL-based learning approaches.
High Quality Facial Surface and Texture Synthesis via Generative Adversarial Networks
Venue: arXiv cs.CG 2018
Year: 2018

In the past several decades, many attempts have been made to model synthetic realistic geometric data. The goal of such models is to generate plausible 3D geometries and textures. Perhaps the best known of its kind is the linear 3D morphable model (3DMM) for faces. Such models can be found at the core of many computer vision applications such as face reconstruction, recognition and authentication to name just a few. Generative adversarial networks (GANs) have shown great promise in imitating high dimensional data distributions. State of the art GANs are capable of performing tasks such as image to image translation as well as auditory and image signal synthesis, producing novel plausible samples from the data distribution at hand. Geometric data is generally more difficult to process due to the inherent lack of an intrinsic parametrization. By bringing geometric data into an aligned space, we are able to map the data onto a 2D plane using a universal parametrization. This alignment process allows for efficient processing of digitally scanned geometric data via image processing tools. Using this methodology, we propose a novel face synthesis model for generation of realistic facial textures together with their corresponding geometry. A GAN is employed in order to imitate the space of parametrized human textures, while corresponding facial geometries are generated by learning the best 3DMM coefficients for each texture. The generated textures are mapped back onto the corresponding geometries to obtain new generated high resolution 3D faces.
Consensus-Before-Talk: Distributed Dynamic Spectrum Access via Distributed Spectrum Ledger Technology
Venue: arXiv cs.DC 2018
Year: 2018

This paper proposes Consensus-Before-Talk (CBT), a spectrum etiquette architecture leveraged by distributed ledger technology (DLT). In CBT, secondary users' spectrum access requests reach a consensus in a distributed way, thereby enabling collision-free distributed dynamic spectrum access. To achieve this consensus, the secondary users need to pay for the extra request exchanging delays. Incorporating the consensus delay, the end-to-end latency under CBT is investigated. Both the latency analysis and numerical evaluation validate that the proposed CBT achieves the lower end-to-end latency particularly under severe secondary user traffic, compared to the Listen-Before-Talk (LBT) benchmark scheme.
Stochastic Collocation with Non-Gaussian Correlated Parameters via a New Quadrature Rule
Venue: arXiv cs.NA 2018
Year: 2018

This paper generalizes stochastic collocation methods to handle correlated non-Gaussian random parameters. The key challenge is to perform a multivariate numerical integration in a correlated parameter space when computing the coefficient of each basis function via a projection step. We propose an optimization model and a block coordinate descent solver to compute the required quadrature samples. Our method is verified with a CMOS ring oscillator and an optical ring resonator, showing 3000x speedup over Monte Carlo.
MADARi: A Web Interface for Joint Arabic Morphological Annotation and Spelling Correction
Venue: arXiv cs.CL 2018
Year: 2018

In this paper, we introduce MADARi, a joint morphological annotation and spelling correction system for texts in Standard and Dialectal Arabic. The MADARi framework provides intuitive interfaces for annotating text and managing the annotation process of a large number of sizable documents. Morphological annotation includes indicating, for a word, in context, its baseword, clitics, part-of-speech, lemma, gloss, and dialect identification. MADARi has a suite of utilities to help with annotator productivity. For example, annotators are provided with pre-computed analyses to assist them in their task and reduce the amount of work needed to complete it. MADARi also allows annotators to query a morphological analyzer for a list of possible analyses in multiple dialects or look up previously submitted analyses. The MADARi management interface enables a lead annotator to easily manage and organize the whole annotation process remotely and concurrently. We describe the motivation, design and implementation of this interface; and we present details from a user study working with this system.
The Complexity of $(Δ+ 1)$Coloring inCongested Clique, Massively Parallel Computation,and Centralized Local Computation
Venue: arXiv cs.DS 2018
Year: 2018

We present new randomized algorithms that improve the complexity of the classic $(Δ+1)$-coloring problem, and its generalization $(Δ+1)$-list-coloring, in three well-studied models of distributed, parallel, and centralized computation: Distributed Congested Clique: We present an $O(1)$-round randomized algorithm for $(Δ+1)$-list coloring in the congested clique model of distributed computing. This settles the asymptotic complexity of this problem. It moreover improves upon the $O(\log^\ast Δ)$-round randomized algorithms of Parter and Su [DISC'18] and $O((\log\log Δ)\cdot \log^\ast Δ)$-round randomized algorithm of Parter [ICALP'18]. Massively Parallel Computation: We present a $(Δ+1)$-list coloring algorithm with round complexity $O(\sqrt{\log\log n})$ in the Massively Parallel Computation (MPC) model with strongly sublinear memory per machine. This algorithm uses a memory of $O(n^α)$ per machine, for any desirable constant $α>0$, and a total memory of $\widetilde{O}(m)$, where $m$ is the size of the graph. Notably, this is the first coloring algorithm with sublogarithmic round complexity, in the sublinear memory regime of MPC. For the quasilinear memory regime of MPC, an $O(1)$-round algorithm was given very recently by Assadi et al. [SODA'19]. Centralized Local Computation: We show that $(Δ+1)$-list coloring can be solved with $Δ^{O(1)} \cdot O(\log n)$ query complexity, in the centralized local computation model. The previous state-of-the-art for $(Δ+1)$-list coloring in the centralized local computation model are based on simulation of known LOCAL algorithms.
A Tutorial on Modular Ontology Modeling with Ontology Design Patterns: The Cooking Recipes Ontology
Venue: arXiv cs.AI 2018
Year: 2018

We provide a detailed example for modular ontology modeling based on ontology design patterns.
Painting Outside the Box: Image Outpainting with GANs
Venue: arXiv cs.CV 2018
Year: 2018

The challenging task of image outpainting (extrapolation) has received comparatively little attention in relation to its cousin, image inpainting (completion). Accordingly, we present a deep learning approach based on Iizuka et al. for adversarially training a network to hallucinate past image boundaries. We use a three-phase training schedule to stably train a DCGAN architecture on a subset of the Places365 dataset. In line with Iizuka et al., we also use local discriminators to enhance the quality of our output. Once trained, our model is able to outpaint $128 \times 128$ color images relatively realistically, thus allowing for recursive outpainting. Our results show that deep learning approaches to image outpainting are both feasible and promising.
Energy Efficient and Fair Resource Allocation for LTE-Unlicensed Uplink Networks: A Two-sided Matching Approach with Partial Information
Venue: arXiv cs.IT 2018
Year: 2018

LTE-Unlicensed (LTE-U) has recently attracted worldwide interest to meet the explosion in cellular traffic data. By using carrier aggregation (CA), licensed and unlicensed bands are integrated to enhance transmission capacity while maintaining reliable and predictable performance. As there may exist other conventional unlicensed band users, such as Wi-Fi users, LTE-U users have to share the same unlicensed bands with them. Thus, an optimized resource allocation scheme to ensure the fairness between LTE-U users and conventional unlicensed band users is critical for the deployment of LTE-U networks. In this paper, we investigate an energy efficient resource allocation problem in LTE-U coexisting with other wireless networks, which aims at guaranteeing fairness among the users of different radio access networks (RANs). We formulate the problem as a multi-objective optimization problem and propose a semi-distributed matching framework with a partial information-based algorithm to solve it. We demonstrate our contributions with simulations in which various network densities and traffic load levels are considered.
Efficient Single Image Super Resolution using Enhanced Learned Group Convolutions
Venue: arXiv cs.CV 2018
Year: 2018

Convolutional Neural Networks (CNNs) have demonstrated great results for the single-image super-resolution (SISR) problem. Currently, most CNN algorithms promote deep and computationally expensive models to solve SISR. However, we propose a novel SISR method that uses relatively less number of computations. On training, we get group convolutions that have unused connections removed. We have refined this system specifically for the task at hand by removing unnecessary modules from original CondenseNet. Further, a reconstruction network consisting of deconvolutional layers has been used in order to upscale to high resolution. All these steps significantly reduce the number of computations required at testing time. Along with this, bicubic upsampled input is added to the network output for easier learning. Our model is named SRCondenseNet. We evaluate the method using various benchmark datasets and show that it performs favourably against the state-of-the-art methods in terms of both accuracy and number of computations required.
Spectral Efficiency Analysis of Multi-Cell Massive MIMO Systems with Ricean Fading
Venue: arXiv cs.IT 2018
Year: 2018

This paper investigates the spectral efficiency of multi-cell massive multiple-input multiple-output systems with Ricean fading that utilize the linear maximal-ratio combining detector. We firstly present closed-form expressions for the effective signal-to-interference-plus-noise ratio (SINR) with the least squares and minimum mean squared error (MMSE) estimation methods, respectively, which apply for any number of base-station antennas $M$ and any Ricean $K$-factor. Also, the obtained results can be particularized in Rayleigh fading conditions when the Ricean $K$-factor is equal to zero. In the following, novel exact asymptotic expressions of the effective SINR are derived in the high $M$ and high Ricean $K$-factor regimes. The corresponding analysis shows that pilot contamination is removed by the MMSE estimator when we consider both infinite $M$ and infinite Ricean $K$-factor, while the pilot contamination phenomenon persists for the rest of cases. All the theoretical results are verified via Monte-Carlo simulations.
A MapReduce based Big-data Framework for Object Extraction from Mosaic Satellite Images
Venue: arXiv cs.DC 2018
Year: 2018

We propose a framework stitching of vector representations of large scale raster mosaic images in distributed computing model. In this way, the negative effect of the lack of resources of the central system and scalability problem can be eliminated. The product obtained by this study can be used in applications requiring spatial and temporal analysis on big satellite map images. This study also shows that big data frameworks are not only used in applications of text-based data mining and machine learning algorithms, but also used in applications of algorithms in image processing. The effectiveness of the product realized with this project is also going to be proven by scalability and performance tests performed on real world LandSat-8 satellite images.
Scale Drift Correction of Camera Geo-Localization using Geo-Tagged Images
Venue: arXiv cs.CV 2018
Year: 2018

Camera geo-localization from a monocular video is a fundamental task for video analysis and autonomous navigation. Although 3D reconstruction is a key technique to obtain camera poses, monocular 3D reconstruction in a large environment tends to result in the accumulation of errors in rotation, translation, and especially in scale: a problem known as scale drift. To overcome these errors, we propose a novel framework that integrates incremental structure from motion (SfM) and a scale drift correction method utilizing geo-tagged images, such as those provided by Google Street View. Our correction method begins by obtaining sparse 6-DoF correspondences between the reconstructed 3D map coordinate system and the world coordinate system, by using geo-tagged images. Then, it corrects scale drift by applying pose graph optimization over Sim(3) constraints and bundle adjustment. Experimental evaluations on large-scale datasets show that the proposed framework not only sufficiently corrects scale drift, but also achieves accurate geo-localization in a kilometer-scale environment.
Trustworthy and Privacy-Aware Sensing for Internet of Things
Venue: arXiv cs.CR 2018
Year: 2018

The Internet of Things (IoT) is considered as the key enabling technology for smart services. Security and privacy are particularly open challenges for IoT applications due to the widespread use of commodity devices. This work introduces two hardware-based lightweight security mechanisms to ensure sensed data trustworthiness (i.e., sensed data protection and sensor node protection) and usage privacy of the sensors (i.e., privacy-aware reporting of the sensed data) for centralized and decentralized IoT applications. Physically unclonable functions (PUF) form the basis of both proposed mechanisms. To demonstrate the feasibility of our PUF-based approach, we have implemented and evaluated PUFs on three platforms (Atmel 8-bit MCU, ARM Cortex M4 32 bit MCU, and Zynq7010 SoC) with varying complexities. We have also implemented our trusted sensing and privacy-aware reporting scheme (for centralized applications) and secure node scheme (for decentralized applications) on a visual sensor node comprising an OV5642 image sensor and a Zynq7010 SoC. Our experimental evaluation shows a low overhead wrt.~latency, storage, hardware, and communication incurred by our security mechanisms.
Analyzing Learned Representations of a Deep ASR Performance Prediction Model
Venue: arXiv cs.CL 2018
Year: 2018

This paper addresses a relatively new task: prediction of ASR performance on unseen broadcast programs. In a previous paper, we presented an ASR performance prediction system using CNNs that encode both text (ASR transcript) and speech, in order to predict word error rate. This work is dedicated to the analysis of speech signal embeddings and text embeddings learnt by the CNN while training our prediction model. We try to better understand which information is captured by the deep model and its relation with different conditioning factors. It is shown that hidden layers convey a clear signal about speech style, accent and broadcast type. We then try to leverage these 3 types of information at training time through multi-task learning. Our experiments show that this allows to train slightly more efficient ASR performance prediction systems that - in addition - simultaneously tag the analyzed utterances according to their speech style, accent and broadcast program origin.
Considerations on Quantum-Based Methods for Communication Security
Venue: arXiv cs.CR 2018
Year: 2018

In this paper we provide an intuitive-level discussion of the challenges and opportunities offered by quantum-based methods for supporting secure communications, e.g., over a network. The goal is to distill down to the most fundamental issues and concepts in order to provide a clear foundation for assessing the potential value of quantum-based technologies relative to classical alternatives. It is hoped that this form of exposition can provide greater clarity of perspective than is typically offered by mathematically-focused treatments of the topic. It is also hoped that this clarity extends to more general applications of quantum information science such as quantum computing and quantum sensing.
Ensemble Learning Applied to Classify GPS Trajectories of Birds into Male or Female
Venue: arXiv cs.LG 2018
Year: 2018

We describe our first-place solution to the Animal Behavior Challenge (ABC 2018) on predicting gender of bird from its GPS trajectory. The task consisted in predicting the gender of shearwater based on how they navigate themselves across a big ocean. The trajectories are collected from GPS loggers attached on shearwaters' body, and represented as a variable-length sequence of GPS points (latitude and longitude), and associated meta-information, such as the sun azimuth, the sun elevation, the daytime, the elapsed time on each GPS location after starting the trip, the local time (date is trimmed), and the indicator of the day starting the from the trip. We used ensemble of several variants of Gradient Boosting Classifier along with Gaussian Process Classifier and Support Vector Classifier after extensive feature engineering and we ranked first out of 74 registered teams. The variants of Gradient Boosting Classifier we tried are CatBoost (Developed by Yandex), LightGBM (Developed by Microsoft), XGBoost (Developed by Distributed Machine Learning Community). Our approach could easily be adapted to other applications in which the goal is to predict a classification output from a variable-length sequence.
Autonomous Driving without a Burden: View from Outside with Elevated LiDAR
Venue: arXiv cs.AI 2018
Year: 2018

The current autonomous driving architecture places a heavy burden in signal processing for the graphics processing units (GPUs) in the car. This directly translates into battery drain and lower energy efficiency, crucial factors in electric vehicles. This is due to the high bit rate of the captured video and other sensing inputs, mainly due to Light Detection and Ranging (LiDAR) sensor at the top of the car which is an essential feature in autonomous vehicles. LiDAR is needed to obtain a high precision map for the vehicle AI to make relevant decisions. However, this is still a quite restricted view from the car. This is the same even in the case of cars without a LiDAR such as Tesla. The existing LiDARs and the cameras have limited horizontal and vertical fields of visions. In all cases it can be argued that precision is lower, given the smaller map generated. This also results in the accumulation of a large amount of data in the order of several TBs in a day, the storage of which becomes challenging. If we are to reduce the effort for the processing units inside the car, we need to uplink the data to edge or an appropriately placed cloud. However, the required data rates in the order of several Gbps are difficult to be met even with the advent of 5G. Therefore, we propose to have a coordinated set of LiDAR's outside at an elevation which can provide an integrated view with a much larger field of vision (FoV) to a centralized decision making body which then sends the required control actions to the vehicles with a lower bit rate in the downlink and with the required latency. The calculations we have based on industry standard equipment from several manufacturers show that this is not just a concept but a feasible system which can be implemented.The proposed system can play a supportive role with existing autonomous vehicle architecture and it is easily applicable in an urban area.