OpenRaiser/Intern-Atlas huggingface dataset:
Learning Rules Explaining Interactive Theorem Proving Tactic Prediction
Venue: arXiv cs.LO 2024
Year: 2024

Formally verifying the correctness of mathematical proofs is more accessible than ever, however, the learning curve remains steep for many of the state-of-the-art interactive theorem provers (ITP). Deriving the most appropriate subsequent proof step, and reasoning about it, given the multitude of possibilities, remains a daunting task for novice users. To improve the situation, several investigations have developed machine learning based guidance for tactic selection. Such approaches struggle to learn non-trivial relationships between the chosen tactic and the structure of the proof state and represent them as symbolic expressions. To address these issues we (i) We represent the problem as an Inductive Logic Programming (ILP) task, (ii) Using the ILP representation we enriched the feature space by encoding additional, computationally expensive properties as background knowledge predicates, (iii) We use this enriched feature space to learn rules explaining when a tactic is applicable to a given proof state, (iv) we use the learned rules to filter the output of an existing tactic selection approach and empirically show improvement over the non-filtering approaches.
Prophet Secretary and Matching: the Significance of the Largest Item
Venue: arXiv cs.DS 2024
Year: 2024

The prophet secretary problem is a combination of the prophet inequality and the secretary problem, where elements are drawn from known independent distributions and arrive in uniformly random order. In this work, we design 1) a $0.688$-competitive algorithm, that breaks the $0.675$ barrier of blind strategies (Correa, Saona, Ziliotto, 2021), and 2) a $0.641$-competitive algorithm for the prophet secretary matching problem, that breaks the $1-1/e\approx 0.632$ barrier for the first time. Our second result also applies to the query-commit model of weighted stochastic matching and improves the state-of-the-art ratio (Derakhshan and Farhadi, 2023).
Efficient Sparse Training with Structured Dropout
Venue: arXiv cs.LG 2024
Year: 2024

Dropout is a common regularisation technique in deep learning that improves generalisation. Even though it introduces sparsity and thus potential for higher throughput, it usually cannot bring speed-ups on GPUs due to its unstructured nature. In this project, I experiment with SparseDrop, a structured, hardware-friendly variant of dropout that can exploit such sparsity. I provide a CUDA implementation of SparseDrop, achieving speed-ups against its dense counterpart even at low sparsity levels. The empirical results demonstrate that SparseDrop provides similar, or sometimes even better, regularisation properties as standard dropout. This suggests its potential as a drop-in replacement to standard dropout with faster training speeds. The source code is available at https://github.com/andylolu2/sparse-dropout
Diversidade linguística e inclusão digital: desafios para uma ia brasileira
Venue: arXiv cs.CL 2024
Year: 2024

Linguistic diversity is a human attribute which, with the advance of generative AIs, is coming under threat. This paper, based on the contributions of sociolinguistics, examines the consequences of the variety selection bias imposed by technological applications and the vicious circle of preserving a variety that becomes dominant and standardized because it has linguistic documentation to feed the large language models for machine learning.
Unfiltered Conversations: A Dataset of 2024 U.S. Presidential Election Discourse on Truth Social
Venue: arXiv cs.SI 2024
Year: 2024

Truth Social, launched as a social media platform with a focus on free speech, has become a prominent space for political discourse, attracting a user base with diverse, yet often conservative, viewpoints. As an emerging platform with minimal content moderation, Truth Social has facilitated discussions around contentious social and political issues but has also seen the spread of conspiratorial and hyper-partisan narratives. In this paper, we introduce and release a comprehensive dataset capturing activity on Truth Social related to the upcoming 2024 U.S. Presidential Election, including posts, replies, user interactions, content and media. This dataset comprises 1.5 million posts published between February, 2024 and October 2024, and encompasses key user engagement features and posts metadata. Data collection began in June 2024, though it includes posts published earlier, with the oldest post dating back to February 2022. This offers researchers a unique resource to study communication patterns, the formation of online communities, and the dissemination of information within Truth Social in the run-up to the election. By providing an in-depth view of Truth Social's user dynamics and content distribution, this dataset aims to support further research on political discourse within an alt-tech social media platform. The dataset is publicly available at https://github.com/kashish-s/TruthSocial_2024ElectionInitiative
Use Digital Twins to Support Fault Diagnosis From System-level Condition-monitoring Data
Venue: arXiv cs.LG 2024
Year: 2024

