OpenRaiser/Intern-Atlas huggingface dataset:
Mining Frequent Itemsets: a Formal Unification
Venue: arXiv cs.DB 2020
Year: 2020

It is generally well agreed that developing a unifying theory is one of the most important issues in Data Mining research. In the last two decades, a great deal of work has been devoted to the algorithmic aspects of the Frequent Itemset (FI) Mining problem. We are motivated by the need for formal modeling in the field. Thus, we introduce and analyze, in this theoretical study, a new model for the FI mining task. Indeed, we encode the itemsets as words over an ordered alphabet, and state this problem by a formal series over the counting semiring $(\mathbb{N},+,\times,0,1)$, whose range constitutes the itemsets and the coefficients are their supports. This formalism offers many advantages in both fundamental and practical aspects: the introduction of a clear and unified theoretical framework through which we can express the main FI-approaches, the possibility of their generalization to mine other more complex objects, and their incrementalisation or parallelisation; in practice, we explain how this problem can be seen as that of word recognition by an automaton, allowing an efficient implementation in $O(|Q|)$ space and $O(|\mathcal{F}_L||Q|])$ time, where $Q$ is the set of states of the automaton used for representing the data, and $\mathcal{F}_L$ the set of prefixial longest FI.
Linear Integer Arithmetic Revisited
Venue: arXiv cs.LO 2020
Year: 2020

We consider feasibility of linear integer programs in the context of verification systems such as SMT solvers or theorem provers. Although satisfiability of linear integer programs is decidable, many state-of-the-art solvers neglect termination in favor of efficiency. It is challenging to design a solver that is both terminating and practically efficient. Recent work by Jovanovic and de Moura constitutes an important step into this direction. Their algorithm CUTSAT is sound, but does not terminate, in general. In this paper we extend their CUTSAT algorithm by refined inference rules, a new type of conflicting core, and a dedicated rule application strategy. This leads to our algorithm CUTSAT++, which guarantees termination.
Elaborating Evaluation-Order Polymorphism
Venue: arXiv cs.PL 2020
Year: 2020

We classify programming languages according to evaluation order: each language fixes one evaluation order as the default, making it transparent to program in that evaluation order, and troublesome to program in the other. This paper develops a type system that is impartial with respect to evaluation order. Evaluation order is implicit in terms, and explicit in types, with by-value and by-name versions of type connectives. A form of intersection type quantifies over evaluation orders, describing code that is agnostic over (that is, polymorphic in) evaluation order. By allowing such generic code, programs can express the by-value and by-name versions of a computation without code duplication. We also formulate a type system that only has by-value connectives, plus a type that generalizes the difference between by-value and by-name connectives: it is either a suspension (by name) or a "no-op" (by value). We show a straightforward encoding of the impartial type system into the more economical one. Then we define an elaboration from the economical language to a call-by-value semantics, and prove that elaborating a well-typed source program, where evaluation order is implicit, produces a well-typed target program where evaluation order is explicit. We also prove a simulation between evaluation of the target program and reductions (either by-value or by-name) in the source program. Finally, we prove that typing, elaboration, and evaluation are faithful to the type annotations given in the source program: if the programmer only writes by-value types, no by-name reductions can occur at run time.
Optimal Sequential Multi-class Diagnosis
Venue: arXiv cs.IT 2020
Year: 2020

