OpenRaiser/Intern-Atlas huggingface dataset:
Interactive Visualization of Saturation Attempts in Vampire
Venue: arXiv cs.LO 2020
Year: 2020

Many applications of formal methods require automated reasoning about system properties, such as system safety and security. To improve the performance of automated reasoning engines, such as SAT/SMT solvers and first-order theorem prover, it is necessary to understand both the successful and failing attempts of these engines towards producing formal certificates, such as logical proofs and/or models. Such an analysis is challenging due to the large number of logical formulas generated during proof/model search. In this paper we focus on saturation-based first-order theorem proving and introduce the SATVIS tool for interactively visualizing saturation-based proof attempts in first-order theorem proving. We build SATVIS on top of the world-leading theorem prover VAMPIRE, by interactively visualizing the saturation attempts of VAMPIRE in SATVIS. Our work combines the automatic layout and visualization of the derivation graph induced by the saturation attempt with interactive transformations and search functionality. As a result, we are able to analyze and debug (failed) proof attempts of VAMPIRE. Thanks to its interactive visualisation, we believe SATVIS helps both experts and non-experts in theorem proving to understand first-order proofs and analyze/refine failing proof attempts of first-order provers.
On fast multiplication of a matrix by its transpose
Venue: arXiv cs.SC 2020
Year: 2020

We present a non-commutative algorithm for the multiplication of a 2x2-block-matrix by its transpose using 5 block products (3 recursive calls and 2 general products) over C or any finite field.We use geometric considerations on the space of bilinear forms describing 2x2 matrix products to obtain this algorithm and we show how to reduce the number of involved additions.The resulting algorithm for arbitrary dimensions is a reduction of multiplication of a matrix by its transpose to general matrix product, improving by a constant factor previously known reductions.Finally we propose schedules with low memory footprint that support a fast and memory efficient practical implementation over a finite field.To conclude, we show how to use our result in LDLT factorization.
Impact of Spatial Multiplexing on the Throughput of Ultra-Dense mmWave AP Networks
Venue: arXiv cs.IT 2020
Year: 2020

The operating range of a single millimeter wave (mmWave) access point (AP) is small due to the high path loss and blockage issues of the frequency band. To achieve the coverage similar to conventional sub-6GHz networks, the ultra-dense deployments of APs are required by the mmWave network. In general, the mmWave APs can be categorized into backhaul-connected APs and relay APs. Though the spatial distribution of backhaul-connected APs can be captured by the Poison point process (PPP), the desired locations of relay APs depend on the transmission protocol operated in the mmWave network. In this paper, we consider modeling the topology of mmWave AP network by incorporating the multihop protocol. We first derive the topology of AP network with the spatial multiplexing disabled for each transmission hop. Then we analyze the topology when the spatial multiplexing is enabled at the mmWave APs. To derive the network throughput, we first quantify the improvement in latency and the degradation of coverage probability with the increase of spatial multiplexing gain at mmWave APs. Then we show the impact of spatial multiplexing on the throughput for the ultra-dense mmWave AP network.
A Bayesian Filter for Multi-view 3D Multi-object Tracking with Occlusion Handling
Venue: arXiv cs.CV 2020
Year: 2020

This paper proposes an online multi-camera multi-object tracker that only requires monocular detector training, independent of the multi-camera configurations, allowing seamless extension/deletion of cameras without retraining effort. The proposed algorithm has a linear complexity in the total number of detections across the cameras, and hence scales gracefully with the number of cameras. It operates in the 3D world frame, and provides 3D trajectory estimates of the objects. The key innovation is a high fidelity yet tractable 3D occlusion model, amenable to optimal Bayesian multi-view multi-object filtering, which seamlessly integrates, into a single Bayesian recursion, the sub-tasks of track management, state estimation, clutter rejection, and occlusion/misdetection handling. The proposed algorithm is evaluated on the latest WILDTRACKS dataset, and demonstrated to work in very crowded scenes on a new dataset.
Memorizing Comprehensively to Learn Adaptively: Unsupervised Cross-Domain Person Re-ID with Multi-level Memory
Venue: arXiv cs.CV 2020
Year: 2020

Unsupervised cross-domain person re-identification (Re-ID) aims to adapt the information from the labelled source domain to an unlabelled target domain. Due to the lack of supervision in the target domain, it is crucial to identify the underlying similarity-and-dissimilarity relationships among the unlabelled samples in the target domain. In order to use the whole data relationships efficiently in mini-batch training, we apply a series of memory modules to maintain an up-to-date representation of the entire dataset. Unlike the simple exemplar memory in previous works, we propose a novel multi-level memory network (MMN) to discover multi-level complementary information in the target domain, relying on three memory modules, i.e., part-level memory, instance-level memory, and domain-level memory. The proposed memory modules store multi-level representations of the target domain, which capture both the fine-grained differences between images and the global structure for the holistic target domain. The three memory modules complement each other and systematically integrate multi-level supervision from bottom to up. Experiments on three datasets demonstrate that the multi-level memory modules cooperatively boost the unsupervised cross-domain Re-ID task, and the proposed MMN achieves competitive results.
NimbRo Logistics -- Project KittingBot
Venue: arXiv cs.RO 2020
Year: 2020

