OpenRaiser/Intern-Atlas huggingface dataset:
Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion
Venue: arXiv cs.PL 2021
Year: 2021

We present a PDR/IC3 algorithm for finding inductive invariants with quantifier alternations. We tackle scalability issues that arise due to the large search space of quantified invariants by combining a breadth-first search strategy and a new syntactic form for quantifier-free bodies. The breadth-first strategy prevents inductive generalization from getting stuck in regions of the search space that are expensive to search and focuses instead on lemmas that are easy to discover. The new syntactic form is well-suited to lemmas with quantifier alternations by allowing both limited conjunction and disjunction in the quantifier-free body, while carefully controlling the size of the search space. Combining the breadth-first strategy with the new syntactic form results in useful inductive bias by prioritizing lemmas according to: (i) well-defined syntactic metrics for simple quantifier structures and quantifier-free bodies, and (ii) the empirically useful heuristic of preferring lemmas that are fast to discover. On a benchmark suite of primarily distributed protocols and complex Paxos variants, we demonstrate that our algorithm can solve more of the most complicated examples than state-of-the-art techniques.
A Large-Scale Benchmark for the Incompressible Navier-Stokes Equations
Venue: arXiv cs.CE 2021
Year: 2021

We introduce a collection of benchmark problems in 2D and 3D (geometry description and boundary conditions), including simple cases with known analytic solution, classical experimental setups, and complex geometries with fabricated solutions for evaluation of numerical schemes for incompressible Navier-Stokes equations in laminar flow regime. We compare the performance of a representative selection of most broadly used algorithms for Navier-Stokes equations on this set of problems. Where applicable, we compare the most common spatial discretization choices (unstructured triangle/tetrahedral meshes and structured or semi-structured quadrilateral/hexahedral meshes). The study shows that while the type of spatial discretization used has a minor impact on the accuracy of the solutions, the choice of time integration method, spatial discretization order, and the choice of solving the coupled equations or reducing them to simpler subproblems have very different properties. Methods that are directly solving the original equations tend to be more accurate than splitting approaches for the same number of degrees of freedom, but numerical or computational difficulty arise when they are scaled to larger problem sizes. Low-order splitting methods are less accurate, but scale more easily to large problems, while higher-order splitting methods are accurate but require dense time discretizations to be stable. We release the description of the experiments and an implementation of our benchmark, which we believe will enable statistically significant comparisons with the state of the art as new approaches for solving the incompressible Navier-Stokes equations are introduced.
Building Autocorrelation-Aware Representations for Fine-Scale Spatiotemporal Prediction
Venue: arXiv cs.LG 2021
Year: 2021

Many scientific prediction problems have spatiotemporal data- and modeling-related challenges in handling complex variations in space and time using only sparse and unevenly distributed observations. This paper presents a novel deep learning architecture, Deep learning predictions for LocATion-dependent Time-sEries data (DeepLATTE), that explicitly incorporates theories of spatial statistics into neural networks to address these challenges. In addition to a feature selection module and a spatiotemporal learning module, DeepLATTE contains an autocorrelation-guided semi-supervised learning strategy to enforce both local autocorrelation patterns and global autocorrelation trends of the predictions in the learned spatiotemporal embedding space to be consistent with the observed data, overcoming the limitation of sparse and unevenly distributed observations. During the training process, both supervised and semi-supervised losses guide the updates of the entire network to: 1) prevent overfitting, 2) refine feature selection, 3) learn useful spatiotemporal representations, and 4) improve overall prediction. We conduct a demonstration of DeepLATTE using publicly available data for an important public health topic, air quality prediction, in a well-studied, complex physical environment - Los Angeles. The experiment demonstrates that the proposed approach provides accurate fine-spatial-scale air quality predictions and reveals the critical environmental factors affecting the results.
Multimodal Interactions Using Pretrained Unimodal Models for SIMMC 2.0
Venue: arXiv cs.CL 2021
Year: 2021

This paper presents our work on the Situated Interactive MultiModal Conversations 2.0 challenge held at Dialog State Tracking Challenge 10. SIMMC 2.0 includes 4 subtasks, and we introduce our multimodal approaches for the subtask \#1, \#2 and the generation of subtask \#4. SIMMC 2.0 dataset is a multimodal dataset containing image and text information, which is more challenging than the problem of only text-based conversations because it must be solved by understanding the relationship between image and text. Therefore, since there is a limit to solving only text models such as BERT or GPT2, we propose a multimodal model combining image and text. We first pretrain the multimodal model to understand the relationship between image and text, then finetune our model for each task. We achieve the 3rd best performance in subtask \#1, \#2 and a runner-up in the generation of subtask \#4. The source code is available at https://github.com/rungjoo/simmc2.0.
Findings on Conversation Disentanglement
Venue: arXiv cs.CL 2021
Year: 2021

