OpenRaiser/Intern-Atlas huggingface dataset:
Craig Interpolation with Clausal First-Order Tableaux
Venue: arXiv cs.LO 2021
Year: 2021

We develop foundations for computing Craig-Lyndon interpolants of two given formulas with first-order theorem provers that construct clausal tableaux. Provers that can be understood in this way include efficient machine-oriented systems based on calculi of two families: goal-oriented such as model elimination and the connection method, and bottom-up such as the hypertableau calculus. We present the first interpolation method for first-order proofs represented by closed tableaux that proceeds in two stages, similar to known interpolation methods for resolution proofs. The first stage is an induction on the tableau structure, which is sufficient to compute propositional interpolants. We show that this can linearly simulate different prominent propositional interpolation methods that operate by an induction on a resolution deduction tree. In the second stage, interpolant lifting, quantified variables that replace certain terms (constants and compound terms) by variables are introduced. We justify the correctness of interpolant lifting (for the case without built-in equality) abstractly on the basis of Herbrand's theorem and for a different characterization of the formulas to be lifted than in the literature. In addition, we discuss various subtle aspects that are relevant for the investigation and practical realization of first-order interpolation based on clausal tableaux.
Fully Automated Functional Fuzzing of Android Apps for Detecting Non-crashing Logic Bugs
Venue: arXiv cs.SE 2021
Year: 2021

Android apps are GUI-based event-driven software and have become ubiquitous in recent years. Obviously, functional correctness is critical for an app's success. However, in addition to crash bugs, non-crashing functional bugs (in short as "non-crashing bugs" in this work) like inadvertent function failures, silent user data lost and incorrect display information are prevalent, even in popular, well-tested apps. These non-crashing functional bugs are usually caused by program logic errors and manifest themselves on the graphic user interfaces (GUIs). In practice, such bugs pose significant challenges in effectively detecting them because (1) current practices heavily rely on expensive, small-scale manual validation (the lack of automation); and (2) modern fully automated testing has been limited to crash bugs (the lack of test oracles). This paper fills this gap by introducing independent view fuzzing, a novel, fully automated approach for detecting non-crashing functional bugs in Android apps. Inspired by metamorphic testing, our key insight is to leverage the commonly-held independent view property of Android apps to manufacture property-preserving mutant tests from a set of seed tests that validate certain app properties. The mutated tests help exercise the tested apps under additional, adverse conditions. Any property violations indicate likely functional bugs for further manual confirmation. We have realized our approach as an automated, end-to-end functional fuzzing tool, Genie. Given an app, (1) Genie automatically detects non-crashing bugs without requiring human-provided tests and oracles (thus fully automated); and (2) the detected non-crashing bugs are diverse (thus general and not limited to specific functional properties), which set Genie apart from prior work.
Mime: Mimicking Centralized Stochastic Algorithms in Federated Learning
Venue: arXiv cs.LG 2021
Year: 2021

Federated learning (FL) is a challenging setting for optimization due to the heterogeneity of the data across different clients which gives rise to the client drift phenomenon. In fact, obtaining an algorithm for FL which is uniformly better than simple centralized training has been a major open problem thus far. In this work, we propose a general algorithmic framework, Mime, which i) mitigates client drift and ii) adapts arbitrary centralized optimization algorithms such as momentum and Adam to the cross-device federated learning setting. Mime uses a combination of control-variates and server-level statistics (e.g. momentum) at every client-update step to ensure that each local update mimics that of the centralized method run on iid data. We prove a reduction result showing that Mime can translate the convergence of a generic algorithm in the centralized setting into convergence in the federated setting. Further, we show that when combined with momentum based variance reduction, Mime is provably faster than any centralized method--the first such result. We also perform a thorough experimental exploration of Mime's performance on real world datasets.
Rectilinear Planarity Testing of Plane Series-Parallel Graphs in Linear Time
Venue: arXiv cs.DS 2021
Year: 2021