Sequential multi-class diagnosis, also known as multi-hypothesis testing, is a classical sequential decision problem with broad applications. However, the optimal solution remains, in general, unknown as the dynamic program suffers from the curse of dimensionality in the posterior belief space. We consider a class of practical problems in which the observation distributions associated with different classes are related through exponential tilting, and show that the reachable beliefs could be restricted on, or near, a set of low-dimensional, time-dependent manifolds with closed-form expressions. This sparsity is driven by the low dimensionality of the observation distributions (which is intuitive) as well as by specific structural interrelations among them (which is less intuitive). We use a matrix factorization approach to uncover the potential low dimensionality hidden in high-dimensional beliefs and reconstruct the beliefs using a diagnostic statistic in lower dimension. For common univariate distributions, e.g., normal, binomial, and Poisson, the belief reconstruction is exact, and the optimal policies can be efficiently computed for a large number of classes. We also characterize the structure of the optimal policy in the reduced dimension. For multivariate distributions, we propose a low-rank matrix approximation scheme that works well when the beliefs are near the low-dimensional manifolds. The optimal policy significantly outperforms the state-of-the-art heuristic policy in quick diagnosis with noisy data. (forthcoming in Operations Research)
Extension Complexity, MSO Logic, and Treewidth
Venue: arXiv cs.DS 2020
Year: 2020

We consider the convex hull $P_φ(G)$ of all satisfying assignments of a given MSO formula $φ$ on a given graph $G$. We show that there exists an extended formulation of the polytope $P_φ(G)$ that can be described by $f(|φ|,τ)\cdot n$ inequalities, where $n$ is the number of vertices in $G$, $τ$ is the treewidth of $G$ and $f$ is a computable function depending only on $φ$ and $τ.$ In other words, we prove that the extension complexity of $P_φ(G)$ is linear in the size of the graph $G$, with a constant depending on the treewidth of $G$ and the formula $φ$. This provides a very general yet very simple meta-theorem about the extension complexity of polytopes related to a wide class of problems and graphs. As a corollary of our main result, we obtain an analogous result % for the weaker MSO$_1$ logic on the wider class of graphs of bounded cliquewidth. Furthermore, we study our main geometric tool which we term the glued product of polytopes. While the glued product of polytopes has been known since the '90s, we are the first to show that it preserves decomposability and boundedness of treewidth of the constraint matrix. This implies that our extension of $P_φ(G)$ is decomposable and has a constraint matrix of bounded treewidth; so far only few classes of polytopes are known to be decomposable. These properties make our extension useful in the construction of algorithms.
Distributed Robust Adaptive Frequency Control of Power Systems with Dynamic Loads
Venue: arXiv cs.SY 2020
Year: 2020

This paper investigates the frequency control of multi-machine power systems subject to uncertain and dynamic net loads. We propose distributed internal model controllers that coordinate synchronous generators and demand response to tackle the unpredictable nature of net loads. Frequency stability is formally guaranteed via Lyapunov analysis. Numerical simulations on the IEEE 68-bus test system demonstrate the effectiveness of the controllers.
Feature-Based Diversity Optimization for Problem Instance Classification
Venue: arXiv cs.NE 2020
Year: 2020

Understanding the behaviour of heuristic search methods is a challenge. This even holds for simple local search methods such as 2-OPT for the Traveling Salesperson problem. In this paper, we present a general framework that is able to construct a diverse set of instances that are hard or easy for a given search heuristic. Such a diverse set is obtained by using an evolutionary algorithm for constructing hard or easy instances that are diverse with respect to different features of the underlying problem. Examining the constructed instance sets, we show that many combinations of two or three features give a good classification of the TSP instances in terms of whether they are hard to be solved by 2-OPT.
Dynamic Balanced Graph Partitioning
Venue: arXiv cs.DS 2020
Year: 2020

This paper initiates the study of the classic balanced graph partitioning problem from an online perspective: Given an arbitrary sequence of pairwise communication requests between $n$ nodes, with patterns that may change over time, the objective is to service these requests efficiently by partitioning the nodes into $\ell$ clusters, each of size $k$, such that frequently communicating nodes are located in the same cluster. The partitioning can be updated dynamically by migrating nodes between clusters. The goal is to devise online algorithms which jointly minimize the amount of inter-cluster communication and migration cost. The problem features interesting connections to other well-known online problems. For example, scenarios with $\ell=2$ generalize online paging, and scenarios with $k=2$ constitute a novel online variant of maximum matching. We present several lower bounds and algorithms for settings both with and without cluster-size augmentation. In particular, we prove that any deterministic online algorithm has a competitive ratio of at least $k$, even with significant augmentation. Our main algorithmic contributions are an $O(k \log{k})$-competitive deterministic algorithm for the general setting with constant augmentation, and a constant competitive algorithm for the maximum matching variant.
3D Time-lapse Reconstruction from Internet Photos
Venue: arXiv cs.CV 2020
Year: 2020

