OpenRaiser/Intern-Atlas huggingface dataset:
The Space of Mathematical Software Systems -- A Survey of Paradigmatic Systems
Venue: arXiv cs.MS 2020
Year: 2020

Mathematical software systems are becoming more and more important in pure and applied mathematics in order to deal with the complexity and scalability issues inherent in mathematics. In the last decades we have seen a cambric explosion of increasingly powerful but also diverging systems. To give researchers a guide to this space of systems, we devise a novel conceptualization of mathematical software that focuses on five aspects: inference covers formal logic and reasoning about mathematical statements via proofs and models, typically with strong emphasis on correctness; computation covers algorithms and software libraries for representing and manipulating mathematical objects, typically with strong emphasis on efficiency; concretization covers generating and maintaining collections of mathematical objects conforming to a certain pattern, typically with strong emphasis on complete enumeration; narration covers describing mathematical contexts and relations, typically with strong emphasis on human readability; finally, organization covers representing mathematical contexts and objects in machine-actionable formal languages, typically with strong emphasis on expressivity and system interoperability. Despite broad agreement that an ideal system would seamlessly integrate all these aspects, research has diversified into families of highly specialized systems focusing on a single aspect and possibly partially integrating others, each with their own communities, challenges, and successes. In this survey, we focus on the commonalities and differences of these systems from the perspective of a future multi-aspect system.
Measurement of Interpersonal Trust in Global Software Development: SLR Protocol
Venue: arXiv cs.SE 2020
Year: 2020

The purpose of this protocol is to be useful to identify, evaluate and synthesize reported knowledge about the measurement of interpersonal trust (IpT) in virtual software teams. To achieve this goal we applied a research technique known as Systematic Literature Review (SLR). The aim of a SLR is to be as objective, analytical, and repeatable as possible.
On Termination of Transactions over Semantic Document Models
Venue: arXiv cs.LO 2020
Year: 2020

We consider the framework of Document Modeling, which lays the formal basis for representing the document lifecycle in Business Process Management systems. We formulate document models in the scope of the logic-based Semantic Modeling language and study the question whether transactions given by a document model terminate on any input. We show that in general this problem is undecidable and formulate sufficient conditions, which guarantee decidability and polynomial boundedness of effects of transactions.
QPEP: A QUIC-Based Approach to Encrypted Performance Enhancing Proxies for High-Latency Satellite Broadband
Venue: arXiv cs.CR 2020
Year: 2020

Satellite broadband services are critical infrastructures enabling advanced technologies to function in the most remote regions of the globe. However, status-quo services are often unencrypted by default and vulnerable to eavesdropping attacks. In this paper, we challenge the historical perception that over-the-air security must trade off with TCP performance in high-latency satellite networks due to the deep-packet inspection requirements of Performance Enhancing Proxies (PEPs). After considering why prior work in this area has failed to find wide adoption, we present an open-source encrypted-by-default PEP - QPEP - which seeks to address these issues. QPEP is built around the open QUIC standard and designed so individual customers may adopt it without ISP involvement. QPEP's performance is assessed through simulations in a replicable docker-based testbed. Across many benchmarks and network conditions, QPEP is found to avoid the perceived security-encryption trade-off in PEP design. Compared to unencrypted PEP implementations, QPEP reduces average page load times by more than 30% while also offering over-the-air privacy. Compared to the traditional VPN encryption available to customers today, QPEP more than halves average page load times. Together, these experiments lead to the conclusion that QPEP represents a promising new approach to protecting modern satellite broadband connections.
Wi-Fi Channel Saturation as a Mechanism to Improve Passive Capture of Bluetooth Through Channel Usage Restriction
Venue: arXiv cs.CR 2020
Year: 2020

Bluetooth is a short-range wireless technology that provides audio and data links between personal smartphones and playback devices, such as speakers, headsets and car entertainment systems. Since its introduction in 2001, security researchers have suggested that the protocol is weak, and prone to a variety of attacks against its authentication, link management and encryption schemes. Key researchers in the field have suggested that reliable passive sniffing of Bluetooth traffic would enable the practical application of a range of currently hypothesised attacks. Restricting Bluetooth's frequency hopping behaviour by manipulation of the available channels, in order to make brute force attacks more effective has been a frequently proposed avenue of future research from the literature. This paper has evaluated the proposed approach in a series of experiments using the software defined radio tools and custom hardware developed by the Ubertooth project. The work concludes that the mechanism suggested by previous researchers may not deliver the proposed improvements, but describes an as yet undocumented interaction between Bluetooth and Wi-Fi technologies which may provide a Denial of Service attack mechanism.
Recursed is not Recursive: A Jarring Result
Venue: arXiv cs.AI 2020
Year: 2020

