OpenRaiser/Intern-Atlas huggingface dataset:
The Densest k Subgraph Problem in b-Outerplanar Graphs
Venue: arXiv cs.DS 2019
Year: 2019

We give an exact $O(nk^2)$ algorithm for finding the densest k subgraph in outerplanar graphs. We extend this to an exact $O(nk^2 8^b)$ algorithm for finding the densest k subgraph in b-outerplanar graphs. Finally, we hypothesize that Baker's PTAS technique will not work for the densest k subgraph problem in planar graphs.
Annotary: A Concolic Execution System for Developing Secure Smart Contracts
Venue: arXiv cs.CR 2019
Year: 2019

Ethereum smart contracts are executable programs, deployed on a peer-to-peer network and executed in a consensus-based fashion. Their bytecode is public, immutable and once deployed to the blockchain, cannot be patched anymore. As smart contracts may hold Ether worth of several million dollars, they are attractive targets for attackers and indeed some contracts have successfully been exploited in the recent past, resulting in tremendous financial losses. The correctness of smart contracts is thus of utmost importance. While first approaches on formal verification exist, they demand users to be well-versed in formal methods which are alien to many developers and are only able to analyze individual contracts, without considering their execution environment, i.e., calls to external contracts, sequences of transaction, and values from the actual blockchain storage. In this paper, we present Annotary, a concolic execution framework to analyze smart contracts for vulnerabilities, supported by annotations which developers write directly in the Solidity source code. In contrast to existing work, Annotary supports analysis of inter-transactional, inter-contract control flows and combines symbolic execution of EVM bytecode with a resolution of concrete values from the public Ethereum blockchain. While the analysis of Annotary tends to weight precision higher than soundness, we analyze inter-transactional call chains to eliminate false positives from unreachable states that traditional symbolic execution would not be able to handle. We present the annotation and analysis concepts of Annotary, explain its implementation on top of the Laser symbolic virtual machine, and demonstrate its usage as a plugin for the Sublime Text editor.
Deep Active Inference as Variational Policy Gradients
Venue: arXiv cs.LG 2019
Year: 2019

Active Inference is a theory of action arising from neuroscience which casts action and planning as a bayesian inference problem to be solved by minimizing a single quantity - the variational free energy. Active Inference promises a unifying account of action and perception coupled with a biologically plausible process theory. Despite these potential advantages, current implementations of Active Inference can only handle small, discrete policy and state-spaces and typically require the environmental dynamics to be known. In this paper we propose a novel deep Active Inference algorithm which approximates key densities using deep neural networks as flexible function approximators, which enables Active Inference to scale to significantly larger and more complex tasks. We demonstrate our approach on a suite of OpenAIGym benchmark tasks and obtain performance comparable with common reinforcement learning baselines. Moreover, our algorithm shows similarities with maximum entropy reinforcement learning and the policy gradients algorithm, which reveals interesting connections between the Active Inference framework and reinforcement learning.
Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts
Venue: arXiv cs.SE 2019
Year: 2019

An effective way to maximize code coverage in software tests is through dynamic symbolic execution$-$a technique that uses constraint solving to systematically explore a program's state space. We introduce an open-source dynamic symbolic execution framework called Manticore for analyzing binaries and Ethereum smart contracts. Manticore's flexible architecture allows it to support both traditional and exotic execution environments, and its API allows users to customize their analysis. Here, we discuss Manticore's architecture and demonstrate the capabilities we have used to find bugs and verify the correctness of code for our commercial clients.
Secure IoT access at scale using blockchains and smart contracts
Venue: arXiv cs.CR 2019
Year: 2019

