OpenRaiser/Intern-Atlas huggingface dataset:
To Memory Safety through Proofs
Venue: arXiv cs.PL 2018
Year: 2018

We present a type system capable of guaranteeing the memory safety of programs that may involve (sophisticated) pointer manipulation such as pointer arithmetic. With its root in a recently developed framework Applied Type System (ATS), the type system imposes a level of abstraction on program states through a novel notion of recursive stateful views and then relies on a form of linear logic to reason about such stateful views. We consider the design and then the formalization of the type system to constitute the primary contribution of the paper. In addition, we also mention a running implementation of the type system and then give some examples in support of the practicality of programming with recursive stateful views.
Long-term area coverage and radio relay positioning using swarms of UAVs
Venue: arXiv cs.RO 2018
Year: 2018

Unmanned Aerial Vehicles (UAVs) are becoming increasingly useful for tasks which require the acquisition of data over large areas. The coverage problem, i.e., the problem of periodically visiting all subregions of an area at a desired frequency, is especially interesting because of its practical applications, both in industry and long-term monitoring of areas hit by a natural disaster. We focus here on the latter scenario, and take into consideration its peculiar characteristic, i.e. the a coverage system should be resilient to a changing environment and not be dependent on pre-existing infrastructures for communication. To this purpose, we designed a novel algorithm for online area coverage and simultaneous signal relay that allows a UAV to cover an area freely, while a variable number of other UAVs provide a stable communication with the base and support in the coverage process at the same time. Finally, a test architecture based on the algorithm has been developed and tests have been performed. By comparison with a simple relay chain system, our approach employs up to 64% less time to reach a certain goal of coverage iterations over the map with only 17% worse average communication cost and no impact on the worst case communication cost.
Trace Abstraction Modulo Probability
Venue: arXiv cs.PL 2018
Year: 2018

We propose trace abstraction modulo probability, a proof technique for verifying high-probability accuracy guarantees of probabilistic programs. Our proofs overapproximate the set of program traces using failure automata, finite-state automata that upper bound the probability of failing to satisfy a target specification. We automate proof construction by reducing probabilistic reasoning to logical reasoning: we use program synthesis methods to select axioms for sampling instructions, and then apply Craig interpolation to prove that traces fail the target specification with only a small probability. Our method handles programs with unknown inputs, parameterized distributions, infinite state spaces, and parameterized specifications. We evaluate our technique on a range of randomized algorithms drawn from the differential privacy literature and beyond. To our knowledge, our approach is the first to automatically establish accuracy properties of these algorithms.
DARKMENTION: A Deployed System to Predict Enterprise-Targeted External Cyberattacks
Venue: arXiv cs.CR 2018
Year: 2018

Recent incidents of data breaches call for organizations to proactively identify cyber attacks on their systems. Darkweb/Deepweb (D2web) forums and marketplaces provide environments where hackers anonymously discuss existing vulnerabilities and commercialize malicious software to exploit those vulnerabilities. These platforms offer security practitioners a threat intelligence environment that allows to mine for patterns related to organization-targeted cyber attacks. In this paper, we describe a system (called DARKMENTION) that learns association rules correlating indicators of attacks from D2web to real-world cyber incidents. Using the learned rules, DARKMENTION generates and submits warnings to a Security Operations Center (SOC) prior to attacks. Our goal was to design a system that automatically generates enterprise-targeted warnings that are timely, actionable, accurate, and transparent. We show that DARKMENTION meets our goal. In particular, we show that it outperforms baseline systems that attempt to generate warnings of cyber attacks related to two enterprises with an average increase in F1 score of about 45% and 57%. Additionally, DARKMENTION was deployed as part of a larger system that is built under a contract with the IARPA Cyber-attack Automated Unconventional Sensor Environment (CAUSE) program. It is actively producing warnings that precede attacks by an average of 3 days.
Machine Translation between Vietnamese and English: an Empirical Study
Venue: arXiv cs.CL 2018
Year: 2018

Machine translation is shifting to an end-to-end approach based on deep neural networks. The state of the art achieves impressive results for popular language pairs such as English - French or English - Chinese. However for English - Vietnamese the shortage of parallel corpora and expensive hyper-parameter search present practical challenges to neural-based approaches. This paper highlights our efforts on improving English-Vietnamese translations in two directions: (1) Building the largest open Vietnamese - English corpus to date, and (2) Extensive experiments with the latest neural models to achieve the highest BLEU scores. Our experiments provide practical examples of effectively employing different neural machine translation models with low-resource language pairs.
Exploring Neural Methods for Parsing Discourse Representation Structures
Venue: arXiv cs.CL 2018
Year: 2018

