arXiv subjects

Hongfei Fu

Publications and source records attributed to Hongfei Fu.

At least 37 records · Page 2Linked to original sources

arXiv2025

Energy dissipation law and maximum bound principle-preserving linear BDF2 schemes with variable steps for the Allen-Cahn equation

In this paper, we propose and analyze a linear, structure-preserving scalar auxiliary variable (SAV) method for solving the Allen--Cahn equation based on the second-order backward differentiation formula (BDF2) with variable time steps. To this end, we first design a novel and essential auxiliary functional that serves twofold functions: (i) ensuring that a first-order approximation to the auxiliary variable, which is essentially important for deriving the unconditional energy dissipation law, does not affect the second-order temporal accuracy of the phase function $ϕ$; and (ii) allowing us to develop effective stabilization terms that are helpful to establish the MBP-preserving linear methods. Together with this novel functional and standard central difference stencil, we then propose a linear, second-order variable-step BDF2 type stabilized exponential SAV scheme, namely BDF2-sESAV-I, which is shown to preserve both the discrete modified energy dissipation law under the temporal stepsize ratio $ 0 < r_{k} := τ_{k}/τ_{k-1} < 4.864 - δ$ with a positive constant $δ$ and the MBP under $ 0 < r_{k} < 1 + \sqrt{2} $. Moreover, an analysis of the approximation to the original energy by the modified one is presented. With the help of the kernel recombination technique, optimal $ H^{1}$- and $ L^{\infty}$-norm error estimates of the variable-step BDF2-sESAV-I scheme are rigorously established. Numerical examples are carried out to verify the theoretical results and demonstrate the effectiveness and efficiency of the proposed scheme.

math.NA↗

arXiv2025

A decoupled linear, mass-conservative block-centered finite difference method for the Keller-Segel chemotaxis system

As a class of nonlinear partial differential equations, the Keller-Segel system is widely used to model chemotaxis in biology. In this paper, we present the construction and analysis of a decoupled linear, mass-conservative, block-centered finite difference method for the classical Keller-Segel chemotaxis system. We show that the scheme is mass conservative for the cell density at the discrete level. In addition, second-order temporal and spatial convergence for both the cell density and the chemoattractant concentration are rigorously discussed, using the mathematical induction method, the discrete energy method and detailed analysis of the truncation errors. Our scheme is proposed and analyzed on non-uniform spatial grids, which leads to more accurate and efficient modeling results for the chemotaxis system with rapid blow-up phenomenon. Furthermore, the existence and uniqueness of solutions to the Keller-Segel chemotaxis system are also discussed. Numerical experiments are presented to verify the theoretical results and to show the robustness and accuracy of the scheme.

math.NA↗

arXiv2024

Affine Disjunctive Invariant Generation with Farkas' Lemma

In the verification of loop programs, disjunctive invariants are essential to capture complex loop dynamics such as phase and mode changes. In this work, we develop a novel approach for the automated generation of affine disjunctive invariants for affine while loops via Farkas' Lemma, a fundamental theorem on linear inequalities. Our main contributions are two-fold. First, we combine Farkas' Lemma with a succinct control flow transformation to derive disjunctive invariants from the conditional branches in the loop. Second, we propose an invariant propagation technique that minimizes the invariant computation effort by propagating previously solved invariants to yet unsolved locations as much as possible. Furthermore, we resolve the infeasibility checking in the application of Farkas' Lemma which has not been addressed previously, and extend our approach to nested loops via loop summary. Experimental evaluation over more than 100 affine while loops (mostly from SV-COMP 2023) demonstrates that our approach is promising to generate tight linear invariants over affine programs.

cs.LO↗

arXiv2024

A fast fractional block-centered finite difference method for two-sided space-fractional diffusion equations on general nonuniform grids

In this paper, a two-sided variable-coefficient space-fractional diffusion equation with fractional Neumann boundary condition is considered. To conquer the weak singularity caused by nonlocal space-fractional differential operators, a fractional block-centered finite difference (BCFD) method on general nonuniform grids is proposed. However, this discretization still results in an unstructured dense coefficient matrix with huge memory requirement and computational complexity. To address this issue, a fast version fractional BCFD algorithm by employing the well-known sum-of-exponentials (SOE) approximation technique is also proposed. Based upon the Krylov subspace iterative methods, fast matrix-vector multiplications of the resulting coefficient matrices with any vector are developed, in which they can be implemented in only $\mathcal{O}(MN_{exp})$ operations per iteration without losing any accuracy compared to the direct solvers, where $N_{exp}\ll M$ is the number of exponentials in the SOE approximation. Moreover, the coefficient matrices do not necessarily need to be generated explicitly, while they can be stored in $\mathcal{O}(MN_{exp})$ memory by only storing some coefficient vectors. Numerical experiments are provided to demonstrate the efficiency and accuracy of the method.

