OpenRaiser/Intern-Atlas huggingface dataset:
On the Effectiveness of Simple Success-Based Parameter Selection Mechanisms for Two Classical Discrete Black-Box Optimization Benchmark Problems
Venue: arXiv cs.NE 2018
Year: 2018

Despite significant empirical and theoretically supported evidence that non-static parameter choices can be strongly beneficial in evolutionary computation, the question how to best adjust parameter values plays only a marginal role in contemporary research on discrete black-box optimization. This has led to the unsatisfactory situation in which feedback-free parameter selection rules such as the cooling schedule of Simulated Annealing are predominant in state-of-the-art heuristics, while, at the same time, we understand very well that such time-dependent selection rules can only perform worse than adjustment rules that do take into account the evolution of the optimization process. A number of adaptive and self-adaptive parameter control strategies have been proposed in the literature, but did not (yet) make their way to a broader public. A key obstacle seems to lie in their rather complex update rules. The purpose of our work is to demonstrate that high-performing online parameter selection rules do not have to be very complicated. More precisely, we experiment with a multiplicative, comparison-based update rule to adjust the mutation probability of a (1+1)~Evolutionary Algorithm. We show that this simple self-adjusting rule outperforms the best static unary unbiased black-box algorithm on LeadingOnes, achieving an almost optimal speedup of about~$18\%$.
Tree dimension in verification of constrained Horn clauses
Venue: arXiv cs.LO 2018
Year: 2018

In this paper, we show how the notion of tree dimension can be used in the verification of constrained Horn clauses (CHCs). The dimension of a tree is a numerical measure of its branching complexity and the concept here applies to Horn clause derivation trees. Derivation trees of dimension zero correspond to derivations using linear CHCs, while trees of higher dimension arise from derivations using non-linear CHCs. We show how to instrument CHCs predicates with an extra argument for the dimension, allowing a CHC verifier to reason about bounds on the dimension of derivations. Given a set of CHCs $P$, we define a transformation of $P$ yielding a dimension bounded set of CHCs $P^{\leq{k}}$. The set of derivations for $P^{\leq{k}}$ consists of the derivations for $P$ that have dimension at most $k$. We also show how to construct a set of clauses denoted $P^{>{k}}$ whose derivations have dimension exceeding $k$. We then present algorithms using these constructions to decompose a CHC verification problem. One variation of this decomposition considers derivations of successively increasing dimension. The paper includes descriptions of implementations and experimental results. Under consideration for publication in Theory and Practice of Logic Programming (TPLP).
Learning how to Prove: From the Coq Proof Assistant to Textbook Style
Venue: arXiv cs.LO 2018
Year: 2018

We have developed an alternative approach to teaching computer science students how to prove. First, students are taught how to prove theorems with the Coq proof assistant. In a second, more difficult, step students will transfer their acquired skills to the area of textbook proofs. In this article we present a realisation of the second step. Proofs in Coq have a high degree of formality while textbook proofs have only a medium one. Therefore our key idea is to reduce the degree of formality from the level of Coq to textbook proofs in several small steps. For that purpose we introduce three proof styles between Coq and textbook proofs, called line by line comments, weakened line by line comments, and structure faithful proofs. While this article is mostly conceptional we also report on experiences with putting our approach into practise.
Totally Looks Like - How Humans Compare, Compared to Machines
Venue: arXiv cs.CV 2018
Year: 2018

Perceptual judgment of image similarity by humans relies on rich internal representations ranging from low-level features to high-level concepts, scene properties and even cultural associations. However, existing methods and datasets attempting to explain perceived similarity use stimuli which arguably do not cover the full breadth of factors that affect human similarity judgments, even those geared toward this goal. We introduce a new dataset dubbed Totally-Looks-Like (TLL) after a popular entertainment website, which contains images paired by humans as being visually similar. The dataset contains 6016 image-pairs from the wild, shedding light upon a rich and diverse set of criteria employed by human beings. We conduct experiments to try to reproduce the pairings via features extracted from state-of-the-art deep convolutional neural networks, as well as additional human experiments to verify the consistency of the collected data. Though we create conditions to artificially make the matching task increasingly easier, we show that machine-extracted representations perform very poorly in terms of reproducing the matching selected by humans. We discuss and analyze these results, suggesting future directions for improvement of learned image representations.
Memorization Precedes Generation: Learning Unsupervised GANs with Memory Networks
Venue: arXiv cs.LG 2018
Year: 2018