Neural methods have had several recent successes in semantic parsing, though they have yet to face the challenge of producing meaning representations based on formal semantics. We present a sequence-to-sequence neural semantic parser that is able to produce Discourse Representation Structures (DRSs) for English sentences with high accuracy, outperforming traditional DRS parsers. To facilitate the learning of the output, we represent DRSs as a sequence of flat clauses and introduce a method to verify that produced DRSs are well-formed and interpretable. We compare models using characters and words as input and see (somewhat surprisingly) that the former performs better than the latter. We show that eliminating variable names from the output using De Bruijn-indices increases parser performance. Adding silver training data boosts performance even further.
Dynamic Type Inference for Gradual Hindley--Milner Typing
Venue: arXiv cs.PL 2018
Year: 2018

Garcia and Cimini study a type inference problem for the ITGL, an implicitly and gradually typed language with let-polymorphism, and develop a sound and complete inference algorithm for it. Soundness and completeness mean that, if the algorithm succeeds, the input term can be translated to a well-typed term of an explicitly typed blame calculus by cast insertion and vice versa. However, in general, there are many possible translations depending on how type variables that were left undecided by static type inference are instantiated with concrete static types. Worse, the translated terms may behave differently---some evaluate to values but others raise blame. In this paper, we propose and formalize a new blame calculus $λ^{\textsf{DTI}}_{\textsf{B}}$ that avoids such divergence as an intermediate language for the ITGL. A main idea is to allow a term to contain type variables (that have not been instantiated during static type inference) and defer instantiation of these type variables to run time. We introduce dynamic type inference (DTI) into the semantics of $λ^{\textsf{DTI}}_{\textsf{B}}$ so that type variables are instantiated along reduction. The DTI-based semantics not only avoids the divergence described above but also is sound and complete with respect to the semantics of fully instantiated terms in the following sense: if the evaluation of a term succeeds (i.e., terminates with a value) in the DTI-based semantics, then there is a fully instantiated version of the term that also succeeds in the explicitly typed blame calculus and vice versa. Finally, we prove the gradual guarantee, which is an important correctness criterion of a gradually typed language, for the ITGL.
Unsupervised Neural Machine Translation Initialized by Unsupervised Statistical Machine Translation
Venue: arXiv cs.CL 2018
Year: 2018

Recent work achieved remarkable results in training neural machine translation (NMT) systems in a fully unsupervised way, with new and dedicated architectures that rely on monolingual corpora only. In this work, we propose to define unsupervised NMT (UNMT) as NMT trained with the supervision of synthetic bilingual data. Our approach straightforwardly enables the use of state-of-the-art architectures proposed for supervised NMT by replacing human-made bilingual data with synthetic bilingual data for training. We propose to initialize the training of UNMT with synthetic bilingual data generated by unsupervised statistical machine translation (USMT). The UNMT system is then incrementally improved using back-translation. Our preliminary experiments show that our approach achieves a new state-of-the-art for unsupervised machine translation on the WMT16 German--English news translation task, for both translation directions.
Feature Trajectory Dynamic Time Warping for Clustering of Speech Segments
Venue: arXiv cs.SD 2018
Year: 2018

Dynamic time warping (DTW) can be used to compute the similarity between two sequences of generally differing length. We propose a modification to DTW that performs individual and independent pairwise alignment of feature trajectories. The modified technique, termed feature trajectory dynamic time warping (FTDTW), is applied as a similarity measure in the agglomerative hierarchical clustering of speech segments. Experiments using MFCC and PLP parametrisations extracted from TIMIT and from the Spoken Arabic Digit Dataset (SADD) show consistent and statistically significant improvements in the quality of the resulting clusters in terms of F-measure and normalised mutual information (NMI).
An assessment of the first "scientific accreditation" for university appointments in Italy
Venue: arXiv cs.DL 2018
Year: 2018

Nations with non-competitive higher education systems and with high levels of corruption, are more exposed to phenomena of discrimination and favoritism in faculty recruitment. Italy is a case in point, as shown by empirical studies, judicial reports and media attention. Governments have intervened repeatedly to reduce the problem, with scarce success. The 2010 reforms to the university recruitment system provided that access to the ranks of associate and full professor would now be possible only through an initial "scientific habilitation" to be awarded by sectorial committees of national experts. The objective of this work is to analyze the relationship of the recent habilitation procedure outcomes to the actual scientific merit of the various candidates, as well as to other variables that are explicative of possible practices of favoritism and discrimination. The analyses identify the presence of potential cases of discrimination and favoritism.
Visual Re-ranking with Natural Language Understanding for Text Spotting
Venue: arXiv cs.CV 2018
Year: 2018

