OpenRaiser/Intern-Atlas huggingface dataset:
A higher-order finite element method with unstructured anisotropic mesh adaption for two phase flows with surface tension
Venue: arXiv cs.CE 2020
Year: 2020

A novel finite element framework is proposed for the numerical simulation of two phase flows with surface tension. The Level-Set (LS) method with piece-wise quadratic (P2) interpolation for the liquid-gas interface is used in order to reach higher-order convergence rates in regions with smooth interface. A balanced-force implementation of the continuum surface force model is used to take into account the surface tension and to solve static problems as accurately as possible. Given that this requires a balance between the discretization used for the LS function, and that used for the pressure field, an equal-order P2/P2/P2 scheme is proposed for the Navier-Stokes and LS advection equations, which are strongly coupled with each other. This fully implicit formulation is stabilized using the residual-based variational multiscale framework. In order to improve the accuracy and obtain optimal convergence rates with a minimum number of elements, an anisotropic mesh adaption method is proposed where the unstructured mesh is kept as fine as possible close to the zero iso-value of the P2 LS function. Elements are automatically stretched in regions with flat interface in order to keep the complexity fixed during the simulation. The accuracy and efficiency of this approach are demonstrated for two and three dimensional simulations of a rising bubble.
Real-Time Edge Classification: Optimal Offloading under Token Bucket Constraints
Venue: arXiv cs.LG 2020
Year: 2020

To deploy machine learning-based algorithms for real-time applications with strict latency constraints, we consider an edge-computing setting where a subset of inputs are offloaded to the edge for processing by an accurate but resource-intensive model, and the rest are processed only by a less-accurate model on the device itself. Both models have computational costs that match available compute resources, and process inputs with low-latency. But offloading incurs network delays, and to manage these delays to meet application deadlines, we use a token bucket to constrain the average rate and burst length of transmissions from the device. We introduce a Markov Decision Process-based framework to make offload decisions under these constraints, based on the local model's confidence and the token bucket state, with the goal of minimizing a specified error measure for the application. Beyond isolated decisions for individual devices, we also propose approaches to allow multiple devices connected to the same access switch to share their bursting allocation. We evaluate and analyze the policies derived using our framework on the standard ImageNet image classification benchmark.
Senate: A Maliciously-Secure MPC Platform for Collaborative Analytics
Venue: arXiv cs.CR 2020
Year: 2020

Many organizations stand to benefit from pooling their data together in order to draw mutually beneficial insights -- e.g., for fraud detection across banks, better medical studies across hospitals, etc. However, such organizations are often prevented from sharing their data with each other by privacy concerns, regulatory hurdles, or business competition. We present Senate, a system that allows multiple parties to collaboratively run analytical SQL queries without revealing their individual data to each other. Unlike prior works on secure multi-party computation (MPC) that assume that all parties are semi-honest, Senate protects the data even in the presence of malicious adversaries. At the heart of Senate lies a new MPC decomposition protocol that decomposes the cryptographic MPC computation into smaller units, some of which can be executed by subsets of parties and in parallel, while preserving its security guarantees. Senate then provides a new query planning algorithm that decomposes and plans the cryptographic computation effectively, achieving a performance of up to 145$\times$ faster than the state-of-the-art.
Versatile Verification of Tree Ensembles
Venue: arXiv cs.LG 2020
Year: 2020

Machine learned models often must abide by certain requirements (e.g., fairness or legal). This has spurred interested in developing approaches that can provably verify whether a model satisfies certain properties. This paper introduces a generic algorithm called Veritas that enables tackling multiple different verification tasks for tree ensemble models like random forests (RFs) and gradient boosting decision trees (GBDTs). This generality contrasts with previous work, which has focused exclusively on either adversarial example generation or robustness checking. Veritas formulates the verification task as a generic optimization problem and introduces a novel search space representation. Veritas offers two key advantages. First, it provides anytime lower and upper bounds when the optimization problem cannot be solved exactly. In contrast, many existing methods have focused on exact solutions and are thus limited by the verification problem being NP-complete. Second, Veritas produces full (bounded suboptimal) solutions that can be used to generate concrete examples. We experimentally show that Veritas outperforms the previous state of the art by (a) generating exact solutions more frequently, (b) producing tighter bounds when (a) is not possible, and (c) offering orders of magnitude speed ups. Subsequently, Veritas enables tackling more and larger real-world verification scenarios.
T$^2$-Net: A Semi-supervised Deep Model for Turbulence Forecasting
Venue: arXiv cs.LG 2020
Year: 2020

