OpenRaiser/Intern-Atlas huggingface dataset:
Reinforcement Learning-Based Air Traffic Deconfliction
Venue: arXiv cs.RO 2023
Year: 2023

Remain Well Clear, keeping the aircraft away from hazards by the appropriate separation distance, is an essential technology for the safe operation of uncrewed aerial vehicles in congested airspace. This work focuses on automating the horizontal separation of two aircraft and presents the obstacle avoidance problem as a 2D surrogate optimization task. By our design, the surrogate task is made more conservative to guarantee the execution of the solution in the primary domain. Using Reinforcement Learning (RL), we optimize the avoidance policy and model the dynamics, interactions, and decision-making. By recursively sampling the resulting policy and the surrogate transitions, the system translates the avoidance policy into a complete avoidance trajectory. Then, the solver publishes the trajectory as a set of waypoints for the airplane to follow using the Robot Operating System (ROS) interface. The proposed system generates a quick and achievable avoidance trajectory that satisfies the safety requirements. Evaluation of our system is completed in a high-fidelity simulation and full-scale airplane demonstration. Moreover, the paper concludes an enormous integration effort that has enabled a real-life demonstration of the RL-based system.
When Cyber Aggression Prediction Meets BERT on Social Media
Venue: arXiv cs.CY 2023
Year: 2023

Increasingly, cyber aggression becomes the prevalent phenomenon that erodes the social media environment. However, due to subjective and expense, the traditional self-reporting questionnaire is hard to be employed in the current cyber area. In this study, we put forward the prediction model for cyber aggression based on the cutting-edge deep learning algorithm. Building on 320 active Weibo users' social media activities, we construct basic, dynamic, and content features. We elaborate cyber aggression on three dimensions: social exclusion, malicious humour, and guilt induction. We then build the prediction model combined with pretrained BERT model. The empirical evidence shows outperformance and supports a stronger prediction with the BERT model than traditional machine learning models without extra pretrained information. This study offers a solid theoretical model for cyber aggression prediction. Furthermore, this study contributes to cyber aggression behaviors' probing and social media platforms' organization.
FireFly: A High-Throughput Hardware Accelerator for Spiking Neural Networks with Efficient DSP and Memory Optimization
Venue: arXiv cs.NE 2023
Year: 2023

Spiking neural networks (SNNs) have been widely used due to their strong biological interpretability and high energy efficiency. With the introduction of the backpropagation algorithm and surrogate gradient, the structure of spiking neural networks has become more complex, and the performance gap with artificial neural networks has gradually decreased. However, most SNN hardware implementations for field-programmable gate arrays (FPGAs) cannot meet arithmetic or memory efficiency requirements, which significantly restricts the development of SNNs. They do not delve into the arithmetic operations between the binary spikes and synaptic weights or assume unlimited on-chip RAM resources by using overly expensive devices on small tasks. To improve arithmetic efficiency, we analyze the neural dynamics of spiking neurons, generalize the SNN arithmetic operation to the multiplex-accumulate operation, and propose a high-performance implementation of such operation by utilizing the DSP48E2 hard block in Xilinx Ultrascale FPGAs. To improve memory efficiency, we design a memory system to enable efficient synaptic weights and membrane voltage memory access with reasonable on-chip RAM consumption. Combining the above two improvements, we propose an FPGA accelerator that can process spikes generated by the firing neuron on-the-fly (FireFly). FireFly is the first SNN accelerator that incorporates DSP optimization techniques into SNN synaptic operations. FireFly is implemented on several FPGA edge devices with limited resources but still guarantees a peak performance of 5.53TOP/s at 300MHz. As a lightweight accelerator, FireFly achieves the highest computational density efficiency compared with existing research using large FPGA devices.
Open-Set Face Identification on Few-Shot Gallery by Fine-Tuning
Venue: arXiv cs.CV 2023
Year: 2023

In this paper, we focus on addressing the open-set face identification problem on a few-shot gallery by fine-tuning. The problem assumes a realistic scenario for face identification, where only a small number of face images is given for enrollment and any unknown identity must be rejected during identification. We observe that face recognition models pretrained on a large dataset and naively fine-tuned models perform poorly for this task. Motivated by this issue, we propose an effective fine-tuning scheme with classifier weight imprinting and exclusive BatchNorm layer tuning. For further improvement of rejection accuracy on unknown identities, we propose a novel matcher called Neighborhood Aware Cosine (NAC) that computes similarity based on neighborhood information. We validate the effectiveness of the proposed schemes thoroughly on large-scale face benchmarks across different convolutional neural network architectures. The source code for this project is available at: https://github.com/1ho0jin1/OSFI-by-FineTuning
Topic Segmentation Model Focusing on Local Context
Venue: arXiv cs.CL 2023
Year: 2023

