OpenRaiser/Intern-Atlas huggingface dataset:
SCorP: Statistics-Informed Dense Correspondence Prediction Directly from Unsegmented Medical Images
Venue: arXiv cs.CV 2024
Year: 2024

Statistical shape modeling (SSM) is a powerful computational framework for quantifying and analyzing the geometric variability of anatomical structures, facilitating advancements in medical research, diagnostics, and treatment planning. Traditional methods for shape modeling from imaging data demand significant manual and computational resources. Additionally, these methods necessitate repeating the entire modeling pipeline to derive shape descriptors (e.g., surface-based point correspondences) for new data. While deep learning approaches have shown promise in streamlining the construction of SSMs on new data, they still rely on traditional techniques to supervise the training of the deep networks. Moreover, the predominant linearity assumption of traditional approaches restricts their efficacy, a limitation also inherited by deep learning models trained using optimized/established correspondences. Consequently, representing complex anatomies becomes challenging. To address these limitations, we introduce SCorP, a novel framework capable of predicting surface-based correspondences directly from unsegmented images. By leveraging the shape prior learned directly from surface meshes in an unsupervised manner, the proposed model eliminates the need for an optimized shape model for training supervision. The strong shape prior acts as a teacher and regularizes the feature learning of the student network to guide it in learning image-based features that are predictive of surface correspondences. The proposed model streamlines the training and inference phases by removing the supervision for the correspondence prediction task while alleviating the linearity assumption.
Over-the-Air Fusion of Sparse Spatial Features for Integrated Sensing and Edge AI over Broadband Channels
Venue: arXiv cs.IT 2024
Year: 2024

The 6G mobile networks feature two new usage scenarios -- distributed sensing and edge artificial intelligence (AI). Their natural integration, termed integrated sensing and edge AI (ISEA), promises to create a platform that enables intelligent environment perception for wide-ranging applications. A basic operation in ISEA is for a fusion center to acquire and fuse features of spatial sensing data distributed at many edge devices (known as agents), which is confronted by a communication bottleneck due to multiple access over hostile wireless channels. To address this issue, we propose a novel framework, called Spatial Over-the-Air Fusion (Spatial AirFusion), which exploits radio waveform superposition to aggregate spatially sparse features over the air and thereby enables simultaneous access. The framework supports simultaneous aggregation over multiple voxels, which partition the 3D sensing region, and across multiple subcarriers. It exploits both spatial feature sparsity with channel diversity to pair voxel-level aggregation tasks and subcarriers to maximize the minimum receive signal-to-noise ratio among voxels. Optimally solving the resultant mixed-integer problem of Voxel-Carrier Pairing and Power Allocation (VoCa-PPA) is a focus of this work. The proposed approach hinges on derivations of optimal power allocation as a closed-form function of voxel-carrier pairing and a useful property of VoCa-PPA that allows dramatic solution space reduction. Both a low-complexity greedy algorithm and an optimal tree-search algorithm are then designed for VoCa-PPA. The latter is accelerated with a customised compact search tree, node pruning and agent ordering. Extensive simulations using real datasets demonstrate that Spatial AirFusion significantly reduces computation errors and improves sensing accuracy compared with conventional over-the-air computation without awareness of spatial sparsity.
Privacy-Preserving, Dropout-Resilient Aggregation in Decentralized Learning
Venue: arXiv cs.CR 2024
Year: 2024