Conversation disentanglement, the task to identify separate threads in conversations, is an important pre-processing step in multi-party conversational NLP applications such as conversational question answering and conversation summarization. Framing it as a utterance-to-utterance classification problem -- i.e. given an utterance of interest (UOI), find which past utterance it replies to -- we explore a number of transformer-based models and found that BERT in combination with handcrafted features remains a strong baseline. We then build a multi-task learning model that jointly learns utterance-to-utterance and utterance-to-thread classification. Observing that the ground truth label (past utterance) is in the top candidates when our model makes an error, we experiment with using bipartite graphs as a post-processing step to learn how to best match a set of UOIs to past utterances. Experiments on the Ubuntu IRC dataset show that this approach has the potential to outperform the conventional greedy approach of simply selecting the highest probability candidate for each UOI independently, indicating a promising future research direction.
MOBAFS: A Multi Objective Bee Algorithm for Feature subset selection in Software Product Lines
Venue: arXiv cs.SE 2021
Year: 2021

Software product line represents software engineering methods, tools and techniques for creating a group of related software systems from a shared set of software assets. Each product is a combination of multiple features. These features are known as software assets. So, the task of production can be mapped to a feature subset selection problem which is an NP-hard combinatorial optimization problem. This issue is much significant when the number of features in a software product line is huge. In this paper, a new method based on Multi Objective Bee Swarm Optimization algorithm (called MOBAFS) is presented. The MOBAFS is a population based optimization algorithm which is inspired by foraging behavior of honey bees. The is used to solve a SBSE problem. This technique is evaluated on five large scale real world software product lines in the range of 1,244 to 6,888 features. The proposed method is compared with the state-of-the-art, SATIBEA. According to results of three solution quality indicators and two diversity metrics, the proposed method, in most cases, surpasses the other algorithm.
Rethinking the Two-Stage Framework for Grounded Situation Recognition
Venue: arXiv cs.CV 2021
Year: 2021

Grounded Situation Recognition (GSR), i.e., recognizing the salient activity (or verb) category in an image (e.g., buying) and detecting all corresponding semantic roles (e.g., agent and goods), is an essential step towards "human-like" event understanding. Since each verb is associated with a specific set of semantic roles, all existing GSR methods resort to a two-stage framework: predicting the verb in the first stage and detecting the semantic roles in the second stage. However, there are obvious drawbacks in both stages: 1) The widely-used cross-entropy (XE) loss for object recognition is insufficient in verb classification due to the large intra-class variation and high inter-class similarity among daily activities. 2) All semantic roles are detected in an autoregressive manner, which fails to model the complex semantic relations between different roles. To this end, we propose a novel SituFormer for GSR which consists of a Coarse-to-Fine Verb Model (CFVM) and a Transformer-based Noun Model (TNM). CFVM is a two-step verb prediction model: a coarse-grained model trained with XE loss first proposes a set of verb candidates, and then a fine-grained model trained with triplet loss re-ranks these candidates with enhanced verb features (not only separable but also discriminative). TNM is a transformer-based semantic role detection model, which detects all roles parallelly. Owing to the global relation modeling ability and flexibility of the transformer decoder, TNM can fully explore the statistical dependency of the roles. Extensive validations on the challenging SWiG benchmark show that SituFormer achieves a new state-of-the-art performance with significant gains under various metrics. Code is available at https://github.com/kellyiss/SituFormer.
An Evaluation and Enhancement of Seredynski-Bouvry CA-based Encryption Scheme
Venue: arXiv cs.CR 2021
Year: 2021

In this paper, we study a block cipher based on cellular automata, proposed by Seredynski and Bouvry in \cite{semabo04} against \emph{plain-text avalanche criteria} and \emph{randomness} tests. Our experiments shows that Seredynski-Bouvry encryption scheme does not pass some NIST statistical tests by neighborhood radius less than three. It also showed that if the CA rule is selected carelessly, it weaken the security of scheme. Therefor, the selection of CA-rule as part of key can not be left to the user. Hence, cryptographic properties such as balancedness and non-linearity should be considered in the selection of CA-rules. This approach is more compliant with Kerckhoffs principle. So security should depend just on security of final data. We also improve Seredynski-Bouvry encryption scheme to satisfy strict avalanche criteria and NIST statistical test suite in about half number of iterations comparing to original scheme. This improvement is achieved by change in the definition of neighborhood.
Linear complementary dual code-based Multi-secret sharing scheme
Venue: arXiv cs.CR 2021
Year: 2021

