OpenRaiser/Intern-Atlas huggingface dataset:
Agent-based Constraint Solving for Resource Allocation in Manycore Systems
Venue: arXiv cs.MA 2022
Year: 2022

For efficiency reasons, manycore systems are increasingly heterogeneous, which makes the mapping of complex workloads a key problem with a high optimization potential. Constraints express the application requirements like which core type to choose, how many cores to choose, exclusively or non-exclusively, using a certain core, etc. In this work, we propose a decentralized solution for solving application resource constraints by means of an agent-based approach in order to obtain scalability. We translate the constraints into a Distributed Constraint Optimization Problem (DCOP) and propose a local search algorithm RESMGM to solve them. For the first time, we demonstrate the viability and efficiency of the DCOP approach for heterogeneous manycore systems. Our RESMGM algorithm supports a far wider range of constraints than state-of-the-art, leading to superior results, but still has comparable overheads w.r.t. computation and communication.
Formal Language Recognition by Hard Attention Transformers: Perspectives from Circuit Complexity
Venue: arXiv cs.CC 2022
Year: 2022

This paper analyzes three formal models of Transformer encoders that differ in the form of their self-attention mechanism: unique hard attention (UHAT); generalized unique hard attention (GUHAT), which generalizes UHAT; and averaging hard attention (AHAT). We show that UHAT and GUHAT Transformers, viewed as string acceptors, can only recognize formal languages in the complexity class AC$^0$, the class of languages recognizable by families of Boolean circuits of constant depth and polynomial size. This upper bound subsumes Hahn's (2020) results that GUHAT cannot recognize the DYCK languages or the PARITY language, since those languages are outside AC$^0$ (Furst et al., 1984). In contrast, the non-AC$^0$ languages MAJORITY and DYCK-1 are recognizable by AHAT networks, implying that AHAT can recognize languages that UHAT and GUHAT cannot.
A Natural Language Processing Approach for Instruction Set Architecture Identification
Venue: arXiv cs.CR 2022
Year: 2022

Binary analysis of software is a critical step in cyber forensics applications such as program vulnerability assessment and malware detection. This involves interpreting instructions executed by software and often necessitates converting the software's binary file data to assembly language. The conversion process requires information about the binary file's target instruction set architecture (ISA). However, ISA information might not be included in binary files due to compilation errors, partial downloads, or adversarial corruption of file metadata. Machine learning (ML) is a promising methodology that can be used to identify the target ISA using binary data in the object code section of binary files. In this paper we propose a binary code feature extraction model to improve the accuracy and scalability of ML-based ISA identification methods. Our feature extraction model can be used in the absence of domain knowledge about the ISAs. Specifically, we adapt models from natural language processing (NLP) to i) identify successive byte patterns commonly observed in binary codes, ii) estimate the significance of each byte pattern to a binary file, and iii) estimate the relevance of each byte pattern in distinguishing between ISAs. We introduce character-level features of encoded binaries to identify fine-grained bit patterns inherent to each ISA. We use a dataset with binaries from 12 different ISAs to evaluate our approach. Empirical evaluations show that using our byte-level features in ML-based ISA identification results in an 8% higher accuracy than the state-of-the-art features based on byte-histograms and byte pattern signatures. We observe that character-level features allow reducing the size of the feature set by up to 16x while maintaining accuracy above 97%.
METRO: Efficient Denoising Pretraining of Large Scale Autoencoding Language Models with Model Generated Signals
Venue: arXiv cs.LG 2022
Year: 2022

We present an efficient method of pretraining large-scale autoencoding language models using training signals generated by an auxiliary model. Originated in ELECTRA, this training strategy has demonstrated sample-efficiency to pretrain models at the scale of hundreds of millions of parameters. In this work, we conduct a comprehensive empirical study, and propose a recipe, namely "Model generated dEnoising TRaining Objective" (METRO), which incorporates some of the best modeling techniques developed recently to speed up, stabilize, and enhance pretrained language models without compromising model effectiveness. The resultant models, METRO-LM, consisting of up to 5.4 billion parameters, achieve new state-of-the-art on the GLUE, SuperGLUE, and SQuAD benchmarks. More importantly, METRO-LM are efficient in that they often outperform previous large models with significantly smaller model sizes and lower pretraining cost.
Copiloting Autonomous Multi-Robot Missions: A Game-inspired Supervisory Control Interface
Venue: arXiv cs.RO 2022
Year: 2022

