OpenRaiser/Intern-Atlas huggingface dataset:
A Precise and Expressive Lattice-theoretical Framework for Efficient Network Verification
Venue: arXiv cs.NI 2019
Year: 2019

Network verification promises to detect errors, such as black holes and forwarding loops, by logically analyzing the control or data plane. To do so efficiently, the state-of-the-art (e.g., Veriflow) partitions packet headers with identical forwarding behavior into the same packet equivalence class (PEC). Recently, Yang and Lam showed how to construct the minimal set of PECs, called atomic predicates. Their construction uses Binary Decision Diagrams (BDDs). However, BDDs have been shown to incur significant overhead per packet header bit, performing poorly when analyzing large-scale data centers. The overhead of atomic predicates prompted ddNF to devise a specialized data structure of Ternary Bit Vectors (TBV) instead. However, TBVs are strictly less expressive than BDDs. Moreover, unlike atomic predicates, ddNF's set of PECs is not minimal. We show that ddNF's non-minimality is due to empty PECs. In addition, empty PECs are shown to trigger wrong analysis results. This reveals an inherent tension between precision, expressiveness and performance in formal network verification. Our paper resolves this tension through a new lattice-theoretical PEC-construction algorithm, #PEC, that advances the field as follows: (i) #PEC can encode more kinds of forwarding rules (e.g., ip-tables) than ddNF and Veriflow, (ii) #PEC verifies a wider class of errors (e.g., shadowed rules) than ddNF, and (iii) on a broad range of real-world datasets, #PEC is 10X faster than atomic predicates. By achieving precision, expressiveness and performance, this paper answers a longstanding quest that has spanned three generations of formal network analysis techniques.
Augmented Unlocking Techniques for Smartphones Using Pre-Touch Information
Venue: arXiv cs.CR 2019
Year: 2019

Smartphones store a significant amount of personal and private information, and are playing an increasingly important role in people's lives. It is important for authentication techniques to be more resistant against two known attacks called shoulder surfing and smudge attacks. In this work, we propose a new technique called 3D Pattern. Our 3D Pattern technique takes advantage of a new input paradigm called pre-touch, which could soon allow smartphones to sense a user's finger position at some distance from the screen. We implement the technique and evaluate it in a pilot study (n=6) by comparing it to PIN and pattern locks. Our results show that although our prototype takes about 8 seconds to authenticate, it is immune to smudge attacks and promises to be more resistant to shoulder surfing.
Demystifying the MLPerf Benchmark Suite
Venue: arXiv cs.LG 2019
Year: 2019

MLPerf, an emerging machine learning benchmark suite strives to cover a broad range of applications of machine learning. We present a study on its characteristics and how the MLPerf benchmarks differ from some of the previous deep learning benchmarks like DAWNBench and DeepBench. We find that application benchmarks such as MLPerf (although rich in kernels) exhibit different features compared to kernel benchmarks such as DeepBench. MLPerf benchmark suite contains a diverse set of models which allows unveiling various bottlenecks in the system. Based on our findings, dedicated low latency interconnect between GPUs in multi-GPU systems is required for optimal distributed deep learning training. We also observe variation in scaling efficiency across the MLPerf models. The variation exhibited by the different models highlight the importance of smart scheduling strategies for multi-GPU training. Another observation is that CPU utilization increases with increase in number of GPUs used for training. Corroborating prior work we also observe and quantify improvements possible by compiler optimizations, mixed-precision training and use of Tensor Cores.
EPP: interpretable score of model predictive power
Venue: arXiv cs.LG 2019
Year: 2019

The most important part of model selection and hyperparameter tuning is the evaluation of model performance. The most popular measures, such as AUC, F1, ACC for binary classification, or RMSE, MAD for regression, or cross-entropy for multilabel classification share two common weaknesses. First is, that they are not on an interval scale. It means that the difference in performance for the two models has no direct interpretation. It makes no sense to compare such differences between datasets. Second is, that for k-fold cross-validation, the model performance is in most cases calculated as an average performance from particular folds, which neglects the information how stable is the performance for different folds. In this talk, we introduce a new EPP rating system for predictive models. We also demonstrate numerous advantages for this system, First, differences in EPP scores have probabilistic interpretation. Based on it we can assess the probability that one model will achieve better performance than another. Second, EPP scores can be directly compared between datasets. Third, they can be used for navigated hyperparameter tuning and model selection. Forth, we can create embeddings for datasets based on EPP scores.
A Planning Framework for Persistent, Multi-UAV Coverage with Global Deconfliction
Venue: arXiv cs.RO 2019
Year: 2019

