OpenRaiser/Intern-Atlas huggingface dataset:
Lassie: HOL4 Tactics by Example
Venue: arXiv cs.PL 2021
Year: 2021

Proof engineering efforts using interactive theorem proving have yielded several impressive projects in software systems and mathematics. A key obstacle to such efforts is the requirement that the domain expert is also an expert in the low-level details in constructing the proof in a theorem prover. In particular, the user needs to select a sequence of tactics that lead to a successful proof, a task that in general requires knowledge of the exact names and use of a large set of tactics. We present Lassie, a tactic framework for the HOL4 theorem prover that allows individual users to define their own tactic language by example and give frequently used tactics or tactic combinations easier-to-remember names. The core of Lassie is an extensible semantic parser, which allows the user to interactively extend the tactic language through a process of definitional generalization. Defining tactics in Lassie thus does not require any knowledge in implementing custom tactics, while proofs written in Lassie retain the correctness guarantees provided by the HOL4 system. We show through case studies how Lassie can be used in small and larger proofs by novice and more experienced interactive theorem prover users, and how we envision it to ease the learning curve in a HOL4 tutorial.
Towards Understanding the Behaviors of Optimal Deep Active Learning Algorithms
Venue: arXiv cs.LG 2021
Year: 2021

Active learning (AL) algorithms may achieve better performance with fewer data because the model guides the data selection process. While many algorithms have been proposed, there is little study on what the optimal AL algorithm looks like, which would help researchers understand where their models fall short and iterate on the design. In this paper, we present a simulated annealing algorithm to search for this optimal oracle and analyze it for several tasks. We present qualitative and quantitative insights into the behaviors of this oracle, comparing and contrasting them with those of various heuristics. Moreover, we are able to consistently improve the heuristics using one particular insight. We hope that our findings can better inform future active learning research. The code is available at https://github.com/YilunZhou/optimal-active-learning.
Blockchain platform for COVID-19 vaccine supply management
Venue: arXiv cs.DC 2021
Year: 2021

In the context of the COVID-19 pandemic, the rapid roll-out of a vaccine and the implementation of a worldwide immunization campaign is critical, but its success will depend on the availability of an operational and transparent distribution chain that can be audited by all relevant stakeholders. In this paper, we discuss how blockchain technology can be used for assuring the transparent tracing of COVID-19 vaccine registration, storage and delivery, and side effects self-reporting. We present such system implementation in which blockchain technology is used for assuring data integrity and immutability in case of beneficiary registration for vaccination, eliminating identity thefts and impersonations. Smart contracts are defined to monitor and track the proper vaccine distribution conditions against the safe handling rules defined by vaccine producers enabling the awareness of all network peers. For vaccine administration, a transparent and tamper-proof side effects self-reporting solution is provided considering person identification and administrated vaccine association. A prototype was implemented using the Ethereum test network, Ropsten, considering the COVID-19 vaccine distribution tracking conditions. The results obtained for each on-chain operation can be checked and validated on the Etherscan, demonstrating various aspects of the proposed system such as immunization actors and safe rules registration, vaccine tracking, and administration. In terms of throughput and scalability, the proposed blockchain system shows promising results.
Bidimensional linear recursive sequences and universality of unambiguous register automata
Venue: arXiv cs.FL 2021
Year: 2021

We study the universality and inclusion problems for register automata over equality data. We show that the universality and the inclusion problems can be solved with 2-EXPTIME complexity when the input automata are without guessing and unambiguous, improving on the currently best-known 2-EXPSPACE upper bound by Mottet and Quaas. When the number of registers of both automata is fixed, we obtain a lower EXPTIME complexity, also improving the EXPSPACE upper bound from Mottet and Quaas for fixed number of registers. We reduce inclusion to universality, and then we reduce universality to the problem of counting the number of orbits of runs of the automaton. We show that the orbit-counting function satisfies a system of bidimensional linear recursive equations with polynomial coefficients (linrec), which generalises analogous recurrences for the Stirling numbers of the second kind, and then we show that universality reduces to the zeroness problem for linrec sequences. While such a counting approach is classical and has successfully been applied to unambiguous finite automata and grammars over finite alphabets, its application to register automata over infinite alphabets is novel. We provide two algorithms to decide the zeroness problem for bidimensional linear recursive sequences arising from orbit-counting functions. Both algorithms rely on techniques from linear non-commutative algebra. The first algorithm performs variable elimination and has elementary complexity. The second algorithm is a refined version of the first one and it relies on the computation of the Hermite normal form of matrices over a skew polynomial field. The second algorithm yields an EXPTIME decision procedure for the zeroness problem of linrec sequences, which in turn yields the claimed bounds for the universality and inclusion problems of register automata.
Transformer for Image Quality Assessment
Venue: arXiv cs.CV 2021
Year: 2021

