OpenRaiser/Intern-Atlas huggingface dataset:
Sequent-Type Calculi for Systems of Nonmonotonic Paraconsistent Logics
Venue: arXiv cs.LO 2020
Year: 2020

Paraconsistent logics constitute an important class of formalisms dealing with non-trivial reasoning from inconsistent premisses. In this paper, we introduce uniform axiomatisations for a family of nonmonotonic paraconsistent logics based on minimal inconsistency in terms of sequent-type proof systems. The latter are prominent and widely-used forms of calculi well-suited for analysing proof search. In particular, we provide sequent-type calculi for Priest's three-valued minimally inconsistent logic of paradox, and for four-valued paraconsistent inference relations due to Arieli and Avron. Our calculi follow the sequent method first introduced in the context of nonmonotonic reasoning by Bonatti and Olivetti, whose distinguishing feature is the use of a so-called rejection calculus for axiomatising invalid formulas. In fact, we present a general method to obtain sequent systems for any many-valued logic based on minimal inconsistency, yielding the calculi for the logics of Priest and of Arieli and Avron as special instances.
LP2PB: Translating Answer Set Programs into Pseudo-Boolean Theories
Venue: arXiv cs.LO 2020
Year: 2020

Answer set programming (ASP) is a well-established knowledge representation formalism. Most ASP solvers are based on (extensions of) technology from Boolean satisfiability solving. While these solvers have shown to be very successful in many practical applications, their strength is limited by their underlying proof system, resolution. In this paper, we present a new tool LP2PB that translates ASP programs into pseudo-Boolean theories, for which solvers based on the (stronger) cutting plane proof system exist. We evaluate our tool, and the potential of cutting-plane-based solving for ASP on traditional ASP benchmarks as well as benchmarks from pseudo-Boolean solving. Our results are mixed: overall, traditional ASP solvers still outperform our translational approach, but several benchmark families are identified where the balance shifts the other way, thereby suggesting that further investigation into a stronger proof system for ASP is valuable.
Constraint Programming Algorithms for Route Planning Exploiting Geometrical Information
Venue: arXiv cs.AI 2020
Year: 2020

Problems affecting the transport of people or goods are plentiful in industry and commerce and they also appear to be at the origin of much more complex problems. In recent years, the logistics and transport sector keeps growing supported by technological progress, i.e. companies to be competitive are resorting to innovative technologies aimed at efficiency and effectiveness. This is why companies are increasingly using technologies such as Artificial Intelligence (AI), Blockchain and Internet of Things (IoT). Artificial intelligence, in particular, is often used to solve optimization problems in order to provide users with the most efficient ways to exploit available resources. In this work we present an overview of our current research activities concerning the development of new algorithms, based on CLP techniques, for route planning problems exploiting the geometric information intrinsically present in many of them or in some of their variants. The research so far has focused in particular on the Euclidean Traveling Salesperson Problem (Euclidean TSP) with the aim to exploit the results obtained also to other problems of the same category, such as the Euclidean Vehicle Routing Problem (Euclidean VRP), in the future.
Influences of Temporal Factors on GPS-based Human Mobility Lifestyle
Venue: arXiv cs.HC 2020
Year: 2020

Analysis of human mobility from GPS trajectories becomes crucial in many aspects such as policy planning for urban citizens, location-based service recommendation/prediction, and especially mitigating the spread of biological and mobile viruses. In this paper, we propose a method to find temporal factors affecting the human mobility lifestyle. We collected GPS data from 100 smartphone users in Japan. We designed a model that consists of 13 temporal patterns. We then applied a multiple linear regression and found that people tend to keep their mobility habits on Thursday and the days in the second week of a month but tend to lose their habits on Friday. We also explained some reasons behind these findings.
Inductive Program Synthesis Over Noisy Data
Venue: arXiv cs.PL 2020
Year: 2020

