Search

In the era of rapid advancements in artificial intelligence (AI), neural network models have achieved notable breakthroughs. However, concerns arise regarding their vulnerability to adversarial attacks. This study focuses on enhancing Concolic Testing, a specialized technique for testing Python programs implementing neural networks. The extended tool, PyCT, now accommodates a broader range of neural network operations, including floating-point and activation function computations. By systematically generating prediction path constraints, the research facilitates the identification of potential adversarial examples. Demonstrating effectiveness across various neural network architectures, the study highlights the vulnerability of Python-based neural network models to adversarial attacks. This research contributes to securing AI-powered applications by emphasizing the need for robust testing methodologies to detect and mitigate potential adversarial threats. It underscores the importance of rigorous testing techniques in fortifying neural network models for reliable applications in Python.

KV-Cache compression methods generally sample a KV-Cache of effectual tokens or quantize it into lower bits. However, these methods cannot exploit the redundancy of the hidden dimension of KV tensors. This paper investigates a unique hidden dimension approach called Palu, a novel KV-Cache compression framework that utilizes low-rank projection. Palu decomposes the linear layers into low-rank matrices, caches the smaller intermediate states, and reconstructs the full keys and values on the fly. To improve accuracy, compression rate, and efficiency, Palu further encompasses (1) a medium-grained low-rank decomposition scheme, (2) an efficient rank search algorithm, (3) a low-rank-aware quantization algorithm, and (4) matrix fusion with optimized GPU kernels. Our extensive experiments with popular LLMs show that Palu can compress KV-Cache by more than 91.25% while maintaining a significantly better accuracy (up to 1.19 lower perplexity) than state-of-the-art KV-Cache quantization methods at a similar or even higher memory usage. When compressing KV-Cache for 50%, Palu delivers up to 1.61x end-to-end speedup for the attention module. Our code is publicly available at https://github.com/shadowpa0327/Palu.

High-dimensional single-cell data poses significant challenges in identifying underlying biological patterns due to the complexity and heterogeneity of cellular states. We propose a comprehensive gene-cell dependency visualization via unsupervised clustering, Growing Hierarchical Self-Organizing Map (GHSOM), specifically designed for analyzing high-dimensional single-cell data like single-cell sequencing and CRISPR screens. GHSOM is applied to cluster samples in a hierarchical structure such that the self-growth structure of clusters satisfies the required variations between and within. We propose a novel Significant Attributes Identification Algorithm to identify features that distinguish clusters. This algorithm pinpoints attributes with minimal variation within a cluster but substantial variation between clusters. These key attributes can then be used for targeted data retrieval and downstream analysis. Furthermore, we present two innovative visualization tools: Cluster Feature Map and Cluster Distribution Map. The Cluster Feature Map highlights the distribution of specific features across the hierarchical structure of GHSOM clusters. This allows for rapid visual assessment of cluster uniqueness based on chosen features. The Cluster Distribution Map depicts leaf clusters as circles on the GHSOM grid, with circle size reflecting cluster data size and color customizable to visualize features like cell type or other attributes. We apply our analysis to three single-cell datasets and one CRISPR dataset (cell-gene database) and evaluate clustering methods with internal and external CH and ARI scores. GHSOM performs well, being the best performer in internal evaluation (CH=4.2). In external evaluation, GHSOM has the third-best performance of all methods., Comment: Abstract presentation at BIOKDD@ACM KDD 2024

Forecast aggregation combines the predictions of multiple forecasters to improve accuracy. However, the lack of knowledge about forecasters' information structure hinders optimal aggregation. Given a family of information structures, robust forecast aggregation aims to find the aggregator with minimal worst-case regret compared to the omniscient aggregator. Previous approaches for robust forecast aggregation rely on heuristic observations and parameter tuning. We propose an algorithmic framework for robust forecast aggregation. Our framework provides efficient approximation schemes for general information aggregation with a finite family of possible information structures. In the setting considered by Arieli et al. (2018) where two agents receive independent signals conditioned on a binary state, our framework also provides efficient approximation schemes by imposing Lipschitz conditions on the aggregator or discrete conditions on agents' reports. Numerical experiments demonstrate the effectiveness of our method by providing a nearly optimal aggregator in the setting considered by Arieli et al. (2018).

In this paper, a new simple and fast orthogonal block Kaczmarz (POBK) algorithm based on preprocessing techniques is proposed to solve large-scale sparse linear systems Ax = f. Firstly, the sparse Reverse Cuthill-McKee Algorithm (RCM) is used to preprocess the linear system, and then a new partitioning strategy is proposed to divide the mutually orthogonal blocks into one category, which greatly reduces computational complexity. In addition, we provide a theoretical proof of the convergence of the POBK algorithm and analyze its faster convergence. Finally, numerical simulations demonstrate that our method outperforms the latest Kaczmarz methods such as GRBK, RBK(k), GREBK(k), and aRBK in terms of CPU time., Comment: 25 pages, 12 figures, 3 tables