Many scene text recognition approaches are based on purely visual information and ignore the semantic relation between scene and text. In this paper, we tackle this problem from natural language processing perspective to fill the gap between language and vision. We propose a post-processing approach to improve scene text recognition accuracy by using occurrence probabilities of words (unigram language model), and the semantic correlation between scene and text. For this, we initially rely on an off-the-shelf deep neural network, already trained with a large amount of data, which provides a series of text hypotheses per input image. These hypotheses are then re-ranked using word frequencies and semantic relatedness with objects or scenes in the image. As a result of this combination, the performance of the original network is boosted with almost no additional cost. We validate our approach on ICDAR'17 dataset.
Informed Democracy: Voting-based Novelty Detection for Action Recognition
Venue: arXiv cs.CV 2018
Year: 2018

Novelty detection is crucial for real-life applications. While it is common in activity recognition to assume a closed-set setting, i.e. test samples are always of training categories, this assumption is impractical in a real-world scenario. Test samples can be of various categories including those never seen before during training. Thus, being able to know what we know and what we do not know is decisive for the model to avoid what can be catastrophic consequences. We present in this work a novel approach for identifying samples of activity classes that are not previously seen by the classifier. Our model employs a voting-based scheme that leverages the estimated uncertainty of the individual classifiers in their predictions to measure the novelty of a new input sample. Furthermore, the voting is privileged to a subset of informed classifiers that can best estimate whether a sample is novel or not when it is classified to a certain known category. In a thorough evaluation on UCF-101 and HMDB-51, we show that our model consistently outperforms state-of-the-art in novelty detection. Additionally, by combining our model with off-the-shelf zero-shot learning (ZSL) approaches, our model leads to a significant improvement in action classification accuracy for the generalized ZSL setting.
DeepTwist: Learning Model Compression via Occasional Weight Distortion
Venue: arXiv cs.LG 2018
Year: 2018

Model compression has been introduced to reduce the required hardware resources while maintaining the model accuracy. Lots of techniques for model compression, such as pruning, quantization, and low-rank approximation, have been suggested along with different inference implementation characteristics. Adopting model compression is, however, still challenging because the design complexity of model compression is rapidly increasing due to additional hyper-parameters and computation overhead in order to achieve a high compression ratio. In this paper, we propose a simple and efficient model compression framework called DeepTwist which distorts weights in an occasional manner without modifying the underlying training algorithms. The ideas of designing weight distortion functions are intuitive and straightforward given formats of compressed weights. We show that our proposed framework improves compression rate significantly for pruning, quantization, and low-rank approximation techniques while the efforts of additional retraining and/or hyper-parameter search are highly reduced. Regularization effects of DeepTwist are also reported.
Coresets for $k$-Means and $k$-Median Clustering and their Applications
Venue: arXiv cs.CG 2018
Year: 2018

$\renewcommand{\Re}{{\rm I\!\hspace{-0.025em} R}} \newcommand{\eps}{\varepsilon} \newcommand{\Coreset}{\mathcal{S}} $ In this paper, we show the existence of small coresets for the problems of computing $k$-median and $k$-means clustering for points in low dimension. In other words, we show that given a point set $P$ in $\Re^d$, one can compute a weighted set $\Coreset \subseteq P$, of size $O(k \eps^{-d} \log{n})$, such that one can compute the $k$-median/means clustering on $\Coreset$ instead of on $P$, and get an $(1+\eps)$-approximation. As a result, we improve the fastest known algorithms for $(1+\eps)$-approximate $k$-means and $k$-median clustering. Our algorithms have linear running time for a fixed $k$ and $\eps$. In addition, we can maintain the $(1+\eps)$-approximate $k$-median or $k$-means clustering of a stream when points are being only inserted, using polylogarithmic space and update time.
General audio tagging with ensembling convolutional neural network and statistical features
Venue: arXiv cs.CV 2018
Year: 2018

Audio tagging aims to infer descriptive labels from audio clips. Audio tagging is challenging due to the limited size of data and noisy labels. In this paper, we describe our solution for the DCASE 2018 Task 2 general audio tagging challenge. The contributions of our solution include: We investigated a variety of convolutional neural network architectures to solve the audio tagging task. Statistical features are applied to capture statistical patterns of audio features to improve the classification performance. Ensemble learning is applied to ensemble the outputs from the deep classifiers to utilize complementary information. a sample re-weight strategy is employed for ensemble training to address the noisy label problem. Our system achieves a mean average precision (mAP@3) of 0.958, outperforming the baseline system of 0.704. Our system ranked the 1st and 4th out of 558 submissions in the public and private leaderboard of DCASE 2018 Task 2 challenge. Our codes are available at https://github.com/Cocoxili/DCASE2018Task2/.
The suitability of h and g indexes for measuring the research performance of institutions. Scientometrics, 97(3), 555-570
Venue: arXiv cs.DL 2018
Year: 2018