Decentralized learning (DL) offers a novel paradigm in machine learning by distributing training across clients without central aggregation, enhancing scalability and efficiency. However, DL's peer-to-peer model raises challenges in protecting against inference attacks and privacy leaks. By forgoing central bottlenecks, DL demands privacy-preserving aggregation methods to protect data from 'honest but curious' clients and adversaries, maintaining network-wide privacy. Privacy-preserving DL faces the additional hurdle of client dropout, clients not submitting updates due to connectivity problems or unavailability, further complicating aggregation. This work proposes three secret sharing-based dropout resilience approaches for privacy-preserving DL. Our study evaluates the efficiency, performance, and accuracy of these protocols through experiments on datasets such as MNIST, Fashion-MNIST, SVHN, and CIFAR-10. We compare our protocols with traditional secret-sharing solutions across scenarios, including those with up to 1000 clients. Evaluations show that our protocols significantly outperform conventional methods, especially in scenarios with up to 30% of clients dropout and model sizes of up to $10^6$ parameters. Our approaches demonstrate markedly high efficiency with larger models, higher dropout rates, and extensive client networks, highlighting their effectiveness in enhancing decentralized learning systems' privacy and dropout robustness.
Optimal Initialization of Batch Bayesian Optimization
Venue: arXiv cs.LG 2024
Year: 2024

Field experiments and computer simulations are effective but time-consuming methods of measuring the quality of engineered systems at different settings. To reduce the total time required, experimenters may employ Bayesian optimization, which is parsimonious with measurements, and take measurements of multiple settings simultaneously, in a batch. In practice, experimenters use very few batches, thus, it is imperative that each batch be as informative as possible. Typically, the initial batch in a Batch Bayesian Optimization (BBO) is constructed from a quasi-random sample of settings values. We propose a batch-design acquisition function, Minimal Terminal Variance (MTV), that designs a batch by optimization rather than random sampling. MTV adapts a design criterion function from Design of Experiments, called I-Optimality, which minimizes the variance of the post-evaluation estimates of quality, integrated over the entire space of settings. MTV weights the integral by the probability that a setting is optimal, making it able to design not only an initial batch but all subsequent batches, as well. Applicability to both initialization and subsequent batches is novel among acquisition functions. Numerical experiments on test functions and simulators show that MTV compares favorably to other BBO methods.
MediFact at MEDIQA-CORR 2024: Why AI Needs a Human Touch
Venue: arXiv cs.CL 2024
Year: 2024

Accurate representation of medical information is crucial for patient safety, yet artificial intelligence (AI) systems, such as Large Language Models (LLMs), encounter challenges in error-free clinical text interpretation. This paper presents a novel approach submitted to the MEDIQA-CORR 2024 shared task (Ben Abacha et al., 2024a), focusing on the automatic correction of single-word errors in clinical notes. Unlike LLMs that rely on extensive generic data, our method emphasizes extracting contextually relevant information from available clinical text data. Leveraging an ensemble of extractive and abstractive question-answering approaches, we construct a supervised learning framework with domain-specific feature engineering. Our methodology incorporates domain expertise to enhance error correction accuracy. By integrating domain expertise and prioritizing meaningful information extraction, our approach underscores the significance of a human-centric strategy in adapting AI for healthcare.
A Formal Model to Prove Instantiation Termination for E-matching-Based Axiomatisations (Extended Version)
Venue: arXiv cs.LO 2024
Year: 2024

SMT-based program analysis and verification often involve reasoning about program features that have been specified using quantifiers; incorporating quantifiers into SMT-based reasoning is, however, known to be challenging. If quantifier instantiation is not carefully controlled, then runtime and outcomes can be brittle and hard to predict. In particular, uncontrolled quantifier instantiation can lead to unexpected incompleteness and even non-termination. E-matching is the most widely-used approach for controlling quantifier instantiation, but when axiomatisations are complex, even experts cannot tell if their use of E-matching guarantees completeness or termination. This paper presents a new formal model that facilitates the proof, once and for all, that giving a complex E-matching-based axiomatisation to an SMT solver, such as Z3 or cvc5, will not cause non-termination. Key to our technique is an operational semantics for solver behaviour that models how the E-matching rules common to most solvers are used to determine when quantifier instantiations are enabled, but abstracts over irrelevant details of individual solvers. We demonstrate the effectiveness of our technique by presenting a termination proof for a set theory axiomatisation adapted from those used in the Dafny and Viper verifiers.
Quality Estimation with $k$-nearest Neighbors and Automatic Evaluation for Model-specific Quality Estimation
Venue: arXiv cs.CL 2024
Year: 2024

