OpenRaiser/Intern-Atlas huggingface dataset:
Efficient Convex Optimization Requires Superlinear Memory
Venue: arXiv cs.LG 2024
Year: 2024

We show that any memory-constrained, first-order algorithm which minimizes $d$-dimensional, $1$-Lipschitz convex functions over the unit ball to $1/\mathrm{poly}(d)$ accuracy using at most $d^{1.25 - δ}$ bits of memory must make at least $\tildeΩ(d^{1 + (4/3)δ})$ first-order queries (for any constant $δ\in [0, 1/4]$). Consequently, the performance of such memory-constrained algorithms are a polynomial factor worse than the optimal $\tilde{O}(d)$ query bound for this problem obtained by cutting plane methods that use $\tilde{O}(d^2)$ memory. This resolves a COLT 2019 open problem of Woodworth and Srebro.
Graded Monads and Behavioural Equivalence Games
Venue: arXiv cs.LO 2024
Year: 2024

The framework of graded semantics uses graded monads to capture behavioural equivalences of varying granularity, for example as found on the linear-time/branching-time spectrum, over general system types. We describe a generic Spoiler-Duplicator game for graded semantics that is extracted from the given graded monad, and may be seen as playing out an equational proof; instances include standard pebble games for simulation and bisimulation as well as games for trace-like equivalences and coalgebraic behavioural equivalence. Considerations on an infinite variant of such games lead to a novel notion of infinite-depth graded semantics. Under reasonable restrictions, the infinite-depth graded semantics associated to a given graded equivalence can be characterized in terms of a determinization construction for coalgebras under the equivalence at hand.
Light Clients for Lazy Blockchains
Venue: arXiv cs.CR 2024
Year: 2024

Lazy blockchains decouple consensus from transaction verification and execution to increase throughput. Although they can contain invalid transactions (e.g., double spends) as a result, these can easily be filtered out by full nodes that check if there have been previous conflicting transactions. However, creating light (SPV) clients that do not see the whole transaction history becomes a challenge: A record of a transaction on the chain does not necessarily entail transaction confirmation. In this paper, we devise a protocol that enables the creation of efficient light clients for lazy blockchains. The number of interaction rounds and the communication complexity of our protocol are logarithmic in the blockchain execution time. Our construction is based on a bisection game that traverses the Merkle tree containing the ledger of all - valid or invalid - transactions. We prove that our proof system is succinct, complete and sound, and empirically demonstrate the feasibility of our scheme.
BBE-LSWCM: A Bootstrapped Ensemble of Long and Short Window Clickstream Models
Venue: arXiv cs.LG 2024
Year: 2024

We consider the problem of developing a clickstream modeling framework for real-time customer event prediction problems in SaaS products like QBO. We develop a low-latency, cost-effective, and robust ensemble architecture (BBE-LSWCM), which combines both aggregated user behavior data from a longer historical window (e.g., over the last few weeks) as well as user activities over a short window in recent-past (e.g., in the current session). As compared to other baseline approaches, we demonstrate the superior performance of the proposed method for two important real-time event prediction problems: subscription cancellation and intended task detection for QBO subscribers. Finally, we present details of the live deployment and results from online experiments in QBO.
PerfectDou: Dominating DouDizhu with Perfect Information Distillation
Venue: arXiv cs.AI 2024
Year: 2024

As a challenging multi-player card game, DouDizhu has recently drawn much attention for analyzing competition and collaboration in imperfect-information games. In this paper, we propose PerfectDou, a state-of-the-art DouDizhu AI system that dominates the game, in an actor-critic framework with a proposed technique named perfect information distillation. In detail, we adopt a perfect-training-imperfect-execution framework that allows the agents to utilize the global information to guide the training of the policies as if it is a perfect information game and the trained policies can be used to play the imperfect information game during the actual gameplay. To this end, we characterize card and game features for DouDizhu to represent the perfect and imperfect information. To train our system, we adopt proximal policy optimization with generalized advantage estimation in a parallel training paradigm. In experiments we show how and why PerfectDou beats all existing AI programs, and achieves state-of-the-art performance.
An Optimal Decentralized Multi-access Coded Caching System
Venue: arXiv cs.IT 2024
Year: 2024