Real-world deployment of new technology and capabilities can be daunting. The recent DARPA Subterranean (SubT) Challenge, for instance, aimed at the advancement of robotic platforms and autonomy capabilities in three one-year development pushes. While multi-agent systems are traditionally deployed in controlled and structured environments that allow for controlled testing (e.g., warehouses), the SubT challenge targeted various types of unknown underground environments that imposed the risk of robot loss in the case of failure. In this work, we introduce a video game-inspired interface, an autonomous mission assistant, and test and deploy these using a heterogeneous multi-agent system in challenging environments. This work leads to improved human-supervisory control for a multi-agent system reducing overhead from application switching, task planning, execution, and verification while increasing available exploration time with this human-autonomy teaming platform.
Second Order Regret Bounds Against Generalized Expert Sequences under Partial Bandit Feedback
Venue: arXiv cs.LG 2022
Year: 2022

We study the problem of expert advice under partial bandit feedback setting and create a sequential minimax optimal algorithm. Our algorithm works with a more general partial monitoring setting, where, in contrast to the classical bandit feedback, the losses can be revealed in an adversarial manner. Our algorithm adopts a universal prediction perspective, whose performance is analyzed with regret against a general expert selection sequence. The regret we study is against a general competition class that covers many settings (such as the switching or contextual experts settings) and the expert selection sequences in the competition class are determined by the application at hand. Our regret bounds are second order bounds in terms of the sum of squared losses and the normalized regret of our algorithm is invariant under arbitrary affine transforms of the loss sequence. Our algorithm is truly online and does not use any preliminary information about the loss sequences.
HASA: Hybrid Architecture Search with Aggregation Strategy for Echinococcosis Classification and Ovary Segmentation in Ultrasound Images
Venue: arXiv cs.CV 2022
Year: 2022

Different from handcrafted features, deep neural networks can automatically learn task-specific features from data. Due to this data-driven nature, they have achieved remarkable success in various areas. However, manual design and selection of suitable network architectures are time-consuming and require substantial effort of human experts. To address this problem, researchers have proposed neural architecture search (NAS) algorithms which can automatically generate network architectures but suffer from heavy computational cost and instability if searching from scratch. In this paper, we propose a hybrid NAS framework for ultrasound (US) image classification and segmentation. The hybrid framework consists of a pre-trained backbone and several searched cells (i.e., network building blocks), which takes advantage of the strengths of both NAS and the expert knowledge from existing convolutional neural networks. Specifically, two effective and lightweight operations, a mixed depth-wise convolution operator and a squeeze-and-excitation block, are introduced into the candidate operations to enhance the variety and capacity of the searched cells. These two operations not only decrease model parameters but also boost network performance. Moreover, we propose a re-aggregation strategy for the searched cells, aiming to further improve the performance for different vision tasks. We tested our method on two large US image datasets, including a 9-class echinococcosis dataset containing 9566 images for classification and an ovary dataset containing 3204 images for segmentation. Ablation experiments and comparison with other handcrafted or automatically searched architectures demonstrate that our method can generate more powerful and lightweight models for the above US image classification and segmentation tasks.
A van Benthem Theorem for Atomic and Molecular Logics
Venue: arXiv cs.LO 2022
Year: 2022

After recalling the definitions of atomic and molecular logics, we show how notions of bisimulation can be automatically defined from the truth conditions of the connectives of any of these logics. Then, we prove a generalization of van Benthem modal characterization theorem for molecular logics. Our molecular connectives should be uniform and contain all conjunctions and disjunctions. We use modal logic, the Lambek calculus and modal intuitionistic logic as case study and compare in particular our work with Olkhovikov's work.
Combining First-Order Classical and Intuitionistic Logic
Venue: arXiv cs.LO 2022
Year: 2022

This paper studies a first-order expansion of a combination C+J of intuitionistic and classical propositional logic, which was studied by Humberstone (1979) and del Cerro and Herzig (1996), from a proof-theoretic viewpoint. While C+J has both classical and intuitionistic implications, our first-order expansion adds classical and intuitionistic universal quantifiers and one existential quantifier to C+J. This paper provides a multi-succedent sequent calculus G(FOC+J) for our combination of the first-order intuitionistic and classical logic. Our sequent calculus G(FOC+J) restricts contexts of the right rules for intuitionistic implication and intuitionistic universal quantifier to particular forms of formulas. The cut-elimination theorem is established to ensure the subformula property. As a corollary, G(FOC+J) is conservative over both first-order intuitionistic and classical logic. Strong completeness of G(FOC+J) is proved via a canonical model argument.
Natural Deduction for Assertibility and Deniability
Venue: arXiv cs.LO 2022
Year: 2022