Accurate air turbulence forecasting can help airlines avoid hazardous turbulence, guide the routes that keep passengers safe, maximize efficiency, and reduce costs. Traditional turbulence forecasting approaches heavily rely on painstakingly customized turbulence indexes, which are less effective in dynamic and complex weather conditions. The recent availability of high-resolution weather data and turbulence records allows more accurate forecasting of the turbulence in a data-driven way. However, it is a non-trivial task for developing a machine learning based turbulence forecasting system due to two challenges: (1) Complex spatio-temporal correlations, turbulence is caused by air movement with complex spatio-temporal patterns, (2) Label scarcity, very limited turbulence labels can be obtained. To this end, in this paper, we develop a unified semi-supervised framework, T$^2$-Net, to address the above challenges. Specifically, we first build an encoder-decoder paradigm based on the convolutional LSTM to model the spatio-temporal correlations. Then, to tackle the label scarcity problem, we propose a novel Dual Label Guessing method to take advantage of massive unlabeled turbulence data. It integrates complementary signals from the main Turbulence Forecasting task and the auxiliary Turbulence Detection task to generate pseudo-labels, which are dynamically utilized as additional training data. Finally, extensive experimental results on a real-world turbulence dataset validate the superiority of our method on turbulence forecasting.
Predict and Use Latent Patterns for Short-Text Conversation
Venue: arXiv cs.CL 2020
Year: 2020

Many neural network models nowadays have achieved promising performances in Chit-chat settings. The majority of them rely on an encoder for understanding the post and a decoder for generating the response. Without given assigned semantics, the models lack the fine-grained control over responses as the semantic mapping between posts and responses is hidden on the fly within the end-to-end manners. Some previous works utilize sampled latent words as a controllable semantic form to drive the generated response around the work, but few works attempt to use more complex semantic patterns to guide the generation. In this paper, we propose to use more detailed semantic forms, including latent responses and part-of-speech sequences sampled from the corresponding distributions, as the controllable semantics to guide the generation. Our results show that the richer semantics are not only able to provide informative and diverse responses, but also increase the overall performance of response quality, including fluency and coherence.
Cross-directional Feature Fusion Network for Building Damage Assessment from Satellite Imagery
Venue: arXiv cs.CV 2020
Year: 2020

Fast and effective responses are required when a natural disaster (e.g., earthquake, hurricane, etc.) strikes. Building damage assessment from satellite imagery is critical before an effective response is conducted. High-resolution satellite images provide rich information with pre- and post-disaster scenes for analysis. However, most existing works simply use pre- and post-disaster images as input without considering their correlations. In this paper, we propose a novel cross-directional fusion strategy to better explore the correlations between pre- and post-disaster images. Moreover, the data augmentation method CutMix is exploited to tackle the challenge of hard classes. The proposed method achieves state-of-the-art performance on a large-scale building damage assessment dataset -- xBD.
Abstracting Gradual Typing Moving Forward: Precise and Space-Efficient (Technical Report)
Venue: arXiv cs.PL 2020
Year: 2020

Abstracting Gradual Typing (AGT) is a systematic approach to designing gradually-typed languages. Languages developed using AGT automatically satisfy the formal semantic criteria for gradual languages identified by Siek et al. [2015]. Nonetheless, vanilla AGT semantics can still have important shortcomings. First, a gradual language's runtime checks should preserve the space-efficiency guarantees inherent to the underlying static and dynamic languages. To the contrary, the default operational semantics of AGT break proper tail calls. Second, a gradual language's runtime checks should enforce basic modular type-based invariants expected from the static type discipline. To the contrary, the default operational semantics of AGT may fail to enforce some invariants in surprising ways. We demonstrate this in the $\text{GTFL}_\lesssim$ language of Garcia et al. [2016]. This paper addresses both problems at once by refining the theory underlying AGT's dynamic checks. Garcia et al. [2016] observe that AGT involves two abstractions of static types: one for the static semantics and one for the dynamic semantics. We recast the latter as an abstract interpretation of subtyping itself, while gradual types still abstract static types. Then we show how forward-completeness [Giacobazzi and Quintarelli 2001] is key to supporting both space-efficient execution and reliable runtime type enforcement.
QBSUM: a Large-Scale Query-Based Document Summarization Dataset from Real-world Applications
Venue: arXiv cs.AI 2020
Year: 2020

Query-based document summarization aims to extract or generate a summary of a document which directly answers or is relevant to the search query. It is an important technique that can be beneficial to a variety of applications such as search engines, document-level machine reading comprehension, and chatbots. Currently, datasets designed for query-based summarization are short in numbers and existing datasets are also limited in both scale and quality. Moreover, to the best of our knowledge, there is no publicly available dataset for Chinese query-based document summarization. In this paper, we present QBSUM, a high-quality large-scale dataset consisting of 49,000+ data samples for the task of Chinese query-based document summarization. We also propose multiple unsupervised and supervised solutions to the task and demonstrate their high-speed inference and superior performance via both offline experiments and online A/B tests. The QBSUM dataset is released in order to facilitate future advancement of this research field.
Out-of-core Training for Extremely Large-Scale Neural Networks With Adaptive Window-Based Scheduling
Venue: arXiv cs.LG 2020
Year: 2020