We present a new framework and associated synthesis algorithms for program synthesis over noisy data, i.e., data that may contain incorrect/corrupted input-output examples. This framework is based on an extension of finite tree automata called {\em weighted finite tree automata}. We show how to apply this framework to formulate and solve a variety of program synthesis problems over noisy data. Results from our implemented system running on problems from the SyGuS 2018 benchmark suite highlight its ability to successfully synthesize programs in the face of noisy data sets, including the ability to synthesize a correct program even when every input-output example in the data set is corrupted.
CodeBLEU: a Method for Automatic Evaluation of Code Synthesis
Venue: arXiv cs.SE 2020
Year: 2020

Evaluation metrics play a vital role in the growth of an area as it defines the standard of distinguishing between good and bad models. In the area of code synthesis, the commonly used evaluation metric is BLEU or perfect accuracy, but they are not suitable enough to evaluate codes, because BLEU is originally designed to evaluate the natural language, neglecting important syntactic and semantic features of codes, and perfect accuracy is too strict thus it underestimates different outputs with the same semantic logic. To remedy this, we introduce a new automatic evaluation metric, dubbed CodeBLEU. It absorbs the strength of BLEU in the n-gram match and further injects code syntax via abstract syntax trees (AST) and code semantics via data-flow. We conduct experiments by evaluating the correlation coefficient between CodeBLEU and quality scores assigned by the programmers on three code synthesis tasks, i.e., text-to-code, code translation, and code refinement. Experimental results show that our proposed CodeBLEU can achieve a better correlation with programmer assigned scores compared with BLEU and accuracy.
Stacked Generalization for Human Activity Recognition
Venue: arXiv cs.LG 2020
Year: 2020

This short paper aims to discuss the effectiveness and performance of classical machine learning approaches for Human Activity Recognition (HAR). It proposes two important models - Extra Trees and Stacked Classifier with the emphasize on the best practices, heuristics and measures that are required to maximize the performance of those models.
Evolutionary Conflict Checking
Venue: arXiv cs.SE 2020
Year: 2020

During the software evolution, existing features may be adversely affected by new changes, which is well known as regression errors. Maintaining a high-quality test suite is helpful to prevent regression errors, whereas it heavily depends on developers. Continuously augmenting the existing test suite based on the new changes can assist developers in investigating the impact of these new changes. And by comparing the executions of the generated test case on two versions, existing techniques are able to detect some common errors. However, the requirements and oracles on the new changes with existing program behaviors are missing. In addition, the new changes may introduce new bugs when they are not sufficiently examined with other unchanged code, which finally fails to meet developers' real intentions on changes. In this paper, we propose the notion of evolutionary conflict checking to validate new changes. By extracting developers' intention reflected by new changes and transforming the linear evolutionary process into one three-way merge, we detect conflicts between existing behaviors and new changes. Our experimental results indicate that evolutionary conflict checking is able to be applied for guaranteeing software quality after changes.
Inter-database validation of a deep learning approach for automatic sleep scoring
Venue: arXiv cs.LG 2020
Year: 2020

In this work we describe a new deep learning approach for automatic sleep staging, and carry out its validation by addressing its generalization capabilities on a wide range of sleep staging databases. Prediction capabilities are evaluated in the context of independent local and external generalization scenarios. Effectively, by comparing both procedures it is possible to better extrapolate the expected performance of the method on the general reference task of sleep staging, regardless of data from a specific database. In addition, we examine the suitability of a novel approach based on the use of an ensemble of individual local models and evaluate its impact on the resulting inter-database generalization performance. Validation results show good general performance, as compared to the expected levels of human expert agreement, as well as state-of-the-art automatic sleep staging approaches
Explainable, Stable, and Scalable Graph Convolutional Networks for Learning Graph Representation
Venue: arXiv cs.LG 2020
Year: 2020