Planning for multi-robot coverage seeks to determine collision-free paths for a fleet of robots, enabling them to collectively observe points of interest in an environment. Persistent coverage is a variant of traditional coverage where coverage-levels in the environment decay over time. Thus, robots have to continuously revisit parts of the environment to maintain a desired coverage-level. Facilitating this in the real world demands we tackle numerous subproblems. While there exist standard solutions to these subproblems, there is no complete framework that addresses all of their individual challenges as a whole in a practical setting. We adapt and combine these solutions to present a planning framework for persistent coverage with multiple unmanned aerial vehicles (UAVs). Specifically, we run a continuous loop of goal assignment and globally deconflicting, kinodynamic path planning for multiple UAVs. We evaluate our framework in simulation as well as the real world. In particular, we demonstrate that (i) our framework exhibits graceful coverage given sufficient resources, we maintain persistent coverage; if resources are insufficient (e.g., having too few UAVs for a given size of the enviornment), coverage-levels decay slowly and (ii) planning with global deconfliction in our framework incurs a negligibly higher price compared to other weaker, more local collision-checking schemes. (Video: https://youtu.be/aqDs6Wymp5Q)
Fine-Grained Complexity of k-OPT in Bounded-Degree Graphs for Solving TSP
Venue: arXiv cs.DS 2019
Year: 2019

Local search is a widely-employed strategy for finding good solutions to Traveling Salesman Problem. We analyze the problem of determining whether the weight of a given cycle can be decreased by a popular $k$-opt move. Earlier work has shown that (i) assuming the Exponential Time Hypothesis, there is no algorithm to find an improving $k$-opt move in time $f(k)n^{o(k/\log k)}$ for any function $f$, while (ii) it is possible to improve on the brute-force running time of $O(n^k)$ and save linear factors in the exponent. Modern TSP heuristics show that very good global solutions can already be reached using only the top-$O(1)$ most promising edges incident to each vertex. Motivated by this, we study the problem of finding an improving $k$-move in bounded degree graphs, presenting new algorithms and conditional lower bounds. We show that the aforementioned ETH lower bound also holds for graphs of maximum degree three, but that in bounded-degree graphs the best improving $k$-move can be found in time $O(n^{23k/135+o(k)})$. This improves upon the best-known bounds for general graphs. Due to its practical importance, we devote special attention to the range of $k$ in which improving $k$-moves in bounded-degree graphs can be found in quasi-linear time. For $k\le 7$, we give quasi-linear time algorithms for general weights. For $k=8$ we obtain a quasi-linear time algorithm for polylogarithmic weights. On the other hand, based on established fine-grained complexity hypotheses, we prove that the $k=9$ case does not admit quasi-linear time algorithms. Hence we fully characterize the values of $k$ for which quasi-linear time algorithms exist for polylogarithmic weights on bounded-degree graphs. As a byproduct, we show a new bound on pathwidth of even graphs which results in improved running time bounds for counting $k$-vertex paths and cycles.
Proximity-based equivalence classes in fuzzy relational database model
Venue: arXiv cs.DB 2019
Year: 2019

One of the first attempts to set a solid theoretical foundation for extending the content of relational databases with incomplete information was the fuzzy relational model by Buckles and Petry. This structure was based on two generalizations of the traditional relational model: (1) A tuple component can be any subset of the corresponding domain, rather than a single element and (2) A similarity relation is defined on each domain. This relation satisfies the properties of reflexivity, symmetry and max-min transitivity, thus having the equality relation as a special case. This generalization keeps two key properties of the relational model - that no two different tuples represent the same information and that the application of any operation of the relation algebra has a unique result. Shenoi and Melton generalized this model and showed how the existence of equivalence classes over the attribute domains can also be preserved with a relation that only satisfies the properties of reflexivity and symmetry (proximity relation). The motivation for this generalization is the strictness of the max-min transitivity property of similarity relations, which complicates the construction of this relation for some domain types. An important characteristic of the Shenoi-Melton model is the dependence of the equivalence classes upon the current content of the database. This characteristic, together with the way the equivalence relation is constructed by the proximity relation, can lead to the equivalence classes that don't correspond well with some database query types. Here we will present a different way of forming the equivalence classes over the attribute domains in fuzzy relational databases in which they depend only on the attribute domain and not on the current database state. We will also show a simple method for automatic construction of proximity relations over some domain types.
Collaborative Computation Offloading in Wireless Powered Mobile-Edge Computing Systems
Venue: arXiv cs.NI 2019
Year: 2019

This paper studies a novel user cooperation model in a wireless powered mobile edge computing system where two wireless users harvest wireless power transferred by one energy node and can offload part of their computation tasks to an edge server (ES) for remote execution. In particular, we consider that the direct communication link between one user to the ES is blocked, such that the other user acts as a relay to forward its offloading data to the server. Meanwhile, instead of forwarding all the received task data, we also allow the helping user to compute part of the received task locally to reduce the potentially high energy and time cost on task offloading to the ES. Our aim is to maximize the amount of data that can be processed within a given time frame of the two users by jointly optimizing the amount of task data computed at each device (users and ES), the system time allocation, the transmit power and CPU frequency of the users. We propose an efficient method to find the optimal solution and show that the proposed user cooperation can effectively enhance the computation performance of the system compared to other representative benchmark methods under different scenarios.
On Measuring and Mitigating Biased Inferences of Word Embeddings
Venue: arXiv cs.CL 2019
Year: 2019

Word embeddings carry stereotypical connotations from the text they are trained on, which can lead to invalid inferences in downstream models that rely on them. We use this observation to design a mechanism for measuring stereotypes using the task of natural language inference. We demonstrate a reduction in invalid inferences via bias mitigation strategies on static word embeddings (GloVe). Further, we show that for gender bias, these techniques extend to contextualized embeddings when applied selectively only to the static components of contextualized embeddings (ELMo, BERT).
Theoretical Issues in Deep Networks: Approximation, Optimization and Generalization
Venue: arXiv cs.LG 2019
Year: 2019

While deep learning is successful in a number of applications, it is not yet well understood theoretically. A satisfactory theoretical characterization of deep learning however, is beginning to emerge. It covers the following questions: 1) representation power of deep networks 2) optimization of the empirical risk 3) generalization properties of gradient descent techniques --- why the expected error does not suffer, despite the absence of explicit regularization, when the networks are overparametrized? In this review we discuss recent advances in the three areas. In approximation theory both shallow and deep networks have been shown to approximate any continuous functions on a bounded domain at the expense of an exponential number of parameters (exponential in the dimensionality of the function). However, for a subset of compositional functions, deep networks of the convolutional type can have a linear dependence on dimensionality, unlike shallow networks. In optimization we discuss the loss landscape for the exponential loss function and show that stochastic gradient descent will find with high probability the global minima. To address the question of generalization for classification tasks, we use classical uniform convergence results to justify minimizing a surrogate exponential-type loss function under a unit norm constraint on the weight matrix at each layer -- since the interesting variables for classification are the weight directions rather than the weights. Our approach, which is supported by several independent new results, offers a solution to the puzzle about generalization performance of deep overparametrized ReLU networks, uncovering the origin of the underlying hidden complexity control.
Reconstructing veriT Proofs in Isabelle/HOL
Venue: arXiv cs.LO 2019
Year: 2019

