arXiv subjects

Hongfei Fu

Publications and source records attributed to Hongfei Fu.

At least 19 recordsLinked to original sources

arXiv2026

Sharp Two-Round Adaptivity and Round Hierarchies for Semantic Regular Expressions

Semantic regular expressions (SemREs) attach external Boolean predicates to matched spans, making both the number and the sequentiality of oracle calls central resources. For a fixed expression and word, we represent membership by a polynomial-size monotone span circuit and identify optimal semantic evaluation with Boolean decision-tree evaluation. We determine the extremal power of adaptivity asymptotically sharply. For every $E\ge2$, there is a unary, star-free, semantic-depth-one instance of syntax size $\Theta(E)$ with $E$ essential oracle keys and only unit-length semantic spans whose one-round cost is $E$, whereas its exact two-round and unrestricted deterministic costs are \[ \log_2 E+\tfrac12\log_2\log_2 E+O(1). \] Consequently, the largest nonadaptive-to-adaptive ratio is $(1+o(1))E/\log_2E$, including the optimal leading constant. A second restricted family exhibits a complete round hierarchy: its optimal $R$-round cost is $\Theta(R E^{1/R})$. Thus the maximal gap already appears in two rounds, while other instances interpolate smoothly across all round budgets. Both constructions admit one-predicate realizations over the fixed alphabet $\{0,1,\#\}$ with logarithmic-length semantic spans and $O(E\log^2 E)$ total representation size. Under pointwise error $\delta<1/2$ and worst-case expected cost, randomized nonadaptive complexity is exactly $(1-2\delta)E$ for every instance with $E$ essential keys. Finally, for a fixed word $w$ and $h$ predicate names, the exact randomized minimax value is $(1-2\delta)h sd(w)$, where $sd(w)$ counts distinct substring values; a span bound $s$ replaces $sd(w)$ by $sd_s(w)$. These results separate semantic information acquisition, parallel latency, and local symbolic matching cost.

cs.FL↗

arXiv2026

A linear, decoupled and positivity-preserving time-staggered block-centered finite difference method for the multi-species Keller-Segel chemotaxis system

In this paper, we present a linearly implicit, second-order block-centered finite difference (BCFD) prediction-then-projection scheme for the multi-species Keller-Segel chemotaxis system on non-uniform spatio-temporal grids. The proposed scheme integrates a standard Crank-Nicolson time-marching algorithm with an $L^2$ projection step to enforce positivity and mass conservation. The use of variable time stepsize and time-staggered discretization fully decouples the solutions of the multi-species cell density variables and the chemoattractant concentration variable while facilitating linearization, thereby greatly enhancing computational efficiency. Notably, the variable time-stepping algorithm and non-uniform grid BCFD discretization jointly enable adaptive resolution and local refinement near blow-up, thereby improving efficiency and accuracy without compromising the desired physical property-preserving in the simulation. Furthermore, using the mathematical induction method and the energy analysis approach, the unique solvability of the proposed scheme is rigorously proved, and we show that cell densities achieve second-order convergence in both time and space in the discrete $L^2$ norm, while the chemoattractant concentration achieves second-order convergence in the discrete $H^1$ norm. Representative numerical experiments are presented to validate the theoretical findings and demonstrate the reliability of the proposed scheme in simulating the blow-up phenomenon.

math.NA↗

arXiv2026

EconCSLib: A Lean Library for Computational Economics and AI-Assisted Research

Mathematical formalization uses interactive theorem provers to turn informal mathematical statements into machine-checkable artifacts. The success of mathlib, a large collaborative library for Lean, illustrates the potential of this approach. Recent progress in AI-assisted programming and theorem proving is also making large-scale formalization more practical. This paper presents EconCSLib, an early Lean 4 library for computational economics, as both infrastructure and a case study for AI-assisted formalization. The library aims to provide reusable definitions and theorems for game theory, mechanism design, social choice, and related areas. Beyond verified proofs of existing results, the library also aims to host machine-checked open problems and formalization of modern research papers. We discuss the design principles behind the library, the lessons learned from its development, and future directions for AI-assisted formalization in computational economics.

cs.GT↗

arXiv2026

Synthesizing Best Abstract Transformers via Parallel Bit-Vector Optimization

Abstract interpretation provides a principled foundation for constructing sound static analyses through systematic abstraction. A central challenge is synthesizing the best abstract transformers that achieve optimal precision within a given abstract domain. This paper addresses this problem for low-level code modeled with fixed-size bit-vectors. Recent approaches formulate the synthesis task as a multi-objective Optimization Modulo Theories (OMT) problem, but suffer from limited scalability. We introduce Spear, a parallel synthesis framework that exploits a key structural insight: while the bits within each objective must be processed sequentially, the objectives themselves are independent. Spear leverages the independence of inter-objective bits to better parallelize the synthesis. Experimental results on benchmarks across two binary analysis domains show that Spear consistently outperforms state-of-the-art OMT solvers, solving more instances and achieving significantly improved runtimes. To our knowledge, this is the first approach to apply parallelism to accelerate the synthesis of optimal abstract transformers.

cs.PL↗

arXiv2026

A variable time-step, second-order, and MBP-preserving linear stabilized scheme for the time-fractional Allen-Cahn equation

In this paper, we present a second-order linear scheme based on the variable-step Alikhanov formula and central difference discretization for the time-fractional Allen-Cahn equation. The nonlinear potential is treated explicitly via a second-order extrapolation with preprocessing, which enables the discrete maximum-bound principle (MBP) to be preserved through an appropriate stabilization technique. Moreover, by developing a discrete fractional Gr\"onwall inequality together with the uniform boundedness of numerical solutions guaranteed by the MBP, we establish an $\alpha$-robust and optimal second-order maximum-norm error estimate under initial weak singularity assumption. In addition, energy stability is proved in the sense that the discrete original energy is uniformly bounded by the initial energy plus a high-order spatiotemporal correction term. Finally, extensive numerical experiments are presented to demonstrate the effectiveness of the proposed scheme.

math.NA↗

arXiv2026

Fully decoupled, linear and structure-preserving block-centered finite difference methods for the Keller-Segel chemotaxis system on staggered non-uniform grids

In this paper, we propose two fully decoupled, linear and structure-preserving block-centered finite difference schemes for the classical Keller-Segel chemotaxis system on staggered non-uniform spatial grids. Both novel schemes are second-order accurate in space; one is first-order accurate in time, while the other achieves second-order temporal accuracy. Moreover, we show that the schemes preserve several inherent physical laws at the discrete level: (i) the positivity of both the cell density and the chemoattractant concentration; (ii) the conservation of total cell mass; and (iii) a discrete energy dissipation property for the first-order scheme. In particular, the temporally first-order scheme unconditionally preserves positivity, mass conservation, and energy dissipation, whereas the second-order scheme ensures positivity under a sufficient (but not necessary) time-step condition. The proposed methods yield more accurate and efficient simulations of chemotactic dynamics, especially in the presence of rapid blow-up phenomena, on specified non-uniform spatial grids. Numerical experiments are conducted to validate the theoretical findings and to illustrate the accuracy and reliability of the proposed schemes.

math.NA↗

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↗

arXiv2026

Probabilistic Verification of Neural Networks via Efficient Probabilistic Hull Generation

The problem of probabilistic verification of a neural network investigates the probability of satisfying the safe constraints in the output space when the input is given by a probability distribution. It is significant to answer this problem when the input is affected by disturbances often modeled by probabilistic variables. In the paper, we propose a novel neural network probabilistic verification framework which computes a guaranteed range for the safe probability by efficiently finding safe and unsafe probabilistic hulls. Our approach consists of three main innovations: (1) a state space subdivision strategy using regression trees to produce probabilistic hulls, (2) a boundary-aware sampling method which identifies the safety boundary in the input space using samples that are later used for building regression trees, and (3) iterative refinement with probabilistic prioritization for computing a guaranteed range for the safe probability. The accuracy and efficiency of our approach are evaluated on various benchmarks including ACAS Xu and a rocket lander controller. The result shows an obvious advantage over the state of the art.

cs.AI↗

arXiv2026

Array-Carrying Symbolic Execution for Function Contract Generation

Function contract generation is a classical problem in program analysis that targets the automated analysis of functions in a program with multiple procedures. The problem is fundamental in inter-procedural analysis where properties of functions are first obtained via the generation of function contracts and then the generated contracts are used as building blocks to analyze the whole program. Typical objectives in function contract generation include pre-/post-conditions and assigns information (that specifies the modification information over program variables and memory segments during function execution). In programs with array manipulations, a crucial point in function contract generation is the treatment of array segments that imposes challenges in inferring invariants and assigns information over such segments. To address this challenge, we propose a novel symbolic execution framework that carries invariants and assigns information over contiguous segments of arrays. We implement our framework as a prototype within LLVM, and further integrate our prototype with the ACSL assertion format and the Frama-C software verification platform. Experimental evaluation over a variety of benchmarks from the literature and functions from realistic libraries shows that our framework is capable of handling array manipulating functions that indeed involve the carry of array information and are beyond existing approaches.

cs.PL↗

arXiv2025

Unconditional optimal-order error estimates of linear relaxation compact difference scheme for the coupled nonlinear Schr\"odinger system

This paper presents a linear, decoupled, mass- and energy-conserving numerical scheme for the multi-dimensional coupled nonlinear Schr\"odinger (CNLS) system. The scheme combines the fourth-order compact difference approximation in space with the relaxation technique in a time-staggered mesh framework, solving the primal unknowns and introduced auxiliary relaxation variables sequentially with high efficiency and high-order accuracy. We show the unique solvability and discrete conservation laws of the developed scheme. In particular, for the first time, leveraging an auxiliary error equation system combined with the cut-off technique, optimal-order error estimates in the discrete H1-norm for the primal variables at the time nodes, and in the discrete L2-norm for the auxiliary relaxation variables at the intermediate time nodes, are rigorously proved without any coupling mesh conditions, which contribute to the primary theoretical contribution of this paper for multi-dimensional CNLS system. Numerical experiments demonstrate convincingly the strong performance of the proposed scheme in long-term simulations, maintaining both physical invariants and high-order accuracy.

math.NA↗

arXiv2025

Numerical analysis and efficient implementation of fast collocation methods for fractional Laplacian model on nonuniform grids

We propose a fast collocation method based on Krylov subspace iterative solver on general nonuniform grids for the fractional Laplacian problem, in which the fractional operator is presented in a singular integral formulation. The method is proved to be uniquely solvable on general nonuniform grids for $\alpha\in(0,1)$, provided that the sum-of-exponentials (SOE) approximation is sufficiently accurate. In addition, a modified scheme is developed and proved to be uniquely solvable on uniform grids for $\alpha\in(0,2)$. Efficient implementation of the proposed fast collocation schemes based on fast matrix-vector multiplication is carefully discussed, in terms of computational complexity and memory requirement. To further improve computational efficiency, a banded preconditioner is incorporated into the Krylov subspace iterative solver. A rigorous maximum-norm error analysis for $\alpha\in(0,1)$ is presented on specific graded grids, which shows that the convergence order depends on the grading parameter. Numerical experiments validate the predicted convergence and demonstrate the efficiency of the fast collocation schemes.

math.NA↗

arXiv2025

Dynamic-stabilization-based linear schemes for the Allen-Cahn equation with degenerate mobility: MBP and energy stability

In this paper, we investigate linear first- and second-order numerical schemes for the Allen--Cahn equation with a general (possibly degenerate) mobility. Compared with existing numerical methods, our schemes employ a novel dynamic stabilization approach that guarantees unconditional preservation of the maximum bound principle (MBP) and energy stability. A key advance is that the discrete energy stability remains valid even in the presence of degenerate mobility-a property we refer to as mobility robustness. Rigorous maximum-norm error estimates are also established. In particular, for the second-order scheme, we introduce a new prediction strategy with a cut-off preprocessing procedure on the extrapolation solution, and only one linear system needs to be solved per time level. Representative numerical examples are provided to validate the theoretical findings and performance of the proposed schemes.

math.NA↗

arXiv2025

High-order nonuniform time-stepping and MBP-preserving linear schemes for the time-fractional Allen-Cahn equation

In this paper, we present a class of nonuniform time-stepping, high-order linear stabilized schemes that can preserve both the discrete energy stability and maximum-bound principle (MBP) for the time-fractional Allen-Cahn equation. To this end, we develop a new prediction strategy to obtain a second-order and MBP-preserving predicted solution, which is then used to handle the nonlinear potential explicitly. Additionally, we introduce an essential nonnegative auxiliary functional that enables the design of an appropriate stabilization term to dominate the predicted nonlinear potential, and thus to preserve the discrete MBP. Combining the newly developed prediction strategy and auxiliary functional, we propose two unconditionally energy-stable linear stabilized schemes, L1 and L2-$1_\sigma$ schemes. We show that the L1 scheme unconditionally preserves the discrete MBP, whereas the L2-$1_\sigma$ scheme requires a mild time-step restriction. Furthermore, we develop an improved L2-$1_\sigma$ scheme with enhanced MBP preservation for large time steps, achieved through a novel unbalanced stabilization term that leverages the boundedness and monotonicity of the auxiliary functional. Representative numerical examples validate the accuracy, effectiveness, and physics-preserving of the proposed methods.

math.NA↗

arXiv2025

Structural Abstraction and Refinement for Probabilistic Programs

In this paper, we present structural abstraction refinement, a novel framework for verifying the threshold problem of probabilistic programs. Our approach represents the structure of a Probabilistic Control-Flow Automaton (PCFA) as a Markov Decision Process (MDP) by abstracting away statement semantics. The maximum reachability of the MDP naturally provides a proper upper bound of the violation probability, termed the structural upper bound. This introduces a fresh ``structural'' characterization of the relationship between PCFA and MDP, contrasting with the traditional ``semantical'' view, where the MDP reflects semantics. The method uniquely features a clean separation of concerns between probability and computational semantics that the abstraction focuses solely on probabilistic computation and the refinement handles only the semantics aspect, where the latter allows non-random program verification techniques to be employed without modification. Building upon this feature, we propose a general counterexample-guided abstraction refinement (CEGAR) framework, capable of leveraging established non-probabilistic techniques for probabilistic verification. We explore its instantiations using trace abstraction. Our method was evaluated on a diverse set of examples against state-of-the-art tools, and the experimental results highlight its versatility and ability to handle more flexible structures swiftly.

cs.FL↗

arXiv2025

Error estimates of linear decoupled structure-preserving incremental viscosity splitting methods for the Cahn--Hilliard--Navier--Stokes system

We propose first- and second-order time discretization schemes for the coupled Cahn--Hilliard--Navier--Stokes model, leveraging the incremental viscosity splitting (IVS) method. The schemes combine the scalar auxiliary variable method and the zero-energy-contribution approach, resulting in a linear, decoupled numerical framework. At each time step, they only require to solve a sequence of constant-coefficient equations, along with a linear equation with one unknown, making the algorithms computationally efficient and easy to implement. In addition, the proposed schemes are proven to be uniquely solvable, mass-conserving, and unconditional energy dissipation. Most importantly, leveraging the mathematical induction method and the regularity properties of the Stokes equation, we perform a rigorous error analysis for the first-order scheme in multiple space dimensions, establishing an unconditional and optimal convergence rate for all relevant variables under different norms. A user-defined, time-dependent parameter plays an important role in the error analysis of the proposed structure-preserving IVS methods. Ample numerical examples are carried out to verify the theoretical findings and to demonstrate the accuracy, effectiveness and efficiency of the proposed schemes.

math.NA↗

arXiv2025

A linear, mass-conserving, multi-time-step compact block-centered finite difference method for incompressible miscible displacement problem in porous media

In this paper, a two-dimensional incompressible miscible displacement model is considered, and a novel decoupled and linearized high-order finite difference scheme is developed, by utilizing the multi-time-step strategy to treat the different time evolutions of concentration and velocity/pressure, and the compact block-centered finite difference approximation for spatial discretization. We show that the scheme is mass-conserving, and has second-order temporal accuracy and fourth-order spatial accuracy for the concentration, the velocity and the pressure simultaneously. The existence and uniqueness of the developed scheme under a rough time-step condition is also proved following the convergence results. Numerical experiments are presented to confirm the theoretical conclusions. Besides, some 'real' simulations are also tested to show good performance of the proposed scheme, in particular, the viscous fingering phenomenon is verified.

math.NA↗

arXiv2025

Polynomial Invariant Generation for Floating-Point Programs

In numeric-intensive computations, it is well known that the execution of floating-point programs is imprecise as floating-point arithmetic incurs round-off errors. Although round-off errors are small for a single floating-point operation, the aggregation of such errors may be dramatic and cause catastrophic program failures. Therefore, to ensure the correctness of floating-point programs, round-off error needs to be carefully taken into account. In this work, we consider polynomial invariant generation for floating-point programs, aiming at generating tight invariants under the perturbation of round-off errors. Our contribution is a novel framework for applying polynomial constraint solving to address the invariant generation problem, which is also the first polynomial constraint solving based approach that handles floating-point errors to our best knowledge. In our framework, we propose a novel combination of round-off error analysis and polynomial constraint solving, aiming to circumvent the cost of handling a large number of error variables in the floating-point model. Experimental results over a variety of challenging benchmarks show that our framework outperforms SOTA approaches in both time efficiency and the precision of generated invariants.

cs.PL↗

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 $\phi$; 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} := \tau_{k}/\tau_{k-1} < 4.864 - \delta $ with a positive constant $\delta$ 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↗