OpenRaiser/Intern-Atlas huggingface dataset:
Is Sized Typing for Coq Practical?
Venue: arXiv cs.PL 2021
Year: 2021

Contemporary proof assistants such as Coq require that recursive functions be terminating and corecursive functions be productive to maintain logical consistency of their type theories, and some ensure these properties using syntactic checks. However, being syntactic, they are inherently delicate and restrictive, preventing users from easily writing obviously terminating or productive functions at their whim. Meanwhile, there exist many sized type theories that perform type-based termination and productivity checking, including theories based on the Calculus of (Co)Inductive Constructions (CIC), the core calculus underlying Coq. These theories are more robust and compositional in comparison. So why haven't they been adapted to Coq? In this paper, we venture to answer this question with CIC$\widehat{*}$, a sized type theory based on CIC. It extends past work on sized types in CIC with additional Coq features such as global and local definitions. We also present a corresponding size inference algorithm and implement it within Coq's kernel; for maximal backward compatibility with existing Coq developments, it requires no additional annotations from the user. In our evaluation of the implementation, we find a severe performance degradation when compiling parts of the Coq standard library, inherent to the algorithm itself. We conclude that if we wish to maintain backward compatibility, using size inference as a replacement for syntactic checking is wildly impractical in terms of performance.
Queueing Analysis of GPU-Based Inference Servers with Dynamic Batching: A Closed-Form Characterization
Venue: arXiv cs.PF 2021
Year: 2021

GPU-accelerated computing is a key technology to realize high-speed inference servers using deep neural networks (DNNs). An important characteristic of GPU-based inference is that the computational efficiency, in terms of the processing speed and energy consumption, drastically increases by processing multiple jobs together in a batch. In this paper, we formulate GPU-based inference servers as a batch service queueing model with batch-size dependent processing times. We first show that the energy efficiency of the server monotonically increases with the arrival rate of inference jobs, which suggests that it is energy-efficient to operate the inference server under a utilization level as high as possible within a latency requirement of inference jobs. We then derive a closed-form upper bound for the mean latency, which provides a simple characterization of the latency performance. Through simulation and numerical experiments, we show that the exact value of the mean latency is well approximated by this upper bound. We further compare this upper bound with the latency curve measured in real implementation of GPU-based inference servers and we show that the real performance curve is well explained by the derived simple formula.
Maintaining Ferment: On Opinion Control Over Social Networks
Venue: arXiv cs.SI 2021
Year: 2021

We consider the design of external inputs to achieve a control objective on the opinions, represented by scalars, in a social network. The opinion dynamics follow a variant of the discrete-time Friedkin-Johnsen model. We first consider two minimum cost optimal control problems over a finite interval $(T_0,T),$ $T_0 >0$ -- (1) TF where opinions at all nodes should exceed a given $τ,$ and (2) GF where a scalar function of the opinion vector should exceed a given $τ.$ For both problems we first provide a Pontryagin maximum principle (PMP) based control function when the controllable nodes are specified. We then show that both these problems exhibit the turnpike property where both the control function and the state vectors stay near their equilibrium for a large fraction of the time. This property is then used to choose the optimum set of controllable nodes. We then consider a third system, MF, which is a cost-constrained optimal control problem where we maximize the minimum value of a scalar function of the opinion vector over $(T_0,T).$ We provide a numerical algorithm to derive the control function for this problem using non-smooth PMP based techniques. Extensive numerical studies illustrate the three models, control techniques and corresponding outcomes.
A Formal Proof of the Irrationality of $ζ(3)$
Venue: arXiv cs.LO 2021
Year: 2021

This paper presents a complete formal verification of a proof that the evaluation of the Riemann zeta function at 3 is irrational, using the Coq proof assistant. This result was first presented by Apéry in 1978, and the proof we have formalized essentially follows the path of his original presentation. The crux of this proof is to establish that some sequences satisfy a common recurrence. We formally prove this result by an a posteriori verification of calculations performed by computer algebra algorithms in a Maple session. The rest of the proof combines arithmetical ingredients and asymptotic analysis, which we conduct by extending the Mathematical Components libraries.
Keyhole Imaging: Non-Line-of-Sight Imaging and Tracking of Moving Objects Along a Single Optical Path
Venue: arXiv cs.CV 2021
Year: 2021