Given an Internet photo collection of a landmark, we compute a 3D time-lapse video sequence where a virtual camera moves continuously in time and space. While previous work assumed a static camera, the addition of camera motion during the time-lapse creates a very compelling impression of parallax. Achieving this goal, however, requires addressing multiple technical challenges, including solving for time-varying depth maps, regularizing 3D point color profiles over time, and reconstructing high quality, hole-free images at every frame from the projected profiles. Our results show photorealistic time-lapses of skylines and natural scenes over many years, with dramatic parallax effects.
UA-DETRAC: A New Benchmark and Protocol for Multi-Object Detection and Tracking
Venue: arXiv cs.CV 2020
Year: 2020

In recent years, numerous effective multi-object tracking (MOT) methods are developed because of the wide range of applications. Existing performance evaluations of MOT methods usually separate the object tracking step from the object detection step by using the same fixed object detection results for comparisons. In this work, we perform a comprehensive quantitative study on the effects of object detection accuracy to the overall MOT performance, using the new large-scale University at Albany DETection and tRACking (UA-DETRAC) benchmark dataset. The UA-DETRAC benchmark dataset consists of 100 challenging video sequences captured from real-world traffic scenes (over 140,000 frames with rich annotations, including occlusion, weather, vehicle category, truncation, and vehicle bounding boxes) for object detection, object tracking and MOT system. We evaluate complete MOT systems constructed from combinations of state-of-the-art object detection and object tracking methods. Our analysis shows the complex effects of object detection accuracy on MOT system performance. Based on these observations, we propose new evaluation tools and metrics for MOT systems that consider both object detection and object tracking for comprehensive analysis.
An Approximation of Theta Functions with Applications to Communications
Venue: arXiv cs.IT 2020
Year: 2020

Computing the theta series of an arbitrary lattice, and more specifically a related quantity known as the flatness factor, has been recently shown to be important for lattice code design in various wireless communication setups. However, the theta series is in general not known in closed form, excluding a small set of very special lattices. In this article, motivated by the practical applications as well as the mathematical problem itself, a simple approximation of the theta series of a lattice is derived. A rigorous analysis of its accuracy is provided. In relation to this, maximum-likelihood decoding in the context of compute-and-forward relaying is studied. Following previous work, it is shown that the related metric can exhibit a flat behavior, which can be characterized by the flatness factor of the decoding function. Contrary to common belief, we note that the decoding metric can be rewritten as a sum over a random lattice only when at most two sources are considered. Using a particular matrix decomposition, a link between the random lattice and the code lattice employed at the transmitter is established, which leads to an explicit criterion for code design, in contrast to implicit criteria derived previously. Finally, candidate lattices are examined with respect to the proposed criterion using the derived theta series approximation.
On the Degrees-of-Freedom of the K-user Distributed Broadcast Channel
Venue: arXiv cs.IT 2020
Year: 2020

We study the Degrees-of-Freedom (DoF) in a wireless setting in which K Transmitters (TXs) aim at jointly serving K users. The performance is studied when the TXs are faced with a distributed Channel State Information (CSI) configuration in which each TX has access to its own multi-user imperfect channel estimate based on which it designs its transmit coefficients. The channel estimates are not only imperfectly acquired but they are also imperfectly shared between the TXs. Our first contribution consists of computing a genie-aided upper bound for the DoF of that setting. Our main contribution is then to develop a new robust transmission scheme that leverages the different qualities of CSI available at the TXs to improve the achieved DoF. We show the surprising result that there is a CSI regime, coined the Weak-CSIT regime, in which the genie-aided upper bound is achieved by the proposed transmission scheme. Interestingly, the optimal DoF in the Weak-CSIT regime only depends on the CSI quality at the best informed TX and not on the CSI quality at all other TXs.
Entangled simultaneity versus classical interactivity in communication complexity
Venue: arXiv cs.CC 2020
Year: 2020