In this paper, we study the following Lane-Emden system with nearly critical non-power nonlinearity \begin{eqnarray*} \left\{ \arraycolsep=1.5pt \begin{array}{lll} -\Delta u =\frac{|v|^{p-1}v}{[\ln(e+|v|)]^\epsilon}\ \ &{\rm in}\ \Omega, \\[2mm] -\Delta v =\frac{|u|^{q-1}u}{[\ln(e+|u|)]^\epsilon}\ \ &{\rm in}\ \Omega, \\[2mm] u= v=0 \ \ & {\rm on}\ \partial\Omega, \end{array} \right. \end{eqnarray*} where $\Omega$ is a bounded smooth domain in $\mathbb{R}^N$, $N\geq 3$, $\epsilon>0$ is a small parameter, $p$ and $q $ lying on the critical Sobolev hyperbola $\frac{1}{p+1}+\frac{1}{q+1}=\frac{N-2}{N}$. We construct multiple blowing-up solutions based on the finite dimensional Lyapunov-Schmidt reduction method as $\epsilon$ goes to zero.

Z3-Noodler is a fork of Z3 that replaces its string theory solver with a custom solver implementing the recently introduced stabilization-based algorithm for solving word equations with regular constraints. An extensive experimental evaluation shows that Z3-Noodler is a fully-fledged solver that can compete with state-of-the-art solvers, surpassing them by far on many benchmarks. Moreover, it is often complementary to other solvers, making it a suitable choice as a candidate to a solver portfolio.

Sports professionals constantly under pressure to perform at the highest level can benefit from sports analysis, which allows coaches and players to reduce manual efforts and systematically evaluate their performance using automated tools. This research aims to advance sports analysis in badminton, systematically detecting hit-frames automatically from match videos using modern deep learning techniques. The data included in hit-frames can subsequently be utilized to synthesize players' strokes and on-court movement, as well as for other downstream applications such as analyzing training tasks and competition strategy. The proposed approach in this study comprises several automated procedures like rally-wise video trimming, player and court keypoints detection, shuttlecock flying direction prediction, and hit-frame detection. In the study, we achieved 99% accuracy on shot angle recognition for video trimming, over 92% accuracy for applying player keypoints sequences on shuttlecock flying direction prediction, and reported the evaluation results of rally-wise video trimming and hit-frame detection.

We study the following elliptic problem involving slightly subcritical non-power nonlinearity $$\left\{\begin{array}{lll} -\Delta u =\frac{|u|^{2^*-2}u}{[\ln(e+|u|)]^\epsilon}\ \ &{\rm in}\ \Omega, \\[2mm] u= 0 \ \ & {\rm on}\ \partial\Omega, \end{array} \right.$$ where $\Omega$ is a bounded smooth domain in $\mathbb{R}^n$, $n\geq 3$, $2^*=\frac{2n}{n-2}$ is the critical Sobolev exponent, $\epsilon>0$ is a small parameter. By the finite dimensional Lyapunov-Schmidt reduction method, we construct a sign changing bubble tower solution with the shape of a tower of bubbles as $\epsilon$ goes to zero.

When designing interventions in public health, development, and education, decision makers rely on social network data to target a small number of people, capitalizing on peer effects and social contagion to bring about the most welfare benefits to the population. Developing new methods that are privacy-preserving for network data collection and targeted interventions is critical for designing sustainable public health and development interventions on social networks. In a similar vein, social media platforms rely on network data and information from past diffusions to organize their ad campaign and improve the efficacy of targeted advertising. Ensuring that these network operations do not violate users' privacy is critical to the sustainability of social media platforms and their ad economies. We study privacy guarantees for influence maximization algorithms when the social network is unknown, and the inputs are samples of prior influence cascades that are collected at random. Building on recent results that address seeding with costly network information, our privacy-preserving algorithms introduce randomization in the collected data or the algorithm output, and can bound each node's (or group of nodes') privacy loss in deciding whether or not their data should be included in the algorithm input. We provide theoretical guarantees of the seeding performance with a limited sample size subject to differential privacy budgets in both central and local privacy regimes. Simulations on synthetic and empirical network datasets reveal the diminishing value of network information with decreasing privacy budget in both regimes., Comment: Preliminary version in AAMAS 2023: https://dl.acm.org/doi/10.5555/3545946.3599081 -- Code and data: https://github.com/aminrahimian/dp-inf-max

The conference peer review process involves three constituencies with different objectives: authors want their papers accepted at prestigious venues (and quickly), conferences want to present a program with many high-quality and few low-quality papers, and reviewers want to avoid being overburdened by reviews. These objectives are far from aligned, primarily because the evaluation of a submission is inherently noisy. Over the years, conferences have experimented with numerous policies to navigate the tradeoffs. These experiments include setting various bars for acceptance, varying the number of reviews per submission, requiring prior reviews to be included with resubmissions, and others. In this work, we investigate, both analytically and empirically, how well various policies work, and more importantly, why they do or do not work. We model the conference-author interactions as a Stackelberg game in which a prestigious conference commits to an acceptance policy; the authors best-respond by (re)submitting or not (re)submitting to the conference in each round of review, the alternative being a "sure accept" (such as a lightly refereed venue). Our main results include the following observations: 1) the conference should typically set a higher acceptance threshold than the actual desired quality; we call this the "resubmission gap". 2) the reviewing load is heavily driven by resubmissions of borderline papers - therefore, a judicious choice of acceptance threshold may lead to fewer reviews while incurring an acceptable loss in conference quality. 3) conference prestige, reviewer inaccuracy, and author patience increase the resubmission gap, and thus increase the review load for a fixed level of conference quality. For robustness, we further consider different models of paper quality and compare our theoretical results to simulations based on plausible parameters estimated from real data.

Case split is a core proof rule in current decision procedures for the theory of string constraints. Its use is the primary cause of the state space explosion in string constraint solving, since it is the only rule that creates branches in the proof tree. Moreover, explicit handling of the case split rule may cause recomputation of the same tasks in multiple branches of the proof tree. In this paper, we propose a symbolic algorithm that significantly reduces such a redundancy. In particular, we encode a string constraint as a regular language and proof rules as rational transducers. This allows us to perform similar steps in the proof tree only once, alleviating the state space explosion. We also extend the encoding to handle arbitrary Boolean combinations of string constraints, length constraints, and regular constraints. In our experimental results, we validate that our technique works in many practical cases where other state-of-the-art solvers fail to provide an answer; our Python prototype implementation solved over 50 % of string constraints that could not be solved by the other tools., Comment: An extended version of a paper from APLAS'20, accepted to Journal of Systems and Software