Recovering the pose of an object from mere point clouds is often hindered by the lack of the information that they provide. In this lab, we address this problem by proposing a method that exploits the symmetry of objects as well as using pictures taken from a static camera of the same scene. We apply this approach to detects nuts in a table top scene that includes screws, nuts, washers and several placeholders for grasp planning.
WICA: nonlinear weighted ICA
Venue: arXiv cs.LG 2020
Year: 2020

Independent Component Analysis (ICA) aims to find a coordinate system in which the components of the data are independent. In this paper we construct a new nonlinear ICA model, called WICA, which obtains better and more stable results than other algorithms. A crucial tool is given by a new efficient method of verifying nonlinear dependence with the use of computation of correlation coefficients for normally weighted data. In addition, authors propose a new baseline nonlinear mixing to perform comparable experiments, and a~reliable measure which allows fair comparison of nonlinear models. Our code for WICA is available on Github https://github.com/gmum/wica.
Separating Content from Style Using Adversarial Learning for Recognizing Text in the Wild
Venue: arXiv cs.CV 2020
Year: 2020

We propose to improve text recognition from a new perspective by separating the text content from complex backgrounds. As vanilla GANs are not sufficiently robust to generate sequence-like characters in natural images, we propose an adversarial learning framework for the generation and recognition of multiple characters in an image. The proposed framework consists of an attention-based recognizer and a generative adversarial architecture. Furthermore, to tackle the issue of lacking paired training samples, we design an interactive joint training scheme, which shares attention masks from the recognizer to the discriminator, and enables the discriminator to extract the features of each character for further adversarial training. Benefiting from the character-level adversarial training, our framework requires only unpaired simple data for style supervision. Each target style sample containing only one randomly chosen character can be simply synthesized online during the training. This is significant as the training does not require costly paired samples or character-level annotations. Thus, only the input images and corresponding text labels are needed. In addition to the style normalization of the backgrounds, we refine character patterns to ease the recognition task. A feedback mechanism is proposed to bridge the gap between the discriminator and the recognizer. Therefore, the discriminator can guide the generator according to the confusion of the recognizer, so that the generated patterns are clearer for recognition. Experiments on various benchmarks, including both regular and irregular text, demonstrate that our method significantly reduces the difficulty of recognition. Our framework can be integrated into recent recognition methods to achieve new state-of-the-art recognition accuracy.
State Representation and Polyomino Placement for the Game Patchwork
Venue: arXiv cs.AI 2020
Year: 2020

Modern board games are a rich source of entertainment for many people, but also contain interesting and challenging structures for game playing research and implementing game playing agents. This paper studies the game Patchwork, a two player strategy game using polyomino tile drafting and placement. The core polyomino placement mechanic is implemented in a constraint model using regular constraints, extending and improving the model in (Lagerkvist, Pesant, 2008) with: explicit rotation handling; optional placements; and new constraints for resource usage. Crucial for implementing good game playing agents is to have great heuristics for guiding the search when faced with large branching factors. This paper divides placing tiles into two parts: a policy used for placing parts and an evaluation used to select among different placements. Policies are designed based on classical packing literature as well as common standard constraint programming heuristics. For evaluation, global propagation guided regret is introduced, choosing placements based on not ruling out later placements. Extensive evaluations are performed, showing the importance of using a good evaluation and that the proposed global propagation guided regret is a very effective guide.
TunnelScatter: Low Power Communication for Sensor Tags using Tunnel Diodes
Venue: arXiv cs.NI 2020
Year: 2020

Due to extremely low power consumption, backscatter has become the transmission mechanism of choice for battery-free devices that operate on harvested energy. However, a limitation of recent backscatter systems is that the communication range scales with the strength of the ambient carrier signal(ACS). This means that to achieve a long range, a backscatter tag needs to reflect a strong ACS, which in practice means that it needs to be close to an ACS emitter. We present TunnelScatter, a mechanism that overcomes this limitation. TunnelScatter uses a tunnel diode-based radio frequency oscillator to enable transmissions when there is no ACS, and the same oscillator as a reflection amplifier to support backscatter transmissions when the ACS is weak. Our results show that even without an ACS, TunnelScatter is able to transmit through several walls covering a distance of 18 meter while consuming a peak biasing power of 57 microwatts. Based on TunnelScatter, we design battery-free sensor tags, called TunnelTags, that can sense physical phenomena and transmit them using the TunnelScatter mechanism.
Fast-Fourier-Forecasting Resource Utilisation in Distributed Systems
Venue: arXiv cs.DC 2020
Year: 2020

