OpenRaiser/Intern-Atlas huggingface dataset:
Weighted propositional configuration logics: A specification language for architectures with quantitative features
Venue: arXiv cs.LO 2020
Year: 2020

We introduce and investigate a weighted propositional configuration logic over commutative semirings. Our logic is intended to serve as a specification language for software architectures with quantitative features. We prove an efficient construction of full normal forms and decidability of equivalence of formulas in this logic. We illustrate the motivation of this work by describing well-known architectures equipped with quantitative characteristics using formulas in our logic.
Network Inspection for Detecting Strategic Attacks
Venue: arXiv cs.GT 2020
Year: 2020

This article studies a problem of strategic network inspection, in which a defender (agency) is tasked with detecting the presence of multiple attacks in the network. An inspection strategy entails monitoring the network components, possibly in a randomized manner, using a given number of detectors. We formulate the network inspection problem $(\mathcal{P})$ as a large-scale bilevel optimization problem, in which the defender seeks to determine an inspection strategy with minimum number of detectors that ensures a target expected detection rate under worst-case attacks. We show that optimal solutions of $(\mathcal{P})$ can be obtained from the equilibria of a large-scale zero-sum game. Our equilibrium analysis involves both game-theoretic and combinatorial arguments, and leads to a computationally tractable approach to solve $(\mathcal{P})$. Firstly, we construct an approximate solution by utilizing solutions of minimum set cover (MSC) and maximum set packing (MSP) problems, and evaluate its detection performance. In fact, this construction generalizes some of the known results in network security games. Secondly, we leverage properties of the optimal detection rate to iteratively refine our MSC/MSP-based solution through a column generation procedure. Computational results on benchmark water networks demonstrate the scalability, performance, and operational feasibility of our approach. The results indicate that utilities can achieve a high level of protection in large-scale networks by strategically positioning a small number of detectors.
Benchmark Dataset for Mid-Price Forecasting of Limit Order Book Data with Machine Learning Methods
Venue: arXiv cs.CE 2020
Year: 2020

Managing the prediction of metrics in high-frequency financial markets is a challenging task. An efficient way is by monitoring the dynamics of a limit order book to identify the information edge. This paper describes the first publicly available benchmark dataset of high-frequency limit order markets for mid-price prediction. We extracted normalized data representations of time series data for five stocks from the NASDAQ Nordic stock market for a time period of ten consecutive days, leading to a dataset of ~4,000,000 time series samples in total. A day-based anchored cross-validation experimental protocol is also provided that can be used as a benchmark for comparing the performance of state-of-the-art methodologies. Performance of baseline approaches are also provided to facilitate experimental comparisons. We expect that such a large-scale dataset can serve as a testbed for devising novel solutions of expert systems for high-frequency limit order book data analysis.
A rational analysis of curiosity
Venue: arXiv cs.AI 2020
Year: 2020

We present a rational analysis of curiosity, proposing that people's curiosity is driven by seeking stimuli that maximize their ability to make appropriate responses in the future. This perspective offers a way to unify previous theories of curiosity into a single framework. Experimental results confirm our model's predictions, showing how the relationship between curiosity and confidence can change significantly depending on the nature of the environment. Please refer to https://psyarxiv.com/wg5m6/ for a more updated version of this manuscript with a more detailed modeling section with extensive experiments.
Bandit Regret Scaling with the Effective Loss Range
Venue: arXiv cs.LG 2020
Year: 2020

We study how the regret guarantees of nonstochastic multi-armed bandits can be improved, if the effective range of the losses in each round is small (e.g. the maximal difference between two losses in a given round). Despite a recent impossibility result, we show how this can be made possible under certain mild additional assumptions, such as availability of rough estimates of the losses, or advance knowledge of the loss of a single, possibly unspecified arm. Along the way, we develop a novel technique which might be of independent interest, to convert any multi-armed bandit algorithm with regret depending on the loss range, to an algorithm with regret depending only on the effective range, while avoiding predictably bad arms altogether.
Kernel Truncated Regression Representation for Robust Subspace Clustering
Venue: arXiv cs.CV 2020
Year: 2020