We introduce a new paradigm for analysing and finding bugs in quantum circuits. In our approach, the problem is given by a triple $\{P\}\,C\,\{Q\}$ and the question is whether, given a set $P$ of quantum states on the input of a circuit $C$, the set of quantum states on the output is equal to (or included in) a set $Q$. While this is not suitable to specify, e.g., functional correctness of a quantum circuit, it is sufficient to detect many bugs in quantum circuits. We propose a technique based on tree automata to compactly represent sets of quantum states and develop transformers to implement the semantics of quantum gates over this representation. Our technique computes with an algebraic representation of quantum states, avoiding the inaccuracy of working with floating-point numbers. We implemented the proposed approach in a prototype tool and evaluated its performance against various benchmarks from the literature. The evaluation shows that our approach is quite scalable, e.g., we managed to verify a large circuit with 40 qubits and 141,527 gates, or catch bugs injected into a circuit with 320 qubits and 1,758 gates, where all tools we compared with failed. In addition, our work establishes a connection between quantum program verification and automata, opening new possibilities to exploit the richness of automata theory and automata-based verification in the world of quantum computing., Comment: This is a technical report for the paper with the same name that appeared at PLDI'23

When eating spaghetti, one should have the sauce and noodles mixed instead of eating them separately. We argue that also in string solving, word equations and regular constraints are better mixed together than approached separately as in most current string solvers. We propose a fast algorithm, complete for the fragment of chain-free constraints, in which word equations and regular constraints are tightly integrated and exchange information, efficiently pruning the cases generated by each other and limiting possible combinatorial explosion. The algorithm is based on a novel language-based characterisation of satisfiability of word equations with regular constraints. We experimentally show that our prototype implementation is competitive with the best string solvers and even superior in that it is the fastest on difficult examples and has the least number of timeouts., Comment: To appear in Proc. of FM'23

We propose new differential privacy solutions for when external \emph{invariants} and \emph{integer} constraints are simultaneously enforced on the data product. These requirements arise in real world applications of private data curation, including the public release of the 2020 U.S. Decennial Census. They pose a great challenge to the production of provably private data products with adequate statistical usability. We propose \emph{integer subspace differential privacy} to rigorously articulate the privacy guarantee when data products maintain both the invariants and integer characteristics, and demonstrate the composition and post-processing properties of our proposal. To address the challenge of sampling from a potentially highly restricted discrete space, we devise a pair of unbiased additive mechanisms, the generalized Laplace and the generalized Gaussian mechanisms, by solving the Diophantine equations as defined by the constraints. The proposed mechanisms have good accuracy, with errors exhibiting sub-exponential and sub-Gaussian tail probabilities respectively. To implement our proposal, we design an MCMC algorithm and supply empirical convergence assessment using estimated upper bounds on the total variation distance via $L$-lag coupling. We demonstrate the efficacy of our proposal with applications to a synthetic problem with intersecting invariants, a sensitive contingency table with known margins, and the 2010 Census county-level demonstration data with mandated fixed state population totals., Comment: Accepted to AAAI 2023

Understanding computational capabilities of simple biological circuits, such as the regulatory circuits of single-cell organisms, remains an active area of research. Recent theoretical work has shown that a simple regulatory architecture based on end-product inhibition can exhibit predictive behavior by learning fluctuation statistics of one or two environmental parameters. Here we extend this analysis to higher dimensions. We show that as the number of inputs increases, a generalized version of the circuit can learn not only the dominant direction of fluctuations, as shown previously, but also the subdominant fluctuation modes., Comment: 8 pages, 6 figures

Peer prediction refers to a collection of mechanisms for eliciting information from human agents when direct verification of the obtained information is unavailable. They are designed to have a game-theoretic equilibrium where everyone reveals their private information truthfully. This result holds under the assumption that agents are Bayesian and they each adopt a fixed strategy across all tasks. Human agents however are observed in many domains to exhibit learning behavior in sequential settings. In this paper, we explore the dynamics of sequential peer prediction mechanisms when participants are learning agents. We first show that the notion of no regret alone for the agents' learning algorithms cannot guarantee convergence to the truthful strategy. We then focus on a family of learning algorithms where strategy updates only depend on agents' cumulative rewards and prove that agents' strategies in the popular Correlated Agreement (CA) mechanism converge to truthful reporting when they use algorithms from this family. This family of algorithms is not necessarily no-regret, but includes several familiar no-regret learning algorithms (e.g multiplicative weight update and Follow the Perturbed Leader) as special cases. Simulation of several algorithms in this family as well as the $\epsilon$-greedy algorithm, which is outside of this family, shows convergence to the truthful strategy in the CA mechanism., Comment: 34 pages, 9 figures

In the literature of data privacy, differential privacy is the most popular model. An algorithm is differentially private if its outputs with and without any individual's data are indistinguishable. In this paper, we focus on data generated from a Markov chain and argue that Bayesian differential privacy (BDP) offers more meaningful guarantees in this context. Our main theoretical contribution is providing a mechanism for achieving BDP when data is drawn from a binary Markov chain. We improve on the state-of-the-art BDP mechanism and show that our mechanism provides the optimal noise-privacy tradeoffs for any local mechanism up to negligible factors. We also briefly discuss a non-local mechanism which adds correlated noise. Lastly, we perform experiments on synthetic data that detail when DP is insufficient, and experiments on real data to show that our privacy guarantees are robust to underlying distributions that are not simple Markov chains.

The recent framework of performative prediction is aimed at capturing settings where predictions influence the target/outcome they want to predict. In this paper, we introduce a natural multi-agent version of this framework, where multiple decision makers try to predict the same outcome. We showcase that such competition can result in interesting phenomena by proving the possibility of phase transitions from stability to instability and eventually chaos. Specifically, we present settings of multi-agent performative prediction where under sufficient conditions their dynamics lead to global stability and optimality. In the opposite direction, when the agents are not sufficiently cautious in their learning/updates rates, we show that instability and in fact formal chaos is possible. We complement our theoretical predictions with simulations showcasing the predictive power of our results.