We propose an approach to address two issues that commonly occur during training of unsupervised GANs. First, since GANs use only a continuous latent distribution to embed multiple classes or clusters of data, they often do not correctly handle the structural discontinuity between disparate classes in a latent space. Second, discriminators of GANs easily forget about past generated samples by generators, incurring instability during adversarial training. We argue that these two infamous problems of unsupervised GAN training can be largely alleviated by a learnable memory network to which both generators and discriminators can access. Generators can effectively learn representation of training samples to understand underlying cluster distributions of data, which ease the structure discontinuity problem. At the same time, discriminators can better memorize clusters of previously generated samples, which mitigate the forgetting problem. We propose a novel end-to-end GAN model named memoryGAN, which involves a memory network that is unsupervisedly trainable and integrable to many existing GAN models. With evaluations on multiple datasets such as Fashion-MNIST, CelebA, CIFAR10, and Chairs, we show that our model is probabilistically interpretable, and generates realistic image samples of high visual fidelity. The memoryGAN also achieves the state-of-the-art inception scores over unsupervised GAN models on the CIFAR10 dataset, without any optimization tricks and weaker divergences.
Calculated attributes of synonym sets
Venue: arXiv cs.CL 2018
Year: 2018

The goal of formalization, proposed in this paper, is to bring together, as near as possible, the theoretic linguistic problem of synonym conception and the computer linguistic methods based generally on empirical intuitive unjustified factors. Using the word vector representation we have proposed the geometric approach to mathematical modeling of synonym set (synset). The word embedding is based on the neural networks (Skip-gram, CBOW), developed and realized as word2vec program by T. Mikolov. The standard cosine similarity is used as the distance between word-vectors. Several geometric characteristics of the synset words are introduced: the interior of synset, the synset word rank and centrality. These notions are intended to select the most significant synset words, i.e. the words which senses are the nearest to the sense of a synset. Some experiments with proposed notions, based on RusVectores resources, are represented. A brief description of this work can be viewed in slides https://goo.gl/K82Fei
Agile Behaviour Design: A Design Approach for Structuring Game Characters and Interactions
Venue: arXiv cs.SE 2018
Year: 2018

In this paper, a novel design methodology-Agile Behaviour Design-is presented that accommodates the requirements for developing complex game agents suitable for industrial environments. An essential part of the design approach is to support independent work of both designers and programmers by reducing bottleneck situations. The approach fosters the creation of more loose and fluid interactions between design and implementation, leaving more freedom for creative expression.
You Are Okay: Towards User Interfaces for Improving Well-being
Venue: arXiv cs.HC 2018
Year: 2018

Well-being is a relatively broad concept which can be succinctly described as the state of being happy, healthy or successful. Interesting things happen when bridging user interface design with the psychology of human well-being. This position paper aims at providing a short on reflection the challenges and opportunities in this context and presents concrete examples on how to tackle these challenges and exploit the existing design opportunities.
Continuous Affect Prediction using Eye Gaze
Venue: arXiv cs.HC 2018
Year: 2018

In recent times, there has been significant interest in the machine recognition of human emotions, due to the suite of applications to which this knowledge can be applied. A number of different modalities, such as speech or facial expression, individually and with eye gaze, have been investigated by the affective computing research community to either classify the emotion (e.g. sad, happy, angry) or predict the continuous values of affective dimensions (e.g. valence, arousal, dominance) at each moment in time. Surprisingly after an extensive literature review, eye gaze as a unimodal input to a continuous affect prediction system has not been considered. In this context, this paper evaluates the use of eye gaze as a unimodal input to a continuous affect prediction system. The performance of continuous prediction of arousal and valence using eye gaze is compared with the performance of a speech system using the AVEC 2014 speech feature set. The experimental evaluation when using eye gaze as the single modality in a continuous affect prediction system produced a correlation result for valence prediction that is better than the correlation result obtained with the AVEC 2014 speech feature set. Furthermore, the eye gaze feature set proposed in this paper contains 98% fewer features compared to the number of features in the AVEC 2014 feature set.
Continuous Affect Prediction Using Eye Gaze and Speech
Venue: arXiv cs.HC 2018
Year: 2018

Affective computing research traditionally focused on labeling a person's emotion as one of a discrete number of classes e.g. happy or sad. In recent times, more attention has been given to continuous affect prediction across dimensions in the emotional space, e.g. arousal and valence. Continuous affect prediction is the task of predicting a numerical value for different emotion dimensions. The application of continuous affect prediction is powerful in domains involving real-time audio-visual communications which could include remote or assistive technologies for psychological assessment of subjects. Modalities used for continuous affect prediction may include speech, facial expressions and physiological responses. As opposed to single modality analysis, the research community have combined multiple modalities to improve the accuracy of continuous affect prediction. In this context, this paper investigates a continuous affect prediction system using the novel combination of speech and eye gaze. A new eye gaze feature set is proposed. This novel approach uses open source software for real-time affect prediction in audio-visual communication environments. A unique advantage of the human-computer interface used here is that it does not require the subject to wear specialized and expensive eye-tracking headsets or intrusive devices. The results indicate that the combination of speech and eye gaze improves arousal prediction by 3.5% and valence prediction by 19.5% compared to using speech alone.
Building an Integrated Mobile Robotic System for Real-Time Applications in Construction
Venue: arXiv cs.RO 2018
Year: 2018