Non-line-of-sight (NLOS) imaging and tracking is an emerging technology that allows the shape or position of objects around corners or behind diffusers to be recovered from transient, time-of-flight measurements. However, existing NLOS approaches require the imaging system to scan a large area on a visible surface, where the indirect light paths of hidden objects are sampled. In many applications, such as robotic vision or autonomous driving, optical access to a large scanning area may not be available, which severely limits the practicality of existing NLOS techniques. Here, we propose a new approach, dubbed keyhole imaging, that captures a sequence of transient measurements along a single optical path, for example, through a keyhole. Assuming that the hidden object of interest moves during the acquisition time, we effectively capture a series of time-resolved projections of the object's shape from unknown viewpoints. We derive inverse methods based on expectation-maximization to recover the object's shape and location using these measurements. Then, with the help of long exposure times and retroreflective tape, we demonstrate successful experimental results with a prototype keyhole imaging system.
Pneumothorax Segmentation: Deep Learning Image Segmentation to predict Pneumothorax
Venue: arXiv cs.CV 2021
Year: 2021

Computer vision has shown promising results in medical image processing. Pneumothorax is a deadly condition and if not diagnosed and treated at time then it causes death. It can be diagnosed with chest X-ray images. We need an expert and experienced radiologist to predict whether a person is suffering from pneumothorax or not by looking at the chest X-ray images. Everyone does not have access to such a facility. Moreover, in some cases, we need quick diagnoses. So we propose an image segmentation model to predict and give the output a mask that will assist the doctor in taking this crucial decision. Deep Learning has proved their worth in many areas and outperformed man state-of-the-art models. We want to use the power of these deep learning model to solve this problem. We have used U-net [13] architecture with ResNet [17] as a backbone and achieved promising results. U-net [13] performs very well in medical image processing and semantic segmentation. Our problem falls in the semantic segmentation category.
PCPATCH: software for the topological construction of multigrid relaxation methods
Venue: arXiv cs.MS 2021
Year: 2021

Effective relaxation methods are necessary for good multigrid convergence. For many equations, standard Jacobi and Gauß-Seidel are inadequate, and more sophisticated space decompositions are required; examples include problems with semidefinite terms or saddle point structure. In this paper we present a unifying software abstraction, PCPATCH, for the topological construction of space decompositions for multigrid relaxation methods. Space decompositions are specified by collecting topological entities in a mesh (such as all vertices or faces) and applying a construction rule (such as taking all degrees of freedom in the cells around each entity). The software is implemented in PETSc and facilitates the elegant expression of a wide range of schemes merely by varying solver options at runtime. In turn, this allows for the very rapid development of fast solvers for difficult problems.
On the hardness of finding normal surfaces
Venue: arXiv cs.CG 2021
Year: 2021

For many fundamental problems in computational topology, such as unknot recognition and $3$-sphere recognition, the existence of a polynomial-time solution remains unknown. A major algorithmic tool behind some of the best known algorithms for these problems is normal surface theory. However, we currently have a poor understanding of the computational complexity of problems in normal surface theory: many such problems are still not known to have polynomial-time algorithms, yet proofs of $\mathrm{NP}$-hardness also remain scarce. We give three results that provide some insight on this front. A number of modern normal surface theoretic algorithms depend critically on the operation of finding a non-trivial normal sphere or disc in a $3$-dimensional triangulation. We formulate an abstract problem that captures the algebraic and combinatorial aspects of this operation, and show that this abstract problem is $\mathrm{NP}$-complete. Assuming $\mathrm{P}\neq\mathrm{NP}$, this result suggests that any polynomial-time procedure for finding a non-trivial normal sphere or disc will need to exploit some geometric or topological intuition. Another key operation, which applies to a much wider range of topological problems, involves finding a vertex normal surface of a certain type. We study two closely-related problems that can be solved using this operation. For one of these problems, we give a simple alternative solution that runs in polynomial time; for the other, we prove $\mathrm{NP}$-completeness.
Malware Makeover: Breaking ML-based Static Analysis by Modifying Executable Bytes
Venue: arXiv cs.CR 2021
Year: 2021

Motivated by the transformative impact of deep neural networks (DNNs) in various domains, researchers and anti-virus vendors have proposed DNNs for malware detection from raw bytes that do not require manual feature engineering. In this work, we propose an attack that interweaves binary-diversification techniques and optimization frameworks to mislead such DNNs while preserving the functionality of binaries. Unlike prior attacks, ours manipulates instructions that are a functional part of the binary, which makes it particularly challenging to defend against. We evaluated our attack against three DNNs in white- and black-box settings, and found that it often achieved success rates near 100%. Moreover, we found that our attack can fool some commercial anti-viruses, in certain cases with a success rate of 85%. We explored several defenses, both new and old, and identified some that can foil over 80% of our evasion attempts. However, these defenses may still be susceptible to evasion by attacks, and so we advocate for augmenting malware-detection systems with methods that do not rely on machine learning.
Safe Adaptation with Multiplicative Uncertainties Using Robust Safe Set Algorithm
Venue: arXiv cs.RO 2021
Year: 2021