In this paper, we consider a multi-access coded caching system with decentralized prefetching, where a server hosts $N$ files, each of size $F$ bits, and is connected to $K$ users through a shared link. There are $c$ caches distributed across the network and each of the $K$ users connects to a random set of $r\leq c$ caches. Initially, we consider the model in which each of the cache subsets is accessed by exactly a specific number of users. For this model, a novel linear delivery scheme is introduced, using which the closed-form expression for the per-user delivery rate is computed. Furthermore, using techniques from index coding, the optimality of the proposed linear delivery scheme among all linear delivery schemes is proved. The results of the decentralized shared caching and conventional decentralized caching schemes are recovered as special cases of the proposed model. The model is further generalized by allowing each cache subset to serve any number of users. This enhances the flexibility of the system, enabling it to accommodate any arbitrary number of users. A delivery scheme is proposed for the generalized model and is shown to be optimal for certain user-to-cache associations.
The higher dimensional propositional calculus
Venue: arXiv cs.LO 2024
Year: 2024

In recent research, some of the present authors introduced the concept of an n-dimensional Boolean algebra and its corresponding propositional logic nCL, generalising the Boolean propositional calculus to n>= 2 perfectly symmetric truth values. This paper presents a sound and complete sequent calculus for nCL, named nLK. We provide two proofs of completeness: one syntactic and one semantic. The former implies as a corollary that nLK enjoys the cut admissibility property. The latter relies on the generalisation to the n-ary case of the classical proof based on the Lindenbaum algebra of formulas and Boolean ultrafilters.
Towards Immersive Humanitarian Visualizations
Venue: arXiv cs.HC 2024
Year: 2024

This paper introduces immersive humanitarian visualization as a promising research area in information visualization. Humanitarian visualizations are data visualizations designed to promote human welfare. This paper explains why immersive display technologies taken broadly (e.g, virtual reality, augmented reality, ambient displays and physical representations) open up a range of opportunities for humanitarian visualization. In particular, immersive displays offer ways to make remote and hidden human suffering more salient. They also offer ways to communicate quantitative facts together with qualitative information and visceral experiences, in order to provide a holistic understanding of humanitarian issues that could support more informed humanitarian decisions. But despite some promising preliminary work, immersive humanitarian visualization has not taken off as a research topic yet. The goal of this paper is to encourage, motivate, and inspire future research in this area.
Buy-Many Mechanisms for Many Unit-Demand Buyers
Venue: arXiv cs.GT 2024
Year: 2024

A recent line of research has established a novel desideratum for designing approximately-revenue-optimal multi-item mechanisms, namely the buy-many constraint. Under this constraint, prices for different allocations made by the mechanism must be subadditive, implying that the price of a bundle cannot exceed the sum of prices of individual items it contains. This natural constraint has enabled several positive results in multi-item mechanism design bypassing well-established impossibility results. Our work addresses the main open question from this literature of extending the buy-many constraint to multiple buyer settings and developing an approximation. We propose a new revenue benchmark for multi-buyer mechanisms via an ex-ante relaxation that captures several different ways of extending the buy-many constraint to the multi-buyer setting. Our main result is that a simple sequential item pricing mechanism with buyer-specific prices can achieve an $O(\log m)$ approximation to this revenue benchmark when all buyers have unit-demand or additive preferences over m items. This is the best possible as it directly matches the previous results for the single-buyer setting where no simple mechanism can obtain a better approximation. From a technical viewpoint we make two novel contributions. First, we develop a supply-constrained version of buy-many approximation for a single buyer. Second, we develop a multi-dimensional online contention resolution scheme for unit-demand buyers that may be of independent interest in mechanism design.
Optimal service resource management strategy for IoT-based health information system considering value co-creation of users
Venue: arXiv cs.LG 2024
Year: 2024

This paper explores optimal service resource management strategy, a continuous challenge for health information service to enhance service performance, optimise service resource utilisation and deliver interactive health information service. An adaptive optimal service resource management strategy was developed considering a value co-creation model in health information service with a focus on collaborative and interactive with users. The deep reinforcement learning algorithm was embedded in the Internet of Things (IoT)-based health information service system (I-HISS) to allocate service resources by controlling service provision and service adaptation based on user engagement behaviour. The simulation experiments were conducted to evaluate the significance of the proposed algorithm under different user reactions to the health information service.
Compositional pre-processing for automated reasoning in dependent type theory
Venue: arXiv cs.LO 2024
Year: 2024

In the context of interactive theorem provers based on a dependent type theory, automation tactics (dedicated decision procedures, call of automated solvers, ...) are often limited to goals which are exactly in some expected logical fragment. This very often prevents users from applying these tactics in other contexts, even similar ones. This paper discusses the design and the implementation of pre-processing operations for automating formal proofs in the Coq proof assistant. It presents the implementation of a wide variety of predictible, atomic goal transformations, which can be composed in various ways to target different backends. A gallery of examples illustrates how it helps to expand significantly the power of automation engines.
Towards Better Understanding of User Satisfaction in Open-Domain Conversational Search
Venue: arXiv cs.IR 2024
Year: 2024