Recursed is a 2D puzzle platform video game featuring treasure chests that, when jumped into, instantiate a room that can later be exited (similar to function calls), optionally generating a jar that returns back to that room (similar to continuations). We prove that Recursed is RE-complete and thus undecidable (not recursive) by a reduction from the Post Correspondence Problem. Our reduction is "practical": the reduction from PCP results in fully playable levels that abide by all constraints governing levels (including the 15x20 room size) designed for the main game. Our reduction is also "efficient": a Turing machine can be simulated by a Recursed level whose size is linear in the encoding size of the Turing machine and whose solution length is polynomial in the running time of the Turing machine.
Online Learning of the Kalman Filter with Logarithmic Regret
Venue: arXiv cs.LG 2020
Year: 2020

In this paper, we consider the problem of predicting observations generated online by an unknown, partially observed linear system, which is driven by stochastic noise. For such systems the optimal predictor in the mean square sense is the celebrated Kalman filter, which can be explicitly computed when the system model is known. When the system model is unknown, we have to learn how to predict observations online based on finite data, suffering possibly a non-zero regret with respect to the Kalman filter's prediction. We show that it is possible to achieve a regret of the order of $\mathrm{poly}\log(N)$ with high probability, where $N$ is the number of observations collected. Our work is the first to provide logarithmic regret guarantees for the widely used Kalman filter. This is achieved using an online least-squares algorithm, which exploits the approximately linear relation between future observations and past observations. The regret analysis is based on the stability properties of the Kalman filter, recent statistical tools for finite sample analysis of system identification, and classical results for the analysis of least-squares algorithms for time series. Our regret analysis can also be applied for state prediction of the hidden state, in the case of unknown noise statistics but known state-space basis. A fundamental technical contribution is that our bounds hold even for the class of non-explosive systems, which includes the class of marginally stable systems, which was an open problem for the case of online prediction under stochastic noise.
Social and Child Care Provision in Kinship Networks: an Agent-Based Model
Venue: arXiv cs.CY 2020
Year: 2020

Providing for the needs of the vulnerable is a critical component of social and health policy-making. In particular, caring for children and for vulnerable older people is vital to the wellbeing of millions of families throughout the world. In most developed countries, this care is provided through both formal and informal means, and is therefore governed by complex policies that interact in non-obvious ways with other areas of policy-making. In this paper we present an agent-based model of social and child care provision in the UK, in which agents can provide informal care or pay for private care for their relatives. Agents make care decisions based on numerous factors including their health status, employment, financial situation, and social and physical distance to those in need. Simulation results show that the model can produce plausible patterns of care need and availability, and therefore can provide an important aid to this complex area of policy-making. We conclude that the model's use of kinship networks for distributing care and the explicit modelling of interactions between social care and child care will enable policy-makers to develop more informed policy interventions in these critical areas.
Signaling in Bayesian Network Congestion Games: the Subtle Power of Symmetry
Venue: arXiv cs.GT 2020
Year: 2020

Network congestion games are a well-understood model of multi-agent strategic interactions. Despite their ubiquitous applications, it is not clear whether it is possible to design information structures to ameliorate the overall experience of the network users. We focus on Bayesian games with atomic players, where network vagaries are modeled via a (random) state of nature which determines the costs incurred by the players. A third-party entity---the sender---can observe the realized state of the network and exploit this additional information to send a signal to each player. A natural question is the following: is it possible for an informed sender to reduce the overall social cost via the strategic provision of information to players who update their beliefs rationally? The paper focuses on the problem of computing optimal ex ante persuasive signaling schemes, showing that symmetry is a crucial property for its solution. Indeed, we show that an optimal ex ante persuasive signaling scheme can be computed in polynomial time when players are symmetric and have affine cost functions. Moreover, the problem becomes NP-hard when players are asymmetric, even in non-Bayesian settings.
Explainable Deep Modeling of Tabular Data using TableGraphNet
Venue: arXiv cs.LG 2020
Year: 2020

The vast majority of research on explainability focuses on post-explainability rather than explainable modeling. Namely, an explanation model is derived to explain a complex black box model built with the sole purpose of achieving the highest performance possible. In part, this trend might be driven by the misconception that there is a trade-off between explainability and accuracy. Furthermore, the consequential work on Shapely values, grounded in game theory, has also contributed to a new wave of post-explainability research on better approximations for various machine learning models, including deep learning models. We propose a new architecture that inherently produces explainable predictions in the form of additive feature attributions. Our approach learns a graph representation for each record in the dataset. Attribute centric features are then derived from the graph and fed into a contribution deep set model to produce the final predictions. We show that our explainable model attains the same level of performance as black box models. Finally, we provide an augmented model training approach that leverages the missingness property and yields high levels of consistency (as required for the Shapely values) without loss of accuracy.
A Matching Mechanism with Anticipatory Tolls for Congestion Pricing
Venue: arXiv cs.GT 2020
Year: 2020