A plane graph is rectilinear planar if it admits an embedding-preserving straight-line drawing where each edge is either horizontal or vertical. We prove that rectilinear planarity testing can be solved in optimal $O(n)$ time for any plane series-parallel graph $G$ with $n$ vertices. If $G$ is rectilinear planar, an embedding-preserving rectilinear planar drawing of $G$ can be constructed in $O(n)$ time. Our result is based on a characterization of rectilinear planar series-parallel graphs in terms of intervals of orthogonal spirality that their components can have, and it leads to an algorithm that can be easily implemented.
Neural Light Transport for Relighting and View Synthesis
Venue: arXiv cs.CV 2021
Year: 2021

The light transport (LT) of a scene describes how it appears under different lighting and viewing directions, and complete knowledge of a scene's LT enables the synthesis of novel views under arbitrary lighting. In this paper, we focus on image-based LT acquisition, primarily for human bodies within a light stage setup. We propose a semi-parametric approach to learn a neural representation of LT that is embedded in the space of a texture atlas of known geometric properties, and model all non-diffuse and global LT as residuals added to a physically-accurate diffuse base rendering. In particular, we show how to fuse previously seen observations of illuminants and views to synthesize a new image of the same scene under a desired lighting condition from a chosen viewpoint. This strategy allows the network to learn complex material effects (such as subsurface scattering) and global illumination, while guaranteeing the physical correctness of the diffuse LT (such as hard shadows). With this learned LT, one can relight the scene photorealistically with a directional light or an HDRI map, synthesize novel views with view-dependent effects, or do both simultaneously, all in a unified framework using a set of sparse, previously seen observations. Qualitative and quantitative experiments demonstrate that our neural LT (NLT) outperforms state-of-the-art solutions for relighting and view synthesis, without separate treatment for both problems that prior work requires.
Co-design and Co-simulation for Engineering Systems: Insights from the Sustainable Infrastructure Planning Game
Venue: arXiv cs.CY 2021
Year: 2021

This paper draws on perspectives from co-design as an integrative and collaborative design activity and co-simulation as a supporting information system to advance engineering design methods for problems of societal significance. Design and implementation of the Sustainable Infrastructure Planning Game provides a prototypical co-design artifact that leverages the High Level Architecture co-simulation standard. Three role players create a strategic infrastructure plan for agriculture, water, and energy sectors to meet sustainability objectives for a growing and urbaninzing population in a fictional desert nation. An observational study conducts 15 co-design sessions to understand underlying dynamics between actors and how co-simulation capabilities influence design outcomes. Results characterize the dependencies and conflicts between player roles based on technical exchange of resource flows, identifying tension between agriculture and water roles based on water demands for irrigation. Analysis shows a correlation between data exchange, facilitated by synchronous co-simulation, and highly-ranked achievement of joint sustainability outcomes. Conclusions reflect on the opportunities and challenges presented by co-simulation in co-design settings to address engineering systems problems.
Approximation in (Poly-) Logarithmic Space
Venue: arXiv cs.DS 2021
Year: 2021

We develop new approximation algorithms for classical graph and set problems in the RAM model under space constraints. As one of our main results, we devise an algorithm for d-Hitting Set that runs in time n^{O(d^2 + d/ε})}, uses O((d^2 + d/ε) log n) bits of space, and achieves an approximation ratio of O((d/ε) n^ε) for any positive ε\leq 1 and any natural number d. In particular, this yields a factor-O(log n) approximation algorithm which runs in time n^{O(log n)} and uses O(log^2 n) bits of space (for constant d). As a corollary, we obtain similar bounds for Vertex Cover and several graph deletion problems. For bounded-multiplicity problem instances, one can do better. We devise a factor-2 approximation algorithm for Vertex Cover on graphs with maximum degree Δ, and an algorithm for computing maximal independent sets which both run in time n^{O(Δ)} and use O(Δlog n) bits of space. For the more general d-Hitting Set problem, we devise a factor-d approximation algorithm which runs in time n^{O(d δ^2)} and uses O(d δ^2 log n) bits of space on set families where each element appears in at most δsets. For Independent Set restricted to graphs with average degree d, we give a factor-(2d) approximation algorithm which runs in polynomial time and uses O(log n) bits of space. We also devise a factor-O(d^2) approximation algorithm for Dominating Set on d-degenerate graphs which runs in time n^{O(log n)} and uses O(log^2 n) bits of space. For d-regular graphs, we show how a known randomized factor-O(log d) approximation algorithm can be derandomized to run in time n^{O(1)} and use O(log n) bits of space. Our results use a combination of ideas from the theory of kernelization, distributed algorithms and randomized algorithms.
DTVNet+: A High-Resolution Scenic Dataset for Dynamic Time-lapse Video Generation
Venue: arXiv cs.CV 2021
Year: 2021