One of the major challenges of a real-time autonomous robotic system for construction monitoring is to simultaneously localize, map, and navigate over the lifetime of the robot, with little or no human intervention. Past research on Simultaneous Localization and Mapping (SLAM) and context-awareness are two active research areas in the computer vision and robotics communities. The studies that integrate both in real-time into a single modular framework for construction monitoring still need further investigation. A monocular vision system and real-time scene understanding are computationally heavy and the major state-of-the-art algorithms are tested on high-end desktops and/or servers with a high CPU- and/or GPU- computing capabilities, which affect their mobility and deployment for real-world applications. To address these challenges and achieve automation, this paper proposes an integrated robotic computer vision system, which generates a real-world spatial map of the obstacles and traversable space present in the environment in near real-time. This is done by integrating contextual Awareness and visual SLAM into a ground robotics agent. This paper presents the hardware utilization and performance of the aforementioned system for three different outdoor environments, which represent the applicability of this pipeline to diverse outdoor scenes in near real-time. The entire system is also self-contained and does not require user input, which demonstrates the potential of this computer vision system for autonomous navigation.
A generalized parametric 3D shape representation for articulated pose estimation
Venue: arXiv cs.CV 2018
Year: 2018

We present a novel parametric 3D shape representation, Generalized sum of Gaussians (G-SoG), which is particularly suitable for pose estimation of articulated objects. Compared with the original sum-of-Gaussians (SoG), G-SoG can handle both isotropic and anisotropic Gaussians, leading to a more flexible and adaptable shape representation yet with much fewer anisotropic Gaussians involved. An articulated shape template can be developed by embedding G-SoG in a tree-structured skeleton model to represent an articulated object. We further derive a differentiable similarity function between G-SoG (the template) and SoG (observed data) that can be optimized analytically for efficient pose estimation. The experimental results on a standard human pose estimation dataset show the effectiveness and advantages of G-SoG over the original SoG as well as the promise compared with the recent algorithms that use more complicated shape models.
Data Sustainability and Reuse Pathways of Natural Resources and Environmental Scientists
Venue: arXiv cs.DL 2018
Year: 2018

This paper presents a multifarious examination of natural resources and environmental scientists' adventures navigating the policy change towards open access and cultural shift in data management, sharing, and reuse. Situated in the institutional context of Virginia Tech, a focus group and multiple individual interviews were conducted exploring the domain scientists' all-around experiences, performances, and perspectives on their collection, adoption, integration, preservation, and management of data. The results reveal the scientists' struggles, concerns, and barriers encountered, as well as their shared values, beliefs, passions, and aspirations when working with data. Based on these findings, this study provides suggestions on data modeling and knowledge representation strategies to support the long-term viability, stewardship, accessibility, and sustainability of scientific data. It also discusses the art of curation as creative scholarship and new opportunities for data librarians and information professionals to mobilize the data revolution.
EPTAS for Max Clique on Disks and Unit Balls
Venue: arXiv cs.CG 2018
Year: 2018

We propose a polynomial-time algorithm which takes as input a finite set of points of $\mathbb R^3$ and compute, up to arbitrary precision, a maximum subset with diameter at most $1$. More precisely, we give the first randomized EPTAS and deterministic PTAS for Maximum Clique in unit ball graphs. Our approximation algorithm also works on disk graphs with arbitrary radii. Almost three decades ago, an elegant polynomial-time algorithm was found for Maximum Clique on unit disk graphs [Clark, Colbourn, Johnson; Discrete Mathematics '90]. Since then, it has been an intriguing open question whether or not tractability can be extended to general disk graphs. Recently, it was shown that the disjoint union of two odd cycles is never the complement of a disk graph [Bonnet, Giannopoulos, Kim, Rzążewski, Sikora; SoCG '18]. This enabled the authors to derive a QPTAS and a subexponential algorithm for Max Clique on disk graphs. In this paper, we improve the approximability to a randomized EPTAS (and a deterministic PTAS). More precisely, we obtain a randomized EPTAS for computing the independence number on graphs having no disjoint union of two odd cycles as an induced subgraph, bounded VC-dimension, and large independence number. We then address the question of computing Max Clique for disks in higher dimensions. We show that intersection graphs of unit balls, like disk graphs, do not admit the complement of two odd cycles as an induced subgraph. This, in combination with the first result, straightforwardly yields a randomized EPTAS for Max Clique on unit ball graphs. In stark contrast, we show that on ball and unit 4-dimensional disk graphs, Max Clique is NP-hard and does not admit an approximation scheme even in subexponential-time, unless the Exponential Time Hypothesis fails.
SACRE: Supporting contextual requirements' adaptation in modern self-adaptive systems in the presence of uncertainty at runtime
Venue: arXiv cs.SE 2018
Year: 2018