Deep learning models have created great opportunities for data-driven fault diagnosis but they require large amount of labeled failure data for training. In this paper, we propose to use a digital twin to support developing data-driven fault diagnosis model to reduce the amount of failure data used in the training process. The developed fault diagnosis models are also able to diagnose component-level failures based on system-level condition-monitoring data. The proposed framework is evaluated on a real-world robot system. The results showed that the deep learning model trained by digital twins is able to diagnose the locations and modes of 9 faults/failure from $4$ different motors. However, the performance of the model trained by a digital twin can still be improved, especially when the digital twin model has some discrepancy with the real system.
How Memory-Safe is IoT? Assessing the Impact of Memory-Protection Solutions for Securing Wireless Gateways
Venue: arXiv cs.CR 2024
Year: 2024

The rapid development of the Internet of Things (IoT) has enabled novel user-centred applications, including many in safety-critical areas such as healthcare, smart environment security, and emergency response systems. The diversity in IoT manufacturers, standards, and devices creates a combinatorial explosion of such deployment scenarios, leading to increased security and safety threats due to the difficulty of managing such heterogeneity. In almost every IoT deployment, wireless gateways are crucial for interconnecting IoT devices and providing services, yet they are vulnerable to external threats and serve as key entry points for large-scale IoT attacks. Memory-based vulnerabilities are among the most serious threats in software, with no universal solution yet available. Legacy memory protection mechanisms, such as canaries, RELRO, NX, and Fortify, have enhanced memory safety but remain insufficient for comprehensive protection. Emerging technologies like ARM-MTE, CHERI, and Rust are based on more universal and robust Secure-by-Design (SbD) memory safety principles, yet each entails different trade-offs in hardware or code modifications. Given the challenges of balancing security levels with associated overheads in IoT systems, this paper explores the impact of memory safety on the IoT domain through an empirical large-scale analysis of memory-related vulnerabilities in modern wireless gateways. Our results show that memory vulnerabilities constitute the majority of IoT gateway threats, underscoring the necessity for SbD solutions, with the choice of memory-protection technology depending on specific use cases and associated overheads.
Improving Deep Reinforcement Learning Agent Trading Performance in Forex using Auxiliary Task
Venue: arXiv cs.CE 2024
Year: 2024

Advanced algorithms based on Deep Reinforcement Learning (DRL) have been able to become a reliable tool for the Forex market traders and provide a suitable strategy for maximizing profit and reducing trading risk. These tools try to find the most profitable strategy in this market by examining past market data. Artificial intelligent agents based on the Proximal Policy Optimization (PPO) algorithm, one of the DRL algorithms, have shown a special ability to determine a profitable strategy. In this research, to increase profitability and determine the optimal strategy for the PPO, an auxiliary task has been used. The auxiliary function helps the PPO to model the reward function in a better way by recognizing and classifying patterns to obtain additional information from the problem's inputs and data. The results of simulation and backtesting on the EUR/USD currency pair have shown that the new proposed model has been able to increase the overall return from -25.25% to 14.86% and the value of sharp ratio from -2.61 to 0.24 in dataset 1 and increased overall return from 2.12% to 42.22% and the value of sharp ratio from -2.93 to 0.47 in dataset 2. These results indicate better identification of trends, timely trading, and great improvement in risk reduction while increasing the profit. It has also reduced the transaction risk and can be used as an effective tool for automatic trading in the complex forex market
Efficient Medical Image Retrieval Using DenseNet and FAISS for BIRADS Classification
Venue: arXiv cs.CV 2024
Year: 2024

That datasets that are used in todays research are especially vast in the medical field. Different types of medical images such as X-rays, MRI, CT scan etc. take up large amounts of space. This volume of data introduces challenges like accessing and retrieving specific images due to the size of the database. An efficient image retrieval system is essential as the database continues to grow to save time and resources. In this paper, we propose an approach to medical image retrieval using DenseNet for feature extraction and use FAISS for similarity search. DenseNet is well-suited for feature extraction in complex medical images and FAISS enables efficient handling of high-dimensional data in large-scale datasets. Unlike existing methods focused solely on classification accuracy, our method prioritizes both retrieval speed and diagnostic relevance, addressing a critical gap in real-time case comparison for radiologists. We applied the classification of breast cancer images using the BIRADS system. We utilized DenseNet's powerful feature representation and FAISSs efficient indexing capabilities to achieve high precision and recall in retrieving relevant images for diagnosis. We experimented on a dataset of 2006 images from the Categorized Digital Database for Low Energy and Subtracted Contrast Enhanced Spectral Mammography (CDD-CESM) images available on The Cancer Imaging Archive (TCIA). Our method outperforms conventional retrieval techniques, achieving a precision of 80% at k=5 for BIRADS classification. The dataset includes annotated CESM images and medical reports, providing a comprehensive foundation for our research.
LinRec: Linear Attention Mechanism for Long-term Sequential Recommender Systems
Venue: arXiv cs.IR 2024
Year: 2024

