OpenRaiser/Intern-Atlas huggingface dataset:
Weighted Model Counting in the two variable fragment with Cardinality Constraints: A Closed Form Formula
Venue: arXiv cs.AI 2021
Year: 2021

Weighted First-Order Model Counting (WFOMC) computes the weighted sum of the models of a first-order theory on a given finite domain. WFOMC has emerged as a fundamental tool for probabilistic inference. Algorithms for WFOMC that run in polynomial time w.r.t. the domain size are called lifted inference algorithms. Such algorithms have been developed for multiple extensions of FO2(the fragment of first-order logic with two variables) for the special case of symmetric weight functions. We introduce the concept of lifted interpretations as a tool for formulating polynomials for WFOMC. Using lifted interpretations, we reconstruct the closed-form formula for polynomial-time FOMC in the universal fragment of FO2, earlier proposed by Beame et al. We then expand this closed-form to incorporate existential quantifiers and cardinality constraints without losing domain-liftability. Finally, we show that the obtained closed-form motivates a natural definition of a family of weight functions strictly larger than symmetric weight functions.
Trace-Checking CPS Properties: Bridging the Cyber-Physical Gap
Venue: arXiv cs.SE 2021
Year: 2021

Cyber-physical systems combine software and physical components. Specification-driven trace-checking tools for CPS usually provide users with a specification language to express the requirements of interest, and an automatic procedure to check whether these requirements hold on the execution traces of a CPS. Although there exist several specification languages for CPS, they are often not sufficiently expressive to allow the specification of complex CPS properties related to the software and the physical components and their interactions. In this paper, we propose (i) the Hybrid Logic of Signals (HLS), a logic-based language that allows the specification of complex CPS requirements, and (ii) ThEodorE, an efficient SMT-based trace-checking procedure. This procedure reduces the problem of checking a CPS requirement over an execution trace, to checking the satisfiability of an SMT formula. We evaluated our contributions by using a representative industrial case study in the satellite domain. We assessed the expressiveness of HLS by considering 212 requirements of our case study. HLS could express all the 212 requirements. We also assessed the applicability of ThEodorE by running the trace-checking procedure for 747 trace-requirement combinations. ThEodorE was able to produce a verdict in 74.5% of the cases. Finally, we compared HLS and ThEodorE with other specification languages and trace-checking tools from the literature. Our results show that, from a practical standpoint, our approach offers a better trade-off between expressiveness and performance.
On the Approximability of Robust Network Design
Venue: arXiv cs.CC 2021
Year: 2021

Given the dynamic nature of traffic, we investigate the variant of robust network design where we have to determine the capacity to reserve on each link so that each demand vector belonging to a polyhedral set can be routed. The objective is either to minimize congestion or a linear cost. Routing is assumed to be fractional and dynamic (i.e., dependent on the current traffic vector). We first prove that the robust network design problem with minimum congestion cannot be approximated within any constant factor. Then, using the ETH conjecture, we get a $Ω(\frac{\log n}{\log \log n})$ lower bound for the approximability of this problem. This implies that the well-known $O(\log n)$ approximation ratio established by Räcke in 2008 is tight. Using Lagrange relaxation, we obtain a new proof of the $O(\log n)$ approximation. An important consequence of the Lagrange-based reduction and our inapproximability results is that the robust network design problem with linear reservation cost cannot be approximated within any constant ratio. This answers a long-standing open question of Chekuri (2007). We also give another proof of the result of Goyal\&al (2009) stating that the optimal linear cost under static routing can be $Ω(\log n)$ more expensive than the cost obtained under dynamic routing. Finally, we show that even if only two given paths are allowed for each commodity, the robust network design problem with minimum congestion or linear cost is hard to approximate within some constant.
Cross-individual Recognition of Emotions by a Dynamic Entropy based on Pattern Learning with EEG features
Venue: arXiv cs.LG 2021
Year: 2021

Use of the electroencephalogram (EEG) and machine learning approaches to recognize emotions can facilitate affective human computer interactions. However, the type of EEG data constitutes an obstacle for cross-individual EEG feature modelling and classification. To address this issue, we propose a deep-learning framework denoted as a dynamic entropy-based pattern learning (DEPL) to abstract informative indicators pertaining to the neurophysiological features among multiple individuals. DEPL enhanced the capability of representations generated by a deep convolutional neural network by modelling the interdependencies between the cortical locations of dynamical entropy based features. The effectiveness of the DEPL has been validated with two public databases, commonly referred to as the DEAP and MAHNOB-HCI multimodal tagging databases. Specifically, the leave one subject out training and testing paradigm has been applied. Numerous experiments on EEG emotion recognition demonstrate that the proposed DEPL is superior to those traditional machine learning (ML) methods, and could learn between electrode dependencies w.r.t. different emotions, which is meaningful for developing the effective human-computer interaction systems by adapting to human emotions in the real world applications.
A Primal-Dual Subgradient Approachfor Fair Meta Learning
Venue: arXiv cs.LG 2021
Year: 2021

