OpenRaiser/Intern-Atlas huggingface dataset:
A Coq-based synthesis of Scala programs which are correct-by-construction
Venue: arXiv cs.PL 2017
Year: 2017

The present paper introduces Scala-of-Coq, a new compiler that allows a Coq-based synthesis of Scala programs which are "correct-by-construction". A typical workflow features a user implementing a Coq functional program, proving this program's correctness with regards to its specification and making use of Scala-of-Coq to synthesize a Scala program that can seamlessly be integrated into an existing industrial Scala or Java application.
Declarative Modeling for Building a Cloud Federation and Cloud Applications
Venue: arXiv cs.DC 2017
Year: 2017

The paper illustrates how we built a federated cloud computing platform dedicated to the Italian research community. Building a cloud platform is a daunting task, that requires coordinating the deployment of many services, interrelated and dependent on each other. Provisioning, servicing and maintaining the platform must be automated. For our deployment, we chose a declarative modeling tool, that allows describing the parts that compose the system and their relations of supplier/consumer of specific interfaces. The tool arranges the steps to bring the deployment to convergence by transforming the state of the system until it reaches a configuration that satisfies all constraints. We chose a declarative service modeling approach for orchestrating both the deployment of the platform by the administrators and the deployment of applications by users. The cloud platform has been designed so that it can be managed by this kind of automation, facilitating the deployment of federated regions by anyone wishing to join and to contribute resources to the federation. Federated resources are integrated into a single cloud platform available to any user of the federation. The federation can also seamlessly include public clouds. We describe the architectural choices, how we adapted the OpenStack basic facilities to the needs of a federation of multiple independent organizations, how we control resource allocation according to committed plans and correspondingly how we handle accounting and billing of resource usage. Besides providing traditional IaaS services, the cloud supports self-service deployment of cloud applications. The cloud thus addresses the long tail of science, allowing researchers of any discipline, without expertise in system or cloud administration, to deploy applications readily available for their perusal.
Limits to rover miniaturisation and their implications for solar system exploration
Venue: arXiv cs.RO 2017
Year: 2017

Semiautonomous rover scaling is examined for exploration throughout the solar system. Communications to a relay orbiter is a major constraint, due to power requirements and decreasing antenna gain at small sizes. Also, analysis time scales adversely for power hungry Raman or surface abrasion, and also for low photon count gamma ray spectroscopy. 1 cm scale rovers with a MER like capability should be possible, and could operate on solar power to 40 AU. At 2 cm, rovers powered by current RTGs are feasible, and are useful in the outer solar system. Such rovers will return images, autonomously navigate from interest point to interest point, and autonomously deploy instruments. Analyses include elemental APX and gamma ray spectroscopy for elemental and Raman and IR spectroscopy for molecular and or mineralogical compositions. They can be built with current technology, the component size is similar to watch movements. Low temperatures are not an obstacle. Very high temperatures, e.g. 390 to 480 C for surface Venus, will require more work on high temperature electronics, but current work suggests that dense ICs for Venusian conditions should be feasible in the near future. Mm size rovers, designed primarily for imaging, are feasible at inner solar system solar flux levels. If deployed in large numbers, manufacturing developments would be needed to allow mechanised assembly of multiple MEMS systems. Miniature, degassing to space, RTGs could provide power in cold vacuum environments, as could advanced betavoltaic systems, though much work would be required to develop the latter.
Twigraph: Discovering and Visualizing Influential Words between Twitter Profiles
Venue: arXiv cs.SI 2017
Year: 2017

The social media craze is on an ever increasing spree, and people are connected with each other like never before, but these vast connections are visually unexplored. We propose a methodology Twigraph to explore the connections between persons using their Twitter profiles. First, we propose a hybrid approach of recommending social media profiles, articles, and advertisements to a user.The profiles are recommended based on the similarity score between the user profile, and profile under evaluation. The similarity between a set of profiles is investigated by finding the top influential words thus causing a high similarity through an Influence Term Metric for each word. Then, we group profiles of various domains such as politics, sports, and entertainment based on the similarity score through a novel clustering algorithm. The connectivity between profiles is envisaged using word graphs that help in finding the words that connect a set of profiles and the profiles that are connected to a word. Finally, we analyze the top influential words over a set of profiles through clustering by finding the similarity of that profiles enabling to break down a Twitter profile with a lot of followers to fine level word connections using word graphs. The proposed method was implemented on datasets comprising 1.1 M Tweets obtained from Twitter. Experimental results show that the resultant influential words were highly representative of the relationship between two profiles or a set of profiles
Mining Social Media to Inform Peatland Fire and Haze Disaster Management
Venue: arXiv cs.SI 2017
Year: 2017