It is becoming ever more common to use bibliometric indicators to evaluate the performance of research institutions, however there is often a failure to recognize the limits and drawbacks of such indicators. Since performance measurement is aimed at supporting critical decisions by research administrators and policy makers, it is essential to carry out empirical testing of the robustness of the indicators used. In this work we examine the accuracy of the popular "h" and "g" indexes for measuring university research performance by comparing the ranking lists derived from their application to the ranking list from a third indicator that better meets the requirements for robust and reliable assessment of institutional productivity. The test population is all Italian universities in the hard sciences, observed over the period 2001-2005. The analysis quantifies the correlations between the three university rankings (by discipline) and the shifts that occur under changing indicators, to measure the distortion inherent in use of the h and g indexes and their comparative accuracy for assessing institutions.
Data Poisoning Attack against Unsupervised Node Embedding Methods
Venue: arXiv cs.LG 2018
Year: 2018

Unsupervised node embedding methods (e.g., DeepWalk, LINE, and node2vec) have attracted growing interests given their simplicity and effectiveness. However, although these methods have been proved effective in a variety of applications, none of the existing work has analyzed the robustness of them. This could be very risky if these methods are attacked by an adversarial party. In this paper, we take the task of link prediction as an example, which is one of the most fundamental problems for graph analysis, and introduce a data positioning attack to node embedding methods. We give a complete characterization of attacker's utilities and present efficient solutions to adversarial attacks for two popular node embedding methods: DeepWalk and LINE. We evaluate our proposed attack model on multiple real-world graphs. Experimental results show that our proposed model can significantly affect the results of link prediction by slightly changing the graph structures (e.g., adding or removing a few edges). We also show that our proposed model is very general and can be transferable across different embedding methods. Finally, we conduct a case study on a coauthor network to better understand our attack method.
Limited Visibility and Uncertainty Aware Motion Planning for Automated Driving
Venue: arXiv cs.RO 2018
Year: 2018

Adverse weather conditions and occlusions in urban environments result in impaired perception. The uncertainties are handled in different modules of an automated vehicle, ranging from sensor level over situation prediction until motion planning. This paper focuses on motion planning given an uncertain environment model with occlusions. We present a method to remain collision free for the worst-case evolution of the given scene. We define criteria that measure the available margins to a collision while considering visibility and interactions, and consequently integrate conditions that apply these criteria into an optimization-based motion planner. We show the generality of our method by validating it in several distinct urban scenarios.
Birds of a Feather Flock Together? A Study of Developers' Flocking and Migration Behavior in GitHub and Stack Overflow
Venue: arXiv cs.SI 2018
Year: 2018

Interactions between individuals and their participation in community activities are governed by how individuals identify themselves with their peers. We want to investigate such behavior for developers while they are learning and contributing on socially collaborative environments, specifically code hosting sites and question/answer sites. In this study, we investigate the following questions about advocates, developers who can be identified as well-rounded community contributors and active learners. Do advocates flock together in a community? How do flocks of advocates migrate within a community? Do these flocks of advocates migrate beyond a single community? To understand such behavior, we collected 12,578 common advocates across a code hosting site - GitHub and a question/answering site - Stack Overflow. These advocates were involved in 1,549 projects on GitHub and were actively asking 114,569 questions and responding 408,858 answers and 1,001,125 comments on Stack Overflow. We performed an in-depth empirical analysis using social networks to find the flocks of advocates and their migratory pattern on GitHub, Stack Overflow, and across both communities. We found that 7.5% of the advocates create flocks on GitHub and 8.7% on Stack Overflow. Further, these flocks of advocates migrate on an average of 5 times on GitHub and 2 times on Stack Overflow. In particular, advocates in flocks of two migrate more frequently than larger flocks. However, this migration behavior was only common within a single community. Our findings indicate that advocates' flocking and migration behavior differs substantially from the ones found in other social environments. This suggests a need to investigate the factors that demotivate the flocking and migration behavior of advocates and ways to enhance and integrate support for such behavior in collaborative software tools.
Compression Performance of Grayscale-based Image Encryption for Encryption-then-Compression Systems
Venue: arXiv cs.CR 2018
Year: 2018

This paper considers a new grayscale-based image encryption for Encryption-then-Compression (EtC) systems with JPEG compression. Firstly, generation methods of grayscale-based images are discussed in terms of the selection of color space. In addition, a new JPEG quantization table for the grayscale-based images is proposed to provide a better compression performance. Moreover, the quality of both images uploaded to Social Network Services (SNS) and downloaded from SNS, are discussed and evaluated. In the experiments, encrypted images are compressed using various compression parameters and quantization tables, and uploaded to Twitter and Facebook. The results proved that the selection of color space and the proposed quantization table can improve the compression performances of not only uploaded images but also downloaded ones.