OpenRaiser/Intern-Atlas huggingface dataset:
A Theorem Prover for Scientific and Educational Purposes
Venue: arXiv cs.HC 2018
Year: 2018

We present a prototype of an integrated reasoning environment for educational purposes. The presented tool is a fragment of a proof assistant and automated theorem prover. We describe the existing and planned functionality of the theorem prover and especially the functionality of the educational fragment. This currently supports working with terms of the untyped lambda calculus and addresses both undergraduate students and researchers. We show how the tool can be used to support the students' understanding of functional programming and discuss general problems related to the process of building theorem proving software that aims at supporting both research and education.
Two-sided popular matchings in bipartite graphs with forbidden/forced elements and weights
Venue: arXiv cs.DM 2018
Year: 2018

Two-sided popular matchings in bipartite graphs are a well-known generalization of stable matchings in the marriage setting, and they are especially relevant when preference lists are incomplete. In this case, the cardinality of a stable matching can be as small as half the size of a maximum matching. Popular matchings allow for assignments of larger size while still guaranteeing a certain fairness condition. In fact, stable matchings are popular matchings of minimum size, and a maximum size popular matching can be as large as twice the size of a(ny) stable matching in a given instance. The structure of popular matchings seems to be more complex, and currently less understood, than that of stable matchings. In this paper, we focus on three optimization problems related to popular matchings. First, we give a granular analysis of the complexity of popular matching with forbidden and forced elements problems, thus complementing results from [Cseh and Kavitha, 2016]. In particular, we show that deciding whether there exists a popular matching with (or without) two given edges is NP-Hard. This implies that finding a popular matching of maximum (resp. minimum) weight is NP-Hard and, even if all weights are nonnegative, inapproximable up to a factor 1/2 (resp. up to any factor). A decomposition theorem from [Cseh and Kavitha, 2016] can be employed to give a 1/2 approximation to the maximum weighted popular matching problem with nonnegative weights, thus completely settling the complexity of those problems.
Programmable Switch as a Parallel Computing Device
Venue: arXiv cs.NI 2018
Year: 2018

Modern switches have packet processing capacity of up to multi-tera bits per second, and they are also becoming more and more programmable. We seek to understand whether the programmability can translate packet processing capacity to computational power for parallel computing applications. In this paper, we first develop a simple mathematical model to understand the costs and overheads of data plane computation. Then we validate the the performance benefits of offloading computation to network. Using experiments on real data center network, we finnd that offloading computation to the data plane results in up to 20x speed-up for a simple Map-Reduce application. Motivated by this, we propose a parallel programming framework, p4mr, to help users efficiently program multiple switches. We successfully build and test a prototype of p4mr on a simulated testbed.
Tracking Top-K Influential Vertices in Dynamic Networks
Venue: arXiv cs.SI 2018
Year: 2018

Influence propagation in networks has enjoyed fruitful applications and has been extensively studied in literature. However, only very limited preliminary studies tackled the challenges in handling highly dynamic changes in real networks. In this paper, we tackle the problem of tracking top-$k$ influential vertices in dynamic networks, where the dynamic changes are modeled as a stream of edge weight updates. Under the popularly adopted linear threshold (LT) model and the independent cascade (IC) model, we address two essential versions of the problem: tracking the top-$k$ influential individuals and finding the best $k$-seed set to maximize the influence spread (Influence Maximization). We adopt the polling-based method and maintain a sample of random RR sets so that we can approximate the influence of vertices with provable quality guarantees. It is known that updating RR sets over dynamic changes of a network can be easily done by a reservoir sampling method, so the key challenge is to efficiently decide how many RR sets are needed to achieve good quality guarantees. We use two simple signals, which both can be accessed in $O(1)$ time, to decide a proper number of RR sets. We prove the effectiveness of our methods. For both tasks the error incurred in our method is only a multiplicative factor to the ground truth. For influence maximization, we also propose an efficient query algorithm for finding the $k$ seeds, which is one order of magnitude faster than the state-of-the-art query algorithm in practice. In addition to the thorough theoretical results, our experimental results on large real networks clearly demonstrate the effectiveness and efficiency of our algorithms.
Predicting Webpage Aesthetics with Heatmap Entropy
Venue: arXiv cs.HC 2018
Year: 2018

