OpenRaiser/Intern-Atlas huggingface dataset:
Probabilistic Bisimulation for Parameterized Systems (Technical Report)
Venue: arXiv cs.SE 2020
Year: 2020

Probabilistic bisimulation is a fundamental notion of process equivalence for probabilistic systems. Among others, it has important applications including formalizing the anonymity property of several communication protocols. There is a lot of work on verifying probabilistic bisimulation for finite systems. This is however not the case for parameterized systems, where the problem is in general undecidable. In this paper we provide a generic framework for reasoning about probabilistic bisimulation for parameterized systems. Our approach is in the spirit of software verification, wherein we encode proof rules for probabilistic bisimulation and use a decidable first-order theory to specify systems and candidate bisimulation relations, which can then be checked automatically against the proof rules. As a case study, we show that our framework is sufficiently expressive for proving the anonymity property of the parameterized dining cryptographers protocol and the parameterized grades protocol, when supplied with a candidate regular bisimulation relation. Both of these protocols hitherto could not be verified by existing automatic methods. Moreover, with the help of standard automata learning algorithms, we show that the candidate relations can be synthesized fully automatically, making the verification fully automated.
A Neuro-Symbolic Method for Solving Differential and Functional Equations
Venue: arXiv cs.LG 2020
Year: 2020

When neural networks are used to solve differential equations, they usually produce solutions in the form of black-box functions that are not directly mathematically interpretable. We introduce a method for generating symbolic expressions to solve differential equations while leveraging deep learning training methods. Unlike existing methods, our system does not require learning a language model over symbolic mathematics, making it scalable, compact, and easily adaptable for a variety of tasks and configurations. As part of the method, we propose a novel neural architecture for learning mathematical expressions to optimize a customizable objective. The system is designed to always return a valid symbolic formula, generating a useful approximation when an exact analytic solution to a differential equation is not or cannot be found. We demonstrate through examples how our method can be applied on a number of differential equations, often obtaining symbolic approximations that are useful or insightful. Furthermore, we show how the system can be effortlessly generalized to find symbolic solutions to other mathematical tasks, including integration and functional equations.
The dynamic effect of mechanical losses of actuators on the equations of motion of legged robots
Venue: arXiv cs.RO 2020
Year: 2020

Industrial manipulators do not collapse under their own weight when powered off due to the friction in their joints. Although these mechanism are effective for stiff position control of pick-and-place, they are inappropriate for legged robots which must rapidly regulate compliant interactions with the environment. However, no metric exists to quantify the robot's perform degradation due to mechanical losses in the actuators. This letter provides a novel formulation which describes how the efficiency of individual actuators propagate to the equations of motion of the whole robot. We quantitatively demonstrate the intuitive fact that the apparent inertia of the robots increase in the presence of joint friction. We also reproduce the empirical result that robots which employ high gearing and low efficiency actuators can statically sustain more substantial external loads. We expect that the framework presented here will provide the foundations to design the next generation of legged robots which can effectively interact with the world.
Opinion Dynamics with Varying Susceptibility to Persuasion via Non-Convex Local Search
Venue: arXiv cs.SI 2020
Year: 2020