The network embedding problem that maps nodes in a graph to vectors in Euclidean space can be very useful for addressing several important tasks on a graph. Recently, graph neural networks (GNNs) have been proposed for solving such a problem. However, most embedding algorithms and GNNs are difficult to interpret and do not scale well to handle millions of nodes. In this paper, we tackle the problem from a new perspective based on the equivalence of three constrained optimization problems: the network embedding problem, the trace maximization problem of the modularity matrix in a sampled graph, and the matrix factorization problem of the modularity matrix in a sampled graph. The optimal solutions to these three problems are the dominant eigenvectors of the modularity matrix. We proposed two algorithms that belong to a special class of graph convolutional networks (GCNs) for solving these problems: (i) Clustering As Feature Embedding GCN (CAFE-GCN) and (ii) sphere-GCN. Both algorithms are stable trace maximization algorithms, and they yield good approximations of dominant eigenvectors. Moreover, there are linear-time implementations for sparse graphs. In addition to solving the network embedding problem, both proposed GCNs are capable of performing dimensionality reduction. Various experiments are conducted to evaluate our proposed GCNs and show that our proposed GCNs outperform almost all the baseline methods. Moreover, CAFE-GCN could be benefited from the labeled data and have tremendous improvements in various performance metrics.
Efficiently Finding a Maximal Clique Summary via Effective Sampling
Venue: arXiv cs.DB 2020
Year: 2020

Maximal clique enumeration (MCE) is a fundamental problem in graph theory and is used in many applications, such as social network analysis, bioinformatics, intelligent agent systems, cyber security, etc. Most existing MCE algorithms focus on improving the efficiency rather than reducing the output size. The output unfortunately could consist of a large number of maximal cliques. In this paper, we study how to report a summary of less overlapping maximal cliques. The problem was studied before, however, after examining the pioneer approach, we consider it still not satisfactory. To advance the research along this line, our paper attempts to make four contributions: (a) we propose a more effective sampling strategy, which produces a much smaller summary but still ensures that the summary can somehow witness all the maximal cliques and the expectation of each maximal clique witnessed by the summary is above a predefined threshold; (b) we prove that the sampling strategy is optimal under certain optimality conditions; (c) we apply clique-size bounding and design new enumeration order to approach the optimality conditions; and (d) to verify experimentally, we test eight real benchmark datasets that have a variety of graph characteristics. The results show that our new sampling strategy consistently outperforms the state-of-the-art approach by producing smaller summaries and running faster on all the datasets.
CREDIT: Coarse-to-Fine Sequence Generation for Dialogue State Tracking
Venue: arXiv cs.CL 2020
Year: 2020

In dialogue systems, a dialogue state tracker aims to accurately find a compact representation of the current dialogue status, based on the entire dialogue history. While previous approaches often define dialogue states as a combination of separate triples ({\em domain-slot-value}), in this paper, we employ a structured state representation and cast dialogue state tracking as a sequence generation problem. Based on this new formulation, we propose a {\bf C}oa{\bf R}s{\bf E}-to-fine {\bf DI}alogue state {\bf T}racking ({\bf CREDIT}) approach. Taking advantage of the structured state representation, which is a marked language sequence, we can further fine-tune the pre-trained model (by supervised learning) by optimizing natural language metrics with the policy gradient method. Like all generative state tracking methods, CREDIT does not rely on pre-defined dialogue ontology enumerating all possible slot values. Experiments demonstrate our tracker achieves encouraging joint goal accuracy for the five domains in MultiWOZ 2.0 and MultiWOZ 2.1 datasets.
Self-Supervised Learning of Non-Rigid Residual Flow and Ego-Motion
Venue: arXiv cs.CV 2020
Year: 2020

