OpenRaiser/Intern-Atlas huggingface dataset:
A Case Study in Analytic Protocol Analysis in ACL2
Venue: arXiv cs.LO 2023
Year: 2023

When verifying computer systems we sometimes want to study their asymptotic behaviors, i.e., how they behave in the long run. In such cases, we need real analysis, the area of mathematics that deals with limits and the foundations of calculus. In a prior work, we used real analysis in ACL2s to study the asymptotic behavior of the RTO computation, commonly used in congestion control algorithms across the Internet. One key component in our RTO computation analysis was proving in ACL2s that for all alpha in [0, 1), the limit as n approaches infinity of alpha raised to n is zero. Whereas the most obvious proof strategy involves the logarithm, whose codomain includes irrationals, by default ACL2 only supports rationals, which forced us to take a non-standard approach. In this paper, we explore different approaches to proving the above result in ACL2(r) and ACL2s, from the perspective of a relatively new user to each. We also contextualize the theorem by showing how it allowed us to prove important asymptotic properties of the RTO computation. Finally, we discuss tradeoffs between the various proof strategies and directions for future research.
Verification of a Rust Implementation of Knuth's Dancing Links using ACL2
Venue: arXiv cs.LO 2023
Year: 2023

Dancing Links connotes an optimization to a circular doubly-linked list data structure implementation which provides for fast list element removal and restoration. The Dancing Links optimization is used primarily in fast algorithms to find exact covers, and has been popularized by Knuth in Volume 4B of his seminal series The Art of Computer Programming. We describe an implementation of the Dancing Links optimization in the Rust programming language, as well as its formal verification using the ACL2 theorem prover. Rust has garnered significant endorsement in the past few years as a modern, memory-safe successor to C/C++ at companies such as Amazon, Google, and Microsoft, and is being integrated into both the Linux and Windows operating system kernels. Our interest in Rust stems from its potential as a hardware/software co-assurance language, with application to critical systems. We have crafted a Rust subset, inspired by Russinoff's Restricted Algorithmic C (RAC), which we have imaginatively named Restricted Algorithmic Rust, or RAR. In previous work, we described our initial implementation of a RAR toolchain, wherein we simply transpile the RAR source into RAC. By so doing, we leverage a number of existing hardware/software co-assurance tools with a minimum investment of time and effort. In this paper, we describe the RAR Rust subset, describe our improved prototype RAR toolchain, and detail the design and verification of a circular doubly-linked list data structure employing the Dancing Links optimization in RAR, with full proofs of functional correctness accomplished using the ACL2 theorem prover.
Aerial IRS with Robotic Anchoring Capabilities: A Novel Way for Adaptive Coverage Enhancement
Venue: arXiv cs.NI 2023
Year: 2023

It is widely accepted that integrating intelligent reflecting surfaces (IRSs) with unmanned aerial vehicles (UAV) or drones can assist wireless networks in improving network coverage and end user Quality of Service (QoS). However, the critical constrain of drones is their very limited hovering/flying time. In this paper we propose the concept of robotic aerial IRSs (RA-IRSs), which are in essence drones that in addition to IRS embed an anchoring mechanism that allows them to grasp in an energy neutral manner at tall urban landforms such as lampposts. By doing so, RA-IRSs can completely eliminate the flying/hovering energy consumption and can offer service for multiple hours or even days (something not possible with UAV-mounted IRSs). Using that property we show how RA-IRS can increase network performance by changing their anchoring location to follow the spatio-temporal traffic demand. The proposed methodology, developed through Integer Linear Programming (ILP) formulations offers a significant Signal-to-Noise (SNR) gain in highly heterogeneous regions in terms of traffic demand compared to fixed IRS; hence, addressing urban coverage discrepancies effectively. Numerical simulations validate the superiority of RA-IRSs over fixed terrestrial IRSs in terms of traffic serviceability, sustaining more than 2 times the traffic demand in areas experiencing high heterogeneity, emphasizing their adaptability in improving coverage and QoS in complex urban terrains.
Llamas Know What GPTs Don't Show: Surrogate Models for Confidence Estimation
Venue: arXiv cs.CL 2023
Year: 2023

