OpenRaiser/Intern-Atlas huggingface dataset:
PolyAdd: Polynomial Formal Verification of Adder Circuits
Venue: arXiv cs.AR 2021
Year: 2021

Only by formal verification approaches functional correctness can be ensured. While for many circuits fast verification is possible, in other cases the approaches fail. In general no efficient algorithms can be given, since the underlying verification problem is NP-complete. In this paper we prove that for different types of adder circuits polynomial verification can be ensured based on BDDs. While it is known that the output functions for addition are polynomially bounded, we show in the following that the entire construction process can be carried out in polynomial time. This is shown for the simple Ripple Carry Adder, but also for fast adders like the Conditional Sum Adder and the Carry Look Ahead Adder. Properties about the adder function are proven and the core principle of polynomial verification is described that can also be extended to other classes of functions and circuit realizations.
Dual-constrained Deep Semi-Supervised Coupled Factorization Network with Enriched Prior
Venue: arXiv cs.LG 2021
Year: 2021

Nonnegative matrix factorization is usually powerful for learning the "shallow" parts-based representation, but it clearly fails to discover deep hierarchical information within both the basis and representation spaces. In this paper, we technically propose a new enriched prior based Dual-constrained Deep Semi-Supervised Coupled Factorization Network, called DS2CF-Net, for learning the hierarchical coupled representations. To ex-tract hidden deep features, DS2CF-Net is modeled as a deep-structure and geometrical structure-constrained neural network. Specifically, DS2CF-Net designs a deep coupled factorization architecture using multi-layers of linear transformations, which coupled updates the bases and new representations in each layer. To improve the discriminating ability of learned deep representations and deep coefficients, our network clearly considers enriching the supervised prior by the joint deep coefficients-regularized label prediction, and incorporates enriched prior information as additional label and structure constraints. The label constraint can enable the samples of the same label to have the same coordinate in the new feature space, while the structure constraint forces the coefficient matrices in each layer to be block-diagonal so that the enhanced prior using the self-expressive label propagation are more accurate. Our network also integrates the adaptive dual-graph learning to retain the local manifold structures of both the data manifold and feature manifold by minimizing the reconstruction errors in each layer. Extensive experiments on several real databases demonstrate that our DS2CF-Net can obtain state-of-the-art performance for representation learning and clustering.
Intraoperative Liver Surface Completion with Graph Convolutional VAE
Venue: arXiv cs.CV 2021
Year: 2021

In this work we propose a method based on geometric deep learning to predict the complete surface of the liver, given a partial point cloud of the organ obtained during the surgical laparoscopic procedure. We introduce a new data augmentation technique that randomly perturbs shapes in their frequency domain to compensate the limited size of our dataset. The core of our method is a variational autoencoder (VAE) that is trained to learn a latent space for complete shapes of the liver. At inference time, the generative part of the model is embedded in an optimisation procedure where the latent representation is iteratively updated to generate a model that matches the intraoperative partial point cloud. The effect of this optimisation is a progressive non-rigid deformation of the initially generated shape. Our method is qualitatively evaluated on real data and quantitatively evaluated on synthetic data. We compared with a state-of-the-art rigid registration algorithm, that our method outperformed in visible areas.
Low-Rank Training of Deep Neural Networks for Emerging Memory Technology
Venue: arXiv cs.LG 2021
Year: 2021

The recent success of neural networks for solving difficult decision tasks has incentivized incorporating smart decision making "at the edge." However, this work has traditionally focused on neural network inference, rather than training, due to memory and compute limitations, especially in emerging non-volatile memory systems, where writes are energetically costly and reduce lifespan. Yet, the ability to train at the edge is becoming increasingly important as it enables real-time adaptability to device drift and environmental variation, user customization, and federated learning across devices. In this work, we address two key challenges for training on edge devices with non-volatile memory: low write density and low auxiliary memory. We present a low-rank training scheme that addresses these challenges while maintaining computational efficiency. We then demonstrate the technique on a representative convolutional neural network across several adaptation problems, where it out-performs standard SGD both in accuracy and in number of weight writes.
Momentum-based Gradient Methods in Multi-Objective Recommendation
Venue: arXiv cs.LG 2021
Year: 2021

