OpenRaiser/Intern-Atlas huggingface dataset:
Isabelle's Metalogic: Formalization and Proof Checker
Venue: arXiv cs.LO 2021
Year: 2021

Isabelle is a generic theorem prover with a fragment of higher-order logic as a metalogic for defining object logics. Isabelle also provides proof terms. We formalize this metalogic and the language of proof terms in Isabelle/HOL, define an executable (but inefficient) proof term checker and prove its correctness w.r.t. the metalogic. We integrate the proof checker with Isabelle and run it on a range of logics and theories to check the correctness of all the proofs in those theories.
Computational Group Selection
Venue: arXiv cs.CY 2021
Year: 2021

Humans spend a significant part of their lives being a part of groups. In this document we propose research directions that would make it possible to computationally form productive groups. We bring to light several issues that need to be addressed in the pursuit of this goal (not amplifying existing biases and inequality, for example), as well as multiple avenues to study that would help achieve us this task efficiently.
Target-free Extrinsic Calibration of a 3D-Lidar and an IMU
Venue: arXiv cs.RO 2021
Year: 2021

This work presents a novel target-free extrinsic calibration algorithm for a 3D Lidar and an IMU pair using an Extended Kalman Filter (EKF) which exploits the \textit{motion based calibration constraint} for state update. The steps include, data collection by motion excitation of the Lidar Inertial Sensor suite along all degrees of freedom, determination of the inter sensor rotation by using rotational component of the aforementioned \textit{motion based calibration constraint} in a least squares optimization framework, and finally, the determination of inter sensor translation using the \textit{motion based calibration constraint} for state update in an Extended Kalman Filter (EKF) framework. We experimentally validate our method using data collected in our lab and open-source (https://github.com/unmannedlab/imu_lidar_calibration) our contribution for the robotics research community.
Class Equilibrium using Coulomb's Law
Venue: arXiv cs.CV 2021
Year: 2021

Projection algorithms learn a transformation function to project the data from input space to the feature space, with the objective of increasing the inter-class distance. However, increasing the inter-class distance can affect the intra-class distance. Maintaining an optimal inter-class separation among the classes without affecting the intra-class distance of the data distribution is a challenging task. In this paper, inspired by the Coulomb's law of Electrostatics, we propose a new algorithm to compute the equilibrium space of any data distribution where the separation among the classes is optimal. The algorithm further learns the transformation between the input space and equilibrium space to perform classification in the equilibrium space. The performance of the proposed algorithm is evaluated on four publicly available datasets at three different resolutions. It is observed that the proposed algorithm performs well for low-resolution images.
A unified Neural Network Approach to E-CommerceRelevance Learning
Venue: arXiv cs.IR 2021
Year: 2021

Result relevance scoring is critical to e-commerce search user experience. Traditional information retrieval methods focus on keyword matching and hand-crafted or counting-based numeric features, with limited understanding of item semantic relevance. We describe a highly-scalable feed-forward neural model to provide relevance score for (query, item) pairs, using only user query and item title as features, and both user click feedback as well as limited human ratings as labels. Several general enhancements were applied to further optimize eval/test metrics, including Siamese pairwise architecture, random batch negative co-training, and point-wise fine-tuning. We found significant improvement over GBDT baseline as well as several off-the-shelf deep-learning baselines on an independently constructed ratings dataset. The GBDT model relies on 10 times more features. We also present metrics for select subset combinations of techniques mentioned above.
Auto-weighted low-rank representation for clustering
Venue: arXiv cs.LG 2021
Year: 2021

In this paper, a novel unsupervised low-rank representation model, i.e., Auto-weighted Low-Rank Representation (ALRR), is proposed to construct a more favorable similarity graph (SG) for clustering. In particular, ALRR enhances the discriminability of SG by capturing the multi-subspace structure and extracting the salient features simultaneously. Specifically, an auto-weighted penalty is introduced to learn a similarity graph by highlighting the effective features, and meanwhile, overshadowing the disturbed features. Consequently, ALRR obtains a similarity graph that can preserve the intrinsic geometrical structures within the data by enforcing a smaller similarity on two dissimilar samples. Moreover, we employ a block-diagonal regularizer to guarantee the learned graph contains $k$ diagonal blocks. This can facilitate a more discriminative representation learning for clustering tasks. Extensive experimental results on synthetic and real databases demonstrate the superiority of ALRR over other state-of-the-art methods with a margin of 1.8\%$\sim$10.8\%.
Stochastic Recurrent Neural Network for Multistep Time Series Forecasting
Venue: arXiv cs.LG 2021
Year: 2021

Time series forecasting based on deep architectures has been gaining popularity in recent years due to their ability to model complex non-linear temporal dynamics. The recurrent neural network is one such model capable of handling variable-length input and output. In this paper, we leverage recent advances in deep generative models and the concept of state space models to propose a stochastic adaptation of the recurrent neural network for multistep-ahead time series forecasting, which is trained with stochastic gradient variational Bayes. In our model design, the transition function of the recurrent neural network, which determines the evolution of the hidden states, is stochastic rather than deterministic as in a regular recurrent neural network; this is achieved by incorporating a latent random variable into the transition process which captures the stochasticity of the temporal dynamics. Our model preserves the architectural workings of a recurrent neural network for which all relevant information is encapsulated in its hidden states, and this flexibility allows our model to be easily integrated into any deep architecture for sequential modelling. We test our model on a wide range of datasets from finance to healthcare; results show that the stochastic recurrent neural network consistently outperforms its deterministic counterpart.
Revisiting the size effect in software fault prediction models
Venue: arXiv cs.SE 2021
Year: 2021

BACKGROUND: In object oriented (OO) software systems, class size has been acknowledged as having an indirect effect on the relationship between certain artifact characteristics, captured via metrics, and faultproneness, and therefore it is recommended to control for size when designing fault prediction models. AIM: To use robust statistical methods to assess whether there is evidence of any true effect of class size on fault prediction models. METHOD: We examine the potential mediation and moderation effects of class size on the relationships between OO metrics and number of faults. We employ regression analysis and bootstrapping-based methods to investigate the mediation and moderation effects in two widely-used datasets comprising seventeen systems. RESULTS: We find no strong evidence of a significant mediation or moderation effect of class size on the relationships between OO metrics and faults. In particular, size appears to have a more significant mediation effect on CBO and Fan-out than other metrics, although the evidence is not consistent in all examined systems. On the other hand, size does appear to have a significant moderation effect on WMC and CBO in most of the systems examined. Again, the evidence provided is not consistent across all examined systems CONCLUSION: We are unable to confirm if class size has a significant mediation or moderation effect on the relationships between OO metrics and the number of faults. We contend that class size does not fully explain the relationships between OO metrics and the number of faults, and it does not always affect the strength/magnitude of these relationships. We recommend that researchers consider the potential mediation and moderation effect of class size when building their prediction models, but this should be examined independently for each system.
Efficient Hyperparameter Optimization for Physics-based Character Animation
Venue: arXiv cs.GR 2021
Year: 2021

Physics-based character animation has seen significant advances in recent years with the adoption of Deep Reinforcement Learning (DRL). However, DRL-based learning methods are usually computationally expensive and their performance crucially depends on the choice of hyperparameters. Tuning hyperparameters for these methods often requires repetitive training of control policies, which is even more computationally prohibitive. In this work, we propose a novel Curriculum-based Multi-Fidelity Bayesian Optimization framework (CMFBO) for efficient hyperparameter optimization of DRL-based character control systems. Using curriculum-based task difficulty as fidelity criterion, our method improves searching efficiency by gradually pruning search space through evaluation on easier motor skill tasks. We evaluate our method on two physics-based character control tasks: character morphology optimization and hyperparameter tuning of DeepMimic. Our algorithm significantly outperforms state-of-the-art hyperparameter optimization methods applicable for physics-based character animation. In particular, we show that hyperparameters optimized through our algorithm result in at least 5x efficiency gain comparing to author-released settings in DeepMimic.
International Migration in Academia and Citation Performance: An Analysis of German-Affiliated Researchers by Gender and Discipline Using Scopus Publications 1996-2020
Venue: arXiv cs.DL 2021
Year: 2021

Germany has become a major country of immigration, as well as a research powerhouse in Europe. As Germany spends a higher fraction of its GDP on research and development than most countries with advanced economies, there is an expectation that Germany should be able to attract and retain international scholars who have high citation performance. Using an exhaustive set of over eight million Scopus publications, we analyze the trends in international migration to and from Germany among published researchers over the past 24 years. We assess changes in institutional affiliations for over one million researchers who have published with a German affiliation address at some point during the 1996-2020 period. We show that while Germany has been highly integrated into the global movement of researchers, with particularly strong ties to the US, the UK, and Switzerland, the country has been sending more published researchers abroad than it has attracted. While the balance has been largely negative over time, analyses disaggregated by gender, citation performance, and field of research show that compositional differences in migrant flows may help to alleviate persistent gender inequalities in selected fields.
A dissemination workshop for introducing young Italian students to NLP
Venue: arXiv cs.CL 2021
Year: 2021

We describe and make available the game-based material developed for a laboratory run at several Italian science festivals to popularize NLP among young students.
Model Guided Road Intersection Classification
Venue: arXiv cs.CV 2021
Year: 2021

Understanding complex scenarios from in-vehicle cameras is essential for safely operating autonomous driving systems in densely populated areas. Among these, intersection areas are one of the most critical as they concentrate a considerable number of traffic accidents and fatalities. Detecting and understanding the scene configuration of these usually crowded areas is then of extreme importance for both autonomous vehicles and modern ADAS aimed at preventing road crashes and increasing the safety of vulnerable road users. This work investigates inter-section classification from RGB images using well-consolidate neural network approaches along with a method to enhance the results based on the teacher/student training paradigm. An extensive experimental activity aimed at identifying the best input configuration and evaluating different network parameters on both the well-known KITTI dataset and the new KITTI-360 sequences shows that our method outperforms current state-of-the-art approaches on a per-frame basis and prove the effectiveness of the proposed learning scheme.
Generation of musical patterns through operads
Venue: arXiv cs.SD 2021
Year: 2021

We introduce the notion of multi-pattern, a combinatorial abstraction of polyphonic musical phrases. The interest of this approach lies in the fact that this offers a way to compose two multi-patterns in order to produce a longer one. This dives musical phrases into an algebraic context since the set of multi-patterns has the structure of an operad; operads being structures offering a formalization of the notion of operators and their compositions. Seeing musical phrases as operators allows us to perform computations on phrases and admits applications in generative music: given a set of short patterns, we propose various algorithms to randomly generate a new and longer phrase inspired by the inputted patterns.
What Makes a Message Persuasive? Identifying Adaptations Towards Persuasiveness in Nine Exploratory Case Studies
Venue: arXiv cs.CL 2021
Year: 2021

The ability to persuade others is critical to professional and personal success. However, crafting persuasive messages is demanding and poses various challenges. We conducted nine exploratory case studies to identify adaptations that professional and non-professional writers make in written scenarios to increase their subjective persuasiveness. Furthermore, we identified challenges that those writers faced and identified strategies to resolve them with persuasive natural language generation, i.e., artificial intelligence. Our findings show that humans can achieve high degrees of persuasiveness (more so for professional-level writers), and artificial intelligence can complement them to achieve increased celerity and alignment in the process.
3D Scene Compression through Entropy Penalized Neural Representation Functions
Venue: arXiv cs.CV 2021
Year: 2021

Some forms of novel visual media enable the viewer to explore a 3D scene from arbitrary viewpoints, by interpolating between a discrete set of original views. Compared to 2D imagery, these types of applications require much larger amounts of storage space, which we seek to reduce. Existing approaches for compressing 3D scenes are based on a separation of compression and rendering: each of the original views is compressed using traditional 2D image formats; the receiver decompresses the views and then performs the rendering. We unify these steps by directly compressing an implicit representation of the scene, a function that maps spatial coordinates to a radiance vector field, which can then be queried to render arbitrary viewpoints. The function is implemented as a neural network and jointly trained for reconstruction as well as compressibility, in an end-to-end manner, with the use of an entropy penalty on the parameters. Our method significantly outperforms a state-of-the-art conventional approach for scene compression, achieving simultaneously higher quality reconstructions and lower bitrates. Furthermore, we show that the performance at lower bitrates can be improved by jointly representing multiple scenes using a soft form of parameter sharing.
Reconfigurable Adaptive Channel Sensing
Venue: arXiv cs.IT 2021
Year: 2021

Channel sensing consists of probing the channel from time to time to check whether or not it is active - say, because of an incoming message. When communication is sparse with information being sent once in a long while, channel sensing becomes a significant source of energy consumption. How to reliably detect messages while minimizing the receiver energy consumption? This paper addresses this problem through a reconfigurable scheme, referred to as AdaSense, which exploits the dependency between the receiver noise figure (i.e., the receiver added noise) and the receiver power consumption; a higher power typically translates into less noisy channel observations. AdaSense begins in a low power low reliability mode and makes a first tentative decision based on a few channel observations. If a message is declared, it switches to a high power high reliability mode to confirm the decision, else it sleeps for the entire duration of the second phase. Compared to prominent detection schemes such as the BMAC protocol, AdaSense provides relative energy gains that grow unbounded in the small probability of false-alarm regime, as communication gets sparser. In the non-asymptotic regime energy gains are 30% to 75% for communication scenarios typically found in the context of wake-up receivers.
GPT2MVS: Generative Pre-trained Transformer-2 for Multi-modal Video Summarization
Venue: arXiv cs.CV 2021
Year: 2021

Traditional video summarization methods generate fixed video representations regardless of user interest. Therefore such methods limit users' expectations in content search and exploration scenarios. Multi-modal video summarization is one of the methods utilized to address this problem. When multi-modal video summarization is used to help video exploration, a text-based query is considered as one of the main drivers of video summary generation, as it is user-defined. Thus, encoding the text-based query and the video effectively are both important for the task of multi-modal video summarization. In this work, a new method is proposed that uses a specialized attention network and contextualized word representations to tackle this task. The proposed model consists of a contextualized video summary controller, multi-modal attention mechanisms, an interactive attention network, and a video summary generator. Based on the evaluation of the existing multi-modal video summarization benchmark, experimental results show that the proposed model is effective with the increase of +5.88% in accuracy and +4.06% increase of F1-score, compared with the state-of-the-art method.
Microservice Dynamic Architecture-Level Deployment Orchestration (Extended Version)
Venue: arXiv cs.DC 2021
Year: 2021

In the context of the BI-REX (Big Data Innovation and Research Excellence) competence center SEAWALL (SEAmless loW lAtency cLoud pLatforms) project (scientific coordinator Prof. Maurizio Gabbrielli) we develop a novel approach for run-time global adaptation of microservice applications, based on synthesis of architecture-level reconfiguration orchestrations. More precisely, we devise an algorithm for automatic reconfiguration that reaches a target system Maximum Computational Load by performing optimal deployment orchestrations. To conceive and simulate our approach, we introduce a novel integrated timed architectural modeling/execution language based on an extension of the actor-based object-oriented Abstract Behavioral Specification (ABS) language. In particular, we realize a timed extension of SmartDeployer, whose ABS code annotations make it possible to express architectural properties. Our Timed SmartDeployer tool fully integrates time features of ABS and architectural annotations by generating timed deployment orchestrations. We evaluate the applicability of our approach on a realistic microservice application taken from the literature: an Email Pipeline Processing System. We prove its effectiveness by simulating such an application and by comparing architecture-level reconfiguration with traditional local scaling techniques (which detect scaling needs and enact replications at the level of single microservices). Our comparison results show that our approach avoids cascading slowdowns and consequent increased message loss and latency, which affect traditional local scaling.
Simulation Modelling and Analysis of Primary Health Centre Operations
Venue: arXiv cs.CY 2021
Year: 2021

We present discrete-event simulation models of the operations of primary health centres (PHCs) in the Indian context. Our PHC simulation models incorporate four types of patients seeking medical care: outpatients, inpatients, childbirth cases, and patients seeking antenatal care. A generic modelling approach was adopted to develop simulation models of PHC operations. This involved developing an archetype PHC simulation, which was then adapted to represent two other PHC configurations, differing in numbers of resources and types of services provided, encountered during PHC visits. A model representing a benchmark configuration conforming to government-mandated operational guidelines, with demand estimated from disease burden data and service times closer to international estimates (higher than observed), was also developed. Simulation outcomes for the three observed configurations indicate negligible patient waiting times and low resource utilisation values at observed patient demand estimates. However, simulation outcomes for the benchmark configuration indicated significantly higher resource utilisation. Simulation experiments to evaluate the effect of potential changes in operational patterns on reducing the utilisation of stressed resources for the benchmark case were performed. Our analysis also motivated the development of simple analytical approximations of the average utilisation of a server in a queueing system with characteristics similar to the PHC doctor/patient system. Our study represents the first step in an ongoing effort to establish the computational infrastructure required to analyse public health operations in India, and can provide researchers in other settings with hierarchical health systems a template for the development of simulation models of their primary healthcare facilities.
Unified Spatio-Temporal Modeling for Traffic Forecasting using Graph Neural Network
Venue: arXiv cs.LG 2021
Year: 2021

Research in deep learning models to forecast traffic intensities has gained great attention in recent years due to their capability to capture the complex spatio-temporal relationships within the traffic data. However, most state-of-the-art approaches have designed spatial-only (e.g. Graph Neural Networks) and temporal-only (e.g. Recurrent Neural Networks) modules to separately extract spatial and temporal features. However, we argue that it is less effective to extract the complex spatio-temporal relationship with such factorized modules. Besides, most existing works predict the traffic intensity of a particular time interval only based on the traffic data of the previous one hour of that day. And thereby ignores the repetitive daily/weekly pattern that may exist in the last hour of data. Therefore, we propose a Unified Spatio-Temporal Graph Convolution Network (USTGCN) for traffic forecasting that performs both spatial and temporal aggregation through direct information propagation across different timestamp nodes with the help of spectral graph convolution on a spatio-temporal graph. Furthermore, it captures historical daily patterns in previous days and current-day patterns in current-day traffic data. Finally, we validate our work's effectiveness through experimental analysis, which shows that our model USTGCN can outperform state-of-the-art performances in three popular benchmark datasets from the Performance Measurement System (PeMS). Moreover, the training time is reduced significantly with our proposed USTGCN model.