This paper presents a novel end-to-end dynamic time-lapse video generation framework, named DTVNet, to generate diversified time-lapse videos from a single landscape image conditioned on normalized motion vectors. The proposed DTVNet consists of two submodules: \emph{Optical Flow Encoder} (OFE) and \emph{Dynamic Video Generator} (DVG). The OFE maps a sequence of optical flow maps to a \emph{normalized motion vector} that encodes the motion information of the generated video. The DVG contains motion and content streams to learn from the motion vector and the single landscape image. Besides, it contains an encoder to learn shared content features and a decoder to construct video frames with corresponding motion. Specifically, the \emph{motion stream} introduces multiple \emph{adaptive instance normalization} (AdaIN) layers to integrate multi-level motion information for controlling the object motion. In the testing stage, videos with the same content but various motion information can be generated by different \emph{normalized motion vectors} based on only one input image. Also, we propose a high-resolution scenic time-lapse video dataset, named Quick-Sky-Time, to evaluate different approaches, which can be viewed as a new benchmark for high-quality scenic image and video generation tasks. We further conduct experiments on Sky Time-lapse, Beach, and Quick-Sky-Time datasets. The results demonstrate the superiority of our approach over state-of-the-art methods for generating high-quality and various dynamic videos.
Learning to See Through Obstructions with Layered Decomposition
Venue: arXiv cs.CV 2021
Year: 2021

We present a learning-based approach for removing unwanted obstructions, such as window reflections, fence occlusions, or adherent raindrops, from a short sequence of images captured by a moving camera. Our method leverages motion differences between the background and obstructing elements to recover both layers. Specifically, we alternate between estimating dense optical flow fields of the two layers and reconstructing each layer from the flow-warped images via a deep convolutional neural network. This learning-based layer reconstruction module facilitates accommodating potential errors in the flow estimation and brittle assumptions, such as brightness consistency. We show that the proposed approach learned from synthetically generated data performs well to real images. Experimental results on numerous challenging scenarios of reflection and fence removal demonstrate the effectiveness of the proposed method.
Settling SETH vs. Approximate Sparse Directed Unweighted Diameter (up to (NU)NSETH)
Venue: arXiv cs.DS 2021
Year: 2021