The problem of learning to generalize to unseen classes during training, known as few-shot classification, has attracted considerable attention. Initialization based methods, such as the gradient-based model agnostic meta-learning (MAML), tackle the few-shot learning problem by "learning to fine-tune". The goal of these approaches is to learn proper model initialization, so that the classifiers for new classes can be learned from a few labeled examples with a small number of gradient update steps. Few shot meta-learning is well-known with its fast-adapted capability and accuracy generalization onto unseen tasks. Learning fairly with unbiased outcomes is another significant hallmark of human intelligence, which is rarely touched in few-shot meta-learning. In this work, we propose a Primal-Dual Fair Meta-learning framework, namely PDFM, which learns to train fair machine learning models using only a few examples based on data from related tasks. The key idea is to learn a good initialization of a fair model's primal and dual parameters so that it can adapt to a new fair learning task via a few gradient update steps. Instead of manually tuning the dual parameters as hyperparameters via a grid search, PDFM optimizes the initialization of the primal and dual parameters jointly for fair meta-learning via a subgradient primal-dual approach. We further instantiate examples of bias controlling using mean difference and decision boundary covariance as fairness constraints to each task for supervised regression and classification, respectively. We demonstrate the versatility of our proposed approach by applying our approach to various real-world datasets. Our experiments show substantial improvements over the best prior work for this setting.
f-Divergence Variational Inference
Venue: arXiv cs.LG 2021
Year: 2021

This paper introduces the $f$-divergence variational inference ($f$-VI) that generalizes variational inference to all $f$-divergences. Initiated from minimizing a crafty surrogate $f$-divergence that shares the statistical consistency with the $f$-divergence, the $f$-VI framework not only unifies a number of existing VI methods, e.g. Kullback-Leibler VI, Rényi's $α$-VI, and $χ$-VI, but offers a standardized toolkit for VI subject to arbitrary divergences from $f$-divergence family. A general $f$-variational bound is derived and provides a sandwich estimate of marginal likelihood (or evidence). The development of the $f$-VI unfolds with a stochastic optimization scheme that utilizes the reparameterization trick, importance weighting and Monte Carlo approximation; a mean-field approximation scheme that generalizes the well-known coordinate ascent variational inference (CAVI) is also proposed for $f$-VI. Empirical examples, including variational autoencoders and Bayesian neural networks, are provided to demonstrate the effectiveness and the wide applicability of $f$-VI.
STR: Secure Computation on Additive Shares Using the Share-Transform-Reveal Strategy
Venue: arXiv cs.CR 2021
Year: 2021

The rapid development of cloud computing has probably benefited each of us. However, the privacy risks brought by untrustworthy cloud servers arise the attention of more and more people and legislatures. In the last two decades, plenty of works seek to outsource various specific tasks while ensuring the security of private data. The tasks to be outsourced are countless; however, the computations involved are similar. In this paper, we construct a series of novel protocols that support the secure computation of various functions on numbers (e.g., the basic elementary functions) and matrices (e.g., the calculation of eigenvectors and eigenvalues) in arbitrary $n\geq 2$ servers. All protocols only require constant rounds of interactions and achieve the low computation complexity. Moreover, the proposed $n$-party protocols ensure the security of private data even though $n-1$ servers collude. The convolutional neural network models are utilized as the case studies to verify the protocols. The theoretical analysis and experimental results demonstrate the correctness, efficiency, and security of the proposed protocols.
Analysis of IoT-Based Load Altering Attacks Against Power Grids Using the Theory of Second-Order Dynamical Systems
Venue: arXiv cs.CR 2021
Year: 2021

Recent research has shown that large-scale Internet of Things (IoT)-based load altering attacks can have a serious impact on power grid operations such as causing unsafe frequency excursions and destabilizing the grid's control loops. In this work, we present an analytical framework to investigate the impact of IoT-based static/dynamic load altering attacks (S/DLAAs) on the power grid's dynamic response. Existing work on this topic has mainly relied on numerical simulations and, to date, there is no analytical framework to identify the victim nodes from which that attacker can launch the most impactful attacks. To address these shortcomings, we use results from second-order dynamical systems to analyze the power grid frequency control loop under S/DLAAs. We use parametric sensitivity of the system's eigensolutions to identify victim nodes that correspond to the least-effort destabilizing DLAAs. Further, to analyze the SLAAs, we present closed-form expression for the system's frequency response in terms of the attacker's inputs, helping us characterize the minimum load change required to cause unsafe frequency excursions. Using these results, we formulate the defense against S/DLAAs as a linear programming problem in which we determine the minimum amount of load that needs to be secured at the victim nodes to ensure system safety/stability. Extensive simulations conducted using benchmark IEEE-bus systems validate the accuracy and efficacy of our approach.
Extendible and Efficient Python Framework for Solving Evolution Equations with Stabilized Discontinuous Galerkin Method
Venue: arXiv cs.MS 2021
Year: 2021