Hiding a secret is needed in many situations. Secret sharing plays an important role in protecting information from getting lost, stolen, or destroyed and has been applicable in recent years. A secret sharing scheme is a cryptographic protocol in which a dealer divides the secret into several pieces of share and one share is given to each participant. To recover the secret, the dealer requires a subset of participants called access structure. In this paper, we present a multi-secret sharing scheme over a local ring based on linear complementary dual codes using Blakley's method. We take a large secret space over a local ring that is greater than other code-based schemes and obtain a perfect and almost ideal scheme.
Music demixing with the sliCQ transform
Venue: arXiv cs.SD 2021
Year: 2021

Music source separation is the task of extracting an estimate of one or more isolated sources or instruments (for example, drums or vocals) from musical audio. The task of music demixing or unmixing considers the case where the musical audio is separated into an estimate of all of its constituent sources that can be summed back to the original mixture. The Music Demixing Challenge was created to inspire new demixing research. Open-Unmix (UMX), and the improved variant CrossNet-Open-Unmix (X-UMX), were included in the challenge as the baselines. Both models use the Short-Time Fourier Transform (STFT) as the representation of music signals. The time-frequency uncertainty principle states that the STFT of a signal cannot have maximal resolution in both time and frequency. The tradeoff in time-frequency resolution can significantly affect music demixing results. Our proposed adaptation of UMX replaced the STFT with the sliCQT, a time-frequency transform with varying time-frequency resolution. Unfortunately, our model xumx-sliCQ achieved lower demixing scores than UMX.
A Validation Tool for Designing Reinforcement Learning Environments
Venue: arXiv cs.LG 2021
Year: 2021

Reinforcement learning (RL) has gained increasing attraction in the academia and tech industry with launches to a variety of impactful applications and products. Although research is being actively conducted on many fronts (e.g., offline RL, performance, etc.), many RL practitioners face a challenge that has been largely ignored: determine whether a designed Markov Decision Process (MDP) is valid and meaningful. This study proposes a heuristic-based feature analysis method to validate whether an MDP is well formulated. We believe an MDP suitable for applying RL should contain a set of state features that are both sensitive to actions and predictive in rewards. We tested our method in constructed environments showing that our approach can identify certain invalid environment formulations. As far as we know, performing validity analysis for RL problem formulation is a novel direction. We envision that our tool will serve as a motivational example to help practitioners apply RL in real-world problems more easily.
An Embarrassingly Pragmatic Introduction to Vision-based Autonomous Robots
Venue: arXiv cs.RO 2021
Year: 2021

Autonomous robots are currently one of the most popular Artificial Intelligence problems, having experienced significant advances in the last decade, from Self-driving cars and humanoids to delivery robots and drones. Part of the problem is to get a robot to emulate the perception of human beings, our sense of sight, replacing the eyes with cameras and the brain with mathematical models such as Neural Networks. Developing an AI able to drive a car without human intervention and a small robot to deliver packages in the city may seem like different problems, nevertheless from the point of view of perception and vision, both problems have several similarities. The main solutions we currently find focus on the environment perception through visual information using Computer Vision techniques, Machine Learning, and various algorithms to make the robot understand the environment or scene, move, adapt its trajectory and perform its tasks (maintenance, exploration, etc.) without the need for human intervention. In this work, we develop a small-scale autonomous vehicle from scratch, capable of understanding the scene using only visual information, navigating through industrial environments, detecting people and obstacles, or performing simple maintenance tasks. We review the state-of-the-art of fundamental problems and demonstrate that many methods employed at small-scale are similar to the ones employed in real Self-driving cars from companies like Tesla or Lyft. Finally, we discuss the current state of Robotics and autonomous driving and the technological and ethical limitations that we can find in this field.
PACMAN: PAC-style bounds accounting for the Mismatch between Accuracy and Negative log-loss
Venue: arXiv cs.LG 2021
Year: 2021

The ultimate performance of machine learning algorithms for classification tasks is usually measured in terms of the empirical error probability (or accuracy) based on a testing dataset. Whereas, these algorithms are optimized through the minimization of a typically different--more convenient--loss function based on a training set. For classification tasks, this loss function is often the negative log-loss that leads to the well-known cross-entropy risk which is typically better behaved (from a numerical perspective) than the error probability. Conventional studies on the generalization error do not usually take into account the underlying mismatch between losses at training and testing phases. In this work, we introduce an analysis based on point-wise PAC approach over the generalization gap considering the mismatch of testing based on the accuracy metric and training on the negative log-loss. We label this analysis PACMAN. Building on the fact that the mentioned mismatch can be written as a likelihood ratio, concentration inequalities can be used to provide some insights for the generalization problem in terms of some point-wise PAC bounds depending on some meaningful information-theoretic quantities. An analysis of the obtained bounds and a comparison with available results in the literature are also provided.
Eigenspace Restructuring: a Principle of Space and Frequency in Neural Networks
Venue: arXiv cs.LG 2021
Year: 2021

