OpenRaiser/Intern-Atlas huggingface dataset:
From Matching Logic To Parallel Imperative Language Verification
Venue: arXiv cs.LO 2021
Year: 2021

Program verification is to develop the program's proof system, and to prove the proof system soundness with respect to a trusted operational semantics of the program. However, many practical program verifiers are not based on operational semantics and can't seriously validate the program. Matching logic is proposed to make program verification based on operational semantics. In this paper, following Grigore Ro{ş}u 's work, we consider matching logic for parallel imperative language(PIMP). According to our investigation, this paper is the first study on matching logic for PIMP. In our matching logic, we redefine "interference-free" to character parallel rule and prove the soundness of matching logic to the operational semantics of PIMP. We also link PIMP's operational semantics and PIMP's verification formally by constructing a matching logic verifier for PIMP which executes rewriting logic semantics symbolically on configuration patterns and is sound and complete to matching logic for PIMP. That is our matching logic verifier for PIMP is sound to the operational semantics of PIMP. Finally, we also verify the matching logic verifier through an example which is a standard problem in parallel programming.
Simultaneous Localization and Mapping Related Datasets: A Comprehensive Survey
Venue: arXiv cs.RO 2021
Year: 2021

Due to the complicated procedure and costly hardware, Simultaneous Localization and Mapping (SLAM) has been heavily dependent on public datasets for drill and evaluation, leading to many impressive demos and good benchmark scores. However, with a huge contrast, SLAM is still struggling on the way towards mature deployment, which sounds a warning: some of the datasets are overexposed, causing biased usage and evaluation. This raises the problem on how to comprehensively access the existing datasets and correctly select them. Moreover, limitations do exist in current datasets, then how to build new ones and which directions to go? Nevertheless, a comprehensive survey which can tackle the above issues does not exist yet, while urgently demanded by the community. To fill the gap, this paper strives to cover a range of cohesive topics about SLAM related datasets, including general collection methodology and fundamental characteristic dimensions, SLAM related tasks taxonomy and datasets categorization, introduction of state-of-the-arts, overview and comparison of existing datasets, review of evaluation criteria, and analyses and discussions about current limitations and future directions, looking forward to not only guiding the dataset selection, but also promoting the dataset research.
Towards Accurate RGB-D Saliency Detection with Complementary Attention and Adaptive Integration
Venue: arXiv cs.CV 2021
Year: 2021

Saliency detection based on the complementary information from RGB images and depth maps has recently gained great popularity. In this paper, we propose Complementary Attention and Adaptive Integration Network (CAAI-Net), a novel RGB-D saliency detection model that integrates complementary attention based feature concentration and adaptive cross-modal feature fusion into a unified framework for accurate saliency detection. Specifically, we propose a context-aware complementary attention (CCA) module, which consists of a feature interaction component, a complementary attention component, and a global-context component. The CCA module first utilizes the feature interaction component to extract rich local context features. The resulting features are then fed into the complementary attention component, which employs the complementary attention generated from adjacent levels to guide the attention at the current layer so that the mutual background disturbances are suppressed and the network focuses more on the areas with salient objects. Finally, we utilize a specially-designed adaptive feature integration (AFI) module, which sufficiently considers the low-quality issue of depth maps, to aggregate the RGB and depth features in an adaptive manner. Extensive experiments on six challenging benchmark datasets demonstrate that CAAI-Net is an effective saliency detection model and outperforms nine state-of-the-art models in terms of four widely-used metrics. In addition, extensive ablation studies confirm the effectiveness of the proposed CCA and AFI modules.
Sensor Planning for Large Numbers of Robots
Venue: arXiv cs.RO 2021
Year: 2021

*The following abbreviates the abstract. Please refer to the thesis for the full abstract.* After a disaster, locating and extracting victims quickly is critical because mortality rises rapidly after the first two days. To assist search and rescue teams and improve response times, teams of camera-equipped aerial robots can engage in tasks such as mapping buildings and locating victims. These sensing tasks encapsulate difficult (NP-Hard) problems. One way to simplify planning for these tasks is to focus on maximizing sensing performance over a short time horizon. Specifically, consider the problem of how to select motions for a team of robots to maximize a notion of sensing quality (the sensing objective) over the near future, say by maximizing the amount of unknown space in a map that robots will observe over the next several seconds. By repeating this process regularly, the team can react quickly to new observations as they work to complete the sensing task. In technical terms, this planning and control process forms an example of receding-horizon control. Fortunately, common sensing objectives benefit from well-known monotonicity properties (e.g. submodularity), and greedy algorithms can exploit these monotonicity properties to solve the receding-horizon optimization problems that we study near-optimally. However, greedy algorithms typically force robots to make decisions sequentially so that planning time grows with the number of robots. Further, recent works that investigate sequential greedy planning, have demonstrated that reducing the number of sequential steps while retaining suboptimality guarantees can be hard or impossible. We demonstrate that halting growth in planning time is sometimes possible. To do so, we introduce novel greedy algorithms involving fixed numbers of sequential steps.
OV$^{2}$SLAM : A Fully Online and Versatile Visual SLAM for Real-Time Applications
Venue: arXiv cs.CV 2021
Year: 2021