We prove several tight results on the fine-grained complexity of approximating the diameter of a graph. First, we prove that, for any $\varepsilon>0$, assuming the Strong Exponential Time Hypothesis (SETH), there are no near-linear time $2-\varepsilon$-approximation algorithms for the Diameter of a sparse directed graph, even in unweighted graphs. This result shows that a simple near-linear time 2-approximation algorithm for Diameter is optimal under SETH, answering a question from a survey of Rubinstein and Vassilevska-Williams (SIGACT '19) for the case of directed graphs. In the same survey, Rubinstein and Vassilevska-Williams also asked if it is possible to show that there are no $2-\varepsilon$ approximation algorithms for Diameter in a directed graph in $O(n^{1.499})$ time. We show that, assuming a hypothesis called NSETH, one cannot use a deterministic SETH-based reduction to rule out the existence of such algorithms. Extending the techniques in these two results, we characterize whether a $2-\varepsilon$ approximation algorithm running in time $O(n^{1+δ})$ for the Diameter of a sparse directed unweighted graph can be ruled out by a deterministic SETH-based reduction for every $δ\in(0,1)$ and essentially every $\varepsilon\in(0,1)$, assuming NSETH. This settles the SETH-hardness of approximating the diameter of sparse directed unweighted graphs for deterministic reductions, up to NSETH. We make the same characterization for randomized SETH-based reductions, assuming another hypothesis called NUNSETH. We prove additional hardness and non-reducibility results for undirected graphs.
Optimal to-do list gamification
Venue: arXiv cs.AI 2021
Year: 2021

What should I work on first? What can wait until later? Which projects should I prioritize and which tasks are not worth my time? These are challenging questions that many people face every day. People's intuitive strategy is to prioritize their immediate experience over the long-term consequences. This leads to procrastination and the neglect of important long-term projects in favor of seemingly urgent tasks that are less important. Optimal gamification strives to help people overcome these problems by incentivizing each task by a number of points that communicates how valuable it is in the long-run. Unfortunately, computing the optimal number of points with standard dynamic programming methods quickly becomes intractable as the number of a person's projects and the number of tasks required by each project increase. Here, we introduce and evaluate a scalable method for identifying which tasks are most important in the long run and incentivizing each task according to its long-term value. Our method makes it possible to create to-do list gamification apps that can handle the size and complexity of people's to-do lists in the real world.
Fine-grained Visual Textual Alignment for Cross-Modal Retrieval using Transformer Encoders
Venue: arXiv cs.CV 2021
Year: 2021

Despite the evolution of deep-learning-based visual-textual processing systems, precise multi-modal matching remains a challenging task. In this work, we tackle the task of cross-modal retrieval through image-sentence matching based on word-region alignments, using supervision only at the global image-sentence level. Specifically, we present a novel approach called Transformer Encoder Reasoning and Alignment Network (TERAN). TERAN enforces a fine-grained match between the underlying components of images and sentences, i.e., image regions and words, respectively, in order to preserve the informative richness of both modalities. TERAN obtains state-of-the-art results on the image retrieval task on both MS-COCO and Flickr30k datasets. Moreover, on MS-COCO, it also outperforms current approaches on the sentence retrieval task. Focusing on scalable cross-modal information retrieval, TERAN is designed to keep the visual and textual data pipelines well separated. Cross-attention links invalidate any chance to separately extract visual and textual features needed for the online search and the offline indexing steps in large-scale retrieval systems. In this respect, TERAN merges the information from the two domains only during the final alignment phase, immediately before the loss computation. We argue that the fine-grained alignments produced by TERAN pave the way towards the research for effective and efficient methods for large-scale cross-modal information retrieval. We compare the effectiveness of our approach against relevant state-of-the-art methods. On the MS-COCO 1K test set, we obtain an improvement of 5.7% and 3.5% respectively on the image and the sentence retrieval tasks on the Recall@1 metric. The code used for the experiments is publicly available on GitHub at https://github.com/mesnico/TERAN.
Profiling Gas Consumption in Solidity Smart Contracts
Venue: arXiv cs.SE 2021
Year: 2021

Nowadays, more and more applications are developed for running on a distributed ledger technology, namely dApps. The business logic of dApps is usually implemented within smart contracts developed through Solidity, a programming language for writing smart contracts on different blockchain platforms, including the popular Ethereum. In Ethereum, the smart contracts run on the machines of miners and the gas corresponds to the execution fee compensating such computing resources. However, the deployment and execution costs of a smart contract depend on the implementation choices done by developers. Unappropriated design choices could lead to higher gas consumption than necessary. In this paper, we (i) identify a set of 19 Solidity code smells affecting the deployment and transaction costs of a smart contract, and (ii) assess the relevance of such smells through a survey involving 34 participants. On top of these smells, we propose GasMet, a suite of metrics for statically evaluating the code quality of a smart contract from the gas consumption perspective. An experiment involving 2,186 smart contracts demonstrates that the proposed metrics have direct associations with deployment costs. The metrics in our suite can be used for more easily identifying source code segments that need optimizations.
Poising on Ariadne's thread: An algorithm for computing a maximum clique in polynomial time
Venue: arXiv cs.GT 2021
Year: 2021

In this paper, we present a polynomial-time algorithm for the maximum clique problem, which implies P = NP. Our algorithm is based on a continuous game-theoretic representation of this problem and at its heart lies a discrete-time dynamical system. The rule of our dynamical system depends on a parameter such that if this parameter is equal to the maximum-clique size, the iterates of our dynamical system are guaranteed to converge to a maximum clique.
Distillation-Based Semi-Supervised Federated Learning for Communication-Efficient Collaborative Training with Non-IID Private Data
Venue: arXiv cs.DC 2021
Year: 2021

This study develops a federated learning (FL) framework overcoming largely incremental communication costs due to model sizes in typical frameworks without compromising model performance. To this end, based on the idea of leveraging an unlabeled open dataset, we propose a distillation-based semi-supervised FL (DS-FL) algorithm that exchanges the outputs of local models among mobile devices, instead of model parameter exchange employed by the typical frameworks. In DS-FL, the communication cost depends only on the output dimensions of the models and does not scale up according to the model size. The exchanged model outputs are used to label each sample of the open dataset, which creates an additionally labeled dataset. Based on the new dataset, local models are further trained, and model performance is enhanced owing to the data augmentation effect. We further highlight that in DS-FL, the heterogeneity of the devices' dataset leads to ambiguous of each data sample and lowing of the training convergence. To prevent this, we propose entropy reduction averaging, where the aggregated model outputs are intentionally sharpened. Moreover, extensive experiments show that DS-FL reduces communication costs up to 99% relative to those of the FL benchmark while achieving similar or higher classification accuracy.
A New Path to Code-based Signatures via Identification Schemes with Restricted Errors
Venue: arXiv cs.CR 2021
Year: 2021

In this paper we introduce a variant of the Syndrome Decoding Problem (SDP), that we call Restricted SDP (R-SDP), in which the entries of the searched vector are defined over a subset of the underlying finite field. We prove the NP-completeness of R-SDP, via a reduction from the classical SDP, and describe algorithms which solve such new problem. We study the properties of random codes under this new decoding perspective, in the fashion of traditional coding theory results, and assess the complexity of solving a random R-SDP instance. As a concrete application, we describe how Zero-Knowledge Identification (ZK-ID) schemes based on SDP can be tweaked to rely on R-SDP, and show that this leads to compact public keys as well as significantly reduced communication costs. Thus, these schemes offer an improved basis for the construction of code-based digital signature schemes derived from identification schemes through the well-know Fiat-Shamir transformation.
Three Variants of Differential Privacy: Lossless Conversion and Applications
Venue: arXiv cs.IT 2021
Year: 2021

We consider three different variants of differential privacy (DP), namely approximate DP, Rényi DP (RDP), and hypothesis test DP. In the first part, we develop a machinery for optimally relating approximate DP to RDP based on the joint range of two $f$-divergences that underlie the approximate DP and RDP. In particular, this enables us to derive the optimal approximate DP parameters of a mechanism that satisfies a given level of RDP. As an application, we apply our result to the moments accountant framework for characterizing privacy guarantees of noisy stochastic gradient descent (SGD). When compared to the state-of-the-art, our bounds may lead to about 100 more stochastic gradient descent iterations for training deep learning models for the same privacy budget. In the second part, we establish a relationship between RDP and hypothesis test DP which allows us to translate the RDP constraint into a tradeoff between type I and type II error probabilities of a certain binary hypothesis test. We then demonstrate that for noisy SGD our result leads to tighter privacy guarantees compared to the recently proposed $f$-DP framework for some range of parameters.