Automated theorem provers are now commonly used within interactive theorem provers to discharge an increasingly large number of proof obligations. To maintain the trustworthiness of a proof, the automatically found proof must be verified inside the proof assistant. We present here a reconstruction procedure in the proof assistant Isabelle/HOL for proofs generated by the satisfiability modulo theories solver veriT which is part of the smt tactic. We describe in detail the architecture of our improved reconstruction method and the challenges we faced in designing it. Our experiments show that the veriT-powered smt tactic is regularly suggested by Sledgehammer as the fastest method to automatically solve proof goals.
Bluetooth Mesh under the Microscope: How much ICN is Inside?
Venue: arXiv cs.NI 2019
Year: 2019

Bluetooth (BT) mesh is a new mode of BT operation for low-energy devices that offers group-based publish-subscribe as a network service with additional caching capabilities. These features resemble concepts of information-centric networking (ICN), and the analogy to ICN has been repeatedly drawn in the BT community. In this paper, we compare BT mesh with ICN both conceptually and in real-world experiments. We contrast both architectures and their design decisions in detail. Experiments are performed on an IoT testbed using NDN/CCNx and BT mesh on constrained RIOT nodes. Our findings indicate significant differences both in concepts and in real-world performance. Supported by new insights, we identify synergies and sketch a design of a BT-ICN that benefits from both worlds.
Annals of Library and Information Studies. A bibliometric analysis of the journal and a comparison with the top library and information studies journals in Asia and worldwide (2011_2017)
Venue: arXiv cs.DL 2019
Year: 2019

This paper presents a thorough bibliometric analysis of research published in Annals of Library and Information Studies (ALIS), an India-based journal, for the period 2011_2017. Specifically, it compares this journal's trends with those of other library and information science (LIS) journals from the same geographical area (India, and Asia as a whole) and with the 10 highest-rated LIS journals worldwide. The source of the data used was the multidisciplinary database Scopus. To perform this comparison, ALIS' production was analyzed in order to identify authorship patterns; for example, authors' countries of residence, co-authorship trends, and collaboration networks. Research topics were identified through keyword analysis, while performance was measured by examining the number of citations articles received. This study provides substantial information. The research lines detected through examining the keywords in ALIS articles were determined to be similar to those for the top LIS journals in both Asia and worldwide. Specifically, ALIS authors are focusing on metrics, bibliometrics, and social networking, which follows global trends. Notably, however, collaboration among Asia-based journals was found to be lower than that in the top-indexed journals in the LIS field. The results obtained present a roadmap for expanding the research in this field.
Embarrassingly Simple Binary Representation Learning
Venue: arXiv cs.CV 2019
Year: 2019