While large neural networks demonstrate higher performance in various tasks, training large networks is difficult due to limitations on GPU memory size. We propose a novel out-of-core algorithm that enables faster training of extremely large-scale neural networks with sizes larger than allotted GPU memory. Under a given memory budget constraint, our scheduling algorithm locally adapts the timing of memory transfers according to memory usage of each function, which improves overlap between computation and memory transfers. Additionally, we apply virtual addressing technique, commonly performed in OS, to training of neural networks with out-of-core execution, which drastically reduces the amount of memory fragmentation caused by frequent memory transfers. With our proposed algorithm, we successfully train ResNet-50 with 1440 batch-size with keeping training speed at 55%, which is 7.5x larger than the upper bound of physical memory. It also outperforms a previous state-of-the-art substantially, i.e. it trains a 1.55x larger network than state-of-the-art with faster execution. Moreover, we experimentally show that our approach is also scalable for various types of networks.
Arbitrary Pattern Formation on Infinite Regular Tessellation Graphs
Venue: arXiv cs.DC 2020
Year: 2020

Given a set R of robots, each one located at different vertices of an infinite regular tessellation graph, we aim to explore the Arbitrary Pattern Formation (APF) problem. Given a multiset F of grid vertices such that |R|=|F|, APF asks for a distributed algorithm that moves robots so as to reach a configuration similar to F. Similarity means that robots must be disposed as F regardless of translations, rotations, reflections. So far, as possible graph discretizing the Euclidean plane only the standard square grid has been considered in the context of the classical Look-Compute-Move model. However, it is natural to consider also the other regular tessellation graphs, that are triangular and hexagonal grids. We provide a resolution algorithm for APF when the initial configuration is asymmetric and the considered topology is any regular tessellation graph.
Reconstruction of Voxels with Position- and Angle-Dependent Weightings
Venue: arXiv cs.CV 2020
Year: 2020

The reconstruction problem of voxels with individual weightings can be modeled a position- and angle- dependent function in the forward-projection. This changes the system matrix and prohibits to use standard filtered backprojection. In this work we first formulate this reconstruction problem in terms of a system matrix and weighting part. We compute the pseudoinverse and show that the solution is rank-deficient and hence very ill posed. This is a fundamental limitation for reconstruction. We then derive an iterative solution and experimentally show its uperiority to any closed-form solution.
Computation of Large Asymptotics of 3-Manifold Quantum Invariants
Venue: arXiv cs.CG 2020
Year: 2020

Quantum topological invariants have played an important role in computational topology, and they are at the heart of major modern mathematical conjectures. In this article, we study the experimental problem of computing large $r$ values of Turaev-Viro invariants $\mathrm{TV}_r$. We base our approach on an optimized backtracking algorithm, consisting of enumerating combinatorial data on a triangulation of a 3-manifold. We design an easily computable parameter to estimate the complexity of the enumeration space, based on lattice point counting in polytopes, and show experimentally its accuracy. We apply this parameter to a preprocessing strategy on the triangulation, and combine it with multi-precision arithmetics in order to compute the Turaev-Viro invariants. We finally study the improvements brought by these optimizations compared to state-of-the-art implementations, and verify experimentally Chen and Yang's volume conjecture on a census of closed 3-manifolds.
2FE: Two-Factor Encryption for Cloud Storage
Venue: arXiv cs.CR 2020
Year: 2020

Encrypted cloud storage services are steadily increasing in popularity, with many commercial solutions currently available. In such solutions, the cloud storage is trusted for data availability, but not for confidentiality. Additionally, the user's device is considered secure, and the user is expected to behave correctly. We argue that such assumptions are not met in reality: e.g., users routinely forget passwords and fail to make backups, and users' devices get stolen or become infected with malware. Therefore, we consider a more extensive threat model, where users' devices are susceptible to attacks and common human errors are possible. Given this model, we analyze 10 popular commercial services and show that none of them provides good confidentiality and data availability. Motivated by the lack of adequate solutions in the market, we design a novel scheme called Two-Factor Encryption (2FE) that draws inspiration from two-factor authentication and turns file encryption and decryption into an interactive process where two user devices, like a laptop and a smartphone, must interact. 2FE provides strong confidentiality and availability guarantees, as it withstands compromised cloud storage, one stolen or compromised user device at a time, and various human errors. 2FE achieves this by leveraging secret sharing with additional techniques such as oblivious pseudorandom functions and zero-knowledge proofs. We evaluate 2FE experimentally and show that its performance overhead is small. Finally, we explain how our approach can be adapted to other related use cases such as cryptocurrency wallets.
Size matters in the modal $μ$-calculus
Venue: arXiv cs.LO 2020
Year: 2020