Many applications of Visual SLAM, such as augmented reality, virtual reality, robotics or autonomous driving, require versatile, robust and precise solutions, most often with real-time capability. In this work, we describe OV$^{2}$SLAM, a fully online algorithm, handling both monocular and stereo camera setups, various map scales and frame-rates ranging from a few Hertz up to several hundreds. It combines numerous recent contributions in visual localization within an efficient multi-threaded architecture. Extensive comparisons with competing algorithms shows the state-of-the-art accuracy and real-time performance of the resulting algorithm. For the benefit of the community, we release the source code: \url{https://github.com/ov2slam/ov2slam}.
$\scriptstyle{BASALT}$: A Rock-Solid Foundation for Epidemic Consensus Algorithms in Very Large, Very Open Networks
Venue: arXiv cs.CR 2021
Year: 2021

Recent works have proposed new Byzantine consensus algorithms for blockchains based on epidemics, a design which enables highly scalable performance at a low cost. These methods however critically depend on a secure random peer sampling service: a service that provides a stream of random network nodes where no attacking entity can become over-represented. To ensure this security property, current epidemic platforms use a Proof-of-Stake system to select peer samples. However such a system limits the openness of the system as only nodes with significant stake can participate in the consensus, leading to an oligopoly situation. Moreover, this design introduces a complex interdependency between the consensus algorithm and the cryptocurrency built upon it. In this paper, we propose a radically different security design for the peer sampling service, based on the distribution of IP addresses to prevent Sybil attacks. We propose a new algorithm, $\scriptstyle{BASALT}$, that implements our design using a stubborn chaotic search to counter attackers' attempts at becoming over-represented. We show in theory and using Monte Carlo simulations that $\scriptstyle{BASALT}$ provides samples which are extremely close to the optimal distribution even in adversarial scenarios such as tentative Eclipse attacks. Live experiments on a production cryptocurrency platform confirm that the samples obtained using $\scriptstyle{BASALT}$ are equitably distributed amongst nodes, allowing for a system which is both open and where no single entity can gain excessive power.
Enhance Information Propagation for Graph Neural Network by Heterogeneous Aggregations
Venue: arXiv cs.LG 2021
Year: 2021

Graph neural networks are emerging as continuation of deep learning success w.r.t. graph data. Tens of different graph neural network variants have been proposed, most following a neighborhood aggregation scheme, where the node features are updated via aggregating features of its neighboring nodes from layer to layer. Though related research surges, the power of GNNs are still not on-par-with their counterpart CNNs in computer vision and RNNs in natural language processing. We rethink this problem from the perspective of information propagation, and propose to enhance information propagation among GNN layers by combining heterogeneous aggregations. We argue that as richer information are propagated from shallow to deep layers, the discriminative capability of features formulated by GNN can benefit from it. As our first attempt in this direction, a new generic GNN layer formulation and upon this a new GNN variant referred as HAG-Net is proposed. We empirically validate the effectiveness of HAG-Net on a number of graph classification benchmarks, and elaborate all the design options and criterions along with.
Blue Noise Plots
Venue: arXiv cs.GR 2021
Year: 2021

We propose Blue Noise Plots, two-dimensional dot plots that depict data points of univariate data sets. While often one-dimensional strip plots are used to depict such data, one of their main problems is visual clutter which results from overlap. To reduce this overlap, jitter plots were introduced, whereby an additional, non-encoding plot dimension is introduced, along which the data point representing dots are randomly perturbed. Unfortunately, this randomness can suggest non-existent clusters, and often leads to visually unappealing plots, in which overlap might still occur. To overcome these shortcomings, we introduce BlueNoise Plots where random jitter along the non-encoding plot dimension is replaced by optimizing all dots to keep a minimum distance in 2D i. e., Blue Noise. We evaluate the effectiveness as well as the aesthetics of Blue Noise Plots through both, a quantitative and a qualitative user study. The Python implementation of Blue Noise Plots is available here.
Symbolic computation of hypergeometric type and non-holonomic power series
Venue: arXiv cs.SC 2021
Year: 2021

A term $a_n$ is $m$-fold hypergeometric, for a given positive integer $m$, if the ratio $a_{n+m}/a_n$ is a rational function over a field $K$ of characteristic zero. We establish the structure of holonomic recurrence equation, i.e. linear and homogeneous recurrence equations having polynomial coefficients, that have $m$-fold hypergeometric term solutions over $K$, for any positive integer $m$. Consequently, we describe an algorithm, say $mfoldHyper$, that extends van Hoeij's algorithm (1998) which computes a basis of the subspace of hypergeometric $(m=1)$ term solutions of holonomic recurrence equations to the more general case of $m$-fold hypergeometric terms. We generalize the concept of hypergeometric type power series introduced by Koepf (1992), by considering linear combinations of Laurent-Puiseux series whose coefficients are $m$-fold hypergeometric terms. Thus thanks to $mfoldHyper$, we deduce a complete procedure to compute these power series; indeed, it turns out that every linear combination of power series with $m$-fold hypergeometric term coefficients, for finitely many values of $m$, is detected. On the other hand, we investigate an algorithm to represent power series of non-holonomic functions. The algorithm follows the same steps of Koepf's algorithm, but instead of seeking holonomic differential equations, quadratic differential equations are computed and the Cauchy product rule is used to deduce recurrence equations for the power series coefficients. This algorithm defines a normal function that yields together with enough initial values normal forms for many power series of non-holonomic functions. Therefore, non-trivial identities are automatically proved using this approach. This paper is accompanied by implementations in the Computer Algebra Systems (CAS) Maxima 5.44.0 and Maple 2019.
Compact Java Monitors
Venue: arXiv cs.SE 2021
Year: 2021

For scope and context, the idea we'll describe below, Compact Java Monitors, is intended as a potential replacement implementation for the "synchronized" construct in the HotSpot JVM. The readers is assumed to be familiar with current HotSpot implementation.
Grid-to-Graph: Flexible Spatial Relational Inductive Biases for Reinforcement Learning
Venue: arXiv cs.LG 2021
Year: 2021

Although reinforcement learning has been successfully applied in many domains in recent years, we still lack agents that can systematically generalize. While relational inductive biases that fit a task can improve generalization of RL agents, these biases are commonly hard-coded directly in the agent's neural architecture. In this work, we show that we can incorporate relational inductive biases, encoded in the form of relational graphs, into agents. Based on this insight, we propose Grid-to-Graph (GTG), a mapping from grid structures to relational graphs that carry useful spatial relational inductive biases when processed through a Relational Graph Convolution Network (R-GCN). We show that, with GTG, R-GCNs generalize better both in terms of in-distribution and out-of-distribution compared to baselines based on Convolutional Neural Networks and Neural Logic Machines on challenging procedurally generated environments and MinAtar. Furthermore, we show that GTG produces agents that can jointly reason over observations and environment dynamics encoded in knowledge bases.
Curse of Dimensionality for TSK Fuzzy Neural Networks: Explanation and Solutions
Venue: arXiv cs.LG 2021
Year: 2021

Takagi-Sugeno-Kang (TSK) fuzzy system with Gaussian membership functions (MFs) is one of the most widely used fuzzy systems in machine learning. However, it usually has difficulty handling high-dimensional datasets. This paper explores why TSK fuzzy systems with Gaussian MFs may fail on high-dimensional inputs. After transforming defuzzification to an equivalent form of softmax function, we find that the poor performance is due to the saturation of softmax. We show that two defuzzification operations, LogTSK and HTSK, the latter of which is first proposed in this paper, can avoid the saturation. Experimental results on datasets with various dimensionalities validated our analysis and demonstrated the effectiveness of LogTSK and HTSK.
High-level Approaches to Detect Malicious Political Activity on Twitter
Venue: arXiv cs.SI 2021
Year: 2021

Our work represents another step into the detection and prevention of these ever-more present political manipulation efforts. We, therefore, start by focusing on understanding what the state-of-the-art approaches lack -- since the problem remains, this is a fair assumption. We find concerning issues within the current literature and follow a diverging path. Notably, by placing emphasis on using data features that are less susceptible to malicious manipulation and also on looking for high-level approaches that avoid a granularity level that is biased towards easy-to-spot and low impact cases. We designed and implemented a framework -- Twitter Watch -- that performs structured Twitter data collection, applying it to the Portuguese Twittersphere. We investigate a data snapshot taken on May 2020, with around 5 million accounts and over 120 million tweets (this value has since increased to over 175 million). The analyzed time period stretches from August 2019 to May 2020, with a focus on the Portuguese elections of October 6th, 2019. However, the Covid-19 pandemic showed itself in our data, and we also delve into how it affected typical Twitter behavior. We performed three main approaches: content-oriented, metadata-oriented, and network interaction-oriented. We learn that Twitter's suspension patterns are not adequate to the type of political trolling found in the Portuguese Twittersphere -- identified by this work and by an independent peer - nor to fake news posting accounts. We also surmised that the different types of malicious accounts we independently gathered are very similar both in terms of content and interaction, through two distinct analysis, and are simultaneously very distinct from regular accounts.
Regularization for convolutional kernel tensors to avoid unstable gradient problem in convolutional neural networks
Venue: arXiv cs.LG 2021
Year: 2021

Convolutional neural networks are very popular nowadays. Training neural networks is not an easy task. Each convolution corresponds to a structured transformation matrix. In order to help avoid the exploding/vanishing gradient problem, it is desirable that the singular values of each transformation matrix are not large/small in the training process. We propose three new regularization terms for a convolutional kernel tensor to constrain the singular values of each transformation matrix. We show how to carry out the gradient type methods, which provides new insight about the training of convolutional neural networks.
Soccer Event Detection Using Deep Learning
Venue: arXiv cs.CV 2021
Year: 2021

Event detection is an important step in extracting knowledge from the video. In this paper, we propose a deep learning approach to detect events in a soccer match emphasizing the distinction between images of red and yellow cards and the correct detection of the images of selected events from other images. This method includes the following three modules: i) the variational autoencoder (VAE) module to differentiate between soccer images and others image, ii) the image classification module to classify the images of events, and iii) the fine-grain image classification module to classify the images of red and yellow cards. Additionally, a new dataset was introduced for soccer images classification that is employed to train the networks mentioned in the paper. In the final section, 10 UEFA Champions League matches are used to evaluate the networks' performance and precision in detecting the events. The experiments demonstrate that the proposed method achieves better performance than state-of-the-art methods.
A Theoretical Answer to "Does the IRC-SINR of an Interference Rejection Combiner always Increase with an Increase in Number of Receive Antennas?"
Venue: arXiv cs.IT 2021
Year: 2021