Subspace clustering aims to group data points into multiple clusters of which each corresponds to one subspace. Most existing subspace clustering approaches assume that input data lie on linear subspaces. In practice, however, this assumption usually does not hold. To achieve nonlinear subspace clustering, we propose a novel method, called kernel truncated regression representation. Our method consists of the following four steps: 1) projecting the input data into a hidden space, where each data point can be linearly represented by other data points; 2) calculating the linear representation coefficients of the data representations in the hidden space; 3) truncating the trivial coefficients to achieve robustness and block-diagonality; and 4) executing the graph cutting operation on the coefficient matrix by solving a graph Laplacian problem. Our method has the advantages of a closed-form solution and the capacity of clustering data points that lie on nonlinear subspaces. The first advantage makes our method efficient in handling large-scale datasets, and the second one enables the proposed method to conquer the nonlinear subspace clustering challenge. Extensive experiments on six benchmarks demonstrate the effectiveness and the efficiency of the proposed method in comparison with current state-of-the-art approaches.
Fashion Forward: Forecasting Visual Style in Fashion
Venue: arXiv cs.CV 2020
Year: 2020

What is the future of fashion? Tackling this question from a data-driven vision perspective, we propose to forecast visual style trends before they occur. We introduce the first approach to predict the future popularity of styles discovered from fashion images in an unsupervised manner. Using these styles as a basis, we train a forecasting model to represent their trends over time. The resulting model can hypothesize new mixtures of styles that will become popular in the future, discover style dynamics (trendy vs. classic), and name the key visual attributes that will dominate tomorrow's fashion. We demonstrate our idea applied to three datasets encapsulating 80,000 fashion products sold across six years on Amazon. Results indicate that fashion forecasting benefits greatly from visual analysis, much more than textual or meta-data cues surrounding products.
A New 3D Method to Segment the Lumbar Vertebral Bodies and to Determine Bone Mineral Density and Geometry
Venue: arXiv cs.CV 2020
Year: 2020

In this paper we present a new 3D segmentation approach for the vertebrae of the lower thoracic and the lumbar spine in spiral computed tomography datasets. We implemented a multi-step procedure. Its main components are deformable models, volume growing, and morphological operations. The performance analysis that included an evaluation of accuracy using the European Spine Phantom, and of intra-operator precision using clinical CT datasets from 10 patients highlight the potential for clinical use. The intra-operator precision of the segmentation procedure was better than 1% for Bone Mineral Density (BMD) and better than 1.8% for volume. The long-term goal of this work is to enable better fracture prediction and improved patient monitoring in the field of osteoporosis. A true 3D segmentation also enables an accurate measurement of geometrical parameters that can augment the classical measurement of BMD.
Approximate Generalized Matching: $f$-Factors and $f$-Edge Covers
Venue: arXiv cs.DS 2020
Year: 2020

In this paper we present linear time approximation schemes for several generalized matching problems on nonbipartite graphs. Our results include $O_ε(m)$-time algorithms for $(1-ε)$-maximum weight $f$-factor and $(1+ε)$-approximate minimum weight $f$-edge cover. As a byproduct, we also obtain direct algorithms for the exact cardinality versions of these problems running in $O(m\sqrt{f(V)})$ time. The technical contributions of this work include an efficient method for maintaining {\em relaxed complementary slackness} in generalized matching problems and approximation-preserving reductions between the $f$-factor and $f$-edge cover problems.
Extract with Order for Coherent Multi-Document Summarization
Venue: arXiv cs.CL 2020
Year: 2020

In this work, we aim at developing an extractive summarizer in the multi-document setting. We implement a rank based sentence selection using continuous vector representations along with key-phrases. Furthermore, we propose a model to tackle summary coherence for increasing readability. We conduct experiments on the Document Understanding Conference (DUC) 2004 datasets using ROUGE toolkit. Our experiments demonstrate that the methods bring significant improvements over the state of the art methods in terms of informativity and coherence.
Multidimensional Fibonacci Coding
Venue: arXiv cs.IT 2020
Year: 2020