Understanding the fundamental principles behind the massive success of neural networks is one of the most important open questions in deep learning. However, due to the highly complex nature of the problem, progress has been relatively slow. In this note, through the lens of infinite-width networks, a.k.a. neural kernels, we present one such principle resulting from hierarchical localities. It is well-known that the eigenstructure of infinite-width multilayer perceptrons (MLPs) depends solely on the concept frequency, which measures the order of interactions. We show that the topologies from deep convolutional networks (CNNs) restructure the associated eigenspaces into finer subspaces. In addition to frequency, the new structure also depends on the concept space, which measures the spatial distance among nonlinear interaction terms. The resulting fine-grained eigenstructure dramatically improves the network's learnability, empowering them to simultaneously model a much richer class of interactions, including Long-Range-Low-Frequency interactions, Short-Range-High-Frequency interactions, and various interpolations and extrapolations in-between. Additionally, model scaling can improve the resolutions of interpolations and extrapolations and, therefore, the network's learnability. Finally, we prove a sharp characterization of the generalization error for infinite-width CNNs of any depth in the high-dimensional setting. Two corollaries follow: (1) infinite-width deep CNNs can break the curse of dimensionality without losing their expressivity, and (2) scaling improves performance in both the finite and infinite data regimes.
How to Avoid Trivial Solutions in Physics-Informed Neural Networks
Venue: arXiv cs.LG 2021
Year: 2021

The advent of scientific machine learning (SciML) has opened up a new field with many promises and challenges in the field of simulation science by developing approaches at the interface of physics- and data-based modelling. To this end, physics-informed neural networks (PINNs) have been introduced in recent years, which cope for the scarcity in training data by incorporating physics knowledge of the problem at so-called collocation points. In this work, we investigate the prediction performance of PINNs with respect to the number of collocation points used to enforce the physics-based penalty terms. We show that PINNs can fail, learning a trivial solution that fulfills the physics-derived penalty term by definition. We have developed an alternative sampling approach and a new penalty term enabling us to remedy this core problem of PINNs in data-scarce settings with competitive results while reducing the amount of collocation points needed by up to 80 \% for benchmark problems.
Seq-Masks: Bridging the gap between appearance and gait modeling for video-based person re-identification
Venue: arXiv cs.CV 2021
Year: 2021

ideo-based person re-identification (Re-ID) aims to match person images in video sequences captured by disjoint surveillance cameras. Traditional video-based person Re-ID methods focus on exploring appearance information, thus, vulnerable against illumination changes, scene noises, camera parameters, and especially clothes/carrying variations. Gait recognition provides an implicit biometric solution to alleviate the above headache. Nonetheless, it experiences severe performance degeneration as camera view varies. In an attempt to address these problems, in this paper, we propose a framework that utilizes the sequence masks (SeqMasks) in the video to integrate appearance information and gait modeling in a close fashion. Specifically, to sufficiently validate the effectiveness of our method, we build a novel dataset named MaskMARS based on MARS. Comprehensive experiments on our proposed large wild video Re-ID dataset MaskMARS evidenced our extraordinary performance and generalization capability. Validations on the gait recognition metric CASIA-B dataset further demonstrated the capability of our hybrid model.
Preallocation-based Combinatorial Auction for Efficient Fair Channel Assignments in Multi-Connectivity Networks
Venue: arXiv cs.GT 2021
Year: 2021

We consider a general multi-connectivity framework, intended for ultra-reliable low-latency communications (URLLC) services, and propose a novel, preallocation-based combinatorial auction approach for the efficient allocation of channels. We compare the performance of the proposed method with several other state-of-the-art and alternative channel-allocation algorithms. The two proposed performance metrics are the capacity-based and the utility-based context. In the first case, every unit of additional capacity is regarded as beneficial for any tenant, independent of the already allocated quantity, and the main measure is the total throughput of the system. In the second case, we assume a minimal and maximal required capacity value for each tenant, and consider the implied utility values accordingly. In addition to the total system performance, we also analyze fairness and computational requirements in both contexts. We conclude that at the cost of higher but still plausible computational time, the fairness-enhanced version of the proposed preallocation based combinatorial auction algorithm outperforms every other considered method when one considers total system performance and fairness simultaneously, and performs especially well in the utility context. Therefore, the proposed algorithm may be regarded as candidate scheme for URLLC channel allocation problems, where minimal and maximal capacity requirements have to be considered.