In 1999 Raz demonstrated a partial function that had an efficient quantum two-way communication protocol but no efficient classical two-way protocol and asked, whether there existed a function with an efficient quantum one-way protocol, but still no efficient classical two-way protocol. In 2010 Klartag and Regev demonstrated such a function and asked, whether there existed a function with an efficient quantum simultaneous-messages protocol, but still no efficient classical two-way protocol. In this work we answer the latter question affirmatively and present a partial function Shape, which can be computed by a protocol sending entangled simultaneous messages of poly-logarithmic size, and whose classical two-way complexity is lower bounded by a polynomial.
Property Checking Without Inductive Invariants
Venue: arXiv cs.LO 2020
Year: 2020

We introduce a procedure for proving safety properties. This procedure is based on a technique called Partial Quantifier Elimination (PQE). In contrast to complete quantifier elimination, in PQE, only a part of the formula is taken out of the scope of quantifiers. So, PQE can be dramatically more efficient than complete quantifier elimination. The appeal of our procedure is twofold. First, it can prove a property without generating an inductive invariant. Second, it employs depth-first search and so can be used to find deep bugs.
Narrative Smoothing: Dynamic Conversational Network for the Analysis of TV Series Plots
Venue: arXiv cs.SI 2020
Year: 2020

Modern popular TV series often develop complex storylines spanning several seasons, but are usually watched in quite a discontinuous way. As a result, the viewer generally needs a comprehensive summary of the previous season plot before the new one starts. The generation of such summaries requires first to identify and characterize the dynamics of the series subplots. One way of doing so is to study the underlying social network of interactions between the characters involved in the narrative. The standard tools used in the Social Networks Analysis field to extract such a network rely on an integration of time, either over the whole considered period, or as a sequence of several time-slices. However, they turn out to be inappropriate in the case of TV series, due to the fact the scenes showed onscreen alternatively focus on parallel storylines, and do not necessarily respect a traditional chronology. This makes existing extraction methods inefficient to describe the dynamics of relationships between characters, or to get a relevant instantaneous view of the current social state in the plot. This is especially true for characters shown as interacting with each other at some previous point in the plot but temporarily neglected by the narrative. In this article, we introduce narrative smoothing, a novel, still exploratory, network extraction method. It smooths the relationship dynamics based on the plot properties, aiming at solving some of the limitations present in the standard approaches. In order to assess our method, we apply it to a new corpus of 3 popular TV series, and compare it to both standard approaches. Our results are promising, showing narrative smoothing leads to more relevant observations when it comes to the characterization of the protagonists and their relationships. It could be used as a basis for further modeling the intertwined storylines constituting TV series plots.
How effective can simple ordinal peer grading be?
Venue: arXiv cs.AI 2020
Year: 2020

Ordinal peer grading has been proposed as a simple and scalable solution for computing reliable information about student performance in massive open online courses. The idea is to outsource the grading task to the students themselves as follows. After the end of an exam, each student is asked to rank -- in terms of quality -- a bundle of exam papers by fellow students. An aggregation rule then combines the individual rankings into a global one that contains all students. We define a broad class of simple aggregation rules, which we call type-ordering aggregation rules, and present a theoretical framework for assessing their effectiveness. When statistical information about the grading behaviour of students is available (in terms of a noise matrix that characterizes the grading behaviour of the average student from a student population), the framework can be used to compute the optimal rule from this class with respect to a series of performance objectives that compare the ranking returned by the aggregation rule to the underlying ground truth ranking. For example, a natural rule known as Borda is proved to be optimal when students grade correctly. In addition, we present extensive simulations that validate our theory and prove it to be extremely accurate in predicting the performance of aggregation rules even when only rough information about grading behaviour (i.e., an approximation of the noise matrix) is available. Both in the application of our theoretical framework and in our simulations, we exploit data about grading behaviour of students that have been extracted from two field experiments in the University of Patras.
On higher order computations, rewiring the connectome, and non-von Neumann computer architecture
Venue: arXiv cs.NE 2020
Year: 2020