Topic segmentation is important in understanding scientific documents since it can not only provide better readability but also facilitate downstream tasks such as information retrieval and question answering by creating appropriate sections or paragraphs. In the topic segmentation task, topic coherence is critical in predicting segmentation boundaries. Most of the existing models have tried to exploit as many contexts as possible to extract useful topic-related information. However, additional context does not always bring promising results, because the local context between sentences becomes incoherent despite more sentences being supplemented. To alleviate this issue, we propose siamese sentence embedding layers which process two input sentences independently to get appropriate amount of information without being hampered by excessive information. Also, we adopt multi-task learning techniques including Same Topic Prediction (STP), Topic Classification (TC) and Next Sentence Prediction (NSP). When these three classification layers are combined in a multi-task manner, they can make up for each other's limitations, improving performance in all three tasks. We experiment different combinations of the three layers and report how each layer affects other layers in the same combination as well as the overall segmentation performance. The model we proposed achieves the state-of-the-art result in the WikiSection dataset.
StitchNet: Composing Neural Networks from Pre-Trained Fragments
Venue: arXiv cs.LG 2023
Year: 2023

We propose StitchNet, a novel neural network creation paradigm that stitches together fragments (one or more consecutive network layers) from multiple pre-trained neural networks. StitchNet allows the creation of high-performing neural networks without the large compute and data requirements needed under traditional model creation processes via backpropagation training. We leverage Centered Kernel Alignment (CKA) as a compatibility measure to efficiently guide the selection of these fragments in composing a network for a given task tailored to specific accuracy needs and computing resource constraints. We then show that these fragments can be stitched together to create neural networks with accuracy comparable to that of traditionally trained networks at a fraction of computing resource and data requirements. Finally, we explore a novel on-the-fly personalized model creation and inference application enabled by this new paradigm. The code is available at https://github.com/steerapi/stitchnet.
Energy Efficient Semantic Communication over Wireless Networks with Rate Splitting
Venue: arXiv cs.IT 2023
Year: 2023

In this paper, the problem of wireless resource allocation and semantic information extraction for energy efficient semantic communications over wireless networks with rate splitting is investigated. In the considered model, a base station (BS) first extracts semantic information from its large-scale data, and then transmits the small-sized semantic information to each user which recovers the original data based on its local common knowledge. At the BS side, the probability graph is used to extract multi-level semantic information. In the downlink transmission, a rate splitting scheme is adopted, while the private small-sized semantic information is transmitted through private message and the common knowledge is transmitted through common message. Due to limited wireless resource, both computation energy and transmission energy are considered. This joint computation and communication problem is formulated as an optimization problem aiming to minimize the total communication and computation energy consumption of the network under computation, latency, and transmit power constraints. To solve this problem, an alternating algorithm is proposed where the closed-form solutions for semantic information extraction ratio and computation frequency are obtained at each step. Numerical results verify the effectiveness of the proposed algorithm.
Max-Min Diversification with Fairness Constraints: Exact and Approximation Algorithms
Venue: arXiv cs.DS 2023
Year: 2023

Diversity maximization aims to select a diverse and representative subset of items from a large dataset. It is a fundamental optimization task that finds applications in data summarization, feature selection, web search, recommender systems, and elsewhere. However, in a setting where data items are associated with different groups according to sensitive attributes like sex or race, it is possible that algorithmic solutions for this task, if left unchecked, will under- or over-represent some of the groups. Therefore, we are motivated to address the problem of \emph{max-min diversification with fairness constraints}, aiming to select $k$ items to maximize the minimum distance between any pair of selected items while ensuring that the number of items selected from each group falls within predefined lower and upper bounds. In this work, we propose an exact algorithm based on integer linear programming that is suitable for small datasets as well as a $\frac{1-\varepsilon}{5}$-approximation algorithm for any $\varepsilon \in (0, 1)$ that scales to large datasets. Extensive experiments on real-world datasets demonstrate the superior performance of our proposed algorithms over existing ones.
Defining Logical Systems via Algebraic Constraints on Proofs
Venue: arXiv cs.LO 2023
Year: 2023