Fibonacci codes are self-synchronizing variable-length codes that are proven useful for their robustness and compression capability. Asymptotically, these codes provide better compression efficiency as the order of the underlying Fibonacci sequence increases, but at the price of the increased suffix length. We propose a circumvention to this problem by introducing higher-dimensional Fibonacci codes for integer vectors. In the process, we provide extensive theoretical background and generalize the theorem of Zeckendorf to higher order. As thus, our work unify several variations of Zeckendorf's theorem while also providing new grounds for its legitimacy.
A Tutorial on Thompson Sampling
Venue: arXiv cs.LG 2020
Year: 2020

Thompson sampling is an algorithm for online decision problems where actions are taken sequentially in a manner that must balance between exploiting what is known to maximize immediate performance and investing to accumulate new information that may improve future performance. The algorithm addresses a broad range of problems in a computationally efficient manner and is therefore enjoying wide use. This tutorial covers the algorithm and its application, illustrating concepts through a range of examples, including Bernoulli bandit problems, shortest path problems, product recommendation, assortment, active learning with neural networks, and reinforcement learning in Markov decision processes. Most of these problems involve complex information structures, where information revealed by taking an action informs beliefs about other actions. We will also discuss when and why Thompson sampling is or is not effective and relations to alternative algorithms.
Polynomial-time algorithm for Maximum Weight Independent Set on $P_6$-free graphs
Venue: arXiv cs.DS 2020
Year: 2020

In the classic Maximum Weight Independent Set problem we are given a graph $G$ with a nonnegative weight function on vertices, and the goal is to find an independent set in $G$ of maximum possible weight. While the problem is NP-hard in general, we give a polynomial-time algorithm working on any $P_6$-free graph, that is, a graph that has no path on $6$ vertices as an induced subgraph. This improves the polynomial-time algorithm on $P_5$-free graphs of Lokshtanov et al. (SODA 2014), and the quasipolynomial-time algorithm on $P_6$-free graphs of Lokshtanov et al (SODA 2016). The main technical contribution leading to our main result is enumeration of a polynomial-size family $\mathcal{F}$ of vertex subsets with the following property: for every maximal independent set $I$ in the graph, $\mathcal{F}$ contains all maximal cliques of some minimal chordal completion of $G$ that does not add any edge incident to a vertex of $I$.
On Euler's inequality and automated reasoning with dynamic geometry
Venue: arXiv cs.SC 2020
Year: 2020

Euler's inequality $R\geq 2r$ can be investigated in a novel way by using implicit loci in GeoGebra. Some unavoidable side effects of the implicit locus computation introduce unexpected algebraic curves. By using a mixture of symbolic and numerical methods a possible approach is sketched up to investigate the situation. By exploiting fast GPU computations, a web application written in CindyJS helps in understanding the situation even better.
Chessboard and chess piece recognition with the support of neural networks
Venue: arXiv cs.CV 2020
Year: 2020

Chessboard and chess piece recognition is a computer vision problem that has not yet been efficiently solved. However, its solution is crucial for many experienced players who wish to compete against AI bots, but also prefer to make decisions based on the analysis of a physical chessboard. It is also important for organizers of chess tournaments who wish to digitize play for online broadcasting or ordinary players who wish to share their gameplay with friends. Typically, such digitization tasks are performed by humans or with the aid of specialized chessboards and pieces. However, neither solution is easy or convenient. To solve this problem, we propose a novel algorithm for digitizing chessboard configurations. We designed a method that is resistant to lighting conditions and the angle at which images are captured, and works correctly with numerous chessboard styles. The proposed algorithm processes pictures iteratively. During each iteration, it executes three major sub-processes: detecting straight lines, finding lattice points, and positioning the chessboard. Finally, we identify all chess pieces and generate a description of the board utilizing standard notation. For each of these steps, we designed our own algorithm that surpasses existing solutions. We support our algorithms by utilizing machine learning techniques whenever possible. The described method performs extraordinarily well and achieves an accuracy over $99.5\%$ for detecting chessboard lattice points (compared to the $74\%$ for the best alternative), $95\%$ (compared to $60\%$ for the best alternative) for positioning the chessboard in an image, and almost $95\%$ for chess piece recognition.
Complete algorithms for algebraic strongest postconditions and weakest preconditions in polynomial ODEs
Venue: arXiv cs.LO 2020
Year: 2020