math.NA↗

arXiv2024

Fractional-step High-order and Bound-preserving Method for Convection Diffusion Equations

In this paper, we derive two bound-preserving and mass-conserving schemes based on the fractional-step method and high-order compact (HOC) finite difference method for nonlinear convection-dominated diffusion equations. We split the one-dimensional equation into three stages, and employ appropriate temporal and spatial discrete schemes respectively. We show that our scheme is weakly monotonic and that the bound-preserving property can be achieved using the bound-preserving limiter under some mild step constraints. By employing the alternating direction implicit (ADI) method, we extend the scheme to two-dimensional problems, further reducing computational cost. We also provide various numerical experiments to verify our theoretical results.

math.NA↗

arXiv2024

Strang splitting structure-preserving high-order compact difference schemes for nonlinear convection diffusion equations

In this paper, we present a class of high-order and efficient compact difference schemes for nonlinear convection diffusion equations, which can preserve both bounds and mass. For the one-dimensional problem, we first introduce a high-order compact Strang splitting scheme (denoted as HOC-Splitting), which is fourth-order accurate in space and second-order accurate in time. Then, by incorporating the Lagrange multiplier approach with the HOC-Splitting scheme, we construct two additional bound-preserving or/and mass-conservative HOC-Splitting schemes that do not require excessive computational cost and can automatically ensure the uniform bounds of the numerical solution. These schemes combined with an alternating direction implicit (ADI) method are generalized to the two-dimensional problem, which further enhance the computational efficiency for large-scale modeling and simulation. Besides, we present an optimal-order error estimate for the bound-preserving ADI scheme in the discrete $L_2$ norm. Finally, ample numerical examples are presented to verify the theoretical results and demonstrate the accuracy, efficiency, and effectiveness in preserving bounds or/and mass of the proposed schemes.

math.NA↗

arXiv2024

Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving

In Bayesian probabilistic programming, a central problem is to estimate the normalised posterior distribution (NPD) of a probabilistic program with conditioning via score (a.k.a. observe) statements. Most previous approaches address this problem by Markov Chain Monte Carlo and variational inference, and therefore could not generate guaranteed outcomes within a finite time limit. Moreover, existing methods for exact inference either impose syntactic restrictions or cannot guarantee successful inference in general. In this work, we propose a novel automated approach to derive guaranteed bounds for NPD via polynomial solving. We first establish a fixed-point theorem for the wide class of score-at-end Bayesian probabilistic programs that terminate almost-surely and have a single bounded score statement at program termination. Then, we propose a multiplicative variant of Optional Stopping Theorem (OST) to address score-recursive Bayesian programs where score statements with weights greater than one could appear inside a loop. Finally, we use polynomial solving to implement our fixed-point theorem and OST variant. To improve the accuracy of the polynomial solving, we further propose a truncation operation and the synthesis of multiple bounds over various program inputs. Our approach can handle Bayesian probabilistic programs with unbounded while loops and continuous distributions with infinite supports. Experiments over a wide range of benchmarks show that compared with the most relevant approach (Beutner et al., PLDI 2022) for guaranteed NPD analysis via recursion unrolling, our approach is more time efficient and derives comparable or even tighter NPD bounds. Furthermore, our approach can handle score-recursive programs which previous approaches could not.

cs.PL↗

arXiv2024

Equational Bit-Vector Solving via Strong Gröbner Bases