Deep learning (DL) models have provided state-of-the-art performance in various medical imaging benchmarking challenges, including the Brain Tumor Segmentation (BraTS) challenges. However, the task of focal pathology multi-compartment segmentation (e.g., tumor and lesion sub-regions) is particularly challenging, and potential errors hinder translating DL models into clinical workflows. Quantifying the reliability of DL model predictions in the form of uncertainties could enable clinical review of the most uncertain regions, thereby building trust and paving the way toward clinical translation. Several uncertainty estimation methods have recently been introduced for DL medical image segmentation tasks. Developing scores to evaluate and compare the performance of uncertainty measures will assist the end-user in making more informed decisions. In this study, we explore and evaluate a score developed during the BraTS 2019 and BraTS 2020 task on uncertainty quantification (QU-BraTS) and designed to assess and rank uncertainty estimates for brain tumor multi-compartment segmentation. This score (1) rewards uncertainty estimates that produce high confidence in correct assertions and those that assign low confidence levels at incorrect assertions, and (2) penalizes uncertainty measures that lead to a higher percentage of under-confident correct assertions. We further benchmark the segmentation uncertainties generated by 14 independent participating teams of QU-BraTS 2020, all of which also participated in the main BraTS segmentation task. Overall, our findings confirm the importance and complementary value that uncertainty estimates provide to segmentation algorithms, highlighting the need for uncertainty quantification in medical image analyses. Finally, in favor of transparency and reproducibility, our evaluation code is made publicly available at: https://github.com/RagMeh11/QU-BraTS., Comment: Accepted for publication at the Journal of Machine Learning for Biomedical Imaging (MELBA): https://www.melba-journal.org/papers/2022:026.html

Existing disk-based database systems largely fall into two categories -- they either provide very high performance but few guarantees, or expose the transaction abstraction satisfying the full ACID guarantees at the cost of lower performance. In this paper, we present an alternative that achieves the best of both worlds, namely good performance and transactional properties. Our key observation is that, because of the frequent use of synchronization primitives, systems with strong durability can hardly utilize the extremely high parallelism granted by modern storage devices. Thus, we explore the notion of weakly durable transactions, and discuss how to safely relax durability without compromising other transactional properties. We present AciKV, a transactional system whose design is centered around weak durability. AciKV exposes to users the normal transactional interface, but what sets it apart from others is a new "persist" primitive that decouples durability from commit. AciKV is a middle ground between systems that perform fast atomic operations, and ones that support transactions; this middle ground is useful as it provides similar performance to the former, while prevents isolation and consistency anomalies like the latter. Our evaluation using the YCSB benchmark shows that AciKV, under workloads that involve write requests, exhibits more than two orders of magnitude higher throughput than existing strongly durable systems.

Since its selection as the method of the year in 2013, single-cell technologies have become mature enough to provide answers to complex research questions. With the growth of single-cell profiling technologies, there has also been a significant increase in data collected from single-cell profilings, resulting in computational challenges to process these massive and complicated datasets. To address these challenges, deep learning (DL) is positioning as a competitive alternative for single-cell analyses besides the traditional machine learning approaches. Here we present a processing pipeline of single-cell RNA-seq data, survey a total of 25 DL algorithms and their applicability for a specific step in the processing pipeline. Specifically, we establish a unified mathematical representation of all variational autoencoder, autoencoder, and generative adversarial network models, compare the training strategies and loss functions for these models, and relate the loss functions of these models to specific objectives of the data processing step. Such presentation will allow readers to choose suitable algorithms for their particular objective at each step in the pipeline. We envision that this survey will serve as an important information portal for learning the application of DL for scRNA-seq analysis and inspire innovative use of DL to address a broader range of new challenges in emerging multi-omics and spatial single-cell sequencing., Comment: 74 pages

5d transition metal Pt is the canonical spin Hall material for efficient generation of spin-orbit torques (SOTs) in Pt/ferromagnetic layer (FM) heterostructures. However, for a long while with tremendous engineering endeavors, the damping-like SOT efficiencies (${\xi}_{DL}$) of Pt and Pt alloys have still been limited to ${\xi}_{DL}$<0.5. Here we present that with proper alloying elements, particularly 3d transition metals V and Cr, a high spin-orbital Hall conductivity (${\sigma}_{SH}{\sim}6.5{\times}10^{5}({\hbar}/2e){\Omega}^{-1}{\cdot} m^{-1}$) can be developed. Especially for the Cr-doped case, an extremely high ${\xi}_{DL}{\sim}0.9$ in a Pt$_{0.69}$Cr$_{0.31}$/Co device can be achieved with a moderate Pt$_{0.69}$Cr$_{0.31}$ resistivity of ${\rho}_{xx}{\sim}133 {\mu}{\Omega}{\cdot}cm$. A low critical SOT-driven switching current density of $J_{c}{\sim}3.2{\times}10^{6} A{\cdot}cm^{-2}$ is also demonstrated. The damping constant (${\alpha}$) of Pt$_{0.69}$Cr$_{0.31}$/FM structure is also found to be reduced to 0.052 from the pure Pt/FM case of 0.078. The overall high ${\sigma}_{SH}$, giant ${\xi}_{DL}$, moderate ${\rho}_{xx}$, and reduced ${\alpha}$ of such a Pt-Cr/FM heterostructure makes it promising for versatile extremely low power consumption SOT memory applications., Comment: 52 pages, 12 figures, 3 table

Many data applications have certain invariant constraints due to practical needs. Data curators who employ differential privacy need to respect such constraints on the sanitized data product as a primary utility requirement. Invariants challenge the formulation, implementation, and interpretation of privacy guarantees. We propose subspace differential privacy, to honestly characterize the dependence of the sanitized output on confidential aspects of the data. We discuss two design frameworks that convert well-known differentially private mechanisms, such as the Gaussian and the Laplace mechanisms, to subspace differentially private ones that respect the invariants specified by the curator. For linear queries, we discuss the design of near-optimal mechanisms that minimize the mean squared error. Subspace differentially private mechanisms rid the need for post-processing due to invariants, preserve transparency and statistical intelligibility of the output, and can be suitable for distributed implementation. We showcase the proposed mechanisms on the 2020 Census Disclosure Avoidance demonstration data, and a spatio-temporal dataset of mobile access point connections on a large university campus., Comment: 25 pages, 3 figures; Published in AAAI'22