Runtime uncertainty such as unpredictable resource unavailability, changing environmental conditions and user needs, as well as system intrusions or faults represents one of the main current challenges of self-adaptive systems. Moreover, today's systems are increasingly more complex, distributed, decentralized, etc. and therefore have to reason about and cope with more and more unpredictable events. Approaches to deal with such changing requirements in complex today's systems are still missing. This work presents SACRE (Smart Adaptation through Contextual REquirements), our approach leveraging an adaptation feedback loop to detect self-adaptive systems' contextual requirements affected by uncertainty and to integrate machine learning techniques to determine the best operationalization of context based on sensed data at runtime. SACRE is a step forward of our former approach ACon which focus had been on adapting the context in contextual requirements, as well as their basic implementation. SACRE primarily focuses on architectural decisions, addressing self-adaptive systems' engineering challenges. Furthering the work on ACon, in this paper, we perform an evaluation of the entire approach in different uncertainty scenarios in real-time in the extremely demanding domain of smart vehicles. The real-time evaluation is conducted in a simulated environment in which the smart vehicle is implemented through software components. The evaluation results provide empirical evidence about the applicability of SACRE in real and complex software system domains.
Style Memory: Making a Classifier Network Generative
Venue: arXiv cs.NE 2018
Year: 2018

Deep networks have shown great performance in classification tasks. However, the parameters learned by the classifier networks usually discard stylistic information of the input, in favour of information strictly relevant to classification. We introduce a network that has the capacity to do both classification and reconstruction by adding a "style memory" to the output layer of the network. We also show how to train such a neural network as a deep multi-layer autoencoder, jointly minimizing both classification and reconstruction losses. The generative capacity of our network demonstrates that the combination of style-memory neurons with the classifier neurons yield good reconstructions of the inputs when the classification is correct. We further investigate the nature of the style memory, and how it relates to composing digits and letters. Finally, we propose that this architecture enables the bidirectional flow of information used in predictive coding, and that such bidirectional networks can help mitigate against being fooled by ambiguous or adversarial input.
Costs and Rewards in Priced Timed Automata
Venue: arXiv cs.LO 2018
Year: 2018

We consider Pareto analysis of reachable states of multi-priced timed automata (MPTA): timed automata equipped with multiple observers that keep track of costs (to be minimised) and rewards (to be maximised) along a computation. Each observer has a constant non-negative derivative which may depend on the location of the MPTA. We study the Pareto Domination Problem, which asks whether it is possible to reach a target location via a run in which the accumulated costs and rewards Pareto dominate a given objective vector. We show that this problem is undecidable in general, but decidable for MPTA with at most three observers. For MPTA whose observers are all costs or all rewards, we show that the Pareto Domination Problem is PSPACE-complete. We also consider an epsilon-approximate Pareto Domination Problem that is decidable without restricting the number and types of observers. We develop connections between MPTA and Diophantine equations. Undecidability of the Pareto Domination Problem is shown by reduction from Hilbert's 10th Problem, while decidability for three observers is shown by a translation to a fragment of arithmetic involving quadratic forms.
HexaConv
Venue: arXiv cs.LG 2018
Year: 2018

The effectiveness of Convolutional Neural Networks stems in large part from their ability to exploit the translation invariance that is inherent in many learning problems. Recently, it was shown that CNNs can exploit other invariances, such as rotation invariance, by using group convolutions instead of planar convolutions. However, for reasons of performance and ease of implementation, it has been necessary to limit the group convolution to transformations that can be applied to the filters without interpolation. Thus, for images with square pixels, only integer translations, rotations by multiples of 90 degrees, and reflections are admissible. Whereas the square tiling provides a 4-fold rotational symmetry, a hexagonal tiling of the plane has a 6-fold rotational symmetry. In this paper we show how one can efficiently implement planar convolution and group convolution over hexagonal lattices, by re-using existing highly optimized convolution routines. We find that, due to the reduced anisotropy of hexagonal filters, planar HexaConv provides better accuracy than planar convolution with square filters, given a fixed parameter budget. Furthermore, we find that the increased degree of symmetry of the hexagonal grid increases the effectiveness of group convolutions, by allowing for more parameter sharing. We show that our method significantly outperforms conventional CNNs on the AID aerial scene classification dataset, even outperforming ImageNet pre-trained models.