Bit-vectors, which are integers in a finite number of bits, are ubiquitous in software and hardware systems. In this work, we consider the satisfiability modulo theories (SMT) of bit-vectors. Unlike normal integers, the arithmetics of bit-vectors are modular upon integer overflow. Therefore, the SMT solving of bit-vectors needs to resolve the underlying modular arithmetics. In the literature, two prominent approaches for SMT solving are bit-blasting (that transforms the SMT problem into boolean satisfiability) and integer solving (that transforms the SMT problem into integer properties). Both approaches ignore the algebraic properties of the modular arithmetics and hence could not utilize these properties to improve the efficiency of SMT solving. In this work, we consider the equational theory of bit-vectors and capture the algebraic properties behind them via strong Gröbner bases. First, we apply strong Gröbner bases to the quantifier-free equational theory of bit-vectors and propose a novel algorithmic improvement in the key computation of multiplicative inverse modulo a power of two. Second, we resolve the important case of invariant generation in quantified equational bit-vector properties via strong Gröbner bases and linear congruence solving. Experimental results over an extensive range of benchmarks show that our approach outperforms existing methods in both time efficiency and memory consumption.

cs.LO↗

arXiv2024

Maximum-Norm Error Estimates of Fourth-Order Compact and ADI Compact Finite Difference Methods for Nonlinear Coupled Bacterial Systems

In this paper, by introducing two temporal-derivative-dependent auxiliary variables, a linearized and decoupled fourth-order compact finite difference method is developed and analyzed for the nonlinear coupled bacterial systems. The temporal-spatial error splitting technique and discrete energy method are employed to prove the unconditional stability and convergence of the method in discrete maximum norm. Furthermore, to improve the computational efficiency, an alternating direction implicit (ADI) compact difference algorithm is proposed, and the unconditional stability and optimal-order maximum-norm error estimate for the ADI scheme are also strictly established. Finally, several numerical experiments are conducted to validate the theoretical convergence and to simulate the phenomena of bacterial extinction as well as the formation of endemic diseases.

math.NA↗

arXiv2023

An efficient two-grid fourth-order compact difference scheme with variable-step BDF2 method for the semilinear parabolic equation

Due to the lack of corresponding analysis on appropriate mapping operator between two grids, high-order two-grid difference algorithms are rarely studied. In this paper, we firstly discuss the boundedness of a local bi-cubic Lagrange interpolation operator. And then, taking the semilinear parabolic equation as an example, we first construct a variable-step high-order nonlinear difference algorithm using compact difference technique in space and the second-order backward differentiation formula (BDF2) with variable temporal stepsize in time. With the help of discrete orthogonal convolution (DOC) kernels and a cut-off numerical technique, the unique solvability and corresponding error estimates of the high-order nonlinear difference scheme are established under assumptions that the temporal stepsize ratio satisfies rk < 4.8645 and the maximum temporal stepsize satisfies tau = o(h^1/2 ). Then, an efficient two-grid high-order difference algorithm is developed by combining a small-scale variable-step high-order nonlinear difference algorithm on the coarse grid and a large-scale variable-step high-order linearized difference algorithm on the fine grid, in which the constructed piecewise bi-cubic Lagrange interpolation mapping operator is adopted to project the coarse-grid solution to the fine grid. Under the same temporal stepsize ratio restriction rk < 4.8645 and a weaker maximum temporal stepsize condition tau = o(H^1.2 ), optimal fourth-order in space and second-order in time error estimates of the two-grid difference scheme is established if the coarse-fine grid stepsizes satisfy H = O(h^4/7). Finally, several numerical experiments are carried out to demonstrate the effectiveness and efficiency of the proposed scheme.

math.NA↗

arXiv2023

High order numerical methods based on quadratic spline collocation method and averaged L1 scheme for the variable-order time fractional mobile/immobile diffusion equation

In this paper, we consider the variable-order time fractional mobile/immobile diffusion (TF-MID) equation in two-dimensional spatial domain, where the fractional order $α(t)$ satisfies $0<α_{*}\leq α(t)\leq α^{*}<1$. We combine the quadratic spline collocation (QSC) method and the $L1^+$ formula to propose a QSC-$L1^+$ scheme. It can be proved that, the QSC-$L1^+$ scheme is unconditionally stable and convergent with $\mathcal{O}(τ^{\min{\{3-α^*-α(0),2\}}} + Δx^{2}+Δy^{2})$, where $τ$, $Δx$ and $Δy$ are the temporal and spatial step sizes, respectively. With some proper assumptions on $α(t)$, the QSC-$L1^+$ scheme has second temporal convergence order even on the uniform mesh, without any restrictions on the solution of the equation. We further construct a novel alternating direction implicit (ADI) framework to develop an ADI-QSC-$L1^+$ scheme, which has the same unconditionally stability and convergence orders. In addition, a fast implementation for the ADI-QSC-$L1^+$ scheme based on the exponential-sum-approximation (ESA) technique is proposed. Moreover, we also introduce the optimal QSC method to improve the spatial convergence to fourth-order. Numerical experiments are attached to support the theoretical analysis, and to demonstrate the effectiveness of the proposed schemes.