To maintain user trust, large language models (LLMs) should signal low confidence on examples where they are incorrect, instead of misleading the user. The standard approach of estimating confidence is to use the softmax probabilities of these models, but as of November 2023, state-of-the-art LLMs such as GPT-4 and Claude-v1.3 do not provide access to these probabilities. We first study eliciting confidence linguistically -- asking an LLM for its confidence in its answer -- which performs reasonably (80.5% AUC on GPT-4 averaged across 12 question-answering datasets -- 7% above a random baseline) but leaves room for improvement. We then explore using a surrogate confidence model -- using a model where we do have probabilities to evaluate the original model's confidence in a given question. Surprisingly, even though these probabilities come from a different and often weaker model, this method leads to higher AUC than linguistic confidences on 9 out of 12 datasets. Our best method composing linguistic confidences and surrogate model probabilities gives state-of-the-art confidence estimates on all 12 datasets (84.6% average AUC on GPT-4).
CLIMB: Curriculum Learning for Infant-inspired Model Building
Venue: arXiv cs.CL 2023
Year: 2023

We describe our team's contribution to the STRICT-SMALL track of the BabyLM Challenge. The challenge requires training a language model from scratch using only a relatively small training dataset of ten million words. We experiment with three variants of cognitively-motivated curriculum learning and analyze their effect on the performance of the model on linguistic evaluation tasks. In the vocabulary curriculum, we analyze methods for constraining the vocabulary in the early stages of training to simulate cognitively more plausible learning curves. In the data curriculum experiments, we vary the order of the training instances based on i) infant-inspired expectations and ii) the learning behavior of the model. In the objective curriculum, we explore different variations of combining the conventional masked language modeling task with a more coarse-grained word class prediction task to reinforce linguistic generalization capabilities. Our results did not yield consistent improvements over our own non-curriculum learning baseline across a range of linguistic benchmarks; however, we do find marginal gains on select tasks. Our analysis highlights key takeaways for specific combinations of tasks and settings which benefit from our proposed curricula. We moreover determine that careful selection of model architecture, and training hyper-parameters yield substantial improvements over the default baselines provided by the BabyLM challenge.
Cost Sharing under Private Costs and Connection Control on Directed Acyclic Graphs
Venue: arXiv cs.GT 2023
Year: 2023

We consider a cost sharing problem on a weighted directed acyclic graph (DAG) with a source node to which all the other nodes want to connect. The cost (weight) of each edge is private information reported by multiple contractors, and among them, only one contractor is selected as the builder. All the nodes except for the source need to share the total cost of the used edges. However, they may block others' connections to the source by strategically cutting their outgoing edges to reduce their cost share, which may increase the total cost of connectivity. To minimize the total cost of connectivity, we design a cost sharing mechanism to incentivize each node to offer all its outgoing edges and each contractor to report all the edges' weights truthfully, and show the properties of the proposed mechanism. In addition, our mechanism outperforms the two benchmark mechanisms.
Leveraging Activation Maximization and Generative Adversarial Training to Recognize and Explain Patterns in Natural Areas in Satellite Imagery
Venue: arXiv cs.CV 2023
Year: 2023

Natural protected areas are vital for biodiversity, climate change mitigation, and supporting ecological processes. Despite their significance, comprehensive mapping is hindered by a lack of understanding of their characteristics and a missing land cover class definition. This paper aims to advance the explanation of the designating patterns forming protected and wild areas. To this end, we propose a novel framework that uses activation maximization and a generative adversarial model. With this, we aim to generate satellite images that, in combination with domain knowledge, are capable of offering complete and valid explanations for the spatial and spectral patterns that define the natural authenticity of these regions. Our proposed framework produces more precise attribution maps pinpointing the designating patterns forming the natural authenticity of protected areas. Our approach fosters our understanding of the ecological integrity of the protected natural areas and may contribute to future monitoring and preservation efforts.
A Multimodal Dataset of 21,412 Recorded Nights for Sleep and Respiratory Research
Venue: arXiv cs.LG 2023
Year: 2023