Multi-objective gradient methods are becoming the standard for solving multi-objective problems. Among others, they show promising results in developing multi-objective recommender systems with both correlated and conflicting objectives. Classic multi-gradient~descent usually relies on the combination of the gradients, not including the computation of first and second moments of the gradients. This leads to a brittle behavior and misses important areas in the solution space. In this work, we create a multi-objective model-agnostic Adamize method that leverages the benefits of the Adam optimizer in single-objective problems. This corrects and stabilizes~the~gradients of every objective before calculating a common gradient descent vector that optimizes all the objectives simultaneously. We evaluate the benefits of Multi-objective Adamize on two multi-objective recommender systems and for three different objective combinations, both correlated or conflicting. We report significant improvements, measured with three different Pareto front metrics: hypervolume, coverage, and spacing. Finally, we show that the \textit{Adamized} Pareto front strictly dominates the previous one on multiple objective pairs.
Tiered Random Matching Markets: Rank is Proportional to Popularity
Venue: arXiv cs.GT 2021
Year: 2021

We study the stable marriage problem in two-sided markets with randomly generated preferences. We consider agents on each side divided into a constant number of "soft tiers", which intuitively indicate the quality of the agent. Specifically, every agent within a tier has the same public score, and agents on each side have preferences independently generated proportionally to the public scores of the other side. We compute the expected average rank which agents in each tier have for their partners in the men-optimal stable matching, and prove concentration results for the average rank in asymptotically large markets. Furthermore, we show that despite having a significant effect on ranks, public scores do not strongly influence the probability of an agent matching to a given tier of the other side. This generalizes results of [Pittel 1989] which correspond to uniform preferences. The results quantitatively demonstrate the effect of competition due to the heterogeneous attractiveness of agents in the market, and we give the first explicit calculations of rank beyond uniform markets.
CounteRGAN: Generating Realistic Counterfactuals with Residual Generative Adversarial Nets
Venue: arXiv cs.LG 2021
Year: 2021

The prevalence of machine learning models in various industries has led to growing demands for model interpretability and for the ability to provide meaningful recourse to users. For example, patients hoping to improve their diagnoses or loan applicants seeking to increase their chances of approval. Counterfactuals can help in this regard by identifying input perturbations that would result in more desirable prediction outcomes. Meaningful counterfactuals should be able to achieve the desired outcome, but also be realistic, actionable, and efficient to compute. Current approaches achieve desired outcomes with moderate actionability but are severely limited in terms of realism and latency. To tackle these limitations, we apply Generative Adversarial Nets (GANs) toward counterfactual search. We also introduce a novel Residual GAN (RGAN) that helps to improve counterfactual realism and actionability compared to regular GANs. The proposed CounteRGAN method utilizes an RGAN and a target classifier to produce counterfactuals capable of providing meaningful recourse. Evaluations on two popular datasets highlight how the CounteRGAN is able to overcome the limitations of existing methods, including latency improvements of >50x to >90,000x, making meaningful recourse available in real-time and applicable to a wide range of domains.
Guessing Gr{ö}bner Bases of Structured Ideals of Relations of Sequences
Venue: arXiv cs.SC 2021
Year: 2021

Assuming sufficiently many terms of a n-dimensional table defined over a field are given, we aim at guessing the linear recurrence relations with either constant or polynomial coefficients they satisfy. In many applications, the table terms come along with a structure: for instance, they may be zero outside of a cone, they may be built from a Gr{ö}bner basis of an ideal invariant under the action of a finite group. Thus, we show how to take advantage of this structure to both reduce the number of table queries and the number of operations in the base field to recover the ideal of relations of the table. In applications like in combinatorics, where all these zero terms make us guess many fake relations, this allows us to drastically reduce these wrong guesses. These algorithms have been implemented and, experimentally, they let us handle examples that we could not manage otherwise. Furthermore, we show which kind of cone and lattice structures are preserved by skew polynomial multiplication. This allows us to speed up the guessing of linear recurrence relations with polynomial coefficients by computing sparse Gr{ö}bner bases or Gr{ö}bner bases of an ideal invariant under the action of a finite group in a ring of skew polynomials.
HECTOR-V: A Heterogeneous CPU Architecture for a Secure RISC-V Execution Environment
Venue: arXiv cs.CR 2021
Year: 2021

To ensure secure and trustworthy execution of applications, vendors frequently embed trusted execution environments into their systems. Here, applications are protected from adversaries, including a malicious operating system. TEEs are usually built by integrating protection mechanisms directly into the processor or by using dedicated external secure elements. However, both of these approaches only cover a narrow threat model resulting in limited security guarantees. Enclaves in the application processor typically provide weak isolation between the secure and non-secure domain, especially when considering side-channel attacks. Although secure elements do provide strong isolation, the slow communication interface to the application processor is exposed to adversaries and restricts the use cases. Independently of the used implementation approach, TEEs often lack the possibility to establish secure communication to external peripherals, and most operating systems executed inside TEEs do not provide state-of-the-art defense strategies, making them vulnerable against various attacks. We argue that TEEs implemented on the main application processor are insecure, especially when considering side-channel attacks. We demonstrate how a heterogeneous architecture can be utilized to realize a secure TEE design. We directly embed a processor into our architecture to provide strong isolation between the secure and non-secure domain. The tight coupling of TEE and REE enables HECTOR-V to provide mechanisms for establishing secure communication channels. We further introduce RISC-V Secure Co-Processor, a security-hardened processor tailored for TEEs. To secure applications executed inside the TEE, RVSCP provides control-flow integrity, rigorously restricts I/O accesses to certain execution states, and provides operating system services directly in hardware.
TREX: Tree-Ensemble Representer-Point Explanations
Venue: arXiv cs.LG 2021
Year: 2021