With the increasing popularity of conversational search, how to evaluate the performance of conversational search systems has become an important question in the IR community. Existing works on conversational search evaluation can mainly be categorized into two streams: (1) constructing metrics based on semantic similarity (e.g. BLUE, METEOR and BERTScore), or (2) directly evaluating the response ranking performance of the system using traditional search methods (e.g. nDCG, RBP and nERR). However, these methods either ignore the information need of the user or ignore the mixed-initiative property of conversational search. This raises the question of how to accurately model user satisfaction in conversational search scenarios. Since explicitly asking users to provide satisfaction feedback is difficult, traditional IR studies often rely on the Cranfield paradigm (i.e., third-party annotation) and user behavior modeling to estimate user satisfaction in search. However, the feasibility and effectiveness of these two approaches have not been fully explored in conversational search. In this paper, we dive into the evaluation of conversational search from the perspective of user satisfaction. We build a novel conversational search experimental platform and construct a Chinese open-domain conversational search behavior dataset containing rich annotations and search behavior data. We also collect third-party satisfaction annotation at the session-level and turn-level, to investigate the feasibility of the Cranfield paradigm in the conversational search scenario. Experimental results show both some consistency and considerable differences between the user satisfaction annotations and third-party annotations. We also propose dialog continuation or ending behavior models (DCEBM) to capture session-level user satisfaction based on turn-level information.
TeleGraph: A Benchmark Dataset for Hierarchical Link Prediction
Venue: arXiv cs.SI 2024
Year: 2024

Link prediction is a key problem for network-structured data, attracting considerable research efforts owing to its diverse applications. The current link prediction methods focus on general networks and are overly dependent on either the closed triangular structure of networks or node attributes. Their performance on sparse or highly hierarchical networks has not been well studied. On the other hand, the available tree-like benchmark datasets are either simulated, with limited node information, or small in scale. To bridge this gap, we present a new benchmark dataset TeleGraph, a highly sparse and hierarchical telecommunication network associated with rich node attributes, for assessing and fostering the link inference techniques. Our empirical results suggest that most of the algorithms fail to produce a satisfactory performance on a nearly tree-like dataset, which calls for special attention when designing or deploying the link prediction algorithm in practice.
Visual Attention Methods in Deep Learning: An In-Depth Survey
Venue: arXiv cs.CV 2024
Year: 2024