Most of the current scene flow methods choose to model scene flow as a per point translation vector without differentiating between static and dynamic components of 3D motion. In this work we present an alternative method for end-to-end scene flow learning by joint estimation of non-rigid residual flow and ego-motion flow for dynamic 3D scenes. We propose to learn the relative rigid transformation from a pair of point clouds followed by an iterative refinement. We then learn the non-rigid flow from transformed inputs with the deducted rigid part of the flow. Furthermore, we extend the supervised framework with self-supervisory signals based on the temporal consistency property of a point cloud sequence. Our solution allows both training in a supervised mode complemented by self-supervisory loss terms as well as training in a fully self-supervised mode. We demonstrate that decomposition of scene flow into non-rigid flow and ego-motion flow along with an introduction of the self-supervisory signals allowed us to outperform the current state-of-the-art supervised methods.
A survey on Kornia: an Open Source Differentiable Computer Vision Library for PyTorch
Venue: arXiv cs.CV 2020
Year: 2020

This work presents Kornia, an open source computer vision library built upon a set of differentiable routines and modules that aims to solve generic computer vision problems. The package uses PyTorch as its main backend, not only for efficiency but also to take advantage of the reverse auto-differentiation engine to define and compute the gradient of complex functions. Inspired by OpenCV, Kornia is composed of a set of modules containing operators that can be integrated into neural networks to train models to perform a wide range of operations including image transformations,camera calibration, epipolar geometry, and low level image processing techniques, such as filtering and edge detection that operate directly on high dimensional tensor representations on graphical processing units, generating faster systems. Examples of classical vision problems implemented using our framework are provided including a benchmark comparing to existing vision libraries.
The Relativity of Induction
Venue: arXiv cs.AI 2020
Year: 2020

Lately there has been a lot of discussion about why deep learning algorithms perform better than we would theoretically suspect. To get insight into this question, it helps to improve our understanding of how learning works. We explore the core problem of generalization and show that long-accepted Occam's razor and parsimony principles are insufficient to ground learning. Instead, we derive and demonstrate a set of relativistic principles that yield clearer insight into the nature and dynamics of learning. We show that concepts of simplicity are fundamentally contingent, that all learning operates relative to an initial guess, and that generalization cannot be measured or strongly inferred, but that it can be expected given enough observation. Using these principles, we reconstruct our understanding in terms of distributed learning systems whose components inherit beliefs and update them. We then apply this perspective to elucidate the nature of some real world inductive processes including deep learning.
Mosques Smart Domes System using Machine Learning Algorithms
Venue: arXiv cs.CY 2020
Year: 2020

Millions of mosques around the world are suffering some problems such as ventilation and difficulty getting rid of bacteria, especially in rush hours where congestion in mosques leads to air pollution and spread of bacteria, in addition to unpleasant odors and to a state of discomfort during the pray times, where in most mosques there are no enough windows to ventilate the mosque well. This paper aims to solve these problems by building a model of smart mosques domes using weather features and outside temperatures. Machine learning algorithms such as k Nearest Neighbors and Decision Tree were applied to predict the state of the domes open or close. The experiments of this paper were applied on Prophet mosque in Saudi Arabia, which basically contains twenty seven manually moving domes. Both machine learning algorithms were tested and evaluated using different evaluation methods. After comparing the results for both algorithms, DT algorithm was achieved higher accuracy 98% comparing with 95% accuracy for kNN algorithm. Finally, the results of this study were promising and will be helpful for all mosques to use our proposed model for controlling domes automatically.
An Exponential Factorization Machine with Percentage Error Minimization to Retail Sales Forecasting
Venue: arXiv cs.LG 2020
Year: 2020