Maintaining safety under adaptation has long been considered to be an important capability for autonomous systems. As these systems estimate and change the ego-model of the system dynamics, questions regarding how to develop safety guarantees for such systems continue to be of interest. We propose a novel robust safe control methodology that uses set-based safety constraints to make a robotic system with dynamical uncertainties safely adapt and operate in its environment. The method consists of designing a scalar energy function (safety index) for an adaptive system with parametric uncertainty and an optimization-based approach for control synthesis. Simulation studies on a two-link manipulator are conducted and the results demonstrate the effectiveness of our proposed method in terms of generating provably safe control for adaptive systems with parametric uncertainty.
NFAD: Fixing anomaly detection using normalizing flows
Venue: arXiv cs.LG 2021
Year: 2021

Anomaly detection is a challenging task that frequently arises in practically all areas of industry and science, from fraud detection and data quality monitoring to finding rare cases of diseases and searching for new physics. Most of the conventional approaches to anomaly detection, such as one-class SVM and Robust Auto-Encoder, are one-class classification methods, i.e. focus on separating normal data from the rest of the space. Such methods are based on the assumption of separability of normal and anomalous classes, and subsequently do not take into account any available samples of anomalies. Nonetheless, in practical settings, some anomalous samples are often available; however, usually in amounts far lower than required for a balanced classification task, and the separability assumption might not always hold. This leads to an important task -- incorporating known anomalous samples into training procedures of anomaly detection models. In this work, we propose a novel model-agnostic training procedure to address this task. We reformulate one-class classification as a binary classification problem with normal data being distinguished from pseudo-anomalous samples. The pseudo-anomalous samples are drawn from low-density regions of a normalizing flow model by feeding tails of the latent distribution into the model. Such an approach allows to easily include known anomalies into the training process of an arbitrary classifier. We demonstrate that our approach shows comparable performance on one-class problems, and, most importantly, achieves comparable or superior results on tasks with variable amounts of known anomalies.
Download Time Analysis for Distributed Storage Codes with Locality and Availability
Venue: arXiv cs.PF 2021
Year: 2021

The paper presents techniques for analyzing the expected download time in distributed storage systems that employ systematic availability codes. These codes provide access to hot data through the systematic server containing the object and multiple recovery groups. When a request for an object is received, it can be replicated (forked) to the systematic server and all recovery groups. We first consider the low-traffic regime and present the close-form expression for the download time. By comparison across systems with availability, maximum distance separable (MDS), and replication codes, we demonstrate that availability codes can reduce download time in some settings but are not always optimal. In the high-traffic regime, the system consists of multiple inter-dependent Fork-Join queues, making exact analysis intractable. Accordingly, we present upper and lower bounds on the download time, and an M/G/1 queue approximation for several cases of interest. Via extensive numerical simulations, we evaluate our bounds and demonstrate that the M/G/1 queue approximation has a high degree of accuracy.
Bandit Multiclass Linear Classification for the Group Linear Separable Case
Venue: arXiv cs.LG 2021
Year: 2021