A system of polynomial ordinary differential equations (ODEs) is specified via a vector of multivariate polynomials, or vector field, $F$. A safety assertion $ψ\rightarrow[F]ϕ$ means that the trajectory of the system will lie in a subset $ϕ$ (the postcondition) of the state-space, whenever the initial state belongs to a subset $ψ$ (the precondition). We consider the case when $ϕ$ and $ψ$ are algebraic varieties, that is, zero sets of polynomials. In particular, polynomials specifying the postcondition can be seen as a system's conservation laws implied by $ψ$. Checking the validity of algebraic safety assertions is a fundamental problem in, for instance, hybrid systems. We consider a generalized version of this problem, and offer an algorithm that, given a user specified polynomial set $P$ and an algebraic precondition $ψ$, finds the largest subset of polynomials in $P$ implied by $ψ$ (relativized strongest postcondition). Under certain assumptions on $ϕ$, this algorithm can also be used to find the largest algebraic invariant included in $ϕ$ and the weakest algebraic precondition for $ϕ$. Applications to continuous semialgebraic systems are also considered. The effectiveness of the proposed algorithm is demonstrated on several case studies from the literature.
Learning Actionable Analytics from Multiple Software Projects
Venue: arXiv cs.SE 2020
Year: 2020

The current generation of software analytics tools are mostly prediction algorithms (e.g. support vector machines, naive bayes, logistic regression, etc). While prediction is useful, after prediction comes planning about what actions to take in order to improve quality. This research seeks methods that generate demonstrably useful guidance on "what to do" within the context of a specific software project. Specifically, we propose XTREE (for within-project planning) and BELLTREE (for cross-project planning) to generating plans that can improve software quality. Each such plan has the property that, if followed, it reduces the expected number of future defect reports. To find this expected number, planning was first applied to data from release x. Next, we looked for changes in release x+1 that conformed to our plans. This procedure was applied using a range of planners from the literature, as well as XTREE. In 10 open-source JAVA systems, several hundreds of defects were reduced in sections of the code that conformed to XTREE's plans. Further, when compared to other planners, XTREE's plans were found to be easier to implement (since they were shorter) and more effective at reducing the expected number of defects.
Read Mapping Near Non-Volatile Memory
Venue: arXiv cs.DC 2020
Year: 2020

DNA sequencing is the physical/biochemical process of identifying the location of the four bases (Adenine, Guanine, Cytosine, Thymine) in a DNA strand. As semiconductor technology revolutionized computing, modern DNA sequencing technology (termed Next Generation Sequencing, NGS)revolutionized genomic research. As a result, modern NGS platforms can sequence hundreds of millions of short DNA fragments in parallel. The sequenced DNA fragments, representing the output of NGS platforms, are termed reads. Besides genomic variations, NGS imperfections induce noise in reads. Mapping each read to (the most similar portion of) a reference genome of the same species, i.e., read mapping, is a common critical first step in a diverse set of emerging bioinformatics applications. Mapping represents a search-heavy memory-intensive similarity matching problem, therefore, can greatly benefit from near-memory processing. Intuition suggests using fast associative search enabled by Ternary Content Addressable Memory (TCAM) by construction. However, the excessive energy consumption and lack of support for similarity matching (under NGS and genomic variation induced noise) renders direct application of TCAM infeasible, irrespective of volatility, where only non-volatile TCAM can accommodate the large memory footprint in an area-efficient way. This paper introduces GeNVoM, a scalable, energy-efficient and high-throughput solution. Instead of optimizing an algorithm developed for general-purpose computers or GPUs, GeNVoM rethinks the algorithm and non-volatile TCAM-based accelerator design together from the ground up. Thereby GeNVoM can improve the throughput by up to 113.5 times (3.6); the energy consumption, by up to 210.9 times (1.36), when compared to a GPU (accelerator) baseline, which represents one of the highest-throughput implementations known.
Multi-level Chaotic Maps for 3D Textured Model Encryption
Venue: arXiv cs.CV 2020
Year: 2020