In this paper we split every basic propositional connective into two versions, one is called extensional and the other one intensional. The extensional connectives are semantically characterized by standard truth conditions that are relative to possible worlds. Assertibility and deniability of sentences built out of atomic sentences by extensional connectives are defined in terms of the notion of truth. The intensional connectives are characterized directly by assertibility and deniability conditions without the notion of truth. We pay special attention to the deniability condition for intensional implication. We characterize the logic of this mixed language by a system of natural deduction that sheds some light on the inferential behaviour of these two kinds of connectives and on the way they can interact.
Monadicity of Non-deterministic Logical Matrices is Undecidable
Venue: arXiv cs.LO 2022
Year: 2022

The notion of non-deterministic logical matrix (where connectives are interpreted as multi-functions) preserves many good properties of traditional semantics based on logical matrices (where connectives are interpreted as functions) whilst finitely characterizing a much wider class of logics, and has proven to be decisive in a myriad of recent compositional results in logic. Crucially, when a finite non-deterministic matrix satisfies monadicity (distinct truth-values can be separated by unary formulas) one can automatically produce an axiomatization of the induced logic. Furthermore, the resulting calculi are analytical and enable algorithmic proof-search and symbolic counter-model generation. For finite (deterministic) matrices it is well known that checking monadicity is decidable. We show that, in the presence of non-determinism, the property becomes undecidable. As a consequence, we conclude that there is no algorithm for computing the set of all multi-functions expressible in a given finite Nmatrix. The undecidability result is obtained by reduction from the halting problem for deterministic counter machines.
Routley Star in Information-Based Semantics
Venue: arXiv cs.LO 2022
Year: 2022

It is common in various non-classical logics, especially in relevant logics, to characterize negation semantically via the operation known as Routley star. This operation works well within relational semantic frameworks based on prime theories. We study this operation in the context of "information-based" semantics for which it is characteristic that sets of formulas supported by individual information states are theories that do not have to be prime. We will show that, somewhat surprisingly, the incorporation of Routley star into the information-based semantics does not lead to a collapse or a trivialization of the whole semantic system. On the contrary, it leads to a technically elegant though quite restricted semantic framework that determines a particular logic. We study some basic properties of this semantics. For example, we show that within this framework double negation law is valid only in involutive linear frames. We characterize axiomatically the logic of all linear frames and show that the logic of involutive linear frames coincides with a system that Mike Dunn coined Kalman logic. This logic is the fragment (for the language restricted to conjunction, disjunction and negation) of the "semi-relevant" logic known as R-mingle. Finally, we characterize by a deductive system the logic of all information frames equipped with Routley star.
Dunn Semantics for Contra-Classical Logics
Venue: arXiv cs.LO 2022
Year: 2022

In this paper I show, with a rich and systematized diet of examples, that many contra-classical logics can be presented as variants of FDE, obtained by modifying at least one of the truth or falsity conditions of some connective. Then I argue that using Dunn semantics provides a clear understanding of the source of contra-classicality, namely, connectives that have either the classical truth or the classical falsity condition of another connective. This requires a fine-grained analysis of the sorts of modifications that can be made to an evaluation condition, analysis which I offer here as well.
GLAD: Neural Predicate Synthesis to Repair Omission Faults
Venue: arXiv cs.SE 2022
Year: 2022

Existing template and learning-based APR tools have successfully found patches for many benchmark faults. However, our analysis of existing results shows that omission faults pose a significant challenge to these techniques. For template based approaches, omission faults provide no location to apply templates to; for learning based approaches that formulate repair as Neural Machine Translation (NMT), omission faults similarly do not provide the faulty code to translate. To address these issues, we propose GLAD, a novel learning-based repair technique that specifically targets if-clause synthesis. GLAD does not require a faulty line as it is based on generative Language Models (LMs) instead of machine translation; consequently, it can repair omission faults. GLAD intelligently constrains the language model using a type-based grammar. Further, it efficiently reduces the validation cost by performing dynamic ranking of candidate patches using a debugger. Thanks to the shift from translation to synthesis, GLAD is highly orthogonal to existing techniques: GLAD can correctly fix 16 Defects4J v1.2 faults that previous NMT-based techniques could not, while maintaining a reasonable runtime cost, underscoring its utility as an APR tool and potential to complement existing tools in practice. An inspection of the bugs that GLAD fixes reveals that GLAD can quickly generate expressions that would be challenging for other techniques.
A Feedback Capacity-Achieving Coding Scheme for the $(d,\infty)$-RLL Input-Constrained Binary Erasure Channel
Venue: arXiv cs.IT 2022
Year: 2022