This study introduces a novel, rich dataset obtained from home sleep apnea tests using the FDA-approved WatchPAT-300 device, collected from 7,077 participants over 21,412 nights. The dataset comprises three levels of sleep data: raw multi-channel time-series from sensors, annotated sleep events, and computed summary statistics, which include 447 features related to sleep architecture, sleep apnea, and heart rate variability (HRV). We present reference values for Apnea/Hypopnea Index (AHI), sleep efficiency, Wake After Sleep Onset (WASO), and HRV sample entropy, stratified by age and sex. Moreover, we demonstrate that the dataset improves the predictive capability for various health related traits, including body composition, bone density, blood sugar levels and cardiovascular health. These results illustrate the dataset's potential to advance sleep research, personalized healthcare, and machine learning applications in biomedicine.
Counting Small Induced Subgraphs with Edge-monotone Properties
Venue: arXiv cs.CC 2023
Year: 2023

We study the parameterized complexity of #IndSub($Φ$), where given a graph $G$ and an integer $k$, the task is to count the number of induced subgraphs on $k$ vertices that satisfy the graph property $Φ$. Focke and Roth [STOC 2022] completely characterized the complexity for each $Φ$ that is a hereditary property (that is, closed under vertex deletions): #IndSub($Φ$) is #W[1]-hard except in the degenerate cases when every graph satisfies $Φ$ or only finitely many graphs satisfy $Φ$. We complement this result with a classification for each $Φ$ that is edge monotone (that is, closed under edge deletions): #IndSub($Φ$) is #W[1]-hard except in the degenerate case when there are only finitely many integers $k$ such that $Φ$ is nontrivial on $k$-vertex graphs. Our result generalizes earlier results for specific properties $Φ$ that are related to the connectivity or density of the graph. Further, we extend the #W[1]-hardness result by a lower bound which shows that #IndSub($Φ$) cannot be solved in time $f(k) \cdot |V(G)|^{o(\sqrt{\log k/\log\log k})}$ for any function $f$, unless the Exponential-Time Hypothesis (ETH) fails. For many natural properties, we obtain even a tight bound $f(k) \cdot |V(G)|^{o(k)}$; for example, this is the case for every property $Φ$ that is nontrivial on $k$-vertex graphs for each $k$ greater than some $k_0$.
Simple but Effective Unsupervised Classification for Specified Domain Images: A Case Study on Fungi Images
Venue: arXiv cs.CV 2023
Year: 2023

High-quality labeled datasets are essential for deep learning. Traditional manual annotation methods are not only costly and inefficient but also pose challenges in specialized domains where expert knowledge is needed. Self-supervised methods, despite leveraging unlabeled data for feature extraction, still require hundreds or thousands of labeled instances to guide the model for effective specialized image classification. Current unsupervised learning methods offer automatic classification without prior annotation but often compromise on accuracy. As a result, efficiently procuring high-quality labeled datasets remains a pressing challenge for specialized domain images devoid of annotated data. Addressing this, an unsupervised classification method with three key ideas is introduced: 1) dual-step feature dimensionality reduction using a pre-trained model and manifold learning, 2) a voting mechanism from multiple clustering algorithms, and 3) post-hoc instead of prior manual annotation. This approach outperforms supervised methods in classification accuracy, as demonstrated with fungal image data, achieving 94.1% and 96.7% on public and private datasets respectively. The proposed unsupervised classification method reduces dependency on pre-annotated datasets, enabling a closed-loop for data classification. The simplicity and ease of use of this method will also bring convenience to researchers in various fields in building datasets, promoting AI applications for images in specialized domains.
Self-Annotated 3D Geometric Learning for Smeared Points Removal
Venue: arXiv cs.CV 2023
Year: 2023