This paper proposes a new approach to sales forecasting for new products with long lead time but short product life cycle. These SKUs are usually sold for one season only, without any replenishments. An exponential factorization machine (EFM) sales forecast model is developed to solve this problem which not only considers SKU attributes, but also pairwise interactions. The EFM model is significantly different from the original Factorization Machines (FM) from two-fold: (1) the attribute-level formulation for explanatory variables and (2) exponential formulation for the positive response variable. The attribute-level formation excludes infeasible intra-attribute interactions and results in more efficient feature engineering comparing with the conventional one-hot encoding, while the exponential formulation is demonstrated more effective than the log-transformation for the positive but not skewed distributed responses. In order to estimate the parameters, percentage error squares (PES) and error squares (ES) are minimized by a proposed adaptive batch gradient descent method over the training set. Real-world data provided by a footwear retailer in Singapore is used for testing the proposed approach. The forecasting performance in terms of both mean absolute percentage error (MAPE) and mean absolute error (MAE) compares favourably with not only off-the-shelf models but also results reported by extant sales and demand forecasting studies. The effectiveness of the proposed approach is also demonstrated by two external public datasets. Moreover, we prove the theoretical relationships between PES and ES minimization, and present an important property of the PES minimization for regression models; that it trains models to underestimate data. This property fits the situation of sales forecasting where unit-holding cost is much greater than the unit-shortage cost.
ThingML+ Augmenting Model-Driven Software Engineering for the Internet of Things with Machine Learning
Venue: arXiv cs.SE 2020
Year: 2020

In this paper, we present the current position of the research project ML-Quadrat, which aims to extend the methodology, modeling language and tool support of ThingML - an open source modeling tool for IoT/CPS - to address Machine Learning needs for the IoT applications. Currently, ThingML offers a modeling language and tool support for modeling the components of the system, their communication interfaces as well as their behaviors. The latter is done through state machines. However, we argue that in many cases IoT/CPS services involve system components and physical processes, whose behaviors are not well understood in order to be modeled using state machines. Hence, quite often a data-driven approach that enables inference based on the observed data, e.g., using Machine Learning is preferred. To this aim, ML-Quadrat integrates the necessary Machine Learning concepts into ThingML both on the modeling level (syntax and semantics of the modeling language) and on the code generators level. We plan to support two target platforms for code generation regarding Stream Processing and Complex Event Processing, namely Apache SAMOA and Apama.
Domain Specific Modeling (DSM) as a Service for the Internet of Things & Services
Venue: arXiv cs.SE 2020
Year: 2020

In this paper, we propose a novel approach for developing Sense-Compute-Control (SCC) applications for the Internet of Things and Services (IoTS) following the Model-Driven Software Engineering (MDSE) methodology. We review the recent approaches to MDSE and argue that Domain Specific Modeling (DSM) suites our needs very well. However, in line with the recent trends in cloud computing and the emer-gence of the IoTS, we believe that both DSM creation tools and DSM solutions that are created via those tools should also be provided to their respective users in a service-oriented fashion through the cloud in the IoTS. In this work, we concentrate on the latter, i.e., DSM solu-tions that are created via a DSM creation tool. We argue that it makes sense for the owners of a DSM solution in a domain to provide their DSM solution as a service, following the well known Software as a Ser-vice (SaaS) model, to the interested customers through the IoTS. Our proposed approach concentrates on such a DSM solution for developing SCC applications in the IoTS. However, the idea could be applied to DSM solutions in other domains as well.
Google COVID-19 community mobility reports: insights from multi-criteria decision making
Venue: arXiv cs.SI 2020
Year: 2020

Social distancing (SD) has been critical in the fight against the novel coronavirus disease (COVID-19). To aid SD monitoring, many technology companies have made available mobility data, the most prominent example being the community mobility reports (CMR) provided by Google. Given the wide range of research fields that have been drawing insights from CMR data, there has been a rising concern for methodological discussion on how to use them. Indeed, Google recently released their own guidelines, concerning the nature of the place categories and the need for calibrating regional values. In this work, we discuss how measures developed in the field of multi-criteria decision making (MCDM) might benefit researchers analyzing this data. Concretely, we discuss how Pareto dominance and performance measures adopted in MCDM enable the mobility evaluation for (i) multiple categories for a given time period and (ii) multiple categories over multiple time periods. We empirically demonstrate these approaches conducting both a region- and country-level analysis, comparing some of the most relevant outbreak examples from different continents.