This paper studies the design of optimal proper scoring rules when the principal has partial knowledge of an agent's signal distribution. Recent work characterizes the proper scoring rules that maximize the increase of an agent's payoff when the agent chooses to access a costly signal to refine a posterior belief from her prior prediction, under the assumption that the agent's signal distribution is fully known to the principal. In our setting, the principal only knows about a set of distributions where the agent's signal distribution belongs. We formulate the scoring rule design problem as a max-min optimization that maximizes the worst-case increase in payoff across the set of distributions. We propose an efficient algorithm to compute an optimal scoring rule when the set of distributions is finite, and devise a fully polynomial-time approximation scheme that accommodates various infinite sets of distributions. We further remark that widely used scoring rules, such as the quadratic and log rules, as well as previously identified optimal scoring rules under full knowledge, can be far from optimal in our partial knowledge settings.

Recent advances in multi-task peer prediction have greatly expanded our knowledge about the power of multi-task peer prediction mechanisms. Various mechanisms have been proposed in different settings to elicit different types of information. But we still lack understanding about when desirable mechanisms will exist for a multi-task peer prediction problem. In this work, we study the elicitability of multi-task peer prediction problems. We consider a designer who has certain knowledge about the underlying information structure and wants to elicit certain information from a group of participants. Our goal is to infer the possibility of having a desirable mechanism based on the primitives of the problem. Our contribution is twofold. First, we provide a characterization of the elicitable multi-task peer prediction problems, assuming that the designer only uses scoring mechanisms. Scoring mechanisms are the mechanisms that reward participants' reports for different tasks separately. The characterization uses a geometric approach based on the power diagram characterization in the single-task setting ([Lambert and Shoham, 2009, Frongillo and Witkowski, 2017]). For general mechanisms, we also give a necessary condition for a multi-task problem to be elicitable. Second, we consider the case when the designer aims to elicit some properties that are linear in the participant's posterior about the state of the world. We first show that in some cases, the designer basically can only elicit the posterior itself. We then look into the case when the designer aims to elicit the participants' posteriors. We give a necessary condition for the posterior to be elicitable. This condition implies that the mechanisms proposed by Kong and Schoenebeck are already the best we can hope for in their setting, in the sense that their mechanisms can solve any problem instance that can possibly be elicitable.

When can cooperation arise from self-interested decisions in public goods games? And how can we help agents to act cooperatively? We examine these classical questions in a pivotal participation game, a variant of public good games, where heterogeneous agents make binary participation decisions on contributing their endowments, and the public project succeeds when it has enough contributions. We prove it is NP-complete to decide the existence of a cooperative Nash equilibrium such that the project succeeds. We also identify two natural special scenarios where this decision problem is tractable. We then propose two algorithms to help cooperation in the game. Our first algorithm adds an external investment to the public project, and our second algorithm uses matching funds. We show that the cost to induce a cooperative Nash equilibrium is near-optimal for both algorithms. Finally, the cost of matching funds can always be smaller than the cost of adding an external investment. Intuitively, matching funds provide a greater incentive for cooperation than adding an external investment does., Comment: 14 pages, 1 figure, accepted at IJCAI'21: International Joint Conference on Artificial Intelligence

Since no effective therapies exist for Alzheimer's disease (AD), prevention has become more critical through lifestyle factor changes and interventions. Analyzing electronic health records (EHR) of patients with AD can help us better understand lifestyle's effect on AD. However, lifestyle information is typically stored in clinical narratives. Thus, the objective of the study was to demonstrate the feasibility of natural language processing (NLP) models to classify lifestyle factors (e.g., physical activity and excessive diet) from clinical texts. We automatically generated labels for the training data by using a rule-based NLP algorithm. We conducted weak supervision for pre-trained Bidirectional Encoder Representations from Transformers (BERT) models on the weakly labeled training corpus. These models include the BERT base model, PubMedBERT(abstracts + full text), PubMedBERT(only abstracts), Unified Medical Language System (UMLS) BERT, Bio BERT, and Bio-clinical BERT. We performed two case studies: physical activity and excessive diet, in order to validate the effectiveness of BERT models in classifying lifestyle factors for AD. These models were compared on the developed Gold Standard Corpus (GSC) on the two case studies. The PubmedBERT(Abs) model achieved the best performance for physical activity, with its precision, recall, and F-1 scores of 0.96, 0.96, and 0.96, respectively. Regarding classifying excessive diet, the Bio BERT model showed the highest performance with perfect precision, recall, and F-1 scores. The proposed approach leveraging weak supervision could significantly increase the sample size, which is required for training the deep learning models. The study also demonstrates the effectiveness of BERT models for extracting lifestyle factors for Alzheimer's disease from clinical notes.

Semi-quantum private comparison (SQPC) allows two participants with limited quantum ability to securely compare the equality of their secrets with the help of a semi-dishonest third party (TP). Recently, Jiang proposed a SQPC protocol based on Bell states (Quantum Inf Process 19(6): 180, 2020) and claimed it is secure. In this paper, we present two types of attack on Jiang's SQPC protocol. In the first type of attack, an outside eavesdropper will make participants accept a wrong result. In the second type of attack, a malicious participant will not only make the other participant accept a wrong result, but also learn the secret of the honest participant. Neither type of attack will be detected. In addition, we propose an improved SQPC protocol that can resist these two types of attack., Comment: 10 pages and minor revisions are made

Prediction markets are powerful tools to elicit and aggregate beliefs from strategic agents. However, in current prediction markets, agents may exhaust the social welfare by competing to be the first to update the market. We initiate the study of the trade-off between how quickly information is aggregated by the market, and how much this information costs. We design markets to aggregate timely information from strategic agents to maximize social welfare. To this end, the market must incentivize agents to invest the correct amount of effort to acquire information: quickly enough to be useful, but not faster (and more expensively) than necessary. The market also must ensure that agents report their information truthfully and on time. We consider two settings: in the first, information is only valuable before a deadline; in the second, the value of information decreases as time passes. We use both theorems and simulations to demonstrate the mechanisms.