How can we identify the training examples that contribute most to the prediction of a tree ensemble? In this paper, we introduce TREX, an explanation system that provides instance-attribution explanations for tree ensembles, such as random forests and gradient boosted trees. TREX builds on the representer point framework previously developed for explaining deep neural networks. Since tree ensembles are non-differentiable, we define a kernel that captures the structure of the specific tree ensemble. By using this kernel in kernel logistic regression or a support vector machine, TREX builds a surrogate model that approximates the original tree ensemble. The weights in the kernel expansion of the surrogate model are used to define the global or local importance of each training example. Our experiments show that TREX's surrogate model accurately approximates the tree ensemble; its global importance weights are more effective in dataset debugging than the previous state-of-the-art; its explanations identify the most influential samples better than alternative methods under the remove and retrain evaluation framework; it runs orders of magnitude faster than alternative methods; and its local explanations can identify and explain errors due to domain mismatch.
Linear Shannon Capacity of Cayley Graphs
Venue: arXiv cs.IT 2021
Year: 2021

The Shannon capacity of a graph is a fundamental quantity in zero-error information theory measuring the rate of growth of independent sets in graph powers. Despite being well-studied, this quantity continues to hold several mysteries. Lovász famously proved that the Shannon capacity of $C_5$ (the 5-cycle) is at most $\sqrt{5}$ via his theta function. This bound is achieved by a simple linear code over $\mathbb{F}_5$ mapping $x \mapsto 2x$. This motivates the notion of linear Shannon capacity of graphs, which is the largest rate achievable when restricting oneself to linear codes. We give a simple proof based on the polynomial method that the linear Shannon capacity of $C_5$ is $\sqrt{5}$. Our method applies more generally to Cayley graphs over the additive group of finite fields $\mathbb{F}_q$, giving an upper bound on the linear Shannon capacity. We compare this bound to the Lovász theta function, showing that they match for self-complementary Cayley graphs (such as $C_5$), and that the bound is smaller in some cases. We also exhibit a quadratic gap between linear and general Shannon capacity for some graphs.
Generator Versus Segmentor: Pseudo-healthy Synthesis
Venue: arXiv cs.CV 2021
Year: 2021

This paper investigates the problem of pseudo-healthy synthesis that is defined as synthesizing a subject-specific pathology-free image from a pathological one. Recent approaches based on Generative Adversarial Network (GAN) have been developed for this task. However, these methods will inevitably fall into the trade-off between preserving the subject-specific identity and generating healthy-like appearances. To overcome this challenge, we propose a novel adversarial training regime, Generator versus Segmentor (GVS), to alleviate this trade-off by a divide-and-conquer strategy. We further consider the deteriorating generalization performance of the segmentor throughout the training and develop a pixel-wise weighted loss by muting the well-transformed pixels to promote it. Moreover, we propose a new metric to measure how healthy the synthetic images look. The qualitative and quantitative experiments on the public dataset BraTS demonstrate that the proposed method outperforms the existing methods. Besides, we also certify the effectiveness of our method on datasets LiTS. Our implementation and pre-trained networks are publicly available at https://github.com/Au3C2/Generator-Versus-Segmentor.
On the security of subspace subcodes of Reed-Solomon codes for public key encryption
Venue: arXiv cs.CR 2021
Year: 2021

This article discusses the security of McEliece-like encryption schemes using subspace subcodes of Reed-Solomon codes, i.e. subcodes of Reed-Solomon codes over $\mathbb{F}_{q^m}$ whose entries lie in a fixed collection of $\mathbb{F}_q$-subspaces of $\mathbb{F}_{q^m}$. These codes appear to be a natural generalisation of Goppa and alternant codes and provide a broader flexibility in designing code based encryption schemes. For the security analysis, we introduce a new operation on codes called the twisted product which yields a polynomial time distinguisher on such subspace subcodes as soon as the chosen $\mathbb{F}_q$-subspaces have dimension larger than $m/2$. From this distinguisher, we build an efficient attack which in particular breaks some parameters of a recent proposal due to Khathuria, Rosenthal and Weger.
ReviewViz: Assisting Developers Perform Empirical Study on Energy Consumption Related Reviews for Mobile Applications
Venue: arXiv cs.LG 2021
Year: 2021