Peatland fires and haze events are disasters with national, regional and international implications. The phenomena lead to direct damage to local assets, as well as broader economic and environmental losses. Satellite imagery is still the main and often the only available source of information for disaster management. In this article, we test the potential of social media to assist disaster management. To this end, we compare insights from two datasets: fire hotspots detected via NASA satellite imagery and almost all GPS-stamped tweets from Sumatra Island, Indonesia, posted during 2014. Sumatra Island is chosen as it regularly experiences a significant number of haze events, which affect citizens in Indonesia as well as in nearby countries including Malaysia and Singapore. We analyse temporal correlations between the datasets and their geo-spatial interdependence. Furthermore, we show how Twitter data reveals changes in users' behavior during severe haze events. Overall, we demonstrate that social media is a valuable source of complementary and supplementary information for haze disaster management. Based on our methodology and findings, an analytics tool to improve peatland fire and haze disaster management by the Indonesian authorities is under development.
A Practical Algorithm for Enumerating Collinear Points
Venue: arXiv cs.CG 2017
Year: 2017

This paper studies the problem of enumerating all maximal collinear subsets of size at least three in a given set of $n$ points. An algorithm for this problem, besides solving degeneracy testing and the exact fitting problem, can also help with other problems, such as point line cover and general position subset selection. The classic \emph{topological sweeping} algorithm of Edelsbrunner and Guibas can find these subsets in $O(n^2)$ time in the dual plane. We present an alternative algorithm that, although asymptotically slower than their algorithm in the worst case, is simpler to implement and more amenable to parallelization. If the input points are decomposed into $m$ convex polygons, our algorithm has time complexity $O(n^2 \log m)$ and space complexity $O(n)$. Our algorithm can be parallelized on the CREW PRAM with time complexity $O(n \log m)$ using $n$ processors.
Probabilistic Jamming/Eavesdropping Attacks to Confuse a Buffer-Aided Transmitter-Receiver Pair
Venue: arXiv cs.IT 2017
Year: 2017

We assume that a buffer-aided transmitter communicates with a receiving node in the presence of an attacker. We investigate the impact of a radio-frequency energy-harvesting attacker that probabilistically operates as a jammer or an eavesdropper. We show that even without the need for an external energy source, the attacker can still degrade the security of the legitimate system. We show that the random data arrival behavior at the transmitter and the channel randomness of the legitimate link can improve the system's security. Moreover, we design a jamming scheme for the attacker and investigate its impact on the secure throughput of the legitimate system. The attacker designs his power splitting parameter and jamming/eavesdropping probability based on the energy state of the attacker's battery to minimize the secure throughput of the legitimate system.
Truly Multi-modal YouTube-8M Video Classification with Video, Audio, and Text
Venue: arXiv cs.CV 2017
Year: 2017

The YouTube-8M video classification challenge requires teams to classify 0.7 million videos into one or more of 4,716 classes. In this Kaggle competition, we placed in the top 3% out of 650 participants using released video and audio features. Beyond that, we extend the original competition by including text information in the classification, making this a truly multi-modal approach with vision, audio and text. The newly introduced text data is termed as YouTube-8M-Text. We present a classification framework for the joint use of text, visual and audio features, and conduct an extensive set of experiments to quantify the benefit that this additional mode brings. The inclusion of text yields state-of-the-art results, e.g. 86.7% GAP on the YouTube-8M-Text validation dataset.
Energy Efficient Scheduling for Loss Tolerant IoT Applications with Uninformed Transmitter
Venue: arXiv cs.IT 2017
Year: 2017

In this work we investigate energy efficient packet scheduling problem for the loss tolerant applications. We consider slow fading channel for a point to point connection with no channel state information at the transmitter side (CSIT). In the absence of CSIT, the slow fading channel has an outage probability associated with every transmit power. As a function of data loss tolerance parameters and peak power constraints, we formulate an optimization problem to minimize the average transmit energy for the user equipment (UE). The optimization problem is not convex and we use stochastic optimization technique to solve the problem. The numerical results quantify the effect of different system parameters on average transmit power and show significant power savings for the loss tolerant applications.
Single item stochastic lot sizing problem considering capital flow and business overdraft
Venue: arXiv cs.CE 2017
Year: 2017

This paper introduces capital flow to the single item stochastic lot sizing problem. A retailer can leverage business overdraft to deal with unexpected capital shortage, but needs to pay interest if its available balance goes below zero. A stochastic dynamic programming model maximizing expected final capital increment is formulated to solve the problem to optimality. We then investigate the performance of four controlling policies: ($R, Q$), ($R, S$), ($s, S$) and ($s$, $\overline{Q}$, $S$); for these policies, we adopt simulation-genetic algorithm to obtain approximate values of the controlling parameters. Finally, a simulation-optimization heuristic is also employed to solve this problem. Computational comparisons among these approaches show that policy $(s, S)$ and policy $(s, \overline{Q}, S)$ provide performance close to that of optimal solutions obtained by stochastic dynamic programming, while simulation-optimization heuristic offers advantages in terms of computational efficiency. Our numerical tests also show that capital availability as well as business overdraft interest rate can substantially affect the retailer's optimal lot sizing decisions.
On affine variety codes from the Klein quartic
Venue: arXiv cs.IT 2017
Year: 2017