Peer prediction mechanisms incentivize agents to truthfully report their signals even in the absence of verification by comparing agents' reports with those of their peers. In the detail-free multi-task setting, agents respond to multiple independent and identically distributed tasks, and the mechanism does not know the prior distribution of agents' signals. The goal is to provide an $\epsilon$-strongly truthful mechanism where truth-telling rewards agents "strictly" more than any other strategy profile (with $\epsilon$ additive error), and to do so while requiring as few tasks as possible. We design a family of mechanisms with a scoring function that maps a pair of reports to a score. The mechanism is strongly truthful if the scoring function is "prior ideal," and $\epsilon$-strongly truthful as long as the scoring function is sufficiently close to the ideal one. This reduces the above mechanism design problem to a learning problem -- specifically learning an ideal scoring function. We leverage this reduction to obtain the following three results. 1) We show how to derive good bounds on the number of tasks required for different types of priors. Our reduction applies to myriad continuous signal space settings. This is the first peer-prediction mechanism on continuous signals designed for the multi-task setting. 2) We show how to turn a soft-predictor of an agent's signals (given the other agents' signals) into a mechanism. This allows the practical use of machine learning algorithms that give good results even when many agents provide noisy information. 3) For finite signal spaces, we obtain $\epsilon$-strongly truthful mechanisms on any stochastically relevant prior, which is the maximal possible prior. In contrast, prior work only achieves a weaker notion of truthfulness (informed truthfulness) or requires stronger assumptions on the prior., Comment: 39 pages, 1 figure

Blind quantum computation (BQC) allows a user who has limited quantum capability to complete a quantum computational task with the aid of a remote quantum server, such that the user's input, output, and even the algorithm can be kept hidden from the server. Up to now, there are mainly two models of BQC. One is that the client just needs the ability to prepare single qubits initiated by Broadbent, Fitzsimons, and Kashefi, and the other is that the client only needs perform single-qubit measurements first given by Morimae. In this paper, we put forward a new model of BQC in which a user only requires implementing a few single-qubit gates. We also propose a specific BQC protocol where a user only needs to implement two kinds of single-qubit gates to show the feasibility of the presented model. This circuit model is quite flexible since various users with the ability to perform different single-qubit gates may all have the chance to achieve BQC. Furthermore, compared with the other two models, it may be more suitable for practical implementation in some experimental setups such as trapped ions and superconducting systems since the single-qubit gates are the most exact operations in such systems., Comment: Some changes have been made. 10 pages, 3 figures

New quantum private database (with N elements) query protocols are presented and analyzed. Protocols preserve O(logN) communication complexity of known protocols for the same task, but achieve several significant improvements in security, especially concerning user privacy. For example, the randomized form of our protocol has a cheat-sensitive property - it allows the user to detect a dishonest database with a nonzero probability, while the phase-encoded private query protocols for the same task do not have such a property. Moreover, when the database performs the computational basis measurement, a particular projective measurement which can cause a significant loss of user privacy in the previous private query protocols with O(logN) communication complexity, at most half of the user privacy could leak to such a database in our protocol, while in the QPQ protocol, the entire user privacy could leak out. In addition, it is proved here that for large N, the user could detect a cheating via the computational basis measurement, with a probability close to 1/2 using O(\sqrt{N}) special queries. Finally, it is shown here, for both forms of our protocol, basic and randomized, how a dishonest database has to act in case it could not learn user's queries.

We study the $r$-complex contagion influence maximization problem. In the influence maximization problem, one chooses a fixed number of initial seeds in a social network to maximize the spread of their influence. In the $r$-complex contagion model, each uninfected vertex in the network becomes infected if it has at least $r$ infected neighbors. In this paper, we focus on a random graph model named the stochastic hierarchical blockmodel, which is a special case of the well-studied stochastic blockmodel. When the graph is not exceptionally sparse, in particular, when each edge appears with probability $\omega(n^{-(1+1/r)})$, under certain mild assumptions, we prove that the optimal seeding strategy is to put all the seeds in a single community. This matches the intuition that in a nonsubmodular cascade model placing seeds near each other creates synergy. However, it sharply contrasts with the intuition for submodular cascade models (e.g., the independent cascade model and the linear threshold model) in which nearby seeds tend to erode each others' effects. Our key technique is a novel time-asynchronized coupling of four cascade processes. Finally, we show that this observation yields a polynomial time dynamic programming algorithm which outputs optimal seeds if each edge appears with a probability either in $\omega(n^{-(1+1/r)})$ or in $o(n^{-2})$., Comment: 30 pages, 5 figures; Published in RANDOM'19: International Conference on Randomization and Computation

We consider the influence maximization problem (selecting $k$ seeds in a network maximizing the expected total influence) on undirected graphs under the linear threshold model. On the one hand, we prove that the greedy algorithm always achieves a $(1 - (1 - 1/k)^k + \Omega(1/k^3))$-approximation, showing that the greedy algorithm does slightly better on undirected graphs than the generic $(1- (1 - 1/k)^k)$ bound which also applies to directed graphs. On the other hand, we show that substantial improvement on this bound is impossible by presenting an example where the greedy algorithm can obtain at most a $(1- (1 - 1/k)^k + O(1/k^{0.2}))$ approximation. This result stands in contrast to the previous work on the independent cascade model. Like the linear threshold model, the greedy algorithm obtains a $(1-(1-1/k)^k)$-approximation on directed graphs in the independent cascade model. However, Khanna and Lucier showed that, in undirected graphs, the greedy algorithm performs substantially better: a $(1-(1-1/k)^k + c)$ approximation for constant $c > 0$. Our results show that, surprisingly, no such improvement occurs in the linear threshold model. Finally, we show that, under the linear threshold model, the approximation ratio $(1 - (1 - 1/k)^k)$ is tight if 1) the graph is directed or 2) the vertices are weighted. In other words, under either of these two settings, the greedy algorithm cannot achieve a $(1 - (1 - 1/k)^k + f(k))$-approximation for any positive function $f(k)$. The result in setting 2) is again in a sharp contrast to Khanna and Lucier's $(1 - (1 - 1/k)^k + c)$-approximation result for the independent cascade model, where the $(1 - (1 - 1/k)^k + c)$ approximation guarantee can be extended to the setting where vertices are weighted. We also discuss extensions to more generalized settings including those with edge-weighted graphs., Comment: 36 pages, 1 figure, accepted at AAMAS'20: International Conference on Autonomous Agents and Multi-Agent Systems