This paper presents a matching mechanism for assigning drivers to routes where the drivers pay a toll for the marginal delay they impose on other drivers. The simple matching mechanism is derived from the RANKING algorithm for online bipartite matching proposed by Karp et al. [8]. The toll, which is anticipatory in design, is an adaption of one proposed by Dong et al. [5]. Our research proves that the matching mechanism proposed here is pareto user-optimal and can be adapted to give network optimal results for the minimizing total social cost of travel.
Cooperative Observation of Targets moving over a Planar Graph with Prediction of Positions
Venue: arXiv cs.AI 2020
Year: 2020

Consider a team with two types of agents: targets and observers. Observers are aerial UAVs that observe targets moving on land with their movements restricted to the paths that form a planar graph on the surface. Observers have limited range of vision and targets do not avoid observers. The objective is to maximize the integral of the number of targets observed in the observation interval. Taking advantage of the fact that the future positions of targets in the short term are predictable, we show in this article a modified hill climbing algorithm that surpasses its previous versions in this new setting of the CTO problem.
CEB Improves Model Robustness
Venue: arXiv cs.LG 2020
Year: 2020

We demonstrate that the Conditional Entropy Bottleneck (CEB) can improve model robustness. CEB is an easy strategy to implement and works in tandem with data augmentation procedures. We report results of a large scale adversarial robustness study on CIFAR-10, as well as the ImageNet-C Common Corruptions Benchmark, ImageNet-A, and PGD attacks.
Recurrent Attention Model with Log-Polar Mapping is Robust against Adversarial Attacks
Venue: arXiv cs.CV 2020
Year: 2020

Convolutional neural networks are vulnerable to small $\ell^p$ adversarial attacks, while the human visual system is not. Inspired by neural networks in the eye and the brain, we developed a novel artificial neural network model that recurrently collects data with a log-polar field of view that is controlled by attention. We demonstrate the effectiveness of this design as a defense against SPSA and PGD adversarial attacks. It also has beneficial properties observed in the animal visual system, such as reflex-like pathways for low-latency inference, fixed amount of computation independent of image size, and rotation and scale invariance. The code for experiments is available at https://gitlab.com/exwzd-public/kiritani_ono_2020.
Tight Lower Bounds for Combinatorial Multi-Armed Bandits
Venue: arXiv cs.LG 2020
Year: 2020

The Combinatorial Multi-Armed Bandit problem is a sequential decision-making problem in which an agent selects a set of arms on each round, observes feedback for each of these arms and aims to maximize a known reward function of the arms it chose. While previous work proved regret upper bounds in this setting for general reward functions, only a few works provided matching lower bounds, all for specific reward functions. In this work, we prove regret lower bounds for combinatorial bandits that hold under mild assumptions for all smooth reward functions. We derive both problem-dependent and problem-independent bounds and show that the recently proposed Gini-weighted smoothness parameter (Merlis and Mannor, 2019) also determines the lower bounds for monotone reward functions. Notably, this implies that our lower bounds are tight up to log-factors.
Identifying Audio Adversarial Examples via Anomalous Pattern Detection
Venue: arXiv cs.LG 2020
Year: 2020

Audio processing models based on deep neural networks are susceptible to adversarial attacks even when the adversarial audio waveform is 99.9% similar to a benign sample. Given the wide application of DNN-based audio recognition systems, detecting the presence of adversarial examples is of high practical relevance. By applying anomalous pattern detection techniques in the activation space of these models, we show that 2 of the recent and current state-of-the-art adversarial attacks on audio processing systems systematically lead to higher-than-expected activation at some subset of nodes and we can detect these with up to an AUC of 0.98 with no degradation in performance on benign samples.
Air-to-Air Communications Beyond 5G: A Novel 3D CoMP Transmission Scheme
Venue: arXiv cs.IT 2020
Year: 2020

In this paper, a novel $3$D cellular model consisting of aerial base stations (aBSs) and aerial user equipments (aUEs) is proposed, by integrating the coordinated multi-point (CoMP) transmission technique with the theory of stochastic geometry. For this new $3$D architecture, a tractable model for aBSs' deployment based on the binomial-Delaunay tetrahedralization is developed, which ensures seamless coverage for a given space. In addition, a versatile and practical frequency allocation scheme is designed to eliminate the inter-cell interference effectively. Based on this model, performance metrics including the achievable data rate and coverage probability are derived for two types of aUEs: {\it i)} the general aUE (i.e., an aUE having distinct distances from its serving aBSs) and {\it ii)} the worst-case aUE (i.e., an aUE having equal distances from its serving aBSs). Simulation and numerical results demonstrate that the proposed approach emphatically outperforms the conventional binomial-Voronoi tessellation without CoMP. Insightfully, it provides a similar performance to the binomial-Voronoi tessellation which utilizes the conventional CoMP scheme; yet, introducing a considerably reduced computational complexity and backhaul/signaling overhead.
Chaotic Phase Synchronization and Desynchronization in an Oscillator Network for Object Selection
Venue: arXiv cs.CV 2020
Year: 2020