Providing quality scores along with Machine Translation (MT) output, so-called reference-free Quality Estimation (QE), is crucial to inform users about the reliability of the translation. We propose a model-specific, unsupervised QE approach, termed $k$NN-QE, that extracts information from the MT model's training data using $k$-nearest neighbors. Measuring the performance of model-specific QE is not straightforward, since they provide quality scores on their own MT output, thus cannot be evaluated using benchmark QE test sets containing human quality scores on premade MT output. Therefore, we propose an automatic evaluation method that uses quality scores from reference-based metrics as gold standard instead of human-generated ones. We are the first to conduct detailed analyses and conclude that this automatic method is sufficient, and the reference-based MetricX-23 is best for the task.
Study of Clustering Techniques and Scheduling Algorithms with Fairness for Cell-Free MIMO Networks
Venue: arXiv cs.IT 2024
Year: 2024

In this work, we propose a clustering technique based on information rates for cell-free massive multiple-input multiple-output (MIMO) networks. Unlike existing clustering approaches that rely on the large scale fading coefficients of the channels and user-centric techniques, we develop an approach that is based on the information rates of cell-free massive MIMO networks. We also devise a resource allocation technique to incorporate the proposed clustering and schedule users with fairness. An analysis of the proposed clustering approach based on information rates is carried out along with an assessment of its benefits for scheduling. Numerical results show that the proposed techniques outperform existing approaches.
Scalable, Interpretable Distributed Protocol Verification by Inductive Proof Slicing
Venue: arXiv cs.DC 2024
Year: 2024

Many techniques for automated inference of inductive invariants for distributed protocols have been developed over the past several years, but their performance can still be unpredictable and their failure modes opaque for large-scale verification tasks. In this paper, we present inductive proof slicing, a new automated, compositional technique for inductive invariant inference that scales effectively to large distributed protocol verification tasks. Our technique is built on a core, novel data structure, the inductive proof graph, which explicitly represents the lemma and action dependencies of an inductive invariant and is built incrementally during the inference procedure, backwards from a target safety property. We present an invariant inference algorithm that integrates localized syntax-guided lemma synthesis routines at nodes of this graph, which are accelerated by computation of localized grammar and state variable slices. Additionally, in the case of failure to produce a complete inductive invariant, maintenance of this proof graph structure allows failures to be localized to small sub-components of this graph, enabling fine-grained failure diagnosis and repair by a user. We evaluate our technique on several complex distributed and concurrent protocols, including a large scale specification of the Raft consensus protocol, which is beyond the capabilities of modern distributed protocol verification tools, and also demonstrate how its interpretability features allow effective diagnosis and repair in cases of initial failure.
Efficient LLM Inference with Kcache
Venue: arXiv cs.CL 2024
Year: 2024

Large Language Models(LLMs) have had a profound impact on AI applications, particularly in the domains of long-text comprehension and generation. KV Cache technology is one of the most widely used techniques in the industry. It ensures efficient sequence generation by caching previously computed KV states. However, it also introduces significant memory overhead. We discovered that KV Cache is not necessary and proposed a novel KCache technique to alleviate the memory bottleneck issue during the LLMs inference process. KCache can be used directly for inference without any training process, Our evaluations show that KCache improves the throughput of popular LLMs by 40% with the baseline, while keeping accuracy.
Prompt Customization for Continual Learning
Venue: arXiv cs.CV 2024
Year: 2024

Contemporary continual learning approaches typically select prompts from a pool, which function as supplementary inputs to a pre-trained model. However, this strategy is hindered by the inherent noise of its selection approach when handling increasing tasks. In response to these challenges, we reformulate the prompting approach for continual learning and propose the prompt customization (PC) method. PC mainly comprises a prompt generation module (PGM) and a prompt modulation module (PMM). In contrast to conventional methods that employ hard prompt selection, PGM assigns different coefficients to prompts from a fixed-sized pool of prompts and generates tailored prompts. Moreover, PMM further modulates the prompts by adaptively assigning weights according to the correlations between input data and corresponding prompts. We evaluate our method on four benchmark datasets for three diverse settings, including the class, domain, and task-agnostic incremental learning tasks. Experimental results demonstrate consistent improvement (by up to 16.2\%), yielded by the proposed method, over the state-of-the-art (SOTA) techniques.
Type Inference for Isabelle2Cpp
Venue: arXiv cs.LO 2024
Year: 2024