Interference rejection combiners (IRCs) are very popular in 4G/5G systems. In particular, they are often times used in co-ordinated multi-point (CoMP) networks where the antennas of a neighboring cell's base station (BS) are used in an IRC receiver, in conjunction with the antennas of the BS of a cell-edge UE's own cell, to improve the IRC-SINR of a cell-edge user. But does the IRC-SINR always increase with an increase in the number of antennas? In this paper, we attempt to answer the question theoretically. We give a theoretical derivation that quantifies the improvement in the IRC-SINR when the number of antennas increases by unity. We show that this improvement in IRC-SINR is always greater than or equal to zero. Thus we prove that increasing the number of antennas even by unity will always improve the IRC-SINR. Selecting the extra antennas of the neighbouring cell can be viewed as a special case of antenna selection described in [1]. We also present the IRC-SINR improvement in an uplink CoMP scenario by simulations and verify that it indeed matches with the theoretical gains derived in this paper.
Unlocking Pixels for Reinforcement Learning via Implicit Attention
Venue: arXiv cs.LG 2021
Year: 2021

There has recently been significant interest in training reinforcement learning (RL) agents in vision-based environments. This poses many challenges, such as high dimensionality and the potential for observational overfitting through spurious correlations. A promising approach to solve both of these problems is an attention bottleneck, which provides a simple and effective framework for learning high performing policies, even in the presence of distractions. However, due to poor scalability of attention architectures, these methods cannot be applied beyond low resolution visual inputs, using large patches (thus small attention matrices). In this paper we make use of new efficient attention algorithms, recently shown to be highly effective for Transformers, and demonstrate that these techniques can be successfully adopted for the RL setting. This allows our attention-based controllers to scale to larger visual inputs, and facilitate the use of smaller patches, even individual pixels, improving generalization. We show this on a range of tasks from the Distracting Control Suite to vision-based quadruped robots locomotion. We provide rigorous theoretical analysis of the proposed algorithm.
Regular Model Checking Approach to Knowledge Reasoning over Parameterized Systems (technical report)
Venue: arXiv cs.FL 2021
Year: 2021

We present a general framework for modelling and verifying epistemic properties over parameterized multi-agent systems that communicate by truthful public announcements. In our framework, the number of agents or the amount of certain resources are parameterized (i.e. not known a priori), and the corresponding verification problem asks whether a given epistemic property is true regardless of the instantiation of the parameters. For example, in a muddy children puzzle, one could ask whether each child will eventually find out whether (s)he is muddy, regardless of the number of children. Our framework is regular model checking (RMC)-based, wherein synchronous finite-state automata (equivalently, monadic second-order logic over words) are used to specify the systems. We propose an extension of public announcement logic as specification language. Of special interests is the addition of the so-called iterated public announcement operators, which are crucial for reasoning about knowledge in parameterized systems. Although the operators make the model checking problem undecidable, we show that this becomes decidable when an appropriate "disappearance relation" is given. Further, we show how Angluin's L*-algorithm for learning finite automata can be applied to find a disappearance relation, which is guaranteed to terminate if it is regular. We have implemented the algorithm and apply this to such examples as the Muddy Children Puzzle, the Russian Card Problem, and Large Number Challenge.