Today, eye trackers are extensively used in user interface evaluations. However, it's still hard to analyze and interpret eye tracking data from the aesthetic point of view. To find quantitative links between eye movements and aesthetic experience, we tracked 30 observers' initial landings for 40 web pages (each displayed for 3 seconds). The web pages were also rated based on the observers' subjective aesthetic judgments. Shannon entropy was introduced to analyze the eye-tracking data. The result shows that the heatmap entropy (visual attention entropy, VAE) is highly correlated with the observers' aesthetic judgements of the web pages. Its improved version, relative VAE (rVAE), has a more significant correlation with the perceived aesthetics. (r=-0.65, F= 26.84, P$<$0.0001). This single metric alone can distinguish between good- and bad-looking pages with an approximate 85\% accuracy. Further investigation reveals that the performance of both VAE and rVAE became stable after 1 second. The curves indicate that their performances could be better, if the tracking time was extended beyond 3 seconds.
Motion and Cooperative Transportation Planning for Multi-Agent Systems under Temporal Logic Formulas
Venue: arXiv cs.SY 2018
Year: 2018

This paper presents a hybrid control framework for the motion planning of a multi-agent system including N robotic agents and M objects, under high level goals expressed as Linear Temporal Logic (LTL) formulas. In particular, we design control protocols that allow the transition of the agents as well as the cooperative transportation of the objects by the agents, among predefined regions of interest in the workspace. This allows to abstract the coupled behavior of the agents and the objects as a finite transition system and to design a high-level multi-agent plan that satisfies the agents' and the objects' specifications, given as temporal logic formulas. Simulation results verify the proposed framework.
N-body Networks: a Covariant Hierarchical Neural Network Architecture for Learning Atomic Potentials
Venue: arXiv cs.LG 2018
Year: 2018

We describe N-body networks, a neural network architecture for learning the behavior and properties of complex many body physical systems. Our specific application is to learn atomic potential energy surfaces for use in molecular dynamics simulations. Our architecture is novel in that (a) it is based on a hierarchical decomposition of the many body system into subsytems, (b) the activations of the network correspond to the internal state of each subsystem, (c) the "neurons" in the network are constructed explicitly so as to guarantee that each of the activations is covariant to rotations, (d) the neurons operate entirely in Fourier space, and the nonlinearities are realized by tensor products followed by Clebsch-Gordan decompositions. As part of the description of our network, we give a characterization of what way the weights of the network may interact with the activations so as to ensure that the covariance property is maintained.
String Attractors: Verification and Optimization
Venue: arXiv cs.DS 2018
Year: 2018

String attractors [STOC 2018] are combinatorial objects recently introduced to unify all known dictionary compression techniques in a single theory. A set $Γ\subseteq [1..n]$ is a $k$-attractor for a string $S\in[1..σ]^n$ if and only if every distinct substring of $S$ of length at most $k$ has an occurrence straddling at least one of the positions in $Γ$. Finding the smallest $k$-attractor is NP-hard for $k\geq3$, but polylogarithmic approximations can be found using reductions from dictionary compressors. It is easy to reduce the $k$-attractor problem to a set-cover instance where string's positions are interpreted as sets of substrings. The main result of this paper is a much more powerful reduction based on the truncated suffix tree. Our new characterization of the problem leads to more efficient algorithms for string attractors: we show how to check the validity and minimality of a $k$-attractor in near-optimal time and how to quickly compute exact and approximate solutions. For example, we prove that a minimum $3$-attractor can be found in optimal $O(n)$ time when $σ\in O(\sqrt[3+ε]{\log n})$ for any constant $ε>0$, and $2.45$-approximation can be computed in $O(n)$ time on general alphabets. To conclude, we introduce and study the complexity of the closely-related sharp-$k$-attractor problem: to find the smallest set of positions capturing all distinct substrings of length exactly $k$. We show that the problem is in P for $k=1,2$ and is NP-complete for constant $k\geq 3$.
Event-triggered Learning for Resource-efficient Networked Control
Venue: arXiv cs.SY 2018
Year: 2018

Common event-triggered state estimation (ETSE) algorithms save communication in networked control systems by predicting agents' behavior, and transmitting updates only when the predictions deviate significantly. The effectiveness in reducing communication thus heavily depends on the quality of the dynamics models used to predict the agents' states or measurements. Event-triggered learning is proposed herein as a novel concept to further reduce communication: whenever poor communication performance is detected, an identification experiment is triggered and an improved prediction model learned from data. Effective learning triggers are obtained by comparing the actual communication rate with the one that is expected based on the current model. By analyzing statistical properties of the inter-communication times and leveraging powerful convergence results, the proposed trigger is proven to limit learning experiments to the necessary instants. Numerical and physical experiments demonstrate that event-triggered learning improves robustness toward changing environments and yields lower communication rates than common ETSE.
AspEm: Embedding Learning by Aspects in Heterogeneous Information Networks
Venue: arXiv cs.SI 2018
Year: 2018