Improving the energy efficiency of mobile applications is a topic that has gained a lot of attention recently. It has been addressed in a number of ways such as identifying energy bugs and developing a catalog of energy patterns. Previous work shows that users discuss the battery-related issues (energy inefficiency or energy consumption) of the apps in their reviews. However, there is no work that addresses the automatic extraction of battery-related issues from users' feedback. In this paper, we report on a visualization tool that is developed to empirically study machine learning algorithms and text features to automatically identify the energy consumption specific reviews with the highest accuracy. Other than the common machine learning algorithms, we utilize deep learning models with different word embeddings to compare the results. Furthermore, to help the developers extract the main topics that are discussed in the reviews, two states of the art topic modeling algorithms are applied. The visualizations of the topics represent the keywords that are extracted for each topic along with a comparison with the results of string matching. The developed web-browser based interactive visualization tool is a novel framework developed with the intention of giving the app developers insights about running time and accuracy of machine learning and deep learning models as well as extracted topics. The tool makes it easier for the developers to traverse through the extensive result set generated by the text classification and topic modeling algorithms. The dynamic-data structure used for the tool stores the baseline-results of the discussed approaches and is updated when applied on new datasets. The tool is open-sourced to replicate the research results.
A Survey of FPGA-Based Robotic Computing
Venue: arXiv cs.RO 2021
Year: 2021

Recent researches on robotics have shown significant improvement, spanning from algorithms, mechanics to hardware architectures. Robotics, including manipulators, legged robots, drones, and autonomous vehicles, are now widely applied in diverse scenarios. However, the high computation and data complexity of robotic algorithms pose great challenges to its applications. On the one hand, CPU platform is flexible to handle multiple robotic tasks. GPU platform has higher computational capacities and easy-touse development frameworks, so they have been widely adopted in several applications. On the other hand, FPGA-based robotic accelerators are becoming increasingly competitive alternatives, especially in latency-critical and power-limited scenarios. With specialized designed hardware logic and algorithm kernels, FPGA-based accelerators can surpass CPU and GPU in performance and energy efficiency. In this paper, we give an overview of previous work on FPGA-based robotic accelerators covering different stages of the robotic system pipeline. An analysis of software and hardware optimization techniques and main technical issues is presented, along with some commercial and space applications, to serve as a guide for future work.
Neural Networks Enhancement with Logical Knowledge
Venue: arXiv cs.LG 2021
Year: 2021

In the recent past, there has been a growing interest in Neural-Symbolic Integration frameworks, i.e., hybrid systems that integrate connectionist and symbolic approaches to obtain the best of both worlds. In a previous work, we proposed KENN (Knowledge Enhanced Neural Networks), a Neural-Symbolic architecture that injects prior logical knowledge into a neural network by adding a new final layer which modifies the initial predictions accordingly to the knowledge. Among the advantages of this strategy, there is the inclusion of clause weights, learnable parameters that represent the strength of the clauses, meaning that the model can learn the impact of each clause on the final predictions. As a special case, if the training data contradicts a constraint, KENN learns to ignore it, making the system robust to the presence of wrong knowledge. In this paper, we propose an extension of KENN for relational data. To evaluate this new extension, we tested it with different learning configurations on Citeseer, a standard dataset for Collective Classification. The results show that KENN is capable of increasing the performances of the underlying neural network even in the presence relational data, outperforming other two notable methods that combine learning with logic.
Temporal Answer Set Programming
Venue: arXiv cs.AI 2021
Year: 2021

We present an overview on Temporal Logic Programming under the perspective of its application for Knowledge Representation and declarative problem solving. Such programs are the result of combining usual rules with temporal modal operators, as in Linear-time Temporal Logic (LTL). We focus on recent results of the non-monotonic formalism called Temporal Equilibrium Logic (TEL) that is defined for the full syntax of LTL, but performs a model selection criterion based on Equilibrium Logic, a well known logical characterization of Answer Set Programming (ASP). We obtain a proper extension of the stable models semantics for the general case of arbitrary temporal formulas. We recall the basic definitions for TEL and its monotonic basis, the temporal logic of Here-and-There (THT), and study the differences between infinite and finite traces. We also provide other useful results, such as the translation into other formalisms like Quantified Equilibrium Logic or Second-order LTL, and some techniques for computing temporal stable models based on automata. In a second part, we focus on practical aspects, defining a syntactic fragment called temporal logic programs closer to ASP, and explain how this has been exploited in the construction of the solver TELINGO.