There has been significant progress in improving the accuracy and quality of consumer-level dense depth sensors. Nevertheless, there remains a common depth pixel artifact which we call smeared points. These are points not on any 3D surface and typically occur as interpolations between foreground and background objects. As they cause fictitious surfaces, these points have the potential to harm applications dependent on the depth maps. Statistical outlier removal methods fare poorly in removing these points as they tend also to remove actual surface points. Trained network-based point removal faces difficulty in obtaining sufficient annotated data. To address this, we propose a fully self-annotated method to train a smeared point removal classifier. Our approach relies on gathering 3D geometric evidence from multiple perspectives to automatically detect and annotate smeared points and valid points. To validate the effectiveness of our method, we present a new benchmark dataset: the Real Azure-Kinect dataset. Experimental results and ablation studies show that our method outperforms traditional filters and other self-annotated methods. Our work is publicly available at https://github.com/wangmiaowei/wacv2024_smearedremover.git.
Guided Scale Space Radon Transform for linear structures detection
Venue: arXiv cs.CV 2023
Year: 2023

Using integral transforms to the end of lines detection in images with complex background, makes the detection a hard task needing additional processing to manage the detection. As an integral transform, the Scale Space Radon Transform (SSRT) suffers from such drawbacks, even with its great abilities for thick lines detection. In this work, we propose a method to address this issue for automatic detection of thick linear structures in gray scale and binary images using the SSRT, whatever the image background content. This method involves the calculated Hessian orientations of the investigated image while computing its SSRT, in such a way that linear structures are emphasized in the SSRT space. As a consequence, the subsequent maxima detection in the SSRT space is done on a modified transform space freed from unwanted parts and, consequently, from irrelevant peaks that usually drown the peaks representing lines. Besides, highlighting the linear structure in the SSRT space permitting, thus, to efficiently detect lines of different thickness in synthetic and real images, the experiments show also the method robustness against noise and complex background.
Prophet Inequalities Require Only a Constant Number of Samples
Venue: arXiv cs.DS 2023
Year: 2023