This paper considers the memoryless input-constrained binary erasure channel (BEC). The channel input constraint is the $(d,\infty)$-runlength limited (RLL) constraint, which mandates that any pair of successive $1$s in the input sequence be separated by at least $d$ $0$s. We consider a scenario where there is causal, noiseless feedback from the decoder. We demonstrate a simple, labelling-based, zero-error feedback coding scheme, which we prove to be feedback capacity-achieving, and, as a by-product, obtain an explicit characterization of the feedback capacity. Our proof is based on showing that the rate of our feedback coding scheme equals an upper bound on the feedback capacity derived using the single-letter bounding techniques of Sabag et al. (2017). Further, we note using the tools of Thangaraj (2017) that there is a gap between the feedback and non-feedback capacities of the $(d,\infty)$-RLL input constrained BEC, at least for $d=1,2$.
Explainable Analysis of Deep Learning Methods for SAR Image Classification
Venue: arXiv cs.CV 2022
Year: 2022

Deep learning methods exhibit outstanding performance in synthetic aperture radar (SAR) image interpretation tasks. However, these are black box models that limit the comprehension of their predictions. Therefore, to meet this challenge, we have utilized explainable artificial intelligence (XAI) methods for the SAR image classification task. Specifically, we trained state-of-the-art convolutional neural networks for each polarization format on OpenSARUrban dataset and then investigate eight explanation methods to analyze the predictions of the CNN classifiers of SAR images. These XAI methods are also evaluated qualitatively and quantitatively which shows that Occlusion achieves the most reliable interpretation performance in terms of Max-Sensitivity but with a low-resolution explanation heatmap. The explanation results provide some insights into the internal mechanism of black-box decisions for SAR image classification.
An Exploratory Study of Attestation Mechanisms for Trusted Execution Environments
Venue: arXiv cs.CR 2022
Year: 2022

Attestation is a fundamental building block to establish trust over software systems. When used in conjunction with trusted execution environments, it guarantees that genuine code is executed even when facing strong attackers, paving the way for adoption in several sensitive application domains. This paper reviews existing remote attestation principles and compares the functionalities of current trusted execution environments as Intel SGX, Arm TrustZone and AMD SEV, as well as emerging RISC-V solutions.
Preliminary Results of a Survey on the Use of Self-Adaptation in Industry
Venue: arXiv cs.SE 2022
Year: 2022

Self-adaptation equips a software system with a feedback loop that automates tasks that otherwise need to be performed by operators. Such feedback loops have found their way to a variety of practical applications, one typical example is an elastic cloud. Yet, the state of the practice in self-adaptation is currently not clear. To get insights into the use of self-adaptation in practice, we are running a large-scale survey with industry. This paper reports preliminary results based on survey data that we obtained from 113 practitioners spread over 16 countries, 62 of them work with concrete self-adaptive systems. We highlight the main insights obtained so far: motivations for self-adaptation, concrete use cases, and difficulties encountered when applying self-adaptation in practice. We conclude the paper with outlining our plans for the remainder of the study.
The Vision of Self-Evolving Computing Systems
Venue: arXiv cs.SE 2022
Year: 2022

Computing systems are omnipresent; their sustainability has become crucial for our society. A key aspect of this sustainability is the ability of computing systems to cope with the continuous change they face, ranging from dynamic operating conditions, to changing goals, and technological progress. While we are able to engineer smart computing systems that autonomously deal with various types of changes, handling unanticipated changes requires system evolution, which remains in essence a human-centered process. This will eventually become unmanageable. To break through the status quo, we put forward an arguable opinion for the vision of self-evolving computing systems that are equipped with an evolutionary engine enabling them to evolve autonomously. Specifically, when a self-evolving computing system detects conditions outside its operational domain, such as an anomaly or a new goal, it activates an evolutionary engine that runs online experiments to determine how the system needs to evolve to deal with the changes, thereby evolving its architecture. During this process the engine can integrate new computing elements that are provided by computing warehouses. These computing elements provide specifications and procedures enabling their automatic integration. We motivate the need for self-evolving computing systems in light of the state of the art, outline a conceptual architecture of self-evolving computing systems, and illustrate the architecture for a future smart city mobility system that needs to evolve continuously with changing conditions. To conclude, we highlight key research challenges to realize the vision of self-evolving computing systems.
Double spending prevention of digital Euros using a web-of-trust
Venue: arXiv cs.CR 2022
Year: 2022

In order to provide more security on double-spending, we have implemented a system allowing for a web-of-trust. In this paper, we explore different approaches taken against double-spending and implement our own version to avoid this within TrustChain as part of the ecosystem of EuroToken, the digital version of the euro. We have used the EVA protocol as a means to transfer data between users, building on the existing functionality of transferring money between users. This allows the sender of EuroTokens to leave recommendations of users based on their previous interactions with other users. This dissemination of trust through the network allows users to make more trustworthy decisions. Although this provides an upgrade in terms of usability, the mathematical details of our implementation can be explored further in other research.