Structural plasticity in the brain (i.e. rewiring the connectome) may be viewed as mechanisms for dynamic reconfiguration of neural circuits. First order computations in the brain are done by static neural circuits, whereas higher order computations are done by dynamic reconfigurations of the links (synapses) between the neural circuits. Static neural circuits correspond to first order computable functions. Synapse creation (activation) between them correspond to the mathematical notion of function composition. Functionals are higher order functions that take functions as their arguments. The construction of functionals is based on dynamic reconfigurations of function compositions. Perhaps the functionals correspond to rewiring mechanisms of the connectome. The architecture of human mind is different than the von Neumann computer architecture. Higher order computations in the human brain (based on functionals) may suggest a non-von Neumann computer architecture, a challenge posed by John Backus in 1977 \cite{Backus}. The presented work is a substantial extension and revision of the paper published in Proc. ICANN2016.
Robust Machine Learning for Encrypted Traffic Classification
Venue: arXiv cs.CR 2020
Year: 2020

Desktops and laptops can be maliciously exploited to violate privacy. In this paper, we consider the daily battle between the passive attacker who is targeting a specific user against a user that may be adversarial opponent. In this scenario, while the attacker tries to choose the best vector attack by surreptitiously monitoring the victims encrypted network traffic in order to identify users parameters such as the Operating System (OS), browser and apps. The user may use tools such as a Virtual Private Network (VPN) or even change protocols parameters to protect his/her privacy. We provide a large dataset of more than 20,000 examples for this task. We run a comprehensive set of experiments, that achieves high (above 85) classification accuracy, robustness and resilience to changes of features as a function of different network conditions at test time. We also show the effect of a small training set on the accuracy.
Discriminative Embeddings of Latent Variable Models for Structured Data
Venue: arXiv cs.LG 2020
Year: 2020

Kernel classifiers and regressors designed for structured data, such as sequences, trees and graphs, have significantly advanced a number of interdisciplinary areas such as computational biology and drug design. Typically, kernels are designed beforehand for a data type which either exploit statistics of the structures or make use of probabilistic generative models, and then a discriminative classifier is learned based on the kernels via convex optimization. However, such an elegant two-stage approach also limited kernel methods from scaling up to millions of data points, and exploiting discriminative information to learn feature representations. We propose, structure2vec, an effective and scalable approach for structured data representation based on the idea of embedding latent variable models into feature spaces, and learning such feature spaces using discriminative information. Interestingly, structure2vec extracts features by performing a sequence of function mappings in a way similar to graphical model inference procedures, such as mean field and belief propagation. In applications involving millions of data points, we showed that structure2vec runs 2 times faster, produces models which are $10,000$ times smaller, while at the same time achieving the state-of-the-art predictive performance.
Harnessing Deep Neural Networks with Logic Rules
Venue: arXiv cs.LG 2020
Year: 2020

Combining deep neural networks with structured logic rules is desirable to harness flexibility and reduce uninterpretability of the neural models. We propose a general framework capable of enhancing various types of neural networks (e.g., CNNs and RNNs) with declarative first-order logic rules. Specifically, we develop an iterative distillation method that transfers the structured information of logic rules into the weights of neural networks. We deploy the framework on a CNN for sentiment analysis, and an RNN for named entity recognition. With a few highly intuitive rules, we obtain substantial improvements and achieve state-of-the-art or comparable results to previous best-performing systems.