We study a family of primary affine variety codes defined from the Klein quartic. The duals of these codes have previously been treated in [12, Ex. 3.2]. Among the codes that we construct almost all have parameters as good as the best known codes according to [9] and in the remaining few cases the parameters are almost as good. To establish the code parameters we apply the footprint bound [10, 7] from Gröbner basis theory and for this purpose we develop a new method where we inspired by Buchberger's algorithm perform a series of symbolic computations. 1
Towards the Improvement of Automated Scientific Document Categorization by Deep Learning
Venue: arXiv cs.IR 2017
Year: 2017

This master thesis describes an algorithm for automated categorization of scientific documents using deep learning techniques and compares the results to the results of existing classification algorithms. As an additional goal a reusable API is to be developed allowing the automation of classification tasks in existing software. A design will be proposed using a convolutional neural network as a classifier and integrating this into a REST based API. This is then used as the basis for an actual proof of concept implementation presented as well in this thesis. It will be shown that the deep learning classifier provides very good result in the context of multi-class document categorization and that it is feasible to integrate such classifiers into a larger ecosystem using REST based services.
Fourier-Based Testing for Families of Distributions
Venue: arXiv cs.DS 2017
Year: 2017

We study the general problem of testing whether an unknown distribution belongs to a specified family of distributions. More specifically, given a distribution family $\mathcal{P}$ and sample access to an unknown discrete distribution $\mathbf{P}$, we want to distinguish (with high probability) between the case that $\mathbf{P} \in \mathcal{P}$ and the case that $\mathbf{P}$ is $ε$-far, in total variation distance, from every distribution in $\mathcal{P}$. This is the prototypical hypothesis testing problem that has received significant attention in statistics and, more recently, in theoretical computer science. The sample complexity of this general inference task depends on the underlying family $\mathcal{P}$. The gold standard in distribution property testing is to design sample-optimal and computationally efficient algorithms for this task. The main contribution of this work is a simple and general testing technique that is applicable to all distribution families whose Fourier spectrum satisfies a certain approximate sparsity property. To the best of our knowledge, ours is the first use of the Fourier transform in the context of distribution testing. We apply our Fourier-based framework to obtain near sample-optimal and computationally efficient testers for the following fundamental distribution families: Sums of Independent Integer Random Variables (SIIRVs), Poisson Multinomial Distributions (PMDs), and Discrete Log-Concave Distributions. For the first two, ours are the first non-trivial testers in the literature, vastly generalizing previous work on testing Poisson Binomial Distributions. For the third, our tester improves on prior work in both sample and time complexity.
An Empirical Study of Mini-Batch Creation Strategies for Neural Machine Translation
Venue: arXiv cs.CL 2017
Year: 2017

Training of neural machine translation (NMT) models usually uses mini-batches for efficiency purposes. During the mini-batched training process, it is necessary to pad shorter sentences in a mini-batch to be equal in length to the longest sentence therein for efficient computation. Previous work has noted that sorting the corpus based on the sentence length before making mini-batches reduces the amount of padding and increases the processing speed. However, despite the fact that mini-batch creation is an essential step in NMT training, widely used NMT toolkits implement disparate strategies for doing so, which have not been empirically validated or compared. This work investigates mini-batch creation strategies with experiments over two different datasets. Our results suggest that the choice of a mini-batch creation strategy has a large effect on NMT training and some length-based sorting strategies do not always work well compared with simple shuffling.
Exploring Content-based Artwork Recommendation with Metadata and Visual Features
Venue: arXiv cs.IR 2017
Year: 2017

Compared to other areas, artwork recommendation has received little attention, despite the continuous growth of the artwork market. Previous research has relied on ratings and metadata to make artwork recommendations, as well as visual features extracted with deep neural networks (DNN). However, these features have no direct interpretation to explicit visual features (e.g. brightness, texture) which might hinder explainability and user-acceptance. In this work, we study the impact of artwork metadata as well as visual features (DNN-based and attractiveness-based) for physical artwork recommendation, using images and transaction data from the UGallery online artwork store. Our results indicate that: (i) visual features perform better than manually curated data, (ii) DNN-based visual features perform better than attractiveness-based ones, and (iii) a hybrid approach improves the performance further. Our research can inform the development of new artwork recommenders relying on diverse content data.
How Hard is it to Find (Honest) Witnesses?
Venue: arXiv cs.DS 2017
Year: 2017