math.NA↗

arXiv2023

Automated Tail Bound Analysis for Probabilistic Recurrence Relations

Probabilistic recurrence relations (PRRs) are a standard formalism for describing the runtime of a randomized algorithm. Given a PRR and a time limit $κ$, we consider the classical concept of tail probability $\Pr[T \ge κ]$, i.e., the probability that the randomized runtime $T$ of the PRR exceeds the time limit $κ$. Our focus is the formal analysis of tail bounds that aims at finding a tight asymptotic upper bound $u \geq \Pr[T\geκ]$ in the time limit $κ$. To address this problem, the classical and most well-known approach is the cookbook method by Karp (JACM 1994), while other approaches are mostly limited to deriving tail bounds of specific PRRs via involved custom analysis. In this work, we propose a novel approach for deriving exponentially-decreasing tail bounds (a common type of tail bounds) for PRRs whose preprocessing time and random passed sizes observe discrete or (piecewise) uniform distribution and whose recursive call is either a single procedure call or a divide-and-conquer. We first establish a theoretical approach via Markov's inequality, and then instantiate the theoretical approach with a template-based algorithmic approach via a refined treatment of exponentiation. Experimental evaluation shows that our algorithmic approach is capable of deriving tail bounds that are (i) asymptotically tighter than Karp's method, (ii) match the best-known manually-derived asymptotic tail bound for QuickSelect, and (iii) is only slightly worse (with a $\log\log n$ factor) than the manually-proven optimal asymptotic tail bound for QuickSort. Moreover, our algorithmic approach handles all examples (including realistic PRRs such as QuickSort, QuickSelect, DiameterComputation, etc.) in less than 0.1 seconds, showing that our approach is efficient in practice.

cs.DS↗

arXiv2022

Guided Diffusion Model for Adversarial Purification

With wider application of deep neural networks (DNNs) in various algorithms and frameworks, security threats have become one of the concerns. Adversarial attacks disturb DNN-based image classifiers, in which attackers can intentionally add imperceptible adversarial perturbations on input images to fool the classifiers. In this paper, we propose a novel purification approach, referred to as guided diffusion model for purification (GDMP), to help protect classifiers from adversarial attacks. The core of our approach is to embed purification into the diffusion denoising process of a Denoised Diffusion Probabilistic Model (DDPM), so that its diffusion process could submerge the adversarial perturbations with gradually added Gaussian noises, and both of these noises can be simultaneously removed following a guided denoising process. On our comprehensive experiments across various datasets, the proposed GDMP is shown to reduce the perturbations raised by adversarial attacks to a shallow range, thereby significantly improving the correctness of classification. GDMP improves the robust accuracy by 5%, obtaining 90.1% under PGD attack on the CIFAR10 dataset. Moreover, GDMP achieves 70.94% robustness on the challenging ImageNet dataset.

cs.CV↗

arXiv2020

Quantitative Analysis of Assertion Violations in Probabilistic Programs

In this work, we consider the fundamental problem of deriving quantitative bounds on the probability that a given assertion is violated in a probabilistic program. We provide automated algorithms that obtain both lower and upper bounds on the assertion violation probability in exponential forms. The main novelty of our approach is that we prove new and dedicated fixed-point theorems which serve as the theoretical basis of our algorithms and enable us to reason about assertion violation bounds in terms of pre and post fixed-point functions. To synthesize such fixed-points, we devise algorithms that utilize a wide range of mathematical tools, including repulsing ranking super-martingales, Hoeffding's lemma, Minkowski decompositions, Jensen's inequality, and convex optimization. On the theoretical side, we provide (i) the first automated algorithm for lower-bounds on assertion violation probabilities, (ii) the first complete algorithm for upper-bounds of exponential form in affine programs, and (iii) provably and significantly tighter upper-bounds than the previous approach of stochastic invariants. On the practical side, we show that our algorithms can handle a wide variety of programs from the literature and synthesize bounds that are several orders of magnitude tighter in comparison with previous approaches.

cs.PL↗

arXiv2020