In a prophet inequality problem, $n$ independent random variables are presented to a gambler one by one. The gambler decides when to stop the sequence and obtains the most recent value as reward. We evaluate a stopping rule by the worst-case ratio between its expected reward and the expectation of the maximum variable. In the classic setting, the order is fixed, and the optimal ratio is known to be 1/2. Three variants of this problem have been extensively studied: the prophet-secretary model, where variables arrive in uniformly random order; the free-order model, where the gambler chooses the arrival order; and the i.i.d. model, where the distributions are all the same, rendering the arrival order irrelevant. Most of the literature assumes that distributions are known to the gambler. Recent work has considered the question of what is achievable when the gambler has access only to a few samples per distribution. Surprisingly, in the fixed-order case, a single sample from each distribution is enough to approximate the optimal ratio, but this is not the case in any of the three variants. We provide a unified proof that for all three variants of the problem, a constant number of samples (independent of n) for each distribution is good enough to approximate the optimal ratios. Prior to our work, this was known to be the case only in the i.i.d. variant. We complement our result showing that our algorithms can be implemented in polynomial time. A key ingredient in our proof is an existential result based on a minimax argument, which states that there must exist an algorithm that attains the optimal ratio and does not rely on the knowledge of the upper tail of the distributions. A second key ingredient is a refined sample-based version of a decomposition of the instance into "small" and "large" variables, first introduced by Liu et al. [EC'21].
Assessing Translation capabilities of Large Language Models involving English and Indian Languages
Venue: arXiv cs.CL 2023
Year: 2023

Generative Large Language Models (LLMs) have achieved remarkable advancements in various NLP tasks. In this work, our aim is to explore the multilingual capabilities of large language models by using machine translation as a task involving English and 22 Indian languages. We first investigate the translation capabilities of raw large language models, followed by exploring the in-context learning capabilities of the same raw models. We fine-tune these large language models using parameter efficient fine-tuning methods such as LoRA and additionally with full fine-tuning. Through our study, we have identified the best performing large language model for the translation task involving LLMs, which is based on LLaMA. Our results demonstrate significant progress, with average BLEU scores of 13.42, 15.93, 12.13, 12.30, and 12.07, as well as CHRF scores of 43.98, 46.99, 42.55, 42.42, and 45.39, respectively, using 2-stage fine-tuned LLaMA-13b for English to Indian languages on IN22 (conversational), IN22 (general), flores200-dev, flores200-devtest, and newstest2019 testsets. Similarly, for Indian languages to English, we achieved average BLEU scores of 14.03, 16.65, 16.17, 15.35 and 12.55 along with chrF scores of 36.71, 40.44, 40.26, 39.51, and 36.20, respectively, using fine-tuned LLaMA-13b on IN22 (conversational), IN22 (general), flores200-dev, flores200-devtest, and newstest2019 testsets. Overall, our findings highlight the potential and strength of large language models for machine translation capabilities, including for languages that are currently underrepresented in LLMs.
DMV3D: Denoising Multi-View Diffusion using 3D Large Reconstruction Model
Venue: arXiv cs.CV 2023
Year: 2023

We propose \textbf{DMV3D}, a novel 3D generation approach that uses a transformer-based 3D large reconstruction model to denoise multi-view diffusion. Our reconstruction model incorporates a triplane NeRF representation and can denoise noisy multi-view images via NeRF reconstruction and rendering, achieving single-stage 3D generation in $\sim$30s on single A100 GPU. We train \textbf{DMV3D} on large-scale multi-view image datasets of highly diverse objects using only image reconstruction losses, without accessing 3D assets. We demonstrate state-of-the-art results for the single-image reconstruction problem where probabilistic modeling of unseen object parts is required for generating diverse reconstructions with sharp textures. We also show high-quality text-to-3D generation results outperforming previous 3D diffusion models. Our project website is at: https://justimyhxu.github.io/projects/dmv3d/ .
The value creation potential of digital humans
Venue: arXiv cs.CY 2023
Year: 2023

'Digital humans' are digital reproductions of humans powered by artificial intelligence (AI) and capable of communicating and forming emotional bonds. The value creation potential of digital humans is overlooked due to the limitations of digital human technologies. This article explores the value creation potential and the value realisation limitations of digital humans. The analysis is based on a review of 62 articles retrieved from the Web of Science database. The analysis suggests that digital humans have the potential to alleviate labour and skill shortages, reduce the natural human element in high-risk tasks, avoid design errors, improve the ergonomics of products and workplaces, and provide guidance and emotional support, all of which will benefit natural humans in the workplace. However, technical limits, evolving understanding of digital humans, the social significance and acceptance of digital humans, ethical considerations, and the adjustment of legal tradition limit the value realisation. This review suggests that digital humans' perceived usefulness and ease of development determine organisations' willingness to utilise this technology. Overcoming the limitations, which still involve engineering challenges and a change in how they are perceived, will positively affect realising the value potential of digital humans in organisations.
An Innovative Tool for Uploading/Scraping Large Image Datasets on Social Networks
Venue: arXiv cs.DL 2023
Year: 2023

Nowadays, people can retrieve and share digital information in an increasingly easy and fast fashion through the well-known digital platforms, including sensitive data, inappropriate or illegal content, and, in general, information that might serve as probative evidence in court. Consequently, to assess forensics issues, we need to figure out how to trace back to the posting chain of a digital evidence (e.g., a picture, an audio) throughout the involved platforms -- this is what Digital (also Forensics) Ballistics basically deals with. With the entry of Machine Learning as a tool of the trade in many research areas, the need for vast amounts of data has been dramatically increasing over the last few years. However, collecting or simply find the "right" datasets that properly enables data-driven research studies can turn out to be not trivial in some cases, if not extremely challenging, especially when it comes with highly specialized tasks, such as creating datasets analyzed to detect the source media platform of a given digital media. In this paper we propose an automated approach by means of a digital tool that we created on purpose. The tool is capable of automatically uploading an entire image dataset to the desired digital platform and then downloading all the uploaded pictures, thus shortening the overall time required to output the final dataset to be analyzed.