Inspired by the human cognitive system, attention is a mechanism that imitates the human cognitive awareness about specific information, amplifying critical details to focus more on the essential aspects of data. Deep learning has employed attention to boost performance for many applications. Interestingly, the same attention design can suit processing different data modalities and can easily be incorporated into large networks. Furthermore, multiple complementary attention mechanisms can be incorporated into one network. Hence, attention techniques have become extremely attractive. However, the literature lacks a comprehensive survey on attention techniques to guide researchers in employing attention in their deep models. Note that, besides being demanding in terms of training data and computational resources, transformers only cover a single category in self-attention out of the many categories available. We fill this gap and provide an in-depth survey of 50 attention techniques, categorizing them by their most prominent features. We initiate our discussion by introducing the fundamental concepts behind the success of the attention mechanism. Next, we furnish some essentials such as the strengths and limitations of each attention category, describe their fundamental building blocks, basic formulations with primary usage, and applications specifically for computer vision. We also discuss the challenges and general open questions related to attention mechanisms. Finally, we recommend possible future research directions for deep attention. All the information about visual attention methods in deep learning is provided at \href{https://github.com/saeed-anwar/VisualAttention}{https://github.com/saeed-anwar/VisualAttention}
FedCau: A Proactive Stop Policy for Communication and Computation Efficient Federated Learning
Venue: arXiv cs.LG 2024
Year: 2024

This paper investigates efficient distributed training of a Federated Learning~(FL) model over a wireless network of wireless devices. The communication iterations of the distributed training algorithm may be substantially deteriorated or even blocked by the effects of the devices' background traffic, packet losses, congestion, or latency. We abstract the communication-computation impacts as an `iteration cost' and propose a cost-aware causal FL algorithm~(FedCau) to tackle this problem. We propose an iteration-termination method that trade-offs the training performance and networking costs. We apply our approach when clients use the slotted-ALOHA, the carrier-sense multiple access with collision avoidance~(CSMA/CA), and the orthogonal frequency-division multiple access~(OFDMA) protocols. We show that, given a total cost budget, the training performance degrades as either the background communication traffic or the dimension of the training problem increases. Our results demonstrate the importance of proactively designing optimal cost-efficient stopping criteria to avoid unnecessary communication-computation costs to achieve only a marginal FL training improvement. We validate our method by training and testing FL over the MNIST dataset. Finally, we apply our approach to existing communication efficient FL methods from the literature, achieving further efficiency. We conclude that cost-efficient stopping criteria are essential for the success of practical FL over wireless networks.
Dependence Logics in Temporal Settings
Venue: arXiv cs.LO 2024
Year: 2024

Many forms of dependence manifest themselves over time, with behavior of variables in dynamical systems as a paradigmatic example. This paper studies temporal dependence in dynamical systems from a logical perspective, by enriching a minimal modal base logic of static functional dependencies. We first introduce a logic for dynamical systems featuring temporalized variables, provide a complete axiomatic proof calculus, and show that its satisfiability problem is decidable. Then, to capture explicit reasoning about dynamic transition functions, we enhance the framework with function symbols and term identity. Next we combine temporalized variables with a modality for next-time truth from standard temporal logic, where modal correspondence analysis reveals the principles needed for a complete and decidable logic of timed dynamical systems supporting reductions between the two ways of referring to time. Our final result is an axiomatization of a general decidable logic of dependencies in arbitrary dynamical systems. We conclude with a brief outlook on how the systems introduced here mesh with richer temporal logics of system behavior, and with dynamic topological logic.
Causal Intervention for Subject-Deconfounded Facial Action Unit Recognition
Venue: arXiv cs.CV 2024
Year: 2024

Subject-invariant facial action unit (AU) recognition remains challenging for the reason that the data distribution varies among subjects. In this paper, we propose a causal inference framework for subject-invariant facial action unit recognition. To illustrate the causal effect existing in AU recognition task, we formulate the causalities among facial images, subjects, latent AU semantic relations, and estimated AU occurrence probabilities via a structural causal model. By constructing such a causal diagram, we clarify the causal effect among variables and propose a plug-in causal intervention module, CIS, to deconfound the confounder \emph{Subject} in the causal diagram. Extensive experiments conducted on two commonly used AU benchmark datasets, BP4D and DISFA, show the effectiveness of our CIS, and the model with CIS inserted, CISNet, has achieved state-of-the-art performance.
Bodyless Block Propagation: TPS Fully Scalable Blockchain with Pre-Validation
Venue: arXiv cs.NI 2024
Year: 2024

Despite numerous prior attempts to boost transaction per second (TPS) of blockchain systems, many sacrifice decentralization and security. This paper proposes a bodyless block propagation (BBP) scheme for which the blockbody is not validated and transmitted during block propagation, to increase TPS without compromising security. Nodes in the blockchain network anticipate the transactions and their ordering in the next upcoming block so that these transactions can be pre-executed and pre-validated before the block is born. For a network with $N$ nodes, our theoretical analysis reveals that BBP can improve TPS scalability from $O(1/log(N))$ to $O(1)$. Ensuring consensus on the next block's transaction content is crucial. We propose a transaction selection, ordering, and synchronization algorithm to drive this consensus. To address the undetermined Coinbase address issue, we further present an algorithm for such unresolvable transactions, ensuring a consistent and TPS-efficient scheme. With BBP, most transactions require neither validation nor transmission during block propagation, liberating system from transaction-block dependencies and rendering TPS scalable. Both theoretical analysis and experiments underscore BBP's potential for full TPS scalability. Experimental results reveal a 4x reduction in block propagation time compared to Ethereum blockchain, with TPS performance being limited by node hardware rather than block propagation.
Private measures, random walks, and synthetic data
Venue: arXiv cs.CR 2024
Year: 2024

Differential privacy is a mathematical concept that provides an information-theoretic security guarantee. While differential privacy has emerged as a de facto standard for guaranteeing privacy in data sharing, the known mechanisms to achieve it come with some serious limitations. Utility guarantees are usually provided only for a fixed, a priori specified set of queries. Moreover, there are no utility guarantees for more complex - but very common - machine learning tasks such as clustering or classification. In this paper we overcome some of these limitations. Working with metric privacy, a powerful generalization of differential privacy, we develop a polynomial-time algorithm that creates a private measure from a data set. This private measure allows us to efficiently construct private synthetic data that are accurate for a wide range of statistical analysis tools. Moreover, we prove an asymptotically sharp min-max result for private measures and synthetic data for general compact metric spaces. A key ingredient in our construction is a new superregular random walk, whose joint distribution of steps is as regular as that of independent random variables, yet which deviates from the origin logarithmicaly slowly.