Isabelle2Cpp is a code generation framework that supports automatic generation of C++ code from Isabelle/HOL specifications. However, if some type information of Isabelle/HOL specification is missing, Isabelle2Cpp may not complete the code generation automatically. In order to solve this problem, this paper provides a type system for Isabelle2Cpp, which is used to perform type inference and type unification for expressions of the intermediate representation in Isabelle2Cpp. The system introduces new type inference rules and unification algorithms to enhance the Isabelle2Cpp framework. By incorporating the type system, the Isabelle2Cpp framework can provide more comprehensive type information for expression generation, which leads to more complete and accurate C++ code.
Generative AI for Low-Carbon Artificial Intelligence of Things with Large Language Models
Venue: arXiv cs.NI 2024
Year: 2024

By integrating Artificial Intelligence (AI) with the Internet of Things (IoT), Artificial Intelligence of Things (AIoT) has revolutionized many fields. However, AIoT is facing the challenges of energy consumption and carbon emissions due to the continuous advancement of mobile technology. Fortunately, Generative AI (GAI) holds immense potential to reduce carbon emissions of AIoT due to its excellent reasoning and generation capabilities. In this article, we explore the potential of GAI for carbon emissions reduction and propose a novel GAI-enabled solution for low-carbon AIoT. Specifically, we first study the main impacts that cause carbon emissions in AIoT, and then introduce GAI techniques and their relations to carbon emissions. We then explore the application prospects of GAI in low-carbon AIoT, focusing on how GAI can reduce carbon emissions of network components. Subsequently, we propose a Large Language Model (LLM)-enabled carbon emission optimization framework, in which we design pluggable LLM and Retrieval Augmented Generation (RAG) modules to generate more accurate and reliable optimization problems. Furthermore, we utilize Generative Diffusion Models (GDMs) to identify optimal strategies for carbon emission reduction. Numerical results demonstrate the effectiveness of the proposed framework. Finally, we insightfully provide open research directions for low-carbon AIoT.
ComposerX: Multi-Agent Symbolic Music Composition with LLMs
Venue: arXiv cs.SD 2024
Year: 2024

Music composition represents the creative side of humanity, and itself is a complex task that requires abilities to understand and generate information with long dependency and harmony constraints. While demonstrating impressive capabilities in STEM subjects, current LLMs easily fail in this task, generating ill-written music even when equipped with modern techniques like In-Context-Learning and Chain-of-Thoughts. To further explore and enhance LLMs' potential in music composition by leveraging their reasoning ability and the large knowledge base in music history and theory, we propose ComposerX, an agent-based symbolic music generation framework. We find that applying a multi-agent approach significantly improves the music composition quality of GPT-4. The results demonstrate that ComposerX is capable of producing coherent polyphonic music compositions with captivating melodies, while adhering to user instructions.
Cyber Security in Containerization Platforms: A Comparative Study of Security Challenges, Measures and Best Practices
Venue: arXiv cs.CR 2024
Year: 2024

The paper reviews the comparative study of security measures, challenges, and best practices with a view to enhancing cyber safety in containerized platforms. This review is intended to give insight into the enhanced security posture of containerized environments, with a view to examining safety vulnerabilities in containerization platforms, exploring strategies for increasing containers isolation and assessing how encryption techniques play an important role in providing secure applications. The paper also provides practical guidance for organizations seeking to strengthen their cyber security defenses in the containerization area platforms.
Finding Beautiful and Happy Images for Mental Health and Well-being Applications
Venue: arXiv cs.CV 2024
Year: 2024