Heterogeneous information networks (HINs) are ubiquitous in real-world applications. Due to the heterogeneity in HINs, the typed edges may not fully align with each other. In order to capture the semantic subtlety, we propose the concept of aspects with each aspect being a unit representing one underlying semantic facet. Meanwhile, network embedding has emerged as a powerful method for learning network representation, where the learned embedding can be used as features in various downstream applications. Therefore, we are motivated to propose a novel embedding learning framework---AspEm---to preserve the semantic information in HINs based on multiple aspects. Instead of preserving information of the network in one semantic space, AspEm encapsulates information regarding each aspect individually. In order to select aspects for embedding purpose, we further devise a solution for AspEm based on dataset-wide statistics. To corroborate the efficacy of AspEm, we conducted experiments on two real-words datasets with two types of applications---classification and link prediction. Experiment results demonstrate that AspEm can outperform baseline network embedding learning methods by considering multiple aspects, where the aspects can be selected from the given HIN in an unsupervised manner.
ROUGE 2.0: Updated and Improved Measures for Evaluation of Summarization Tasks
Venue: arXiv cs.IR 2018
Year: 2018

Evaluation of summarization tasks is extremely crucial to determining the quality of machine generated summaries. Over the last decade, ROUGE has become the standard automatic evaluation measure for evaluating summarization tasks. While ROUGE has been shown to be effective in capturing n-gram overlap between system and human composed summaries, there are several limitations with the existing ROUGE measures in terms of capturing synonymous concepts and coverage of topics. Thus, often times ROUGE scores do not reflect the true quality of summaries and prevents multi-faceted evaluation of summaries (i.e. by topics, by overall content coverage and etc). In this paper, we introduce ROUGE 2.0, which has several updated measures of ROUGE: ROUGE-N+Synonyms, ROUGE-Topic, ROUGE-Topic+Synonyms, ROUGE-TopicUniq and ROUGE-TopicUniq+Synonyms; all of which are improvements over the core ROUGE measures.
M3Fusion: A Deep Learning Architecture for Multi-{Scale/Modal/Temporal} satellite data fusion
Venue: arXiv cs.CV 2018
Year: 2018

Modern Earth Observation systems provide sensing data at different temporal and spatial resolutions. Among optical sensors, today the Sentinel-2 program supplies high-resolution temporal (every 5 days) and high spatial resolution (10m) images that can be useful to monitor land cover dynamics. On the other hand, Very High Spatial Resolution images (VHSR) are still an essential tool to figure out land cover mapping characterized by fine spatial patterns. Understand how to efficiently leverage these complementary sources of information together to deal with land cover mapping is still challenging. With the aim to tackle land cover mapping through the fusion of multi-temporal High Spatial Resolution and Very High Spatial Resolution satellite images, we propose an End-to-End Deep Learning framework, named M3Fusion, able to leverage simultaneously the temporal knowledge contained in time series data as well as the fine spatial information available in VHSR information. Experiments carried out on the Reunion Island study area asses the quality of our proposal considering both quantitative and qualitative aspects.
SysML/KAOS Domain Models and B System Specifications
Venue: arXiv cs.SE 2018
Year: 2018

In this paper, we use a combination of the SysML/KAOS requirements engineering method, an extension of SysML, with concepts of the KAOS goal model, and of the B System formal method. Translation rules from a SysML/KAOS goal model to a B System specification have been defined. They allow to obtain a skeleton of the B System specification. To complete it, we have defined a language to express the domain model associated to the goal model. The translation of this domain model gives the structural part of the B System specification. The contribution of this paper is the description of translation rules from SysML/KAOS domain models to B System specifications. We also present the formal verification of these rules and we describe an open source tool that implements the languages and the rules. Finally, we provide a review of the application of the SysML/KAOS method on case studies such as for the formal specification of the hybrid ERTMS/ETCS level 3 standard.
Occupancy Map Prediction Using Generative and Fully Convolutional Networks for Vehicle Navigation
Venue: arXiv cs.LG 2018
Year: 2018

Fast, collision-free motion through unknown environments remains a challenging problem for robotic systems. In these situations, the robot's ability to reason about its future motion is often severely limited by sensor field of view (FOV). By contrast, biological systems routinely make decisions by taking into consideration what might exist beyond their FOV based on prior experience. In this paper, we present an approach for predicting occupancy map representations of sensor data for future robot motions using deep neural networks. We evaluate several deep network architectures, including purely generative and adversarial models. Testing on both simulated and real environments we demonstrated performance both qualitatively and quantitatively, with SSIM similarity measure up to 0.899. We showed that it is possible to make predictions about occupied space beyond the physical robot's FOV from simulated training data. In the future, this method will allow robots to navigate through unknown environments in a faster, safer manner.
The ORCA Hub: Explainable Offshore Robotics through Intelligent Interfaces
Venue: arXiv cs.AI 2018
Year: 2018