With rapid progress of Virtual Reality and Augmented Reality technologies, 3D contents are the next widespread media in many applications. Thus, the protection of 3D models is primarily important. Encryption of 3D models is essential to maintain confidentiality. Previous work on encryption of 3D surface model often consider the point clouds, the meshes and the textures individually. In this work, a multi-level chaotic maps models for 3D textured encryption was presented by observing the different contributions for recognizing cipher 3D models between vertices (point cloud), polygons and textures. For vertices which make main contribution for recognizing, we use high level 3D Lu chaotic map to encrypt them. For polygons and textures which make relatively smaller contributions for recognizing, we use 2D Arnold's cat map and 1D Logistic map to encrypt them, respectively. The experimental results show that our method can get similar performance with the other method use the same high level chaotic map for point cloud, polygons and textures, while we use less time. Besides, our method can resist more method of attacks such as statistic attack, brute-force attack, correlation attack.
Sampling Without Compromising Accuracy in Adaptive Data Analysis
Venue: arXiv cs.LG 2020
Year: 2020

In this work, we study how to use sampling to speed up mechanisms for answering adaptive queries into datasets without reducing the accuracy of those mechanisms. This is important to do when both the datasets and the number of queries asked are very large. In particular, we describe a mechanism that provides a polynomial speed-up per query over previous mechanisms, without needing to increase the total amount of data required to maintain the same generalization error as before. We prove that this speed-up holds for arbitrary statistical queries. We also provide an even faster method for achieving statistically-meaningful responses wherein the mechanism is only allowed to see a constant number of samples from the data per query. Finally, we show that our general results yield a simple, fast, and unified approach for adaptively optimizing convex and strongly convex functions over a dataset.
Parameterized Approximation Schemes for Steiner Trees with Small Number of Steiner Vertices
Venue: arXiv cs.DS 2020
Year: 2020

We study the Steiner Tree problem, in which a set of terminal vertices needs to be connected in the cheapest possible way in an edge-weighted graph. This problem has been extensively studied from the viewpoint of approximation and also parametrization. In particular, on one hand Steiner Tree is known to be APX-hard, and W[2]-hard on the other, if parameterized by the number of non-terminals (Steiner vertices) in the optimum solution. In contrast to this we give an efficient parameterized approximation scheme (EPAS), which circumvents both hardness results. Moreover, our methods imply the existence of a polynomial size approximate kernelization scheme (PSAKS) for the considered parameter. We further study the parameterized approximability of other variants of Steiner Tree, such as Directed Steiner Tree and Steiner Forest. For neither of these an EPAS is likely to exist for the studied parameter: for Steiner Forest an easy observation shows that the problem is APX-hard, even if the input graph contains no Steiner vertices. For Directed Steiner Tree we prove that approximating within any function of the studied parameter is W[1]-hard. Nevertheless, we show that an EPAS exists for Unweighted Directed Steiner Tree, but a PSAKS does not. We also prove that there is an EPAS and a PSAKS for Steiner Forest if in addition to the number of Steiner vertices, the number of connected components of an optimal solution is considered to be a parameter.
Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC)
Venue: arXiv cs.PL 2020
Year: 2020

In order to avoid well-know paradoxes associated with self-referential definitions, higher-order dependent type theories stratify the theory using a countably infinite hierarchy of universes (also known as sorts), Type$_0$ : Type$_1$ : $\cdots$ . Such type systems are called cumulative if for any type $A$ we have that $A$ : Type$_{i}$ implies $A$ : Type$_{i+1}$. The predicative calculus of inductive constructions (pCIC) which forms the basis of the Coq proof assistant, is one such system. In this paper we present and establish the soundness of the predicative calculus of cumulative inductive constructions (pCuIC) which extends the cumulativity relation to inductive types.