arXiv subjects

Yichen Tao

Publications and source records attributed to Yichen Tao.

5 recordsLinked to original sources

arXiv2026

Probabilistic Floating-Point Round-Off Analysis via Concentration Inequalities

Floating-point round-off errors are ubiquitous in numerically intensive programs arising in fields such as scientific computing and optimization. As floating-point errors potentially lead to unexpected and catastrophic program failures, one must derive guaranteed round-off thresholds to ensure the correctness of these programs. However, deterministic round-off thresholds tend to be too conservative to be usable in practice, since they often involve large round-off errors that occur with small probability. Probabilistic thresholds relax deterministic ones by specifying that the probability of the round-off error exceeding a threshold is below a given confidence. In this work, we propose a novel approach to probabilistic round-off analysis, by applying concentration inequalities over the Taylor expansion from FPTaylor (TOPLAS 2018). A major obstacle in applying concentration inequalities is that the Taylor expansion involves absolute value operators that make the calculation of the expected values of the first order partial differential terms difficult. Our first step to overcome this obstacle is a sound over-approximation that removes the absolute value operators in polynomial expressions. Then, we show how to handle fractional expressions by a transformation into polynomial case. Finally, we show how to improve our approach with range partitioning. Our approach is scalable since the key computational part is the calculation of expected values of polynomial expressions with independent variables, for which the linear and independence properties of expectation boost the computation. Experimental results show that our approach is orders of magnitude more time efficient, while producing thresholds with comparable precision against the state of the art.

cs.LO↗

arXiv2024

Floquet Isospectrality of the Zero Potential for Discrete Periodic Schr\"odinger Operators

Let $\Gamma=q_1\mathbb{Z}\oplus q_2 \mathbb{Z}\oplus\cdots\oplus q_d\mathbb{Z}$, with $q_j\in (\mathbb{Z}^+)^d$ for each $j\in \{1,\ldots,d\}$, and denote by $\Delta$ the discrete Laplacian on $\ell^2\left( \mathbb{Z}^d\right)$. Using Macaulay2, we first numerically find complex-valued $\Gamma$-periodic potentials $V:\mathbb{Z}^d\to \mathbb{C}$ such that the operators $\Delta+V$ and $\Delta$ are Floquet isospectral. We then use combinatorial methods to validate these numerical solutions.

math.SP↗

arXiv2024

A Complete Landscape for the Price of Envy-Freeness

We study the efficiency of fair allocations using the well-studied price of fairness concept, which quantitatively measures the worst-case efficiency loss when imposing fairness constraints. Previous works provided partial results on the price of fairness with well-known fairness notions such as envy-freeness up to one good (EF1) and envy-freeness up to any good (EFX). In this paper, we give a complete characterization for the price of envy-freeness in various settings. In particular, we first consider the two-agent case under the indivisible-goods setting and present tight ratios for the price of EF1 (for scaled utility) and EFX (for unscaled utility), which resolve questions left open in the literature. Next, we consider the mixed goods setting which concerns a mixture of both divisible and indivisible goods. We focus on envy-freeness for mixed goods (EFM), which generalizes both envy-freeness and EF1, as well as its strengthening called envy-freeness up to any good for mixed goods (EFXM), which generalizes envy-freeness and EFX. To this end, we settle the price of EFM and EFXM by providing a complete picture of tight bounds for two agents and asymptotically tight bounds for $n$ agents, for both scaled and unscaled utilities.

cs.GT↗

arXiv2023

Verifying Programs with Logic and Extended Proof Rules: Deep Embedding v.s. Shallow Embedding

Many foundational program verification tools have been developed to build machine-checked program correctness proofs, a majority of which are based on Hoare logic. Their program logics, their assertion languages, and their underlying programming languages can be formalized by either a shallow embedding or a deep embedding. Tools like Iris and early versions of Verified Software Toolchain (VST) choose different shallow embeddings to formalize their program logics. But the pros and cons of these different embeddings were not yet well studied. Therefore, we want to study the impact of the program logic's embedding on logic's proof rules in this paper. This paper considers a set of useful extended proof rules, and four different logic embeddings: one deep embedding and three common shallow embeddings. We prove the validity of these extended rules under these embeddings and discuss their main challenges. Furthermore, we propose a method to lift existing shallowly embedded logics to deeply embedded ones to greatly simplify proofs of extended rules in specific proof systems. We evaluate our results on two existing verification tools. We lift the originally shallowly embedded VST to our deeply embedded VST to support extended rules, and we implement Iris-CF and deeply embedded Iris-Imp based on the Iris framework to evaluate our theory in real verification projects.

cs.PL↗

arXiv2023

Impacts of permeability heterogeneity and background flow on supercritical CO2 dissolution in the deep subsurface

Motivated by CO2 capture and sequestration (CCS) design considerations, we consider the coupled effects of permeability heterogeneity and background flow on the dissolution of a supercritical CO2 lens into an underlying deep, confined aquifer. We present the results of a large-scale Monte Carlo simulation study examining the interaction of background flow rate and three parameters describing multi-Gaussian log-permeability fields: mean, variance, and correlation length. Hundreds of high-resolution simulations were performed using the PFLOTRAN finite volume software to model CO2 dissolution in a kilometer-scale aquifer over 1000 y. Predictive dimensionless scaling relationships relating CO2 dissolution rate to heterogeneity statistics, Rayleigh (Ra) and Peclet (Pe) numbers were developed for both gravitationally dominated free convection to background flow-dominated forced convection regimes. An empirical criterion, $\rm Pe\ = Ra^{3/4}$, was discovered for regime transition. All simulations converged quickly to a quasi-steady, approximately linear dissolution rate. However, this rate displayed profound variability between permeability field realizations sharing the same heterogeneity statistics, even under mild permeability heterogeneity. In general, increased heterogeneity was associated with a lower mean and higher variance of dissolution rate, undesirable from a CCS design perspective. The relationship between dissolution rate and background flow was found to be complex and nonlinear. Dimensionless scaling relationships were uncovered for a number of special cases. Results call into question the validity of the Boussinesq approximation in the context of modest-to-high background flow rates and the general applicability of numerical simulations without background flow.

physics.flu-dyn↗