In recent years much effort was put into developing polynomial-time conditional lower bounds for algorithms and data structures in both static and dynamic settings. Along these lines we suggest a framework for proving conditional lower bounds based on the well-known 3SUM conjecture. Our framework creates a \emph{compact representation} of an instance of the 3SUM problem using hashing and domain specific encoding. This compact representation admits false solutions to the original 3SUM problem instance which we reveal and eliminate until we find a true solution. In other words, from all \emph{witnesses} (candidate solutions) we figure out if an \emph{honest} one (a true solution) exists. This enumeration of witnesses is used to prove conditional lower bound on \emph{reporting} problems that generate all witnesses. In turn, these reporting problems are reduced to various decision problems. These help to enumerate the witnesses by constructing appropriate search data structures. Hence, 3SUM-hardness of the decision problems is deduced. We utilize this framework to show conditional lower bounds for several variants of convolutions, matrix multiplication and string problems. Our framework uses a strong connection between all of these problems and the ability to find \emph{witnesses}. While these specific applications are used to demonstrate the techniques of our framework, we believe that this novel framework is useful for many other problems as well.
Generic Approach to Certified Static Checking of Module-like Constructs
Venue: arXiv cs.PL 2017
Year: 2017

In this paper we consider the problem of certified static checking of module-like constructs of programming languages. We argue that there are algorithms and properties related to modules that can be defined and proven in an abstract way. We advocate the design of a generic Coq library, which is aimed to provide three building blocks for each checking mechanism: propositional, computable, and correctness proofs. Implemented part of the library is justified by applying it to a certified static checker of an extension of STLC.
Toward uniform random generation in 1-safe Petri nets
Venue: arXiv cs.FL 2017
Year: 2017

We study the notion of uniform measure on the space of infinite executions of a 1-safe Petri net. Here, executions of 1-safe Petri nets are understood up to commutation of concurrent transitions, which introduces a challenge compared to usual transition systems. We obtain that the random generation of infinite executions reduces to the simulation of a finite state Markov chain. Algorithmic issues are discussed.
Signal Machine And Cellular Automaton Time-Optimal Quasi-Solutions Of The Firing Squad/Mob Synchronisation Problem On Connected Graphs
Venue: arXiv cs.FL 2017
Year: 2017

We construct a time-optimal quasi-solution of the firing mob synchronisation problem over finite, connected, and undirected multigraphs whose maximum degrees are uniformly bounded by a constant. It is only a quasi-solution because its number of states depends on the graph or, from another perspective, does not depend on the graph but is countably infinite. To construct this quasi-solution we introduce signal machines over continuum representations of such multigraphs and construct a signal machine whose discretisation is a cellular automaton that quasi-solves the problem. This automaton uses a time-optimal solution of the firing squad synchronisation problem in dimension one with one general at one end to synchronise edges, and freezes and thaws the synchronisation of edges in such a way that all edges synchronise at the same time.
Deep Counterfactual Networks with Propensity-Dropout
Venue: arXiv cs.LG 2017
Year: 2017

We propose a novel approach for inferring the individualized causal effects of a treatment (intervention) from observational data. Our approach conceptualizes causal inference as a multitask learning problem; we model a subject's potential outcomes using a deep multitask network with a set of shared layers among the factual and counterfactual outcomes, and a set of outcome-specific layers. The impact of selection bias in the observational data is alleviated via a propensity-dropout regularization scheme, in which the network is thinned for every training example via a dropout probability that depends on the associated propensity score. The network is trained in alternating phases, where in each phase we use the training examples of one of the two potential outcomes (treated and control populations) to update the weights of the shared layers and the respective outcome-specific layers. Experiments conducted on data based on a real-world observational study show that our algorithm outperforms the state-of-the-art.
Visual Decoding of Targets During Visual Search From Human Eye Fixations
Venue: arXiv cs.CV 2017
Year: 2017

What does human gaze reveal about a users' intents and to which extend can these intents be inferred or even visualized? Gaze was proposed as an implicit source of information to predict the target of visual search and, more recently, to predict the object class and attributes of the search target. In this work, we go one step further and investigate the feasibility of combining recent advances in encoding human gaze information using deep convolutional neural networks with the power of generative image models to visually decode, i.e. create a visual representation of, the search target. Such visual decoding is challenging for two reasons: 1) the search target only resides in the user's mind as a subjective visual pattern, and can most often not even be described verbally by the person, and 2) it is, as of yet, unclear if gaze fixations contain sufficient information for this task at all. We show, for the first time, that visual representations of search targets can indeed be decoded only from human gaze fixations. We propose to first encode fixations into a semantic representation and then decode this representation into an image. We evaluate our method on a recent gaze dataset of 14 participants searching for clothing in image collages and validate the model's predictions using two human studies. Our results show that 62% (Chance level = 10%) of the time users were able to select the categories of the decoded image right. In our second studies we show the importance of a local gaze encoding for decoding visual search targets of user