Distributed computing systems often consist of hundreds of nodes, executing tasks with different resource requirements. Efficient resource provisioning and task scheduling in such systems are non-trivial and require close monitoring and accurate forecasting of the state of the system, specifically resource utilisation at its constituent machines. Two challenges present themselves towards these objectives. First, collecting monitoring data entails substantial communication overhead. This overhead can be prohibitively high, especially in networks where bandwidth is limited. Second, forecasting models to predict resource utilisation should be accurate and need to exhibit high inference speed. Mission critical scheduling and resource allocation algorithms use these predictions and rely on their immediate availability. To address the first challenge, we present a communication-efficient data collection mechanism. Resource utilisation data is collected at the individual machines in the system and transmitted to a central controller in batches. Each batch is processed by an adaptive data-reduction algorithm based on Fourier transforms and truncation in the frequency domain. We show that the proposed mechanism leads to a significant reduction in communication overhead while incurring only minimal error and adhering to accuracy guarantees. To address the second challenge, we propose a deep learning architecture using complex Gated Recurrent Units to forecast resource utilisation. This architecture is directly integrated with the above data collection mechanism to improve inference speed of our forecasting model. Using two real-world datasets, we demonstrate the effectiveness of our approach, both in terms of forecasting accuracy and inference speed. Our approach resolves challenges encountered in resource provisioning frameworks and can be applied to other forecasting problems.
Tabled Typeclass Resolution
Venue: arXiv cs.PL 2020
Year: 2020

Typeclasses provide an elegant and effective way of managing ad-hoc polymorphism in both programming languages and interactive proof assistants. However, the increasingly sophisticated uses of typeclasses within proof assistants, especially within Lean's burgeoning mathematics library, mathlib, have elevated once-theoretical limitations of existing typeclass resolution procedures into major impediments to ongoing progress. The two most devastating limitations of existing procedures are exponential running times in the presence of diamonds and divergence in the presence of cycles. We present a new procedure, tabled typeclass resolution, that solves both problems by tabling, which is a generalization of memoizing originally introduced to address similar limitations of early logic programming systems. We have implemented our procedure for the upcoming version (v4) of Lean, and have confirmed empirically that our implementation is exponentially faster than existing systems in the presence of diamonds. Although tabling is notoriously difficult to implement, our procedure is notably lightweight and could easily be implemented in other systems. We hope our new procedure facilitates even more sophisticated uses of typeclasses in both software development and interactive theorem proving.
Formal specification of a security framework for smart contracts
Venue: arXiv cs.SE 2020
Year: 2020

As smart contracts are growing in size and complexity, it becomes harder and harder to ensure their correctness and security. Due to the lack of isolation mechanisms a single mistake or vulnerability in the code can bring the whole system down, and due to this smart contract upgrades can be especially dangerous. Traditional ways to ensure the security of a smart contract, including DSLs, auditing and static analysis, are used before the code is deployed to the blockchain, and thus offer no protection after the deployment. After each upgrade the whole code need to be verified again, which is a difficult and time-consuming process that is prone to errors. To address these issues a security protocol and framework for smart contracts called Cap9 was developed. It provides developers the ability to perform upgrades in a secure and robust manner, and improves isolation and transparency through the use of a low level capability-based security model. We have used Isabelle/HOL to develop a formal specification of the Cap9 framework and prove its consistency. The paper presents a refinement-based approach that we used to create the specification, as well as discussion of some encountered difficulties during this process.
Reservoir computing for sensing: an experimental approach
Venue: arXiv cs.ET 2020
Year: 2020

The increasing popularity of machine learning solutions puts increasing restrictions on this field if it is to penetrate more aspects of life. In particular, energy efficiency and speed of operation is crucial, inter alia in portable medical devices. The Reservoir Computing (RC) paradigm poses as a solution to these issues through foundation of its operation: the reservoir of states. Adequate separation of input information translated into the internal state of the reservoir, whose connections do not need to be trained, allow to simplify the readout layer thus significantly accelerating the operation of the system. In this brief review article, the theoretical basis of RC was first described, followed by a description of its individual variants, their development and state-of-the-art applications in chemical sensing and metrology: detection of impedance changes and ion sensing. Presented results indicate applicability of reservoir computing for sensing and validating the SWEET algorithm experimentally.
Classifying All Interacting Pairs in a Single Shot
Venue: arXiv cs.CV 2020
Year: 2020

