OpenRaiser/Intern-Atlas huggingface dataset:
Hanani-Tutte for approximating maps of graphs
Venue: arXiv cs.CG 2022
Year: 2022

We resolve in the affirmative conjectures of Repovs and A. Skopenkov (1998), and M. Skopenkov (2003) generalizing the classical Hanani-Tutte theorem to the setting of approximating maps of graphs on 2-dimensional surfaces by embeddings. Our proof of this result is constructive and almost immediately implies an efficient algorithm for testing if a given piecewise linear map of a graph in a surface is approximable by an embedding. More precisely, an instance of this problem consists of (i) a graph G whose vertices are partitioned into clusters and whose inter-cluster edges are partitioned into bundles, and (ii) a region R of a 2-dimensional compact surface M given as the union of a set of pairwise disjoint discs corresponding to the clusters and a set of pairwise non-intersecting "pipes" corresponding to the bundles, connecting certain pairs of these discs. We are to decide whether G can be embedded inside M so that the vertices in every cluster are drawn in the corresponding disc, the edges in every bundle pass only through its corresponding pipe, and every edge crosses the boundary of each disc at most once.
On the mathematics of beauty: beautiful images
Venue: arXiv cs.CV 2022
Year: 2022

In this paper, we will study the simplest kind of beauty which can be found in simple visual patterns. The proposed approach shows that aesthetically appealing patterns deliver higher amount of information over multiple levels in comparison with less aesthetically appealing patterns when the same amount of energy is used. The proposed approach is used to classify aesthetically appealing patterns.
Undecidability of first-order modal and intuitionistic logics with two variables and one monadic predicate letter
Venue: arXiv cs.LO 2022
Year: 2022

We prove that the positive fragment of first-order intuitionistic logic in the language with two variables and a single monadic predicate letter, without constants and equality, is undecidable. This holds true regardless of whether we consider semantics with expanding or constant domains. We then generalise this result to intervals [QBL, QKC] and [QBL, QFL], where QKC is the logic of the weak law of the excluded middle and QBL and QFL are first-order counterparts of Visser's basic and formal logics, respectively. We also show that, for most "natural" first-order modal logics, the two-variable fragment with a single monadic predicate letter, without constants and equality, is undecidable, regardless of whether we consider semantics with expanding or constant domains. These include all sublogics of QKTB, QGL, and QGrz -- among them, QK, QT, QKB, QD, QK4, and QS4.
Gradient Episodic Memory for Continual Learning
Venue: arXiv cs.LG 2022
Year: 2022

One major obstacle towards AI is the poor ability of models to solve new problems quicker, and without forgetting previously acquired knowledge. To better understand this issue, we study the problem of continual learning, where the model observes, once and one by one, examples concerning a sequence of tasks. First, we propose a set of metrics to evaluate models learning over a continuum of data. These metrics characterize models not only by their test accuracy, but also in terms of their ability to transfer knowledge across tasks. Second, we propose a model for continual learning, called Gradient Episodic Memory (GEM) that alleviates forgetting, while allowing beneficial transfer of knowledge to previous tasks. Our experiments on variants of the MNIST and CIFAR-100 datasets demonstrate the strong performance of GEM when compared to the state-of-the-art.
Kleene Algebra Modulo Theories
Venue: arXiv cs.PL 2022
Year: 2022

Kleene algebras with tests (KATs) offer sound, complete, and decidable equational reasoning about regularly structured programs. Interest in KATs has increased greatly since NetKAT demonstrated how well extensions of KATs with domain-specific primitives and extra axioms apply to computer networks. Unfortunately, extending a KAT to a new domain by adding custom primitives, proving its equational theory sound and complete, and coming up with an efficient implementation is still an expert's task. Abstruse metatheory is holding back KAT's potential. We offer a fast path to a "minimum viable model" of a KAT, formally or in code through our framework, Kleene algebra modulo theories (KMT). Given primitives and a notion of state, we can automatically derive a corresponding KAT's semantics, prove its equational theory sound and complete with respect to a tracing semantics (programs are denoted as traces of states), and derive a normalization-based decision procedure for equivalence checking. Our framework is based on pushback, a generalization of weakest preconditions that specifies how predicates and actions interact. We offer several case studies, showing tracing variants of theories from the literature (bitvectors, NetKAT) along with novel compositional theories (products, temporal logic, and sets). We derive new results over unbounded state, reasoning about monotonically increasing, unbounded natural numbers. Our OCaml implementation closely matches the theory: users define and compose KATs with the module system.
Constructing Light Spanners Deterministically in Near-Linear Time
Venue: arXiv cs.DS 2022
Year: 2022