This paper explores how artificial intelligence (AI) technology can contribute to achieve progress on good health and well-being, one of the United Nations' 17 Sustainable Development Goals. It is estimated that one in ten of the global population lived with a mental disorder. Inspired by studies showing that engaging and viewing beautiful natural images can make people feel happier and less stressful, lead to higher emotional well-being, and can even have therapeutic values, we explore how AI can help to promote mental health by developing automatic algorithms for finding beautiful and happy images. We first construct a large image database consisting of nearly 20K very high resolution colour photographs of natural scenes where each image is labelled with beautifulness and happiness scores by about 10 observers. Statistics of the database shows that there is a good correlation between the beautifulness and happiness scores which provides anecdotal evidence to corroborate that engaging beautiful natural images can potentially benefit mental well-being. Building on this unique database, the very first of its kind, we have developed a deep learning based model for automatically predicting the beautifulness and happiness scores of natural images. Experimental results are presented to show that it is possible to develop AI algorithms to automatically assess an image's beautifulness and happiness values which can in turn be used to develop applications for promoting mental health and well-being.
Testing $C_k$-freeness in bounded-arboricity graphs
Venue: arXiv cs.DS 2024
Year: 2024

We study the problem of testing $C_k$-freeness ($k$-cycle-freeness) for fixed constant $k > 3$ in graphs with bounded arboricity (but unbounded degrees). In particular, we are interested in one-sided error algorithms, so that they must detect a copy of $C_k$ with high constant probability when the graph is $ε$-far from $C_k$-free. We next state our results for constant arboricity and constant $ε$ with a focus on the dependence on the number of graph vertices, $n$. The query complexity of all our algorithms grows polynomially with $1/ε$. (1) As opposed to the case of $k=3$, where the complexity of testing $C_3$-freeness grows with the arboricity of the graph but not with the size of the graph (Levi, ICALP 2021) this is no longer the case already for $k=4$. We show that $Ω(n^{1/4})$ queries are necessary for testing $C_4$-freeness, and that $\widetilde{O}(n^{1/4})$ are sufficient. The same bounds hold for $C_5$. (2) For every fixed $k \geq 6$, any one-sided error algorithm for testing $C_k$-freeness must perform $Ω(n^{1/3})$ queries. (3) For $k=6$ we give a testing algorithm whose query complexity is $\widetilde{O}(n^{1/2})$. (4) For any fixed $k$, the query complexity of testing $C_k$-freeness is upper bounded by ${O}(n^{1-1/\lfloor k/2\rfloor})$. Our $Ω(n^{1/4})$ lower bound for testing $C_4$-freeness in constant arboricity graphs provides a negative answer to an open problem posed by (Goldreich, 2021).
Generative AI for Visualization: State of the Art and Future Directions
Venue: arXiv cs.LG 2024
Year: 2024

Generative AI (GenAI) has witnessed remarkable progress in recent years and demonstrated impressive performance in various generation tasks in different domains such as computer vision and computational design. Many researchers have attempted to integrate GenAI into visualization framework, leveraging the superior generative capacity for different operations. Concurrently, recent major breakthroughs in GenAI like diffusion model and large language model have also drastically increase the potential of GenAI4VIS. From a technical perspective, this paper looks back on previous visualization studies leveraging GenAI and discusses the challenges and opportunities for future research. Specifically, we cover the applications of different types of GenAI methods including sequence, tabular, spatial and graph generation techniques for different tasks of visualization which we summarize into four major stages: data enhancement, visual mapping generation, stylization and interaction. For each specific visualization sub-task, we illustrate the typical data and concrete GenAI algorithms, aiming to provide in-depth understanding of the state-of-the-art GenAI4VIS techniques and their limitations. Furthermore, based on the survey, we discuss three major aspects of challenges and research opportunities including evaluation, dataset, and the gap between end-to-end GenAI and generative algorithms. By summarizing different generation algorithms, their current applications and limitations, this paper endeavors to provide useful insights for future GenAI4VIS research.