We present a comprehensive programme analysing the decomposition of proof systems for non-classical logics into proof systems for other logics, especially classical logic, using an algebra of constraints. That is, one recovers a proof system for a target logic by enriching a proof system for another, typically simpler, logic with an algebra of constraints that act as correctness conditions on the latter to capture the former; for example, one may use Boolean algebra to give constraints in a sequent calculus for classical propositional logic to produce a sequent calculus for intuitionistic propositional logic. The idea behind such forms of reduction is to obtain a tool for uniform and modular treatment of proof theory and provide a bridge between semantics logics and their proof theory. The article discusses the theoretical background of the project and provides several illustrations of its work in the field of intuitionistic and modal logics. The results include the following: a uniform treatment of modular and cut-free proof systems for a large class of propositional logics; a general criterion for a novel approach to soundness and completeness of a logic with respect to a model-theoretic semantics; and, a case study deriving a model-theoretic semantics from a proof-theoretic specification of a logic.
Builtin Types viewed as Inductive Families
Venue: arXiv cs.PL 2023
Year: 2023

State of the art optimisation passes for dependently typed languages can help erase the redundant information typical of invariant-rich data structures and programs. These automated processes do not dramatically change the structure of the data, even though more efficient representations could be available. Using Quantitative Type Theory, we demonstrate how to define an invariant-rich, typechecking time data structure packing an efficient runtime representation together with runtime irrelevant invariants. The compiler can then aggressively erase all such invariants during compilation. Unlike other approaches, the complexity of the resulting representation is entirely predictable, we do not require both representations to have the same structure, and yet we are able to seamlessly program as if we were using the high-level structure.
Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs
Venue: arXiv cs.CL 2023
Year: 2023

The ever-growing complexity of mathematical proofs makes their manual verification by mathematicians very cognitively demanding. Autoformalization seeks to address this by translating proofs written in natural language into a formal representation that is computer-verifiable via interactive theorem provers. In this paper, we introduce a semantic parsing approach, based on the Universal Transformer architecture, that translates elementary mathematical proofs into an equivalent formalization in the language of the Coq interactive theorem prover. The same architecture is also trained to translate simple imperative code decorated with Hoare triples into formally verifiable proofs of correctness in Coq. Experiments on a limited domain of artificial and human-written proofs show that the models generalize well to intermediate lengths not seen during training and variations in natural language.
Do Users Want Platform Moderation or Individual Control? Examining the Role of Third-Person Effects and Free Speech Support in Shaping Moderation Preferences
Venue: arXiv cs.HC 2023
Year: 2023

This study examines social media users' preferences for the use of platform-wide moderation in comparison to user-controlled, personalized moderation tools to regulate three categories of norm-violating content - hate speech, sexually explicit content, and violent content. Via a nationally representative survey of 984 US adults, we explore the influence of third-person effects and support for freedom of expression on this choice. We find that perceived negative effects on others negatively predict while free speech support positively predicts a preference for having personal moderation settings over platform-directed moderation for regulating each speech category. Our findings show that platform governance initiatives need to account for both actual and perceived media effects of norm-violating speech categories to increase user satisfaction. Our analysis suggests that users do not view personal moderation tools as an infringement on others' free speech but as a means to assert greater agency over their social media feeds.
Proof-theoretic Semantics and Tactical Proof
Venue: arXiv cs.LO 2023
Year: 2023

The use of logical systems for problem-solving may be as diverse as in proving theorems in mathematics or in figuring out how to meet up with a friend. In either case, the problem solving activity is captured by the search for an \emph{argument}, broadly conceived as a certificate for a solution to the problem. Crucially, for such a certificate to be a solution, it has be \emph{valid}, and what makes it valid is that they are well-constructed according to a notion of inference for the underlying logical system. We provide a general framework uniformly describing the use of logic as a mathematics of reasoning in the above sense. We use proof-theoretic validity in the Dummett-Prawitz tradition to define validity of arguments, and use the theory of tactical proof to relate arguments, inference, and search.
What You Say Is What You Show: Visual Narration Detection in Instructional Videos
Venue: arXiv cs.CV 2023
Year: 2023

Narrated ''how-to'' videos have emerged as a promising data source for a wide range of learning problems, from learning visual representations to training robot policies. However, this data is extremely noisy, as the narrations do not always describe the actions demonstrated in the video. To address this problem we introduce the novel task of visual narration detection, which entails determining whether a narration is visually depicted by the actions in the video. We propose What You Say is What You Show (WYS^2), a method that leverages multi-modal cues and pseudo-labeling to learn to detect visual narrations with only weakly labeled data. Our model successfully detects visual narrations in in-the-wild videos, outperforming strong baselines, and we demonstrate its impact for state-of-the-art summarization and temporal alignment of instructional videos.
The Usability of Advanced Type Systems: Rust as a Case Study
Venue: arXiv cs.PL 2023
Year: 2023