Transformer has become the new standard method in natural language processing (NLP), and it also attracts research interests in computer vision area. In this paper we investigate the application of Transformer in Image Quality (TRIQ) assessment. Following the original Transformer encoder employed in Vision Transformer (ViT), we propose an architecture of using a shallow Transformer encoder on the top of a feature map extracted by convolution neural networks (CNN). Adaptive positional embedding is employed in the Transformer encoder to handle images with arbitrary resolutions. Different settings of Transformer architectures have been investigated on publicly available image quality databases. We have found that the proposed TRIQ architecture achieves outstanding performance. The implementation of TRIQ is published on Github (https://github.com/junyongyou/triq).
Dynamic Knowledge Graphs as Semantic Memory Model for Industrial Robots
Venue: arXiv cs.RO 2021
Year: 2021

In this paper, we present a model for semantic memory that allows machines to collect information and experiences to become more proficient with time. Post semantic analysis of the sensory and other related data, the processed information is stored in the knowledge graph which is then used to comprehend the work instructions expressed in natural language. This imparts industrial robots cognitive behavior to execute the required tasks in a deterministic manner. The paper outlines the architecture of the system along with an implementation of the proposal.
Binary Dynamic Time Warping in Linear Time
Venue: arXiv cs.DS 2021
Year: 2021

Dynamic time warping distance (DTW) is a widely used distance measure between time series $x, y \in Σ^n$. It was shown by Abboud, Backurs, and Williams that in the \emph{binary case}, where $|Σ| = 2$, DTW can be computed in time $O(n^{1.87})$. We improve this running time $O(n)$. Moreover, if $x$ and $y$ are run-length encoded, then there is an algorithm running in time $\tilde{O}(k + \ell)$, where $k$ and $\ell$ are the number of runs in $x$ and $y$, respectively. This improves on the previous best bound of $O(k\ell)$ due to Dupont and Marteau.
Stereo Correspondence and Reconstruction of Endoscopic Data Challenge
Venue: arXiv cs.CV 2021
Year: 2021

The stereo correspondence and reconstruction of endoscopic data sub-challenge was organized during the Endovis challenge at MICCAI 2019 in Shenzhen, China. The task was to perform dense depth estimation using 7 training datasets and 2 test sets of structured light data captured using porcine cadavers. These were provided by a team at Intuitive Surgical. 10 teams participated in the challenge day. This paper contains 3 additional methods which were submitted after the challenge finished as well as a supplemental section from these teams on issues they found with the dataset.
High-bandwidth nonlinear control for soft actuators with recursive network models
Venue: arXiv cs.RO 2021
Year: 2021

We present a high-bandwidth, lightweight, and nonlinear output tracking technique for soft actuators that combines parsimonious recursive layers for forward output predictions and online optimization using Newton-Raphson. This technique allows for reduced model sizes and increased control loop frequencies when compared with conventional RNN models. Experimental results of this controller prototype on a single soft actuator with soft positional sensors indicate effective tracking of referenced spatial trajectories and rejection of mechanical and electromagnetic disturbances. These are evidenced by root mean squared path tracking errors (RMSE) of 1.8mm using a fully connected (FC) substructure, 1.62mm using a gated recurrent unit (GRU) and 2.11mm using a long short term memory (LSTM) unit, all averaged over three tasks. Among these models, the highest flash memory requirement is 2.22kB enabling co-location of controller and actuator.
Successive Null-Space Precoder Design for Downlink MU-MIMO with Rate Splitting and Single-Stage SIC
Venue: arXiv cs.IT 2021
Year: 2021

In this paper, we consider the precoder design for an under-loaded or critically loaded downlink multi-user multiple-input multiple-output (MU-MIMO) communication system. We propose novel precoding and decoding schemes which enhance system performance based on rate splitting at the transmitter and single-stage successive interference cancellation at the receivers. The proposed successive null-space (SNS) precoding scheme utilizes linear combinations of the null-space basis vectors of the successively augmented MIMO channel matrices of the users as precoding vectors to adjust the inter-user-interference experienced by the receivers. We formulate a non-convex weighted sum rate (WSR) optimization problem, and solve it via successive convex approximation to obtain a suboptimal solution for the precoding vectors and the associated power allocation. Our simulation results reveal that the proposed SNS precoders outperform block diagonalization based linear and rate splitting designs, and in many cases, have a relatively small gap to the maximum sum rate achieved by dirty paper coding.
New Directions in Cloud Programming
Venue: arXiv cs.DC 2021
Year: 2021

Nearly twenty years after the launch of AWS, it remains difficult for most developers to harness the enormous potential of the cloud. In this paper we lay out an agenda for a new generation of cloud programming research aimed at bringing research ideas to programmers in an evolutionary fashion. Key to our approach is a separation of distributed programs into a PACT of four facets: Program semantics, Availablity, Consistency and Targets of optimization. We propose to migrate developers gradually to PACT programming by lifting familiar code into our more declarative level of abstraction. We then propose a multi-stage compiler that emits human-readable code at each stage that can be hand-tuned by developers seeking more control. Our agenda raises numerous research challenges across multiple areas including language design, query optimization, transactions, distributed consistency, compilers and program synthesis.
Design of a Dynamic Parameter-Controlled Chaotic-PRNG in a 65nm CMOS process
Venue: arXiv cs.AR 2021
Year: 2021

In this paper, we present the design of a new chaotic map circuit with a 65nm CMOS process. This chaotic map circuit uses a dynamic parameter-control topology and generates a wide chaotic range. We propose two designs of dynamic parameter-controlled chaotic map (DPCCM)-based pseudo-random number generators (PRNG). The randomness of the generated sequence is verified using three different statistical tests, namely, NIST SP 800-22 test, FIPS PUB 140-2 test, and Diehard test. Our first design offers a throughput of 200 MS/s with an on-chip area of 0.024mm2 and a power consumption of 2.33mW. The throughput of our second design is 300 MS/s with an area consumption of 0.132mm2 and power consumption of 2.14mW. The wider chaotic range and lower-overhead, offered by our designs, can be highly suitable for various applications such as, logic obfuscation, chaos-based cryptography, re-configurable random number generation,and hard-ware security for resource-constrained edge devices like IoT.
Reddit Entity Linking Dataset
Venue: arXiv cs.CL 2021
Year: 2021

We introduce and make publicly available an entity linking dataset from Reddit that contains 17,316 linked entities, each annotated by three human annotators and then grouped into Gold, Silver, and Bronze to indicate inter-annotator agreement. We analyze the different errors and disagreements made by annotators and suggest three types of corrections to the raw data. Finally, we tested existing entity linking models that are trained and tuned on text from non-social media datasets. We find that, although these existing entity linking models perform very well on their original datasets, they perform poorly on this social media dataset. We also show that the majority of these errors can be attributed to poor performance on the mention detection subtask. These results indicate the need for better entity linking models that can be applied to the enormous amount of social media text.
A Research Ecosystem for Secure Computing
Venue: arXiv cs.CY 2021
Year: 2021

Computing devices are vital to all areas of modern life and permeate every aspect of our society. The ubiquity of computing and our reliance on it has been accelerated and amplified by the COVID-19 pandemic. From education to work environments to healthcare to defense to entertainment - it is hard to imagine a segment of modern life that is not touched by computing. The security of computers, systems, and applications has been an active area of research in computer science for decades. However, with the confluence of both the scale of interconnected systems and increased adoption of artificial intelligence, there are many research challenges the community must face so that our society can continue to benefit and risks are minimized, not multiplied. Those challenges range from security and trust of the information ecosystem to adversarial artificial intelligence and machine learning. Along with basic research challenges, more often than not, securing a system happens after the design or even deployment, meaning the security community is routinely playing catch-up and attempting to patch vulnerabilities that could be exploited any minute. While security measures such as encryption and authentication have been widely adopted, questions of security tend to be secondary to application capability. There needs to be a sea-change in the way we approach this critically important aspect of the problem: new incentives and education are at the core of this change. Now is the time to refocus research community efforts on developing interconnected technologies with security "baked in by design" and creating an ecosystem that ensures adoption of promising research developments. To realize this vision, two additional elements of the ecosystem are necessary - proper incentive structures for adoption and an educated citizenry that is well versed in vulnerabilities and risks.
Federated Learning-Based Risk-Aware Decision toMitigate Fake Task Impacts on CrowdsensingPlatforms
Venue: arXiv cs.LG 2021
Year: 2021

Mobile crowdsensing (MCS) leverages distributed and non-dedicated sensing concepts by utilizing sensors imbedded in a large number of mobile smart devices. However, the openness and distributed nature of MCS leads to various vulnerabilities and consequent challenges to address. A malicious user submitting fake sensing tasks to an MCS platform may be attempting to consume resources from any number of participants' devices; as well as attempting to clog the MCS server. In this paper, a novel approach that is based on horizontal federated learning is proposed to identify fake tasks that contain a number of independent detection devices and an aggregation entity. Detection devices are deployed to operate in parallel with each device equipped with a machine learning (ML) module, and an associated training dataset. Furthermore, the aggregation module collects the prediction results from individual devices and determines the final decision with the objective of minimizing the prediction loss. Loss measurement considers the lost task values with respect to misclassification, where the final decision utilizes a risk-aware approach where the risk is formulated as a function of the utility loss. Experimental results demonstrate that using federated learning-driven illegitimate task detection with a risk aware aggregation function improves the detection performance of the traditional centralized framework. Furthermore, the higher performance of detection and lower loss of utility can be achieved by the proposed framework. This scheme can even achieve 100%detection accuracy using small training datasets distributed across devices, while achieving slightly over an 8% increase in detection improvement over traditional approaches.
Multi-Model Least Squares-Based Recomputation Framework for Large Data Analysis
Venue: arXiv cs.LG 2021
Year: 2021

Most multilayer least squares (LS)-based neural networks are structured with two separate stages: unsupervised feature encoding and supervised pattern classification. Once the unsupervised learning is finished, the latent encoding would be fixed without supervised fine-tuning. However, in complex tasks such as handling the ImageNet dataset, there are often many more clues that can be directly encoded, while the unsupervised learning, by definition cannot know exactly what is useful for a certain task. This serves as the motivation to retrain the latent space representations to learn some clues that unsupervised learning has not yet learned. In particular, the error matrix from the output layer is pulled back to each hidden layer, and the parameters of the hidden layer are recalculated with Moore-Penrose (MP) inverse for more generalized representations. In this paper, a recomputation-based multilayer network using MP inverse (RML-MP) is developed. A sparse RML-MP (SRML-MP) model to boost the performance of RML-MP is then proposed. The experimental results with varying training samples (from 3 K to 1.8 M) show that the proposed models provide better generalization performance than most representation learning algorithms.
Advancing Computing's Foundation of US Industry & Society
Venue: arXiv cs.CY 2021
Year: 2021

While past information technology (IT) advances have transformed society, future advances hold even greater promise. For example, we have only just begun to reap the changes from artificial intelligence (AI), especially machine learning (ML). Underlying IT's impact are the dramatic improvements in computer hardware, which deliver performance that unlock new capabilities. For example, recent successes in AI/ML required the synergy of improved algorithms and hardware architectures (e.g., general-purpose graphics processing units). However, unlike in the 20th Century and early 2000s, tomorrow's performance aspirations must be achieved without continued semiconductor scaling formerly provided by Moore's Law and Dennard Scaling. How will one deliver the next 100x improvement in capability at similar or less cost to enable great value? Can we make the next AI leap without 100x better hardware? This whitepaper argues for a multipronged effort to develop new computing approaches beyond Moore's Law to advance the foundation that computing provides to US industry, education, medicine, science, and government. This impact extends far beyond the IT industry itself, as IT is now central for providing value across society, for example in semi-autonomous vehicles, tele-education, health wearables, viral analysis, and efficient administration. Herein we draw upon considerable visioning work by CRA's Computing Community Consortium (CCC) and the IEEE Rebooting Computing Initiative (IEEE RCI), enabled by thought leader input from industry, academia, and the US government.
A Survey on Integrated Access and Backhaul Networks
Venue: arXiv cs.NI 2021
Year: 2021

Benefiting from the usage of the high-frequency band, utilizing part of the large available bandwidth for wireless backhauling is feasible without considerable performance sacrifice. In this context, integrated access and backhaul (IAB) was proposed by 3GPP to reduce the fiber optics deployment cost of 5G and beyond networks. In this paper, we first give a brief introduction of IAB based on the 3GPP release. After that, we survey existing research on IAB networks, the integrations of IAB to cache-enabled network, optical communication transport network, and the non-terrestrial network. Finally, we discuss the challenges and opportunities that might arise while developing and commercializing IAB networks.
Research on Fast Text Recognition Method for Financial Ticket Image
Venue: arXiv cs.CV 2021
Year: 2021

Currently, deep learning methods have been widely applied in and thus promoted the development of different fields. In the financial accounting field, the rapid increase in the number of financial tickets dramatically increases labor costs; hence, using a deep learning method to relieve the pressure on accounting is necessary. At present, a few works have applied deep learning methods to financial ticket recognition. However, first, their approaches only cover a few types of tickets. In addition, the precision and speed of their recognition models cannot meet the requirements of practical financial accounting systems. Moreover, none of the methods provides a detailed analysis of both the types and content of tickets. Therefore, this paper first analyzes the different features of 482 kinds of financial tickets, divides all kinds of financial tickets into three categories and proposes different recognition patterns for each category. These recognition patterns can meet almost all types of financial ticket recognition needs. Second, regarding the fixed format types of financial tickets (accounting for 68.27\% of the total types of tickets), we propose a simple yet efficient network named the Financial Ticket Faster Detection network (FTFDNet) based on a Faster RCNN. Furthermore, according to the characteristics of the financial ticket text, in order to obtain higher recognition accuracy, the loss function, Region Proposal Network (RPN), and Non-Maximum Suppression (NMS) are improved to make FTFDNet focus more on text. Finally, we perform a comparison with the best ticket recognition model from the ICDAR2019 invoice competition. The experimental results illustrate that FTFDNet increases the processing speed by 50\% while maintaining similar precision.