Object selection refers to the mechanism of extracting objects of interest while ignoring other objects and background in a given visual scene. It is a fundamental issue for many computer vision and image analysis techniques and it is still a challenging task to artificial visual systems. Chaotic phase synchronization takes place in cases involving almost identical dynamical systems and it means that the phase difference between the systems is kept bounded over the time, while their amplitudes remain chaotic and may be uncorrelated. Instead of complete synchronization, phase synchronization is believed to be a mechanism for neural integration in brain. In this paper, an object selection model is proposed. Oscillators in the network representing the salient object in a given scene are phase synchronized, while no phase synchronization occurs for background objects. In this way, the salient object can be extracted. In this model, a shift mechanism is also introduced to change attention from one object to another. Computer simulations show that the model produces some results similar to those observed in natural vision systems.
Combining Machine Learning with Knowledge-Based Modeling for Scalable Forecasting and Subgrid-Scale Closure of Large, Complex, Spatiotemporal Systems
Venue: arXiv cs.LG 2020
Year: 2020

We consider the commonly encountered situation (e.g., in weather forecasting) where the goal is to predict the time evolution of a large, spatiotemporally chaotic dynamical system when we have access to both time series data of previous system states and an imperfect model of the full system dynamics. Specifically, we attempt to utilize machine learning as the essential tool for integrating the use of past data into predictions. In order to facilitate scalability to the common scenario of interest where the spatiotemporally chaotic system is very large and complex, we propose combining two approaches:(i) a parallel machine learning prediction scheme; and (ii) a hybrid technique, for a composite prediction system composed of a knowledge-based component and a machine-learning-based component. We demonstrate that not only can this method combining (i) and (ii) be scaled to give excellent performance for very large systems, but also that the length of time series data needed to train our multiple, parallel machine learning components is dramatically less than that necessary without parallelization. Furthermore, considering cases where computational realization of the knowledge-based component does not resolve subgrid-scale processes, our scheme is able to use training data to incorporate the effect of the unresolved short-scale dynamics upon the resolved longer-scale dynamics ("subgrid-scale closure").
Dynamic Role-Based Access Control for Decentralized Applications
Venue: arXiv cs.CR 2020
Year: 2020

Access control management is an integral part of maintaining the security of an application. Although there has been significant work in the field of cloud access control mechanisms, however, with the advent of Distributed Ledger Technology (DLT), on-chain access control management frameworks hardly exist. Existing access control management mechanisms are tightly coupled with the business logic, resulting in governance issues, non-coherent with existing Identity Management Solutions, low security, and compromised usability. We propose a novel framework to implement dynamic role-based access control for decentralized applications (dApps). The framework allows for managing access control on a dApp, which is completely decoupled from the business application and integrates seamlessly with any dApps. The smart contract architecture allows for the independent management of business logic and execution of access control policies. It also facilitates secure, low cost, and a high degree of flexibility of access control management. The proposed framework promotes decentralized governance of access control policies and efficient smart contract upgrades. We also provide quantitative and qualitative metrics for the efficacy and efficiency of the framework. Any Turing complete smart contract programming language is an excellent fit to implement the framework. We expect this framework to benefit enterprise and non-enterprise dApps and provide greater access control flexibility and effective integration with traditional and state of the art identity management solutions.
BiSample: Bidirectional Sampling for Handling Missing Data with Local Differential Privacy
Venue: arXiv cs.CR 2020
Year: 2020

Local differential privacy (LDP) has received much interest recently. In existing protocols with LDP guarantees, a user encodes and perturbs his data locally before sharing it to the aggregator. In common practice, however, users would prefer not to answer all the questions due to different privacy-preserving preferences for different questions, which leads to data missing or the loss of data quality. In this paper, we demonstrate a new approach for addressing the challenges of data perturbation with consideration of users' privacy preferences. Specifically, we first propose BiSample: a bidirectional sampling technique value perturbation in the framework of LDP. Then we combine the BiSample mechanism with users' privacy preferences for missing data perturbation. Theoretical analysis and experiments on a set of datasets confirm the effectiveness of the proposed mechanisms.