Concentration-Bound Analysis for Probabilistic Programs and Probabilistic Recurrence Relations

Analyzing probabilistic programs and randomized algorithms are classical problems in computer science. The first basic problem in the analysis of stochastic processes is to consider the expectation or mean, and another basic problem is to consider concentration bounds, i.e. showing that large deviations from the mean have small probability. Similarly, in the context of probabilistic programs and randomized algorithms, the analysis of expected termination time/running time and their concentration bounds are fundamental problems.In this work, we focus on concentration bounds for probabilistic programs and probabilistic recurrences of randomized algorithms. For probabilistic programs, the basic technique to achieve concentration bounds is to consider martingales and apply the classical Azuma's inequality. For probabilistic recurrences of randomized algorithms, Karp's classical "cookbook" method, which is similar to the master theorem for recurrences, is the standard approach to obtain concentration bounds. In this work, we propose a novel approach for deriving concentration bounds for probabilistic programs and probabilistic recurrence relations through the synthesis of exponential supermartingales. For probabilistic programs, we present algorithms for synthesis of such supermartingales in several cases. We also show that our approach can derive better concentration bounds than simply applying the classical Azuma's inequality over various probabilistic programs considered in the literature. For probabilistic recurrences, our approach can derive tighter bounds than the Karp's well-established methods on classical algorithms. Moreover, we show that our approach could derive bounds comparable to the optimal bound for quicksort, proposed by McDiarmid and Hayward. We also present a prototype implementation that can automatically infer these bounds

cs.PL↗

arXiv2020

Inductive Reachability Witnesses

In this work, we consider the fundamental problem of reachability analysis over imperative programs with real variables. The reachability property requires that a program can reach certain target states during its execution. Previous works that tackle reachability analysis are either unable to handle programs consisting of general loops (e.g. symbolic execution), or lack completeness guarantees (e.g. abstract interpretation), or are not automated (e.g. incorrectness logic/reverse Hoare logic). In contrast, we propose a novel approach for reachability analysis that can handle general programs, is (semi-)complete, and can be entirely automated for a wide family of programs. Our approach extends techniques from both invariant generation and ranking-function synthesis to reachability analysis through the notion of (Universal) Inductive Reachability Witnesses (IRWs/UIRWs). While traditional invariant generation uses over-approximations of reachable states, we consider the natural dual problem of under-approximating the set of program states that can reach a target state. We then apply an argument similar to ranking functions to ensure that all states in our under-approximation can indeed reach the target set in finitely many steps.

cs.PL↗

arXiv2020

Polynomial Invariant Generation for Non-deterministic Recursive Programs

We consider the classical problem of invariant generation for programs with polynomial assignments and focus on synthesizing invariants that are a conjunction of strict polynomial inequalities. We present a sound and semi-complete method based on positivstellensaetze, i.e. theorems in semi-algebraic geometry that characterize positive polynomials over a semi-algebraic set. To the best of our knowledge, this is the first invariant generation method to provide completeness guarantees for invariants consisting of polynomial inequalities. Moreover, on the theoretical side, the worst-case complexity of our approach is subexponential, whereas the worst-case complexity of the previously-known complete method (Colon et al, CAV 2003), which could only handle linear invariants, is exponential. On the practical side, we reduce the invariant generation problem to quadratic programming (QCLP), which is a classical optimization problem with many industrial solvers. Finally, we demonstrate the applicability of our approach by providing experimental results on several academic benchmarks.

cs.LO↗

arXiv2019

Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time

The notion of program sensitivity (aka Lipschitz continuity) specifies that changes in the program input result in proportional changes to the program output. For probabilistic programs the notion is naturally extended to expected sensitivity. A previous approach develops a relational program logic framework for proving expected sensitivity of probabilistic while loops, where the number of iterations is fixed and bounded. In this work, we consider probabilistic while loops where the number of iterations is not fixed, but randomized and depends on the initial input values. We present a sound approach for proving expected sensitivity of such programs. Our sound approach is martingale-based and can be automated through existing martingale-synthesis algorithms. Furthermore, our approach is compositional for sequential composition of while loops under a mild side condition. We demonstrate the effectiveness of our approach on several classical examples from Gambler's Ruin, stochastic hybrid systems and stochastic gradient descent. We also present experimental results showing that our automated approach can handle various probabilistic programs in the literature.

cs.PL↗