In this paper, we introduce a novel human interaction detection approach, based on CALIPSO (Classifying ALl Interacting Pairs in a Single shOt), a classifier of human-object interactions. This new single-shot interaction classifier estimates interactions simultaneously for all human-object pairs, regardless of their number and class. State-of-the-art approaches adopt a multi-shot strategy based on a pairwise estimate of interactions for a set of human-object candidate pairs, which leads to a complexity depending, at least, on the number of interactions or, at most, on the number of candidate pairs. In contrast, the proposed method estimates the interactions on the whole image. Indeed, it simultaneously estimates all interactions between all human subjects and object targets by performing a single forward pass throughout the image. Consequently, it leads to a constant complexity and computation time independent of the number of subjects, objects or interactions in the image. In detail, interaction classification is achieved on a dense grid of anchors thanks to a joint multi-task network that learns three complementary tasks simultaneously: (i) prediction of the types of interaction, (ii) estimation of the presence of a target and (iii) learning of an embedding which maps interacting subject and target to a same representation, by using a metric learning strategy. In addition, we introduce an object-centric passive-voice verb estimation which significantly improves results. Evaluations on the two well-known Human-Object Interaction image datasets, V-COCO and HICO-DET, demonstrate the competitiveness of the proposed method (2nd place) compared to the state-of-the-art while having constant computation time regardless of the number of objects and interactions in the image.
A Verified Packrat Parser Interpreter for Parsing Expression Grammars
Venue: arXiv cs.LO 2020
Year: 2020

Parsing expression grammars (PEGs) offer a natural opportunity for building verified parser interpreters based on higher-order parsing combinators. PEGs are expressive, unambiguous, and efficient to parse in a top-down recursive descent style. We use the rich type system of the PVS specification language and verification system to formalize the metatheory of PEGs and define a reference implementation of a recursive parser interpreter for PEGs. In order to ensure termination of parsing, we define a notion of a well-formed grammar. Rather than relying on an inductive definition of parsing, we use abstract syntax trees that represent the computational trace of the parser to provide an effective proof certificate for correct parsing and ensure that parsing properties including soundness and completeness are maintained. The correctness properties are embedded in the types of the operations so that the proofs can be easily constructed from local proof obligations. Building on the reference parser interpreter, we define a packrat parser interpreter as well as an extension that is capable of semantic interpretation. Both these parser interpreters are proved equivalent to the reference one. All of the parsers are executable. The proofs are formalized in mathematical terms so that similar parser interpreters can be defined in any specification language with a type system similar to PVS.
TurkEyes: A Web-Based Toolbox for Crowdsourcing Attention Data
Venue: arXiv cs.HC 2020
Year: 2020

Eye movements provide insight into what parts of an image a viewer finds most salient, interesting, or relevant to the task at hand. Unfortunately, eye tracking data, a commonly-used proxy for attention, is cumbersome to collect. Here we explore an alternative: a comprehensive web-based toolbox for crowdsourcing visual attention. We draw from four main classes of attention-capturing methodologies in the literature. ZoomMaps is a novel "zoom-based" interface that captures viewing on a mobile phone. CodeCharts is a "self-reporting" methodology that records points of interest at precise viewing durations. ImportAnnots is an "annotation" tool for selecting important image regions, and "cursor-based" BubbleView lets viewers click to deblur a small area. We compare these methodologies using a common analysis framework in order to develop appropriate use cases for each interface. This toolbox and our analyses provide a blueprint for how to gather attention data at scale without an eye tracker.
A Blockchain-Encryption-Based Approach to Protect Fog Federations from Rogue Nodes
Venue: arXiv cs.CR 2020
Year: 2020

People have used cloud computing approach to store their data remotely. As auspicious as this approach is, it brings forth many challenges: from data security to time latency issues with data computation as well as delivery to end users. Fog computing has emerged as an extension for cloud computing to bring data processing and storage close to end-users; however, it minimizes the time latency issue but still suffers from data security challenges. For instance, when a fog node providing services to end users is compromised, the users' data security can be violated. Thus, this paper proposes a secure and fine-grained data access control scheme by integrating the CP-ABE algorithm and blockchain concept to prevent fog nodes from violating end users' data security in a situation where a compromised fog node is being ousted. We also classify the fog nodes into fog federations, based on their attributes such as services and locations, to minimize the time latency and communication overhead between fog nodes and cloud server. Further, the exploitation and integration of the blockchain concept and the CP-ABE algorithm enables fog nodes in the same fog federation to perform the authorization process in a distributed manner. In addition, to solve time latency and communication overhead problems, we equip every fog node with an off-chain database to store most frequently accessed data files for specific time, and with an on-chain access control policies table (On-chain Files Tracking Table) which must be protected from being tampered by malicious (rogue) fog nodes. Therefore, blockchain plays a vital role here as it is tamper-proof by nature. We demonstrate our scheme's efficiency and feasibility by designing algorithms and conducting a security analysis. The provided analysis shows that the proposed scheme is efficient and feasible in ousting malicious (rogue) fog nodes.