Transformer models have achieved remarkable success in sequential recommender systems (SRSs). However, computing the attention matrix in traditional dot-product attention mechanisms results in a quadratic complexity with sequence lengths, leading to high computational costs for long-term sequential recommendation. Motivated by the above observation, we propose a novel L2-Normalized Linear Attention for the Transformer-based Sequential Recommender Systems (LinRec), which theoretically improves efficiency while preserving the learning capabilities of the traditional dot-product attention. Specifically, by thoroughly examining the equivalence conditions of efficient attention mechanisms, we show that LinRec possesses linear complexity while preserving the property of attention mechanisms. In addition, we reveal its latent efficiency properties by interpreting the proposed LinRec mechanism through a statistical lens. Extensive experiments are conducted based on two public benchmark datasets, demonstrating that the combination of LinRec and Transformer models achieves comparable or even superior performance than state-of-the-art Transformer-based SRS models while significantly improving time and memory efficiency.
LLMs and the Madness of Crowds
Venue: arXiv cs.CL 2024
Year: 2024

We investigate the patterns of incorrect answers produced by large language models (LLMs) during evaluation. These errors exhibit highly non-intuitive behaviors unique to each model. By analyzing these patterns, we measure the similarities between LLMs and construct a taxonomy that categorizes them based on their error correlations. Our findings reveal that the incorrect responses are not randomly distributed but systematically correlated across models, providing new insights into the underlying structures and relationships among LLMs.
DesignRepair: Dual-Stream Design Guideline-Aware Frontend Repair with Large Language Models
Venue: arXiv cs.SE 2024
Year: 2024

The rise of Large Language Models (LLMs) has streamlined frontend interface creation through tools like Vercel's V0, yet surfaced challenges in design quality (e.g., accessibility, and usability). Current solutions, often limited by their focus, generalisability, or data dependency, fall short in addressing these complexities. Moreover, none of them examine the quality of LLM-generated UI design. In this work, we introduce DesignRepair, a novel dual-stream design guideline-aware system to examine and repair the UI design quality issues from both code aspect and rendered page aspect. We utilised the mature and popular Material Design as our knowledge base to guide this process. Specifically, we first constructed a comprehensive knowledge base encoding Google's Material Design principles into low-level component knowledge base and high-level system design knowledge base. After that, DesignRepair employs a LLM for the extraction of key components and utilizes the Playwright tool for precise page analysis, aligning these with the established knowledge bases. Finally, we integrate Retrieval-Augmented Generation with state-of-the-art LLMs like GPT-4 to holistically refine and repair frontend code through a strategic divide and conquer approach. Our extensive evaluations validated the efficacy and utility of our approach, demonstrating significant enhancements in adherence to design guidelines, accessibility, and user experience metrics.
EcoAct: Economic Agent Determines When to Register What Action
Venue: arXiv cs.AI 2024
Year: 2024

Recent advancements have enabled Large Language Models (LLMs) to function as agents that can perform actions using external tools. This requires registering, i.e., integrating tool information into the LLM context prior to taking actions. Current methods indiscriminately incorporate all candidate tools into the agent's context and retain them across multiple reasoning steps. This process remains opaque to LLM agents and is not integrated into their reasoning procedures, leading to inefficiencies due to increased context length from irrelevant tools. To address this, we introduce EcoAct, a tool using algorithm that allows LLMs to selectively register tools as needed, optimizing context use. By integrating the tool registration process into the reasoning procedure, EcoAct reduces computational costs by over 50% in multiple steps reasoning tasks while maintaining performance, as demonstrated through extensive experiments. Moreover, it can be plugged into any reasoning pipeline with only minor modifications to the prompt, making it applicable to LLM agents now and future.
Optical Flow Representation Alignment Mamba Diffusion Model for Medical Video Generation
Venue: arXiv cs.CV 2024
Year: 2024

Medical video generation models are expected to have a profound impact on the healthcare industry, including but not limited to medical education and training, surgical planning, and simulation. Current video diffusion models typically build on image diffusion architecture by incorporating temporal operations (such as 3D convolution and temporal attention). Although this approach is effective, its oversimplification limits spatio-temporal performance and consumes substantial computational resources. To counter this, we propose Medical Simulation Video Generator (MedSora), which incorporates three key elements: i) a video diffusion framework integrates the advantages of attention and Mamba, balancing low computational load with high-quality video generation, ii) an optical flow representation alignment method that implicitly enhances attention to inter-frame pixels, and iii) a video variational autoencoder (VAE) with frequency compensation addresses the information loss of medical features that occurs when transforming pixel space into latent features and then back to pixel frames. Extensive experiments and applications demonstrate that MedSora exhibits superior visual quality in generating medical videos, outperforming the most advanced baseline methods. Further results and code are available at https://wongzbb.github.io/MedSora
Barriers to Welfare Maximization with No-Regret Learning
Venue: arXiv cs.GT 2024
Year: 2024