We present the UK Robotics and Artificial Intelligence Hub for Offshore Robotics for Certification of Assets (ORCA Hub), a 3.5 year EPSRC funded, multi-site project. The ORCA Hub vision is to use teams of robots and autonomous intelligent systems (AIS) to work on offshore energy platforms to enable cheaper, safer and more efficient working practices. The ORCA Hub will research, integrate, validate and deploy remote AIS solutions that can operate with existing and future offshore energy assets and sensors, interacting safely in autonomous or semi-autonomous modes in complex and cluttered environments, co-operating with remote operators. The goal is that through the use of such robotic systems offshore, the need for personnel will decrease. To enable this to happen, the remote operator will need a high level of situation awareness and key to this is the transparency of what the autonomous systems are doing and why. This increased transparency will facilitate a trusting relationship, which is particularly key in high-stakes, hazardous situations.
Chebyshev Filter Diagonalization on Modern Manycore Processors and GPGPUs
Venue: arXiv cs.MS 2018
Year: 2018

Chebyshev filter diagonalization is well established in quantum chemistry and quantum physics to compute bulks of eigenvalues of large sparse matrices. Choosing a block vector implementation, we investigate optimization opportunities on the new class of high-performance compute devices featuring both high-bandwidth and low-bandwidth memory. We focus on the transparent access to the full address space supported by both architectures under consideration: Intel Xeon Phi "Knights Landing" and Nvidia "Pascal." We propose two optimizations: (1) Subspace blocking is applied for improved performance and data access efficiency. We also show that it allows transparently handling problems much larger than the high-bandwidth memory without significant performance penalties. (2) Pipelining of communication and computation phases of successive subspaces is implemented to hide communication costs without extra memory traffic. As an application scenario we use filter diagonalization studies on topological insulator materials. Performance numbers on up to 512 nodes of the OakForest-PACS and Piz Daint supercomputers are presented, achieving beyond 100 Tflop/s for computing 100 inner eigenvalues of sparse matrices of dimension one billion.
Exogenous Approach to Grid Cost Allocation in Peer-to-Peer Electricity Markets
Venue: arXiv cs.SY 2018
Year: 2018

The deployment of distributed energy resources, combined with a more proactive demand side, is inducing a new paradigm in power system operation and electricity markets. Within a consumer-centric market framework, peer-to-peer approaches have gained substantial interest. Peer-to-peer markets rely on multi-bilateral direct negotiation among all players to match supply and demand, and with product differentiation. These markets can yield a complete mapping of exchanges onto the grid, hence allowing to rethink our approach to sharing costs related to usage of common infrastructure and services. We propose here to attribute such costs in a number of alternative ways that reflects different views on usage of the grid and on cost allocation, i.e., uniformly and based on the electrical distance between players. Since attribution mechanisms are defined in an exogenous manner and made transparent they eventually affect the trades of the market participants and related grid usage. The interest of our approach is illustrated on a test case using the IEEE 39 bus test system, underlying the impact of attribution mechanisms on trades and grid usage.
Relative Pairwise Relationship Constrained Non-negative Matrix Factorisation
Venue: arXiv cs.LG 2018
Year: 2018

Non-negative Matrix Factorisation (NMF) has been extensively used in machine learning and data analytics applications. Most existing variations of NMF only consider how each row/column vector of factorised matrices should be shaped, and ignore the relationship among pairwise rows or columns. In many cases, such pairwise relationship enables better factorisation, for example, image clustering and recommender systems. In this paper, we propose an algorithm named, Relative Pairwise Relationship constrained Non-negative Matrix Factorisation (RPR-NMF), which places constraints over relative pairwise distances amongst features by imposing penalties in a triplet form. Two distance measures, squared Euclidean distance and Symmetric divergence, are used, and exponential and hinge loss penalties are adopted for the two measures respectively. It is well known that the so-called "multiplicative update rules" result in a much faster convergence than gradient descend for matrix factorisation. However, applying such update rules to RPR-NMF and also proving its convergence is not straightforward. Thus, we use reasonable approximations to relax the complexity brought by the penalties, which are practically verified. Experiments on both synthetic datasets and real datasets demonstrate that our algorithms have advantages on gaining close approximation, satisfying a high proportion of expected constraints, and achieving superior performance compared with other algorithms.
Predictability of sequences and subsequences with spectrum degeneracy at periodically located points
Venue: arXiv cs.IT 2018
Year: 2018

The paper established sufficient conditions of predictability with degeneracy for the spectrum at $M$-periodically located isolated points on the unit circle. It is also shown that $m$-periodic subsequences of these sequences are also predictable if $m$ is a divisor of $M$. The predictability can be achieved for finite horizon with linear predictors defined by convolutions with certain kernels. As an example of applications, it is shown that there exists a class of sequences that is everywhere dense in the class of all square-summable sequences and such that its members can be recovered from their periodic subsequences. This recoverability is associated with certain spectrum degeneracy of a new kind.