We discuss and compare complexity measures for the modal $μ$-calculus, focusing on size and alternation depth. As a yardstick we take Wilke's alternating tree automata, which we shall call parity formulas in the text. Building on work by Bruse, Friedmann & Lange, we compare two size measures for $μ$-calculus formulas: subformula-size,i.e. , the number of subformulas of the given formula, and closure-size. These notions correspond to the representation of a formula as a parity formula based on, respectively, its subformula dag, and its closure graph. What distinguishes our approach is that we are explicit about the role of alpha-equivalence, as naively renaming bound variables can lead to an exponential blow-up. In addition, we match the formula's alternation depth with the index of the parity formula. We start in a setting without alpha-equivalence. We define subformula-size and closure-size and recall that a $μ$-calculus formula can be transformed into a parity formula of size linear wrt subformula size, and give a construction that transforms a $μ$-calculus formula into an equivalent parity formula linear wrt closure-size. Conversely, there is a standard transformation producing a $μ$-calculus formula of exponential subformula -- but linear closure-size in terms of the size of the original parity formula. We identify so-called untwisted parity formulas for which a transformation linear in subformula-size exists. We then introduce size notions that are completely invariant under alpha equivalence. We transfer the result of Bruse et alii, showing that also in our setting closure-size can be exponentially smaller than subformula-size. We also show how to rename bound variables so that alpha-equivalence becomes syntactic identity on the closure set. Finally, we review the complexity of guarded transformations.
Deciding $ω$-Regular Properties on Linear Recurrence Sequences
Venue: arXiv cs.LO 2020
Year: 2020

We consider the problem of deciding $ω$-regular properties on infinite traces produced by linear loops. Here we think of a given loop as producing a single infinite trace that encodes information about the signs of program variables at each time step. Formally, our main result is a procedure that inputs a prefix-independent $ω$-regular property and a sequence of numbers satisfying a linear recurrence, and determines whether the sign description of the sequence (obtained by replacing each positive entry with "$+$", each negative entry with "$-$", and each zero entry with "$0$") satisfies the given property. Our procedure requires that the recurrence be simple, \ie, that the update matrix of the underlying loop be diagonalisable. This assumption is instrumental in proving our key technical lemma: namely that the sign description of a simple linear recurrence sequence is almost periodic in the sense of Muchnik, Semënov, and Ushakov. To complement this lemma, we give an example of a linear recurrence sequence whose sign description fails to be almost periodic. Generalising from sign descriptions, we also consider the verification of properties involving semi-algebraic predicates on program variables.
Structured Visual Search via Composition-aware Learning
Venue: arXiv cs.CV 2020
Year: 2020

This paper studies visual search using structured queries. The structure is in the form of a 2D composition that encodes the position and the category of the objects. The transformation of the position and the category of the objects leads to a continuous-valued relationship between visual compositions, which carries highly beneficial information, although not leveraged by previous techniques. To that end, in this work, our goal is to leverage these continuous relationships by using the notion of symmetry in equivariance. Our model output is trained to change symmetrically with respect to the input transformations, leading to a sensitive feature space. Doing so leads to a highly efficient search technique, as our approach learns from fewer data using a smaller feature space. Experiments on two large-scale benchmarks of MS-COCO and HICO-DET demonstrates that our approach leads to a considerable gain in the performance against competing techniques.
Assured Autonomy: Path Toward Living With Autonomous Systems We Can Trust
Venue: arXiv cs.CY 2020
Year: 2020

The challenge of establishing assurance in autonomy is rapidly attracting increasing interest in the industry, government, and academia. Autonomy is a broad and expansive capability that enables systems to behave without direct control by a human operator. To that end, it is expected to be present in a wide variety of systems and applications. A vast range of industrial sectors, including (but by no means limited to) defense, mobility, health care, manufacturing, and civilian infrastructure, are embracing the opportunities in autonomy yet face the similar barriers toward establishing the necessary level of assurance sooner or later. Numerous government agencies are poised to tackle the challenges in assured autonomy. Given the already immense interest and investment in autonomy, a series of workshops on Assured Autonomy was convened to facilitate dialogs and increase awareness among the stakeholders in the academia, industry, and government. This series of three workshops aimed to help create a unified understanding of the goals for assured autonomy, the research trends and needs, and a strategy that will facilitate sustained progress in autonomy. The first workshop, held in October 2019, focused on current and anticipated challenges and problems in assuring autonomous systems within and across applications and sectors. The second workshop held in February 2020, focused on existing capabilities, current research, and research trends that could address the challenges and problems identified in workshop. The third event was dedicated to a discussion of a draft of the major findings from the previous two workshops and the recommendations.