A celebrated result in the interface of online learning and game theory guarantees that the repeated interaction of no-regret players leads to a coarse correlated equilibrium (CCE) -- a natural game-theoretic solution concept. Despite the rich history of this foundational problem and the tremendous interest it has received in recent years, a basic question still remains open: how many iterations are needed for no-regret players to approximate an equilibrium? In this paper, we establish the first computational lower bounds for that problem in two-player (general-sum) games under the constraint that the CCE reached approximates the optimal social welfare (or some other natural objective). From a technical standpoint, our approach revolves around proving lower bounds for computing a near-optimal $T$-sparse CCE -- a mixture of $T$ product distributions, thereby circumscribing the iteration complexity of no-regret learning even in the centralized model of computation. Our proof proceeds by extending a classical reduction of Gilboa and Zemel [1989] for optimal Nash to sparse (approximate) CCE. In particular, we show that the inapproximability of maximum clique precludes attaining any non-trivial sparsity in polynomial time. Moreover, we strengthen our hardness results to apply in the low-precision regime as well via the planted clique conjecture.
Clustering Based on Density Propagation and Subcluster Merging
Venue: arXiv cs.LG 2024
Year: 2024

We propose the DPSM method, a density-based node clustering approach that automatically determines the number of clusters and can be applied in both data space and graph space. Unlike traditional density-based clustering methods, which necessitate calculating the distance between any two nodes, our proposed technique determines density through a propagation process, thereby making it suitable for a graph space. In DPSM, nodes are partitioned into small clusters based on propagated density. The partitioning technique has been proved to be sound and complete. We then extend the concept of spectral clustering from individual nodes to these small clusters, while introducing the CluCut measure to guide cluster merging. This measure is modified in various ways to account for cluster properties, thus provides guidance on when to terminate the merging process. Various experiments have validated the effectiveness of DOSM and the accuracy of these conclusions.
Fast Semi-supervised Learning on Large Graphs: An Improved Green-function Method
Venue: arXiv cs.LG 2024
Year: 2024

In the graph-based semi-supervised learning, the Green-function method is a classical method that works by computing the Green's function in the graph space. However, when applied to large graphs, especially those sparse ones, this method performs unstably and unsatisfactorily. We make a detailed analysis on it and propose a novel method from the perspective of optimization. On fully connected graphs, the method is equivalent to the Green-function method and can be seen as another interpretation with physical meanings, while on non-fully connected graphs, it helps to explain why the Green-function method causes a mess on large sparse graphs. To solve this dilemma, we propose a workable approach to improve our proposed method. Unlike the original method, our improved method can also apply two accelerating techniques, Gaussian Elimination, and Anchored Graphs to become more efficient on large graphs. Finally, the extensive experiments prove our conclusions and the efficiency, accuracy, and stability of our improved Green's function method.
Can Language Models Enable In-Context Database?
Venue: arXiv cs.DB 2024
Year: 2024

Large language models (LLMs) are emerging as few-shot learners capable of handling a variety of tasks, including comprehension, planning, reasoning, question answering, arithmetic calculations, and more. At the core of these capabilities is LLMs' proficiency in representing and understanding structural or semi-structural data, such as tables and graphs. Numerous studies have demonstrated that reasoning on tabular data or graphs is not only feasible for LLMs but also gives a promising research direction which treats these data as in-context data. The lightweight and human readable characteristics of in-context database can potentially make it an alternative for the traditional database in typical RAG (Retrieval Augmented Generation) settings. However, almost all current work focuses on static in-context data, which does not allow dynamic update. In this paper, to enable dynamic database update, delta encoding of database is proposed. We explore how data stored in traditional RDBMS can be encoded as in-context text and evaluate LLMs' proficiency for CRUD (Create, Read, Update and Delete) operations on in-context databases. A benchmark named InConDB is presented and extensive experiments are conducted to show the performance of different language models in enabling in-context database by varying the database encoding method, prompting method, operation type and input data distribution, revealing both the proficiency and limitations.
Self-Care Practices in the Context of Older Adults Living Independently
Venue: arXiv cs.HC 2024
Year: 2024

Supporting practices around self-care is crucial for enabling older adults to continue living in their own homes and ageing in place. While existing assistive technology and research concerning self-care practices have been centered on a medicalized viewpoint, it neglects a holistic perspective of older adults' preferences in self-care. This paper presents a study involving 12 older adults aged 65 and above in a semi-structured interview study, where we aimed to understand participants' practices around self-care. Our findings show that self-care in such cases involves activities across the physical, emotional and psychological, social, leisure and spiritual domains. This paper provides a comprehensive understanding of the daily self-care practices of older adults including an updated self-care framework identifying key aspects, and a set of design implications for self-care assistive technologies.