Graph spanners are well-studied and widely used both in theory and practice. In a recent breakthrough, Chechik and Wulff-Nilsen [CW18] improved the state-of-the-art for light spanners by constructing a $(2k-1)(1+ε)$-spanner with $O(n^{1+1/k})$ edges and $O_ε(n^{1/k})$ lightness. Soon after, Filtser and Solomon [FS19] showed that the classic greedy spanner construction achieves the same bounds The major drawback of the greedy spanner is its running time of $O(mn^{1+1/k})$ (which is faster than [CW16]). This makes the construction impractical even for graphs of moderate size. Much faster spanner constructions do exist but they only achieve lightness $Ω_ε(kn^{1/k})$, even when randomization is used. The contribution of this paper is deterministic spanner constructions that are fast, and achieve similar bounds as the state-of-the-art slower constructions. Our first result is an $O_ε(n^{2+1/k+ε'})$ time spanner construction which achieves the state-of-the-art bounds. Our second result is an $O_ε(m + n\log n)$ time construction of a spanner with $(2k-1)(1+ε)$ stretch, $O(\log k\cdot n^{1+1/k})$ edges and $O_ε(\log k\cdot n^{1/k})$ lightness. This is an exponential improvement in the dependence on $k$ compared to the previous result with such running time. Finally, for the important special case where $k=\log n$, for every constant $ε>0$, we provide an $O(m+n^{1+ε})$ time construction that produces an $O(\log n)$-spanner with $O(n)$ edges and $O(1)$ lightness which is asymptotically optimal. This is the first known sub-quadratic construction of such a spanner for any $k = ω(1)$. To achieve our constructions, we show a novel deterministic incremental approximate distance oracle, which may be of independent interest.
Stable super-resolution limit and smallest singular value of restricted Fourier matrices
Venue: arXiv cs.IT 2022
Year: 2022

We consider the inverse problem of recovering the locations and amplitudes of a collection of point sources represented as a discrete measure, given $M+1$ of its noisy low-frequency Fourier coefficients. Super-resolution refers to a stable recovery when the distance $Δ$ between the two closest point sources is less than $1/M$. We introduce a clumps model where the point sources are closely spaced within several clumps. Under this assumption, we derive a non-asymptotic lower bound for the minimum singular value of a Vandermonde matrix whose nodes are determined by the point sources. Our estimate is given as a weighted $\ell^2$ sum, where each term only depends on the configuration of each individual clump. The main novelty is that our lower bound obtains an exact dependence on the {\it Super-Resolution Factor} $SRF=(MΔ)^{-1}$. As noise level increases, the {\it sensitivity of the noise-space correlation function in the MUSIC algorithm} degrades according to a power law in $SRF$ where the exponent depends on the cardinality of the largest clump. Numerical experiments validate our theoretical bounds for the minimum singular value and the sensitivity of MUSIC. We also provide lower and upper bounds for a min-max error of super-resolution for the grid model, which in turn is closely related to the minimum singular value of Vandermonde matrices.
Approximations for Generalized Unsplittable Flow on Paths with Application to Power Systems Optimization
Venue: arXiv cs.DS 2022
Year: 2022

The Unsplittable Flow on a Path (UFP) problem has garnered considerable attention as a challenging combinatorial optimization problem with notable practical implications. Steered by its pivotal applications in power engineering, the present work formulates a novel generalization of UFP, wherein demands and capacities in the input instance are monotone step functions over the set of edges. As an initial step towards tackling this generalization, we draw on and extend ideas from prior research to devise a quasi-polynomial time approximation scheme (QPTAS) under the premise that the demands and capacities lie in a quasi-polynomial range. Second, retaining the same assumption, an efficient logarithmic approximation is introduced for the single-source variant of the problem. Finally, we round up the contributions by designing a (kind of) black-box reduction that, under some mild conditions, allows to translate LP-based approximation algorithms for the studied problem into their counterparts for the Alternating Current Optimal Power Flow (AC OPF) problem -- a fundamental workflow in operation and control of power systems.
Connecting Width and Structure in Knowledge Compilation (Extended Version)
Venue: arXiv cs.DB 2022
Year: 2022

Several query evaluation tasks can be done via knowledge compilation: the query result is compiled as a lineage circuit from which the answer can be determined. For such tasks, it is important to leverage some width parameters of the circuit, such as bounded treewidth or pathwidth, to convert the circuit to structured classes, e.g., deterministic structured NNFs (d-SDNNFs) or OBDDs. In this work, we show how to connect the width of circuits to the size of their structured representation, through upper and lower bounds. For the upper bound, we show how bounded-treewidth circuits can be converted to a d-SDNNF, in time linear in the circuit size. Our bound, unlike existing results, is constructive and only singly exponential in the treewidth. We show a related lower bound on monotone DNF or CNF formulas, assuming a constant bound on the arity (size of clauses) and degree (number of occurrences of each variable). Specifically, any d-SDNNF (resp., SDNNF) for such a DNF (resp., CNF) must be of exponential size in its treewidth; and the same holds for pathwidth when compiling to OBDDs. Our lower bounds, in contrast with most previous work, apply to any formula of this class, not just a well-chosen family. Hence, for our language of DNF and CNF, pathwidth and treewidth respectively characterize the efficiency of compiling to OBDDs and (d-)SDNNFs, that is, compilation is singly exponential in the width parameter. We conclude by applying our lower bound results to the task of query evaluation.
Approximating the $2$-Machine Flow Shop Problem with Exact Delays Taking Two Values
Venue: arXiv cs.DS 2022
Year: 2022

In the $2$-Machine Flow Shop problem with exact delays the operations of each job are separated by a given time lag (delay). Leung et al. (2007) established that the problem is strongly NP-hard when the delays may have at most two different values. We present further results for this case: we prove that the existence of $(1.25-\varepsilon)$-approximation implies P$=$NP and develop a $2$-approximation algorithm.
Maximizing Submodular or Monotone Approximately Submodular Functions by Multi-objective Evolutionary Algorithms
Venue: arXiv cs.NE 2022
Year: 2022

Evolutionary algorithms (EAs) are a kind of nature-inspired general-purpose optimization algorithm, and have shown empirically good performance in solving various real-word optimization problems. During the past two decades, promising results on the running time analysis (one essential theoretical aspect) of EAs have been obtained, while most of them focused on isolated combinatorial optimization problems, which do not reflect the general-purpose nature of EAs. To provide a general theoretical explanation of the behavior of EAs, it is desirable to study their performance on general classes of combinatorial optimization problems. To the best of our knowledge, the only result towards this direction is the provably good approximation guarantees of EAs for the problem class of maximizing monotone submodular functions with matroid constraints. The aim of this work is to contribute to this line of research. Considering that many combinatorial optimization problems involve non-monotone or non-submodular objective functions, we study the general problem classes, maximizing submodular functions with/without a size constraint and maximizing monotone approximately submodular functions with a size constraint. We prove that a simple multi-objective EA called GSEMO-C can generally achieve good approximation guarantees in polynomial expected running time.
Towards Practical Verification of Machine Learning: The Case of Computer Vision Systems
Venue: arXiv cs.CR 2022
Year: 2022

Due to the increasing usage of machine learning (ML) techniques in security- and safety-critical domains, such as autonomous systems and medical diagnosis, ensuring correct behavior of ML systems, especially for different corner cases, is of growing importance. In this paper, we propose a generic framework for evaluating security and robustness of ML systems using different real-world safety properties. We further design, implement and evaluate VeriVis, a scalable methodology that can verify a diverse set of safety properties for state-of-the-art computer vision systems with only blackbox access. VeriVis leverage different input space reduction techniques for efficient verification of different safety properties. VeriVis is able to find thousands of safety violations in fifteen state-of-the-art computer vision systems including ten Deep Neural Networks (DNNs) such as Inception-v3 and Nvidia's Dave self-driving system with thousands of neurons as well as five commercial third-party vision APIs including Google vision and Clarifai for twelve different safety properties. Furthermore, VeriVis can successfully verify local safety properties, on average, for around 31.7% of the test images. VeriVis finds up to 64.8x more violations than existing gradient-based methods that, unlike VeriVis, cannot ensure non-existence of any violations. Finally, we show that retraining using the safety violations detected by VeriVis can reduce the average number of violations up to 60.2%.
Flow Decomposition
Venue: arXiv cs.IT 2022
Year: 2022

The decode-forward achievable region is studied for general networks. The region is subject to a fundamental tension in which nodes individually benefit at the expense of others. The complexity of the region depends on all the ways of resolving this tension. Two sets of constraints define an outer-bound on the decode-forward region: first, the conventional mutual-information inequalities implied by the one-relay channel, and second, causality constraints that ensure nodes only forward messages they have already decoded. The framework of flow decomposition is introduced to show these constraints are also sufficient. Flow decomposition provides a way of manipulating regular decode-forward schemes without the long encoding delays and restrictions on bidirectional communication of backward decoding. The two structures that define a flow decomposition are flows and layerings. Flows specify the nodes which encode messages from each source (i.e., the routes) and the encoding delays. Layerings specify the messages decoded at a specific node in the channel. We focus on two types of flow: hierarchical flow, with tree-like routes, and all-cast flow, where each route covers all nodes. For arbitrary flows of either type and any rate-vector satisfying the mutual-information constraints at a specific node, we prove there are equivalent flows and a layering that satisfy both the mutual-information and causality constraints. In separate work, we show that only the mutual-information constraints are active in channels with hierarchical flow, which implies the achievable region has minimal complexity. In channels with all-cast flow, the achievable region is computable.
SWRL2SPIN: A tool for transforming SWRL rule bases in OWL ontologies to object-oriented SPIN rules
Venue: arXiv cs.AI 2022
Year: 2022

Semantic Web Rule Language (SWRL) combines OWL (Web Ontology Language) ontologies with Horn Logic rules of the Rule Markup Language (RuleML) family. Being supported by ontology editors, rule engines and ontology reasoners, it has become a very popular choice for developing rule-based applications on top of ontologies. However, SWRL is probably not go-ing to become a WWW Consortium standard, prohibiting industrial acceptance. On the other hand, SPIN (SPARQL Inferencing Notation) has become a de-facto industry standard to rep-resent SPARQL rules and constraints on Semantic Web models, building on the widespread acceptance of SPARQL (SPARQL Protocol and RDF Query Language). In this paper, we ar-gue that the life of existing SWRL rule-based ontology applications can be prolonged by con-verting them to SPIN. To this end, we have developed the SWRL2SPIN tool in Prolog that transforms SWRL rules into SPIN rules, considering the object-orientation of SPIN, i.e. linking rules to the appropriate ontology classes and optimizing them, as derived by analysing the rule conditions.
Quantum Algorithm Implementations for Beginners
Venue: arXiv cs.ET 2022
Year: 2022

As quantum computers become available to the general public, the need has arisen to train a cohort of quantum programmers, many of whom have been developing classical computer programs for most of their careers. While currently available quantum computers have less than 100 qubits, quantum computing hardware is widely expected to grow in terms of qubit count, quality, and connectivity. This review aims to explain the principles of quantum programming, which are quite different from classical programming, with straightforward algebra that makes understanding of the underlying fascinating quantum mechanical principles optional. We give an introduction to quantum computing algorithms and their implementation on real quantum hardware. We survey 20 different quantum algorithms, attempting to describe each in a succinct and self-contained fashion. We show how these algorithms can be implemented on IBM's quantum computer, and in each case, we discuss the results of the implementation with respect to differences between the simulator and the actual hardware runs. This article introduces computer scientists, physicists, and engineers to quantum algorithms and provides a blueprint for their implementations.
Real-Time Rotation-Invariant Face Detection with Progressive Calibration Networks
Venue: arXiv cs.CV 2022
Year: 2022

Rotation-invariant face detection, i.e. detecting faces with arbitrary rotation-in-plane (RIP) angles, is widely required in unconstrained applications but still remains as a challenging task, due to the large variations of face appearances. Most existing methods compromise with speed or accuracy to handle the large RIP variations. To address this problem more efficiently, we propose Progressive Calibration Networks (PCN) to perform rotation-invariant face detection in a coarse-to-fine manner. PCN consists of three stages, each of which not only distinguishes the faces from non-faces, but also calibrates the RIP orientation of each face candidate to upright progressively. By dividing the calibration process into several progressive steps and only predicting coarse orientations in early stages, PCN can achieve precise and fast calibration. By performing binary classification of face vs. non-face with gradually decreasing RIP ranges, PCN can accurately detect faces with full $360^{\circ}$ RIP angles. Such designs lead to a real-time rotation-invariant face detector. The experiments on multi-oriented FDDB and a challenging subset of WIDER FACE containing rotated faces in the wild show that our PCN achieves quite promising performance.
Generating a Fusion Image: One's Identity and Another's Shape
Venue: arXiv cs.CV 2022
Year: 2022

Generating a novel image by manipulating two input images is an interesting research problem in the study of generative adversarial networks (GANs). We propose a new GAN-based network that generates a fusion image with the identity of input image x and the shape of input image y. Our network can simultaneously train on more than two image datasets in an unsupervised manner. We define an identity loss LI to catch the identity of image x and a shape loss LS to get the shape of y. In addition, we propose a novel training method called Min-Patch training to focus the generator on crucial parts of an image, rather than its entirety. We show qualitative results on the VGG Youtube Pose dataset, Eye dataset (MPIIGaze and UnityEyes), and the Photo-Sketch-Cartoon dataset.
Resource-Bounded Kolmogorov Complexity Provides an Obstacle to Soficness of Multidimensional Shifts
Venue: arXiv cs.DM 2022
Year: 2022

We suggest necessary conditions of soficness of multidimensional shifts formulated in termsof resource-bounded Kolmogorov complexity. Using this technique we provide examples ofeffective and non-sofic shifts on $\mathbb{Z}^2$ with very low block complexity: the number of globallyadmissible patterns of size $n\times n$ grows only as a polynomial in $n$. We also show that moreconventional proofs of non-soficness for multi-dimensional effective shifts can be expressed interms of Kolmogorov complexity with unbounded computational resources.
A Survey on Sentiment and Emotion Analysis for Computational Literary Studies
Venue: arXiv cs.CL 2022
Year: 2022

Emotions are a crucial part of compelling narratives: literature tells us about people with goals, desires, passions, and intentions. Emotion analysis is part of the broader and larger field of sentiment analysis, and receives increasing attention in literary studies. In the past, the affective dimension of literature was mainly studied in the context of literary hermeneutics. However, with the emergence of the research field known as Digital Humanities (DH), some studies of emotions in a literary context have taken a computational turn. Given the fact that DH is still being formed as a field, this direction of research can be rendered relatively new. In this survey, we offer an overview of the existing body of research on emotion analysis as applied to literature. The research under review deals with a variety of topics including tracking dramatic changes of a plot development, network analysis of a literary text, and understanding the emotionality of texts, among other topics.