Recent binary representation learning models usually require sophisticated binary optimization, similarity measure or even generative models as auxiliaries. However, one may wonder whether these non-trivial components are needed to formulate practical and effective hashing models. In this paper, we answer the above question by proposing an embarrassingly simple approach to binary representation learning. With a simple classification objective, our model only incorporates two additional fully-connected layers onto the top of an arbitrary backbone network, whilst complying with the binary constraints during training. The proposed model lower-bounds the Information Bottleneck (IB) between data samples and their semantics, and can be related to many recent `learning to hash' paradigms. We show that, when properly designed, even such a simple network can generate effective binary codes, by fully exploring data semantics without any held-out alternating updating steps or auxiliary models. Experiments are conducted on conventional large-scale benchmarks, i.e., CIFAR-10, NUS-WIDE, and ImageNet, where the proposed simple model outperforms the state-of-the-art methods.
A Methodology to Select Topology Generators for WANET Simulations (Extended Version)
Venue: arXiv cs.NI 2019
Year: 2019

Many academic and industrial research works on WANETs rely on simulations, at least in the first stages, to obtain preliminary results to be subsequently validated in real settings. Topology generators (TG) are commonly used to generate the initial placement of nodes in artificial WANET topologies, where those simulations take place. The significance of these experiments heavily depends on the representativeness of artificial topologies. Indeed, if they were not drawn fairly, obtained results would apply only to a subset of possible configurations, hence they would lack of the appropriate generality required to port them to the real world. Although using many TGs could mitigate this issue by generating topologies in several different ways, that would entail a significant additional effort. Hence, the problem arises of what TGs to choose, among a number of available generators, to maximise the representativeness of generated topologies and reduce the number of TGs to use. In this paper, we address that problem by investigating the presence of bias in the initial placement of nodes in artificial WANET topologies produced by different TGs. We propose a methodology to assess such bias and introduce two metrics to quantify the diversity of the topologies generated by a TG with respect to all the available TGs, which can be used to select what TGs to use. We carry out experiments on three well-known TGs, namely BRITE, NPART and GT-ITM. Obtained results show that using the artificial networks produced by a single TG can introduce bias.
Measuring Patent Claim Generation by Span Relevancy
Venue: arXiv cs.CL 2019
Year: 2019

Our goal of patent claim generation is to realize "augmented inventing" for inventors by leveraging latest Deep Learning techniques. We envision the possibility of building an "auto-complete" function for inventors to conceive better inventions in the era of artificial intelligence. In order to generate patent claims with good quality, a fundamental question is how to measure it. We tackle the problem from a perspective of claim span relevancy. Patent claim language was rarely explored in the NLP field. It is unique in its own way and contains rich explicit and implicit human annotations. In this work, we propose a span-based approach and a generic framework to measure patent claim generation quantitatively. In order to study the effectiveness of patent claim generation, we define a metric to measure whether two consecutive spans in a generated patent claims are relevant. We treat such relevancy measurement as a span-pair classification problem, following the concept of natural language inference. Technically, the span-pair classifier is implemented by fine-tuning a pre-trained language model. The patent claim generation is implemented by fine-tuning the other pre-trained model. Specifically, we fine-tune a pre-trained Google BERT model to measure the patent claim spans generated by a fine-tuned OpenAI GPT-2 model. In this way, we re-use two of the state-of-the-art pre-trained models in the NLP field. Our result shows the effectiveness of the span-pair classifier after fine-tuning the pre-trained model. It further validates the quantitative metric of span relevancy in patent claim generation. Particularly, we found that the span relevancy ratio measured by BERT becomes lower when the diversity in GPT-2 text generation becomes higher.
SliderGAN: Synthesizing Expressive Face Images by Sliding 3D Blendshape Parameters
Venue: arXiv cs.CV 2019
Year: 2019

Image-to-image (i2i) translation is the dense regression problem of learning how to transform an input image into an output using aligned image pairs. Remarkable progress has been made in i2i translation with the advent of Deep Convolutional Neural Networks (DCNNs) and particular using the learning paradigm of Generative Adversarial Networks (GANs). In the absence of paired images, i2i translation is tackled with one or multiple domain transformations (i.e., CycleGAN, StarGAN etc.). In this paper, we study a new problem, that of image-to-image translation, under a set of continuous parameters that correspond to a model describing a physical process. In particular, we propose the SliderGAN which transforms an input face image into a new one according to the continuous values of a statistical blendshape model of facial motion. We show that it is possible to edit a facial image according to expression and speech blendshapes, using sliders that control the continuous values of the blendshape model. This provides much more flexibility in various tasks, including but not limited to face editing, expression transfer and face neutralisation, comparing to models based on discrete expressions or action units.