Blockchains and smart contracts are an emerging, promising technology, that has received considerable attention. We use the blockchain technology, and in particular Ethereum, to implement a large-scale event-based Internet of Things (IoT) control system. We argue that the distributed nature of the "ledger," as well as, Ethereum's capability of parallel execution of replicated "smart contracts", provide the sought after automation, generality, flexibility, resilience, and high availability. We design a realistic blockchain-based IoT architecture, using existing technologies while by taking into consideration the characteristics and limitations of IoT devices and applications. Furthermore, we leverage blockchain's immutability and Ethereum's support for custom tokens to build a robust and efficient token-based access control mechanism. Our evaluation shows that our solution is viable and offers significant security and usability advantages.
Hahahahaha, Duuuuude, Yeeessss!: A two-parameter characterization of stretchable words and the dynamics of mistypings and misspellings
Venue: arXiv cs.CL 2019
Year: 2019

Stretched words like `heellllp' or `heyyyyy' are a regular feature of spoken language, often used to emphasize or exaggerate the underlying meaning of the root word. While stretched words are rarely found in formal written language and dictionaries, they are prevalent within social media. In this paper, we examine the frequency distributions of `stretchable words' found in roughly 100 billion tweets authored over an 8 year period. We introduce two central parameters, `balance' and `stretch', that capture their main characteristics, and explore their dynamics by creating visual tools we call `balance plots' and `spelling trees'. We discuss how the tools and methods we develop here could be used to study the statistical patterns of mistypings and misspellings, along with the potential applications in augmenting dictionaries, improving language processing, and in any area where sequence construction matters, such as genetics.
NTT's Machine Translation Systems for WMT19 Robustness Task
Venue: arXiv cs.CL 2019
Year: 2019

This paper describes NTT's submission to the WMT19 robustness task. This task mainly focuses on translating noisy text (e.g., posts on Twitter), which presents different difficulties from typical translation tasks such as news. Our submission combined techniques including utilization of a synthetic corpus, domain adaptation, and a placeholder mechanism, which significantly improved over the previous baseline. Experimental results revealed the placeholder mechanism, which temporarily replaces the non-standard tokens including emojis and emoticons with special placeholder tokens during translation, improves translation accuracy even with noisy texts.
Systematic method to evaluate energy dissipation in adiabatic quantum-flux-parametron logic
Venue: arXiv cs.ET 2019
Year: 2019

Adiabatic quantum-flux-parametron (AQFP) logic is an energy-efficient superconductor logic. It operates with zero static power dissipation and very low dynamic power dissipation owing to adiabatic switching. In previous numerical studies, we have evaluated the energy dissipation of basic AQFP logic gates and demonstrated sub-kBT switching energy, where kB is the Boltzmann's constant and T is the temperature, by integrating the product of the excitation current and voltage associated with the gates over time. However, this method is not applicable to complex logic gates, especially those in which the number of inputs is different from the number of outputs. In the present study, we establish a systematic method to evaluate the energy dissipation of general AQFP logic gates. In the proposed method, the energy dissipation is calculated by subtracting the energy dissipation of the peripheral circuits from that of the entire circuit. In this way, the energy change due to the interaction between gates, which makes it difficult to evaluate the energy dissipation, can be deducted. We evaluate the energy dissipation of a majority gate using this method.
Proving Properties of Sorting Programs: A Case Study in Horn Clause Verification
Venue: arXiv cs.LO 2019
Year: 2019

The proof of a program property can be reduced to the proof of satisfiability of a set of constrained Horn clauses (CHCs) which can be automatically generated from the program and the property. In this paper we have conducted a case study in Horn clause verification by considering several sorting programs with the aim of exploring the effectiveness of a transformation technique which allows us to eliminate inductive data structures such as lists or trees. If this technique is successful, we derive a set of CHCs with constraints over the integers and booleans only, and the satisfiability check can often be performed in an effective way by using state-of-the-art CHC solvers, such as Eldarica or Z3. In this case study we have also illustrated the usefulness of a companion technique based on the introduction of the so-called difference predicates, whose definitions correspond to lemmata required during the verification. We have considered functional programs which implement the following kinds of sorting algorithms acting on lists of integers: (i) linearly recursive sorting algorithms, such as insertion sort and selection sort, and (ii) non-linearly recursive sorting algorithms, such as quicksort and mergesort, and we have considered the following properties: (i) the partial correctness properties, that is, the orderedness of the output lists, and the equality of the input and output lists when viewed as multisets, and (ii) some arithmetic properties, such as the equality of the sum of the elements before and after sorting.
UnsuperPoint: End-to-end Unsupervised Interest Point Detector and Descriptor
Venue: arXiv cs.CV 2019
Year: 2019

It is hard to create consistent ground truth data for interest points in natural images, since interest points are hard to define clearly and consistently for a human annotator. This makes interest point detectors non-trivial to build. In this work, we introduce an unsupervised deep learning-based interest point detector and descriptor. Using a self-supervised approach, we utilize a siamese network and a novel loss function that enables interest point scores and positions to be learned automatically. The resulting interest point detector and descriptor is UnsuperPoint. We use regression of point positions to 1) make UnsuperPoint end-to-end trainable and 2) to incorporate non-maximum suppression in the model. Unlike most trainable detectors, it requires no generation of pseudo ground truth points, no structure-from-motion-generated representations and the model is learned from only one round of training. Furthermore, we introduce a novel loss function to regularize network predictions to be uniformly distributed. UnsuperPoint runs in real-time with 323 frames per second (fps) at a resolution of $224\times320$ and 90 fps at $480\times640$. It is comparable or better than state-of-the-art performance when measured for speed, repeatability, localization, matching score and homography estimation on the HPatch dataset.
On the Security and Applicability of Fragile Camera Fingerprints
Venue: arXiv cs.MM 2019
Year: 2019

Camera sensor noise is one of the most reliable device characteristics in digital image forensics, enabling the unique linkage of images to digital cameras. This so-called camera fingerprint gives rise to different applications, such as image forensics and authentication. However, if images are publicly available, an adversary can estimate the fingerprint from her victim and plant it into spurious images. The concept of fragile camera fingerprints addresses this attack by exploiting asymmetries in data access: While the camera owner will always have access to a full fingerprint from uncompressed images, the adversary has typically access to compressed images and thus only to a truncated fingerprint. The security of this defense, however, has not been systematically explored yet. This paper provides the first comprehensive analysis of fragile camera fingerprints under attack. A series of theoretical and practical tests demonstrate that fragile camera fingerprints allow a reliable device identification for common compression levels in an adversarial environment.
Domain Adaptation in Multi-Channel Autoencoder based Features for Robust Face Anti-Spoofing
Venue: arXiv cs.CV 2019
Year: 2019

While the performance of face recognition systems has improved significantly in the last decade, they are proved to be highly vulnerable to presentation attacks (spoofing). Most of the research in the field of face presentation attack detection (PAD), was focused on boosting the performance of the systems within a single database. Face PAD datasets are usually captured with RGB cameras, and have very limited number of both bona-fide samples and presentation attack instruments. Training face PAD systems on such data leads to poor performance, even in the closed-set scenario, especially when sophisticated attacks are involved. We explore two paths to boost the performance of the face PAD system against challenging attacks. First, by using multi-channel (RGB, Depth and NIR) data, which is still easily accessible in a number of mass production devices. Second, we develop a novel Autoencoders + MLP based face PAD algorithm. Moreover, instead of collecting more data for training of the proposed deep architecture, the domain adaptation technique is proposed, transferring the knowledge of facial appearance from RGB to multi-channel domain. We also demonstrate, that learning the features of individual facial regions, is more discriminative than the features learned from an entire face. The proposed system is tested on a very recent publicly available multi-channel PAD database with a wide variety of presentation attacks.
Lidar-based Object Classification with Explicit Occlusion Modeling
Venue: arXiv cs.RO 2019
Year: 2019

LIDAR is one of the most important sensors for Unmanned Ground Vehicles (UGV). Object detection and classification based on lidar point cloud is a key technology for UGV. In object detection and classification, the mutual occlusion between neighboring objects is an important factor affecting the accuracy. In this paper, we consider occlusion as an intrinsic property of the point cloud data. We propose a novel approach that explicitly model the occlusion. The occlusion property is then taken into account in the subsequent classification step. We perform experiments on the KITTI dataset. Experimental results indicate that by utilizing the occlusion property that we modeled, the classifier obtains much better performance.
Multitask Learning for Blackmarket Tweet Detection
Venue: arXiv cs.SI 2019
Year: 2019

Online social media platforms have made the world more connected than ever before, thereby making it easier for everyone to spread their content across a wide variety of audiences. Twitter is one such popular platform where people publish tweets to spread their messages to everyone. Twitter allows users to Retweet other users' tweets in order to broadcast it to their network. The more retweets a particular tweet gets, the faster it spreads. This creates incentives for people to obtain artificial growth in the reach of their tweets by using certain blackmarket services to gain inorganic appraisals for their content. In this paper, we attempt to detect such tweets that have been posted on these blackmarket services in order to gain artificially boosted retweets. We use a multitask learning framework to leverage soft parameter sharing between a classification and a regression based task on separate inputs. This allows us to effectively detect tweets that have been posted to these blackmarket services, achieving an F1-score of 0.89 when classifying tweets as blackmarket or genuine.
PTAS and Exact Algorithms for $r$-Gathering Problems on Tree
Venue: arXiv cs.DS 2019
Year: 2019

r-gathering problem is a variant of facility location problems. In this problem, we are given a set of users and a set of facilities on same metric space. We open some of the facilities and assign each user to an open facility, so that at least r users are assigned to every open facility. We aim to minimize the maximum distance between user and assigned facility. In general, this problem is NP-hard and admit an approximation algorithm with factor 3. It is known that the problem does not admit any approximation algorithm within a factor less than 3. In our another paper, we proved that this problem is NP-hard even on spider, which is a special case of tree metric. In this paper, we concentrate on the problems on a tree. First, we give a PTAS for r-gathering problem on a tree. Furthermore, we give PTAS for some variants of the problems on a tree, and also give exact polynomial-time algorithms for another variants of r-gathering problem on a tree.
$r$-Gather Clustering and $r$-Gathering on Spider: FPT Algorithms and Hardness
Venue: arXiv cs.DS 2019
Year: 2019

We consider min-max $r$-gather clustering problem and min-max $r$-gathering problem. In the min-max $r$-gather clustering problem, we are given a set of users and divide them into clusters with size at least $r$; the goal is to minimize the maximum diameter of clusters. In the min-max $r$-gathering problem, we are additionally given a set of facilities and assign each cluster to a facility; the goal is to minimize the maximum distance between the users and the assigned facility. In this study, we consider the case that the users and facilities are located on a ``spider'' and propose the first fixed-parameter tractable (FPT) algorithms for both problems, which are parametrized by only the number of legs. Furthermore, we prove that these problems are NP-hard when the number of legs is arbitrarily large.
Tensor p-shrinkage nuclear norm for low-rank tensor completion
Venue: arXiv cs.LG 2019
Year: 2019

In this paper, a new definition of tensor p-shrinkage nuclear norm (p-TNN) is proposed based on tensor singular value decomposition (t-SVD). In particular, it can be proved that p-TNN is a better approximation of the tensor average rank than the tensor nuclear norm when p < 1. Therefore, by employing the p-shrinkage nuclear norm, a novel low-rank tensor completion (LRTC) model is proposed to estimate a tensor from its partial observations. Statistically, the upper bound of recovery error is provided for the LRTC model. Furthermore, an efficient algorithm, accelerated by the adaptive momentum scheme, is developed to solve the resulting nonconvex optimization problem. It can be further guaranteed that the algorithm enjoys a global convergence rate under the smoothness assumption. Numerical experiments conducted on both synthetic and real-world data sets verify our results and demonstrate the superiority of our p-TNN in LRTC problems over several state-of-the-art methods.
Multiscale Visual Drilldown for the Analysis of Large Ensembles of Multi-Body Protein Complexes
Venue: arXiv cs.HC 2019
Year: 2019

When studying multi-body protein complexes, biochemists use computational tools that can suggest hundreds or thousands of their possible spatial configurations. However, it is not feasible to experimentally verify more than only a very small subset of them. In this paper, we propose a novel multiscale visual drilldown approach that was designed in tight collaboration with proteomic experts, enabling a systematic exploration of the configuration space. Our approach takes advantage of the hierarchical structure of the data -- from the whole ensemble of protein complex configurations to the individual configurations, their contact interfaces, and the interacting amino acids. Our new solution is based on interactively linked 2D and 3D views for individual hierarchy levels and at each level, we offer a set of selection and filtering operations enabling the user to narrow down the number of configurations that need to be manually scrutinized. Furthermore, we offer a dedicated filter interface, which provides the users with an overview of the applied filtering operations and enables them to examine their impact on the explored ensemble. This way, we maintain the history of the exploration process and thus enable the user to return to an earlier point of the exploration. We demonstrate the effectiveness of our approach on two case studies conducted by collaborating proteomic experts.
Linear MIM-Width of Trees
Venue: arXiv cs.DS 2019
Year: 2019

We provide an $O(n \log n)$ algorithm computing the linear maximum induced matching width of a tree and an optimal layout.
A Bridge Anchored on Both Sides: Formal Deduction in Introductory CS, and Code Proofs in Discrete Math
Venue: arXiv cs.PL 2019
Year: 2019

There is a sharp disconnect between the programming and mathematical portions of the standard undergraduate computer science curriculum, leading to student misunderstanding about how the two are related. We propose connecting the subjects early in the curriculum---specifically, in CS1 and the introductory discrete mathematics course---by using formal reasoning about programs as a bridge between them. This article reports on Haverford and Grinnell College's experience in constructing the end points of this bridge between CS1 and discrete mathematics. Haverford's long-standing "3-2-1" curriculum introduces code reasoning in conjunction with introductory programming concepts, and Grinnell's discrete mathematics introduces code reasoning as a motivation for logic and formal deduction. Both courses present code reasoning in a style based on symbolic code execution techniques from the programming language community, but tuned to address the particulars of each course. These courses rely primarily on traditional means of proof authoring with pen-and-paper. This is unsatisfactory for students who receive no feedback until grading on their work and instructors who must shoulder the burden of interpreting students' proofs and giving useful feedback. To this end, we also describe the current state of Orca, an in-development proof assistant for undergraduate education that we are developing to address these issues in our courses. Finally, in teaching our courses, we have discovered a number of educational research questions about the effectiveness of code reasoning in bridging the gap between programming and mathematics, and the ability of tools like \orca to support this pedagogy. We pose these research questions as next steps to formalize our initial experiences in our courses with the hope of eventually generalizing our approaches for wider adoption.
Approximately Stable Matchings with General Constraints
Venue: arXiv cs.GT 2019
Year: 2019

This paper focuses on two-sided matching where one side (a hospital or firm) is matched to the other side (a doctor or worker) so as to maximize a cardinal objective under general feasibility constraints. In a standard model, even though multiple doctors can be matched to a single hospital, a hospital has a responsive preference and a maximum quota. However, in practical applications, a hospital has some complicated cardinal preference and constraints. With such preferences (e.g., submodular) and constraints (e.g., knapsack or matroid intersection), stable matchings may fail to exist. This paper first determines the complexity of checking and computing stable matchings based on preference class and constraint class. Second, we establish a framework to analyze this problem on packing problems and the framework enables us to access the wealth of online packing algorithms so that we construct approximately stable algorithms as a variant of generalized deferred acceptance algorithm. We further provide some inapproximability results.