Advanced type systems that enforce various correctness and safety guarantees--such as linear and ownership types--have a long history in the Programming Languages research community. Despite this history, a human-centered evaluation of these type systems and their usability was all but absent, with empirical evaluations limited to testing their expressiveness in programs written by experts, i.e. the creators of the type system. In the past few years, this has begun to change with the adoption of a version of affine types and ownership in the popular Rust programming language. With the increase in Rust's popularity, various studies have begun empirically evaluating the usability of Rust's Ownership and Lifetime rules, providing a breadth of qualitative and quantitative information on the usability of such type systems. They found that despite Rust's general success in achieving its promise of safety and performance, these rules come with a steep learning curve and have been repeatedly cited as a barrier to adopting Rust. In this report, I provide a brief history of linear types and region-based memory management, which directly inspired Rust's type system. I then introduce Rust's Ownership and Lifetime rules, and present the state-of-the-art in academic research into their usability. I discuss both theoretical arguments and empirical evidence for why these rules are difficult to learn and apply, and survey existing work on addressing some of these difficulties. I also draw from broader works in the HCI and CS Education communities to recommend future work in this area.
Capacity Region of Asynchronous Multiple Access Channels with FTN
Venue: arXiv cs.IT 2023
Year: 2023

This paper studies the capacity region of asynchronous multiple access channel (MAC) with faster-thanNyquist (FTN) signaling. We first express the capacity region in the frequency domain. Next, we calculate an achievable rate region in time domain and prove that it is identical to the capacity region calculated in the frequency domain. Our analysis confirms that asynchronous transmission and FTN bring in significant gains.
CHARM: Composing Heterogeneous Accelerators for Matrix Multiply on Versal ACAP Architecture
Venue: arXiv cs.AR 2023
Year: 2023

Dense matrix multiply (MM) serves as one of the most heavily used kernels in deep learning applications. To cope with the high computation demands of these applications, heterogeneous architectures featuring both FPGA and dedicated ASIC accelerators have emerged as promising platforms. For example, the AMD/Xilinx Versal ACAP architecture combines general-purpose CPU cores and programmable logic with AI Engine processors optimized for AI/ML. With 400 AIEs, it provides up to 6.4 TFLOPs performance for 32-bit floating-point data. However, machine learning models often contain both large and small MM operations. While large MM operations can be parallelized efficiently across many cores, small MM operations typically cannot. We observe that executing some small MM layers from the BERT natural language processing model on a large, monolithic MM accelerator in Versal ACAP achieved less than 5% of the theoretical peak performance. Therefore, one key question arises: How can we design accelerators to fully use the abundant computation resources under limited communication bandwidth for applications with multiple MM layers of diverse sizes? We identify the biggest system throughput bottleneck resulting from the mismatch of massive computation resources of one monolithic accelerator and the various MM layers of small sizes in the application. To resolve this problem, we propose the CHARM framework to compose multiple diverse MM accelerator architectures working concurrently towards different layers in one application. We deploy the CHARM framework for four different applications, including BERT, ViT, NCF, MLP, on the AMD Versal ACAP VCK190 evaluation board. Our experiments show that we achieve 1.46 TFLOPs, 1.61 TFLOPs, 1.74 TFLOPs, and 2.94 TFLOPs inference throughput for BERT, ViT, NCF and MLP, which obtain 5.40x, 32.51x, 1.00x and 1.00x throughput gains compared to one monolithic accelerator.
Code Difference Guided Adversarial Example Generation for Deep Code Models
Venue: arXiv cs.CR 2023
Year: 2023

Adversarial examples are important to test and enhance the robustness of deep code models. As source code is discrete and has to strictly stick to complex grammar and semantics constraints, the adversarial example generation techniques in other domains are hardly applicable. Moreover, the adversarial example generation techniques specific to deep code models still suffer from unsatisfactory effectiveness due to the enormous ingredient search space. In this work, we propose a novel adversarial example generation technique (i.e., CODA) for testing deep code models. Its key idea is to use code differences between the target input (i.e., a given code snippet as the model input) and reference inputs (i.e., the inputs that have small code differences but different prediction results with the target input) to guide the generation of adversarial examples. It considers both structure differences and identifier differences to preserve the original semantics. Hence, the ingredient search space can be largely reduced as the one constituted by the two kinds of code differences, and thus the testing process can be improved by designing and guiding corresponding equivalent structure transformations and identifier renaming transformations. Our experiments on 15 deep code models demonstrate the effectiveness and efficiency of CODA, the naturalness of its generated examples, and its capability of enhancing model robustness after adversarial fine-tuning. For example, CODA reveals 88.05% and 72.51% more faults in models than the state-of-the-art techniques (i.e., CARROT and ALERT) on average, respectively.