This paper discusses a Python interface for the recently published DUNE-FEM-DG module which provides highly efficient implementations of the Discontinuous Galerkin (DG) method for solving a wide range of non linear partial differential equations (PDE). Although the C++ interfaces of DUNE-FEM-DG are highly flexible and customizable, a solid knowledge of C++ is necessary to make use of this powerful tool. With this work easier user interfaces based on Python and the Unified Form Language are provided to open DUNE-FEM-DG for a broader audience. The Python interfaces are demonstrated for both parabolic and first order hyperbolic PDEs.
A Human-in-the-Loop Approach based on Explainability to Improve NTL Detection
Venue: arXiv cs.LG 2021
Year: 2021

Implementing systems based on Machine Learning to detect fraud and other Non-Technical Losses (NTL) is challenging: the data available is biased, and the algorithms currently used are black-boxes that cannot be either easily trusted or understood by stakeholders. This work explains our human-in-the-loop approach to mitigate these problems in a real system that uses a supervised model to detect Non-Technical Losses (NTL) for an international utility company from Spain. This approach exploits human knowledge (e.g. from the data scientists or the company's stakeholders) and the information provided by explanatory methods to guide the system during the training process. This simple, efficient method that can be easily implemented in other industrial projects is tested in a real dataset and the results show that the derived prediction model is better in terms of accuracy, interpretability, robustness and flexibility.
STRATA: Simple, Gradient-Free Attacks for Models of Code
Venue: arXiv cs.LG 2021
Year: 2021

Neural networks are well-known to be vulnerable to imperceptible perturbations in the input, called adversarial examples, that result in misclassification. Generating adversarial examples for source code poses an additional challenge compared to the domains of images and natural language, because source code perturbations must retain the functional meaning of the code. We identify a striking relationship between token frequency statistics and learned token embeddings: the L2 norm of learned token embeddings increases with the frequency of the token except for the highest-frequnecy tokens. We leverage this relationship to construct a simple and efficient gradient-free method for generating state-of-the-art adversarial examples on models of code. Our method empirically outperforms competing gradient-based methods with less information and less computational effort.
The Grey Hoodie Project: Big Tobacco, Big Tech, and the threat on academic integrity
Venue: arXiv cs.CY 2021
Year: 2021

As governmental bodies rely on academics' expert advice to shape policy regarding Artificial Intelligence, it is important that these academics not have conflicts of interests that may cloud or bias their judgement. Our work explores how Big Tech can actively distort the academic landscape to suit its needs. By comparing the well-studied actions of another industry (Big Tobacco) to the current actions of Big Tech we see similar strategies employed by both industries. These strategies enable either industry to sway and influence academic and public discourse. We examine the funding of academic research as a tool used by Big Tech to put forward a socially responsible public image, influence events hosted by and decisions made by funded universities, influence the research questions and plans of individual scientists, and discover receptive academics who can be leveraged. We demonstrate how Big Tech can affect academia from the institutional level down to individual researchers. Thus, we believe that it is vital, particularly for universities and other institutions of higher learning, to discuss the appropriateness and the tradeoffs of accepting funding from Big Tech, and what limitations or conditions should be put in place.
A Comprehensive Review for MRF and CRF Approaches in Pathology Image Analysis
Venue: arXiv cs.CV 2021
Year: 2021

Pathology image analysis is an essential procedure for clinical diagnosis of many diseases. To boost the accuracy and objectivity of detection, nowadays, an increasing number of computer-aided diagnosis (CAD) system is proposed. Among these methods, random field models play an indispensable role in improving the analysis performance. In this review, we present a comprehensive overview of pathology image analysis based on the markov random fields (MRFs) and conditional random fields (CRFs), which are two popular random field models. Firstly, we introduce the background of two random fields and pathology images. Secondly, we summarize the basic mathematical knowledge of MRFs and CRFs from modelling to optimization. Then, a thorough review of the recent research on the MRFs and CRFs of pathology images analysis is presented. Finally, we investigate the popular methodologies in the related works and discuss the method migration among CAD field.
Trust-Region Method with Deep Reinforcement Learning in Analog Design Space Exploration
Venue: arXiv cs.LG 2021
Year: 2021

This paper introduces new perspectives on analog design space search. To minimize the time-to-market, this endeavor better cast as constraint satisfaction problem than global optimization defined in prior arts. We incorporate model-based agents, contrasted with model-free learning, to implement a trust-region strategy. As such, simple feed-forward networks can be trained with supervised learning, where the convergence is relatively trivial. Experiment results demonstrate orders of magnitude improvement on search iterations. Additionally, the unprecedented consideration of PVT conditions are accommodated. On circuits with TSMC 5/6nm process, our method achieve performance surpassing human designers. Furthermore, this framework is in production in industrial settings.
Fast Gravitational Approach for Rigid Point Set Registration with Ordinary Differential Equations
Venue: arXiv cs.CV 2021
Year: 2021

This article introduces a new physics-based method for rigid point set alignment called Fast Gravitational Approach (FGA). In FGA, the source and target point sets are interpreted as rigid particle swarms with masses interacting in a globally multiply-linked manner while moving in a simulated gravitational force field. The optimal alignment is obtained by explicit modeling of forces acting on the particles as well as their velocities and displacements with second-order ordinary differential equations of motion. Additional alignment cues (point-based or geometric features, and other boundary conditions) can be integrated into FGA through particle masses. We propose a smooth-particle mass function for point mass initialization, which improves robustness to noise and structural discontinuities. To avoid prohibitive quadratic complexity of all-to-all point interactions, we adapt a Barnes-Hut tree for accelerated force computation and achieve quasilinear computational complexity. We show that the new method class has characteristics not found in previous alignment methods such as efficient handling of partial overlaps, inhomogeneous point sampling densities, and coping with large point clouds with reduced runtime compared to the state of the art. Experiments show that our method performs on par with or outperforms all compared competing non-deep-learning-based and general-purpose techniques (which do not assume the availability of training data and a scene prior) in resolving transformations for LiDAR data and gains state-of-the-art accuracy and speed when coping with different types of data disturbances.
Backpropagating through Fréchet Inception Distance
Venue: arXiv cs.LG 2021
Year: 2021

The Fréchet Inception Distance (FID) has been used to evaluate hundreds of generative models. We introduce FastFID, which can efficiently train generative models with FID as a loss function. Using FID as an additional loss for Generative Adversarial Networks improves their FID.
Task-Based Analog-to-Digital Converters
Venue: arXiv cs.IT 2021
Year: 2021

Obtaining digital representations of multivariate continuous-time (CT) signals is a challenge encountered in many signal processing systems. In practice, these signals are often acquired to extract some underlying information, i.e., for a specific task. Employing conventional task-agnostic analog-to-digital converters (ADCs), typically designed to minimize the mean squared error (MSE) in reconstructing the CT input signal, can be costly and energy-inefficient in such cases. In this work, we study task-based ADCs, which are designed to obtain a digital representation of a multivariate CT input process with the goal of recovering an underlying statistically related parameter vector, referred to as \emph{the task}. The proposed system employs analog filtering, uniform sampling, and scalar uniform quantization of the input process before recovering the task vector using a linear digital recovery filter. We optimize the analog and digital filters and derive closed-form expressions for the achievable MSE in recovering the task vector from a set of analog signals when utilizing ADCs with a fixed sampling rate and amplitude resolution. Based on our derivation, we provide guidelines for designing practical acquisition systems subject to a constraint on the bit rate. Our analysis proves that the intuitive approaches of either recovering the task vector solely in digital or designing the analog filter to estimate the task vector are inferior to the proposed joint design. We then consider the recovery of a set of matched filter outputs under a rate budget. We numerically verify our theoretical observations and demonstrate that task-based ADCs substantially outperform analog matched filtering as well as applying the matched filter solely in the digital domain. [...]
A Fine-Grained View on Stable Many-To-One Matching Problems with Lower and Upper Quotas
Venue: arXiv cs.GT 2021
Year: 2021

In the Hospital Residents problem with lower and upper quotas ($HR-Q^U_L$), the goal is to find a stable matching of residents to hospitals where the number of residents matched to a hospital is either between its lower and upper quota or zero [Biró et al., TCS 2010]. We analyze this problem from a parameterized perspective using several natural parameters such as the number of hospitals and the number of residents. Moreover, we present a polynomial-time algorithm that finds a stable matching if it exists on instances with maximum lower quota two. Alongside $HR-Q^U_L$, we also consider two closely related models of independent interest, namely, the special case of $HR-Q^U_L$ where each hospital has only a lower quota but no upper quota and the variation of $HR-Q^U_L$ where hospitals do not have preferences over residents, which is also known as the House Allocation problem with lower and upper quotas. Lastly, we investigate how the parameterized complexity of these three models changes if preferences may contain ties.