Complementation of B\"uchi automata is an essential technique used in some approaches for termination analysis of programs. The long search for an optimal complementation construction climaxed with the work of Schewe, who proposed a worst-case optimal rank-based procedure that generates complements of a size matching the theoretical lower bound of $(0.76n)^n$, modulo a polynomial factor of $O(n^2)$. Although worst-case optimal, the procedure in many cases produces automata that are unnecessarily large. In this paper, we propose several ways of how to use the direct and delayed simulation relations to reduce the size of the automaton obtained in the rank-based complementation procedure. Our techniques are based on either (i) ignoring macrostates that cannot be used for accepting a word in the complement or (ii) saturating macrostates with simulation-smaller states, in order to decrease their total number. We experimentally showed that our techniques can indeed considerably decrease the size of the output of the complementation., Comment: An extended version of a paper to appear in Proc. of APLAS'19

We revisit the classic problem of proving safety over parameterised concurrent systems, i.e., an infinite family of finite-state concurrent systems that are represented by some finite (symbolic) means. An example of such an infinite family is a dining philosopher protocol with any number n of processes (n being the parameter that defines the infinite family). Regular model checking is a well-known generic framework for modelling parameterised concurrent systems, where an infinite set of configurations (resp. transitions) is represented by a regular set (resp. regular transducer). Although verifying safety properties in the regular model checking framework is undecidable in general, many sophisticated semi-algorithms have been developed in the past fifteen years that can successfully prove safety in many practical instances. In this paper, we propose a simple solution to synthesise regular inductive invariants that makes use of Angluin's classic L* algorithm (and its variants). We provide a termination guarantee when the set of configurations reachable from a given set of initial configurations is regular. We have tested L* algorithm on standard (as well as new) examples in regular model checking including the dining philosopher protocol, the dining cryptographer protocol, and several mutual exclusion protocols (e.g. Bakery, Burns, Szymanski, and German). Our experiments show that, despite the simplicity of our solution, it can perform at least as well as existing semi-algorithms., Comment: Full version of FMCAD'17 paper

We propose a novel automata model over the alphabet of rational numbers, which we call register automata over the rationals (RA-Q). It reads a sequence of rational numbers and outputs another rational number. RA-Q is an extension of the well-known register automata (RA) over infinite alphabets, which are finite automata equipped with a finite number of registers/variables for storing values. Like in the standard RA, the RA-Q model allows both equality and ordering tests between values. It, moreover, allows to perform linear arithmetic between certain variables. The model is quite expressive: in addition to the standard RA, it also generalizes other well-known models such as affine programs and arithmetic circuits. The main feature of RA-Q is that despite the use of linear arithmetic, the so-called invariant problem---a generalization of the standard non-emptiness problem---is decidable. We also investigate other natural decision problems, namely, commutativity, equivalence, and reachability. For deterministic RA-Q, commutativity and equivalence are polynomial-time inter-reducible with the invariant problem.

Spark is a new promising platform for scalable data-parallel computation. It provides several high-level application programming interfaces (APIs) to perform parallel data aggregation. Since execution of parallel aggregation in Spark is inherently non-deterministic, a natural requirement for Spark programs is to give the same result for any execution on the same data set. We present PureSpark, an executable formal Haskell specification for Spark aggregate combinators. Our specification allows us to deduce the precise condition for deterministic outcomes from Spark aggregation. We report case studies analyzing deterministic outcomes and correctness of Spark programs., Comment: an extended version of a paper accepted at NETYS'17

In this paper, we propose a novel algorithm to learn a B\"uchi automaton from a teacher who knows an $\omega$-regular language. The algorithm is based on learning a formalism named family of DFAs (FDFAs) recently proposed by Angluin and Fisman[10]. The main catch is that we use a classification tree structure instead of the standard observation table structure. The worst case storage space required by our algorithm is quadratically better than the table-based algorithm proposed in [10]. We implement the first publicly available library ROLL (Regular Omega Language Learning ), which consists of all $\omega$-regular learning algorithms available in the literature and the new algorithms proposed in this paper. Experimental results show that our tree-based algorithms have the best performance among others regarding the number of solved learning tasks., Comment: Accepted by TACAS 2017

In this paper, the implementation of an operating system oriented RBAC model is discussed. Firstly, on the basis of RBAC96 model, a new RBAC model named OSR is presented. Secondly, the OSR model is enforced in RFSOS kernel by the way of integrating GFAC method and Capability mechanism together. All parts of the OSR implementation are described in detail., Comment: in Chinese

MapReduce is a popular programming model for data parallel computation. In MapReduce, the reducer produces an output from a list of inputs. Due to the scheduling policy of the platform, the inputs may arrive at the reducers in different order. The commutativity problem of reducers asks if the output of a reducer is independent of the order of its inputs. Although the problem is undecidable in general, the MapReduce programs in practice are usually used for data analytics and thus require very simple control flow. By exploiting the simplicity, we propose a programming language for reducers where the commutativity problem is decidable. The main idea of the reducer language is to separate the control and data flow of programs and disallow arithmetic operations in the control flow. The decision procedure for the commutativity problem is obtained through a reduction to the equivalence problem of streaming numerical transducers (SNTs), a novel automata model over infinite alphabets introduced in this paper. The design of SNTs is inspired by streaming transducers (Alur and Cerny, POPL 2011). Nevertheless, the two models are intrinsically different since the outputs of SNTs are integers while those of streaming transducers are data words. The decidability of the equivalence of SNTs is achieved with an involved combinatorial analysis of the evolvement of the values of the integer variables during the runs of SNTs.