We consider the online multiclass linear classification under the bandit feedback setting. Beygelzimer, Pál, Szörényi, Thiruvenkatachari, Wei, and Zhang [ICML'19] considered two notions of linear separability, weak and strong linear separability. When examples are strongly linearly separable with margin $γ$, they presented an algorithm based on Multiclass Perceptron with mistake bound $O(K/γ^2)$, where $K$ is the number of classes. They employed rational kernel to deal with examples under the weakly linearly separable condition, and obtained the mistake bound of $\min(K\cdot 2^{\tilde{O}(K\log^2(1/γ))},K\cdot 2^{\tilde{O}(\sqrt{1/γ}\log K)})$. In this paper, we refine the notion of weak linear separability to support the notion of class grouping, called group weak linear separable condition. This situation may arise from the fact that class structures contain inherent grouping. We show that under this condition, we can also use the rational kernel and obtain the mistake bound of $K\cdot 2^{\tilde{O}(\sqrt{1/γ}\log L)})$, where $L\leq K$ represents the number of groups.
Low-Complexity Random Rotation-based Schemes for Intelligent Reflecting Surfaces
Venue: arXiv cs.IT 2021
Year: 2021

The employment of intelligent reflecting surfaces (IRSs) is a potential and promising solution to increase the spectral and energy efficiency of wireless communication networks. Despite their many advantages, IRS-aided communications have limitations as they are subject to high propagation losses. To overcome this, the phase rotation (shift) at each element needs to be designed in such a way as to increase the channel gain at the destination. However, this increases the system's complexity as well as its power consumption. In this paper, we present an analytical framework for the performance of random rotation-based IRS-aided communications. Under this framework, we propose four low-complexity and energy efficient schemes, based on a coding or a selection approach. Both of these approaches employ random phase rotations and require limited knowledge of channel state information. Specifically, the coding-based schemes use time-varying random phase rotations to produce an equivalent time-varying channel. On the other hand, the selection-based schemes select a partition of the IRS elements based on the received signal power at the destination. Analytical expressions for the achieved outage probability and energy efficiency of each scheme are derived. It is demonstrated that all schemes can provide significant performance gains as well as full diversity order.
Tag-less Back-Translation
Venue: arXiv cs.CL 2021
Year: 2021

An effective method to generate a large number of parallel sentences for training improved neural machine translation (NMT) systems is the use of the back-translations of the target-side monolingual data. The standard back-translation method has been shown to be unable to efficiently utilize the available huge amount of existing monolingual data because of the inability of translation models to differentiate between the authentic and synthetic parallel data during training. Tagging, or using gates, has been used to enable translation models to distinguish between synthetic and authentic data, improving standard back-translation and also enabling the use of iterative back-translation on language pairs that underperformed using standard back-translation. In this work, we approach back-translation as a domain adaptation problem, eliminating the need for explicit tagging. In the approach -- \emph{tag-less back-translation} -- the synthetic and authentic parallel data are treated as out-of-domain and in-domain data respectively and, through pre-training and fine-tuning, the translation model is shown to be able to learn more efficiently from them during training. Experimental results have shown that the approach outperforms the standard and tagged back-translation approaches on low resource English-Vietnamese and English-German neural machine translation.
Narrowing Down XML Template Expansion and Schema Validation
Venue: arXiv cs.LO 2021
Year: 2021

This work examines how much template instantiation can narrow down schema validation for XML-documents. First, instantiation and validation are formalised. Properties towards their practical meaning are probed, an implementation is developed. Requirements for an unification are elaborated and a comparison is taken out. The semantics are formulated in terms of denotational semantics as well as rule-based referring to the data models chosen. Formalisation makes it clearer instantiation is adequately represented. Both semantics show, that the rules set for both, instantiation and validation, cannot totally be unified. However, reuse of simplified code also simplifies unification. Implementation allows unification of both processes on document-level. The validity of all implementations is guaranteed by a comprehensive test suite. Analysis shows the minimal XML template language has got regular grammar properties, except macros. An explanation was given, why filters and arrows are not best, especially towards a unified language to be variable and extensive. Recommendations for future language design are provided. Instantiation shows a universal gap in applications, for instance, as seen by XSLT. Lack of expressibility of arbitrary functions in a schema is one such example, expressibility of the command language is another basic restriction. Useful unification constraints are found out to be handy, such as typing each slot. In order to obtain most flexibility out of command languages adaptations are required. An alternative to introducing constraints is the effective construction of special NFAs. Comparison criteria are introduced regarding mainly syntax and semantics. Comparisons is done accordingly. Despite its huge syntax definitions XSD was found weaker than RelaxNG or XML template language. As template language the latter is considered universal.
Computational framework for monolithic coupling for thin fluid flow in contact interfaces
Venue: arXiv cs.CE 2021
Year: 2021

We developed a computational framework for simulating thin fluid flow in narrow interfaces between contacting solids, which is relevant for a range of engineering, biological and geophysical applications. The treatment of this problem requires coupling between fluid and solid mechanics equations, further complicated by contact constraints and potentially complex geometrical features of contacting surfaces. We developed a monolithic finite-element framework for handling mechanical contact, thin incompressible viscous flow and fluid-induced tractions on the surface of the solid, suitable for both one- and two-way coupling approaches. Additionally, we consider the possibility of fluid entrapment in "pools" delimited by contact patches and its pressurisation following a non-linear compressibility constitutive law. Furthermore, image analysis algorithms were adapted to identify the local status of each interface element within the Newton-Raphson loop. First, an application of the proposed framework for a problem with a model geometry is given, and the robustness is demonstrated by the residual-wise and status-wise convergence. The full capability of the developed two-way coupling framework is demonstrated on a problem of a fluid flow in contact interface between a solid with representative rough surface and a rigid flat. The evolution of the contact pressure, fluid flow pattern and the morphology of trapped fluid zones until the complete sealing of the interface is displayed. Additionally, we demonstrated an almost mesh-independent result of a refined post-processing approach to the real contact-area computation. The developed framework permits not only to study the evolution of effective properties of contact interfaces, but also to highlight the difference between one- and two-way coupling approaches and to quantify the effect of multiple trapped fluid "pools" on the coupled problem.