A long line of work in social psychology has studied variations in people's susceptibility to persuasion -- the extent to which they are willing to modify their opinions on a topic. This body of literature suggests an interesting perspective on theoretical models of opinion formation by interacting parties in a network: in addition to considering interventions that directly modify people's intrinsic opinions, it is also natural to consider interventions that modify people's susceptibility to persuasion. In this work, motivated by this fact we propose a new framework for social influence. Specifically, we adopt a popular model for social opinion dynamics, where each agent has some fixed innate opinion, and a resistance that measures the importance it places on its innate opinion; agents influence one another's opinions through an iterative process. Under non-trivial conditions, this iterative process converges to some equilibrium opinion vector. For the unbudgeted variant of the problem, the goal is to select the resistance of each agent (from some given range) such that the sum of the equilibrium opinions is minimized. We prove that the objective function is in general non-convex. Hence, formulating the problem as a convex program as in an early version of this work (Abebe et al., KDD'18) might have potential correctness issues. We instead analyze the structure of the objective function, and show that any local optimum is also a global optimum, which is somehow surprising as the objective function might not be convex. Furthermore, we combine the iterative process and the local search paradigm to design very efficient algorithms that can solve the unbudgeted variant of the problem optimally on large-scale graphs containing millions of nodes. Finally, we propose and evaluate experimentally a family of heuristics for the budgeted variation of the problem.
Universal Multi-Source Domain Adaptation
Venue: arXiv cs.CV 2020
Year: 2020

Unsupervised domain adaptation enables intelligent models to transfer knowledge from a labeled source domain to a similar but unlabeled target domain. Recent study reveals that knowledge can be transferred from one source domain to another unknown target domain, called Universal Domain Adaptation (UDA). However, in the real-world application, there are often more than one source domain to be exploited for domain adaptation. In this paper, we formally propose a more general domain adaptation setting, universal multi-source domain adaptation (UMDA), where the label sets of multiple source domains can be different and the label set of target domain is completely unknown. The main challenges in UMDA are to identify the common label set between each source domain and target domain, and to keep the model scalable as the number of source domains increases. To address these challenges, we propose a universal multi-source adaptation network (UMAN) to solve the domain adaptation problem without increasing the complexity of the model in various UMDA settings. In UMAN, we estimate the reliability of each known class in the common label set via the prediction margin, which helps adversarial training to better align the distributions of multiple source domains and target domain in the common label set. Moreover, the theoretical guarantee for UMAN is also provided. Massive experimental results show that existing UDA and multi-source DA (MDA) methods cannot be directly applied to UMDA and the proposed UMAN achieves the state-of-the-art performance in various UMDA settings.
Learning a Decentralized Multi-arm Motion Planner
Venue: arXiv cs.RO 2020
Year: 2020

We present a closed-loop multi-arm motion planner that is scalable and flexible with team size. Traditional multi-arm robot systems have relied on centralized motion planners, whose runtimes often scale exponentially with team size, and thus, fail to handle dynamic environments with open-loop control. In this paper, we tackle this problem with multi-agent reinforcement learning, where a decentralized policy is trained to control one robot arm in the multi-arm system to reach its target end-effector pose given observations of its workspace state and target end-effector pose. The policy is trained using Soft Actor-Critic with expert demonstrations from a sampling-based motion planning algorithm (i.e., BiRRT). By leveraging classical planning algorithms, we can improve the learning efficiency of the reinforcement learning algorithm while retaining the fast inference time of neural networks. The resulting policy scales sub-linearly and can be deployed on multi-arm systems with variable team sizes. Thanks to the closed-loop and decentralized formulation, our approach generalizes to 5-10 multi-arm systems and dynamic moving targets (>90% success rate for a 10-arm system), despite being trained on only 1-4 arm planning tasks with static targets. Code and data links can be found at https://multiarm.cs.columbia.edu.
Time-dependent Performance Analysis of the 802.11p-based Platooning Communications Under Disturbance
Venue: arXiv cs.NI 2020
Year: 2020

Platooning is a critical technology to realize autonomous driving. Each vehicle in platoons adopts the IEEE 802.11p standard to exchange information through communications to maintain the string stability of platoons. However, one vehicle in platoons inevitably suffers from a disturbance resulting from the leader vehicle acceleration/deceleration, wind gust and uncertainties in a platoon control system, i.e., aerodynamics drag and rolling resistance moment etc. Disturbances acting on one vehicle may inevitably affect the following vehicles and cause that the spacing error is propagated or even amplified downstream along the platoon, i.e., platoon string instability. In this case, the connectivity among vehicles is dynamic, resulting in the performance of 802.11p in terms of packet delay and packet delivery ratio being time-varying. The effect of the string instability would be further deteriorated once the time-varying performance of 802.11p cannot satisfy the basic communication requirement. Unlike the existing works which only analyze the steady performance of 802.11p in vehicular networks, we will focus on the impact of disturbance and construct models to analyze the time-dependent performance of 802.11p-based platooning communications. The effectiveness of the models is validated through simulation results. Moreover, the time-dependent performance of 802.11p is analyzed through numerical results and it is validated that 802.11p is able to satisfy the communication requirement under disturbance.
On the Analysis of Spatially Constrained Power of Two Choice Policies
Venue: arXiv cs.DC 2020
Year: 2020

We consider a class of power of two choice based assignment policies for allocating users to servers, where both users and servers are located on a two-dimensional Euclidean plane. In this framework, we investigate the inherent tradeoff between the communication cost, and load balancing performance of different allocation policies. To this end, we first design and evaluate a Spatial Power of two (sPOT) policy in which each user is allocated to the least loaded server among its two geographically nearest servers sequentially. When servers are placed on a two-dimensional square grid, sPOT maps to the classical Power of two (POT) policy on the Delaunay graph associated with the Voronoi tessellation of the set of servers. We show that the associated Delaunay graph is 4-regular and provide expressions for asymptotic maximum load using results from the literature. For uniform placement of servers, we map sPOT to a classical balls and bins allocation policy with bins corresponding to the Voronoi regions associated with the second order Voronoi diagram of the set of servers. We provide expressions for the lower bound on the asymptotic expected maximum load on the servers and prove that sPOT does not achieve POT load balancing benefits. However, experimental results suggest the efficacy of sPOT with respect to expected communication cost. Finally, we propose two non-uniform server sampling based POT policies that achieve the best of both the performance metrics. Experimental results validate the effctiveness of our proposed policies.
Entity Linking in 100 Languages
Venue: arXiv cs.CL 2020
Year: 2020

We propose a new formulation for multilingual entity linking, where language-specific mentions resolve to a language-agnostic Knowledge Base. We train a dual encoder in this new setting, building on prior work with improved feature representation, negative mining, and an auxiliary entity-pairing task, to obtain a single entity retrieval model that covers 100+ languages and 20 million entities. The model outperforms state-of-the-art results from a far more limited cross-lingual linking task. Rare entities and low-resource languages pose challenges at this large-scale, so we advocate for an increased focus on zero- and few-shot evaluation. To this end, we provide Mewsli-9, a large new multilingual dataset (http://goo.gle/mewsli-dataset) matched to our setting, and show how frequency-based analysis provided key insights for our model and training enhancements.
An analysis of the transfer learning of convolutional neural networks for artistic images
Venue: arXiv cs.CV 2020
Year: 2020

Transfer learning from huge natural image datasets, fine-tuning of deep neural networks and the use of the corresponding pre-trained networks have become de facto the core of art analysis applications. Nevertheless, the effects of transfer learning are still poorly understood. In this paper, we first use techniques for visualizing the network internal representations in order to provide clues to the understanding of what the network has learned on artistic images. Then, we provide a quantitative analysis of the changes introduced by the learning process thanks to metrics in both the feature and parameter spaces, as well as metrics computed on the set of maximal activation images. These analyses are performed on several variations of the transfer learning procedure. In particular, we observed that the network could specialize some pre-trained filters to the new image modality and also that higher layers tend to concentrate classes. Finally, we have shown that a double fine-tuning involving a medium-size artistic dataset can improve the classification on smaller datasets, even when the task changes.
Goal-driven Long-Term Trajectory Prediction
Venue: arXiv cs.CV 2020
Year: 2020

The prediction of humans' short-term trajectories has advanced significantly with the use of powerful sequential modeling and rich environment feature extraction. However, long-term prediction is still a major challenge for the current methods as the errors could accumulate along the way. Indeed, consistent and stable prediction far to the end of a trajectory inherently requires deeper analysis into the overall structure of that trajectory, which is related to the pedestrian's intention on the destination of the journey. In this work, we propose to model a hypothetical process that determines pedestrians' goals and the impact of such process on long-term future trajectories. We design Goal-driven Trajectory Prediction model - a dual-channel neural network that realizes such intuition. The two channels of the network take their dedicated roles and collaborate to generate future trajectories. Different than conventional goal-conditioned, planning-based methods, the model architecture is designed to generalize the patterns and work across different scenes with arbitrary geometrical and semantic structures. The model is shown to outperform the state-of-the-art in various settings, especially in large prediction horizons. This result is another evidence for the effectiveness of adaptive structured representation of visual and geometrical features in human behavior analysis.
The Gray Rhino of Pandemic Preparedness: Proactive digital, data, and organizational infrastructure to help humanity build resilience in the face of pandemics
Venue: arXiv cs.CY 2020
Year: 2020

COVID-19 has exposed glaring holes in our existing digital, data, and organizational practices. Researchers ensconced in epidemiological and human health work have repeatedly pointed out how urban encroachment, climate change, and other human-triggered activities and patterns are going to make zoonotic pandemics more frequent and commonplace. The Gray Rhino mindset provides a useful reframing (as opposed to viewing pandemics such as the current one as a Black Swan event) that can help us recover faster from these (increasingly) frequent occurrences and build resiliency in our digital, data, and organizational infrastructure. Mitigating the social and economic impacts of pandemics can be eased through building infrastructure that elucidate leading indicators via passive intelligence gathering so that responses to containing the spread of pandemics are not blanket measures; instead, they can be fine-grained allowing for more efficient utilization of scarce resources and minimizing disruption to our way of life.
NUAA-QMUL at SemEval-2020 Task 8: Utilizing BERT and DenseNet for Internet Meme Emotion Analysis
Venue: arXiv cs.CL 2020
Year: 2020

This paper describes our contribution to SemEval 2020 Task 8: Memotion Analysis. Our system learns multi-modal embeddings from text and images in order to classify Internet memes by sentiment. Our model learns text embeddings using BERT and extracts features from images with DenseNet, subsequently combining both features through concatenation. We also compare our results with those produced by DenseNet, ResNet, BERT, and BERT-ResNet. Our results show that image classification models have the potential to help classifying memes, with DenseNet outperforming ResNet. Adding text features is however not always helpful for Memotion Analysis.
Challenges and strategies for running controlled crowdsourcing experiments
Venue: arXiv cs.HC 2020
Year: 2020

This paper reports on the challenges and lessons we learned while running controlled experiments in crowdsourcing platforms. Crowdsourcing is becoming an attractive technique to engage a diverse and large pool of subjects in experimental research, allowing researchers to achieve levels of scale and completion times that would otherwise not be feasible in lab settings. However, the scale and flexibility comes at the cost of multiple and sometimes unknown sources of bias and confounding factors that arise from technical limitations of crowdsourcing platforms and from the challenges of running controlled experiments in the "wild". In this paper, we take our experience in running systematic evaluations of task design as a motivating example to explore, describe, and quantify the potential impact of running uncontrolled crowdsourcing experiments and derive possible coping strategies. Among the challenges identified, we can mention sampling bias, controlling the assignment of subjects to experimental conditions, learning effects, and reliability of crowdsourcing results. According to our empirical studies, the impact of potential biases and confounding factors can amount to a 38\% loss in the utility of the data collected in uncontrolled settings; and it can significantly change the outcome of experiments. These issues ultimately inspired us to implement CrowdHub, a system that sits on top of major crowdsourcing platforms and allows researchers and practitioners to run controlled crowdsourcing projects.
On cyclic LRC codes that are also LCD codes
Venue: arXiv cs.IT 2020
Year: 2020

Locally recoverable (LRC) codes provide a solution to single node failure in distributed storage systems, where it is a very common problem. On the other hand, linear complementary dual (LCD) codes are useful in fault injections attacks on storage systems. In this paper, we establish a connection between LRC codes and LCD codes. We derive some conditions on the construction of cyclic LRC codes so that they are also LCD codes. A lower bound on the minimum distance of such codes is determined. Some examples have been given to explain the construction.
Local SGD: Unified Theory and New Efficient Methods
Venue: arXiv cs.LG 2020
Year: 2020

We present a unified framework for analyzing local SGD methods in the convex and strongly convex regimes for distributed/federated training of supervised machine learning models. We recover several known methods as a special case of our general framework, including Local-SGD/FedAvg, SCAFFOLD, and several variants of SGD not originally designed for federated learning. Our framework covers both the identical and heterogeneous data settings, supports both random and deterministic number of local steps, and can work with a wide array of local stochastic gradient estimators, including shifted estimators which are able to adjust the fixed points of local iterations for faster convergence. As an application of our framework, we develop multiple novel FL optimizers which are superior to existing methods. In particular, we develop the first linearly converging local SGD method which does not require any data homogeneity or other strong assumptions.
Digital Twins: State of the Art Theory and Practice, Challenges, and Open Research Questions
Venue: arXiv cs.LG 2020
Year: 2020

Digital Twin was introduced over a decade ago, as an innovative all-encompassing tool, with perceived benefits including real-time monitoring, simulation and forecasting. However, the theoretical framework and practical implementations of digital twins (DT) are still far from this vision. Although successful implementations exist, sufficient implementation details are not publicly available, therefore it is difficult to assess their effectiveness, draw comparisons and jointly advance the DT methodology. This work explores the various DT features and current approaches, the shortcomings and reasons behind the delay in the implementation and adoption of digital twin. Advancements in machine learning, internet of things and big data have contributed hugely to the improvements in DT with regards to its real-time monitoring and forecasting properties. Despite this progress and individual company-based efforts, certain research gaps exist in the field, which have caused delay in the widespread adoption of this concept. We reviewed relevant works and identified that the major reasons for this delay are the lack of a universal reference framework, domain dependence, security concerns of shared data, reliance of digital twin on other technologies, and lack of quantitative metrics. We define the necessary components of a digital twin required for a universal reference framework, which also validate its uniqueness as a concept compared to similar concepts like simulation, autonomous systems, etc. This work further assesses the digital twin applications in different domains and the current state of machine learning and big data in it. It thus answers and identifies novel research questions, both of which will help to better understand and advance the theory and practice of digital twins.