We introduce a novel technique for verification and model synthesis of sequential programs. Our technique is based on learning a regular model of the set of feasible paths in a program, and testing whether this model contains an incorrect behavior. Exact learning algorithms require checking equivalence between the model and the program, which is a difficult problem, in general undecidable. Our learning procedure is therefore based on the framework of probably approximately correct (PAC) learning, which uses sampling instead and provides correctness guarantees expressed using the terms error probability and confidence. Besides the verification result, our procedure also outputs the model with the said correctness guarantees. Obtained preliminary experiments show encouraging results, in some cases even outperforming mature software verifiers., Comment: 11 pages

Quantum pseudo-telepathy games are good examples of explaining the strangeness of quantum mechanics and demonstrating the advantage of quantum resources over classical resources. Most of the quantum pseudo-telepathy games are common interest games, nevertheless conflicting interest games are more widely used to model real world situations. Recently Pappa et al. (Phys. Rev. Lett. 114, 020401, 2015) proposed the first two-party conflicting interest game where quantum advice enhances social optimality. In the present paper we give two new three-party conflicting interest games and show that quantum advice can enhance social optimality in a three-party setting. The first game we propose is based on the famous GHZ game which is a common interest game. The second game we propose is related to the Svetlichny inequality which demonstrates quantum mechanics cannot be explained by the local hidden variable model in a three-party setting.

The monolithic integration of electronics and photonics has attracted enormous attention due to its potential applications. However, the realization of such hybrid circuits has remained a challenge because it requires optical communication at nanometer scales. A major challenge to this integration is the identification of a suitable material. After discussing the material aspect of the challenge, we identified atomically thin transition metal dichalcogenides (TMDs) as a perfect material platform to implement the circuit. The selection of TMDs is based on their very distinct property: monolayer TMDs are able to emit and absorb light at the same wavelength determined by direct exciton transitions. To prove the concept, we fabricated simple devices consisting of silver nanowires as plasmonic waveguides and monolayer TMDs as active optoelectronic media. Using photoexcitation, direct optical imaging and spectral analysis, we demonstrated generation and detection of surface plasmon polaritons by monolayer TMDs. Regarded as novel materials for electronics and photonics, transition metal dichalcogenides are expected to find new applications in next generation integrated circuits.

For the nonlinear wave equation $u_{tt} - c(u)\big(c(u) u_x\big)_x~=~0$, it is well known that solutions can develop singularities in finite time. For an open dense set of initial data, the present paper provides a detailed asymptotic description of the solution in a neighborhood of each singular point, where $|u_x|\to\infty$. The different structure of conservative and dissipative solutions is analyzed.

We apply multivariate Lagrange interpolation to synthesize polynomial quantitative loop invariants for probabilistic programs. We reduce the computation of an quantitative loop invariant to solving constraints over program variables and unknown coefficients. Lagrange interpolation allows us to find constraints with less unknown coefficients. Counterexample-guided refinement furthermore generates linear constraints that pinpoint the desired quantitative invariants. We evaluate our technique by several case studies with polynomial quantitative loop invariants in the experiments.

The total dose radiation and annealing responses of the back transistor of Silicon-On-Insulator (SOI) pMOSFETs have been studied by comparing with those of the back transistor of SOI nMOSFETs fabricated on the same wafer. The transistors were irradiated by 60Co {\gamma}-rays with various doses, and the front transistors are biased in a Float-State and Off-State, respectively, during irradiation. The total dose radiation responses of the back transistors are characterized by their threshold voltage shifts. The results show that the total dose radiation response of the back transistor of SOI pMOSFETs, similar to that of SOI nMOSFETs, depends greatly on their bias conditions during irradiation. However, with the Float-State bias, rather than the Off-State bias, the back transistors of SOI pMOSFETs reveal a much higher sensitivity to total dose radiation, which is contrary to those of SOI nMOSFETs. In addition, it is also found that the total dose radiation effect of the back transistor of SOI pMOSFETs irradiated with Off-State bias, as well as that of the SOI nMOSFETs, exhibits an increasing trend as the channel length decreases. The annealing response of the back transistors after irradiation at room temperature without bias, characterized by their threshold voltage shifts, indicates that there is a relatively complex annealing mechanism associated with channel length and type, bias condition during irradiation. In particular, for all the transistors irradiated with Off-State bias, their back transistors show an abnormal annealing effect during early annealing. All the results have been discussed and analyzed in detail by the aid of simulation.

In the probe limit, we numerically construct a holographic p-wave superfluid model in the 4D and 5D AdS black holes coupled to a Maxwell-complex vector field. We find that, for the condensate with the fixed superfluid velocity, the results are similar to the s-wave cases in both 4D and 5D spacetimes. In particular, "The Cave of Winds" and the phase transition always being the second order take place in the 5D case. Moreover, we find the second-first order translating point $\frac{S_y}{\mu}$ increases with the mass squared. Furthermore, for the supercurrent with the fixed temperature, the results agree with the GL prediction near the critical temperature. In addition, this complex vector superfluid model is still a generalization of the SU(2) superfluid model, and also provides a holographic realization of the $He_3$ superfluid system., Comment: Typos corrected;Published in Phys. Rev. D

In this paper, we study the structurally nonlinear stability of supersonic contact discontinuities in three-dimensional compressible isentropic steady flows. Based on the weakly linear stability result and the $L^2$-estimates obtained by the authors in J. Diff. Equ. 255(2013), for the linearized problems of three-dimensional compressible isentropic steady equations at a supersonic contact discontinuity satisfying certain stability conditions, we first derive tame estimates of solutions to the linearized problem in higher order norms by exploring the behavior of vorticities. Since the supersonic contact discontinuities are only weakly linearly stable, so the tame estimates of solutions to the linearized problems have loss of regularity with respect to both of background states and initial data, so to use the tame estimates to study the nonlinear problem we adapt the Nash-Moser-H\"ormander iteration scheme to conclude that weakly linearly stable supersonic contact discontinuities in three-dimensional compressible steady flows are also structurally nonlinearly stable., Comment: 33 pages