More Like this

1. A verified decision procedure for univariate real arithmetic with the BKR algorithm.

   Cordwell, Katherine; Tan, Yong Kiam; Platzer, André (June 2021, 12th International Conference on Interactive Theorem Proving (ITP 2021))

   Cohen, Liron; Kaliszyk, Cezary (Ed.)

   We formalize the univariate fragment of Ben-Or, Kozen, and Reif’s (BKR) decision procedure for first-order real arithmetic in Isabelle/HOL. BKR’s algorithm has good potential for parallelism and was designed to be used in practice. Its key insight is a clever recursive procedure that computes the set of all consistent sign assignments for an input set of univariate polynomials while carefully managing intermediate steps to avoid exponential blowup from naively enumerating all possible sign assignments (this insight is fundamental for both the univariate case and the general case). Our proof combines ideas from BKR and a follow-up work by Renegar that are well-suited for formalization. The resulting proof outline allows us to build substantially on Isabelle/HOL’s libraries for algebra, analysis, and matrices. Our main extensions to existing libraries are also detailed. 

   more » « less
2. A Numerically Verified Parameter-Free Third Order Accurate Reconstruction Method for Cell-Centered Finite Volume Solvers on Arbitrarily Unstructured Grids

   https://doi.org/10.2514/6.2025-0074  

   Tu, Shuangzhang; Jiang, Chao (January 2025, American Institute of Aeronautics and Astronautics)

   This paper presents the implementation of a parameter-free third-order recon- struction method for cell-centered finite volume solvers on unstructured grids. The reconstruction is based on nodal gradients obtained using the least squares approach from solutions at adjacent cell centers. The cell and face gradients are computed by simple arithmetic averaging of vertex gradients, while the face values are obtained through quadratic interpolation. Importantly, the current reconstruction method does not require explicit second derivatives, and its stencil remains as compact as that used in traditional linear reconstruction methods. The third-order accuracy of the left and right states at the face values, along with the second-order accuracy of the face gradients, is numerically verified on various unstructured grids. This verified third-order accuracy is a crucial condition for ensuring the overall accuracy of the finite volume solver. 

   more » « less
3. Proving Query Equivalence Using Linear Integer Arithmetic

   https://doi.org/10.1145/3626768  

   Ding, Haoran; Wang, Zhaoguo; Yang, Yicun; Zhang, Dexin; Xu, Zhenglin; Chen, Haibo; Piskac, Ruzica; Li, Jinyang (December 2023, Proceedings of the ACM on Management of Data)

   Proving the equivalence between SQL queries is a fundamental problem in database research. Existing solvers model queries using algebraic representations and convert such representations into first-order logic formulas so that query equivalence can be verified by solving a satisfiability problem. The main challenge lies in unbounded summations, which appear commonly in a query's algebraic representation in order to model common SQL features, such as projection and aggregate functions. Unfortunately, existing solvers handle unbounded summations in an ad-hoc manner based on heuristics or syntax comparison, which severely limits the set of queries that can be supported. This paper develops a new SQL equivalence prover called SQLSolver, which can handle unbounded summations in a principled way. Our key insight is to use the theory of LIA^*, which extends linear integer arithmetic formulas with unbounded sums and provides algorithms to translate a LIA^* formula to a LIA formula that can be decided using existing SMT solvers. We augment the basic LIA^* theory to handle several complex scenarios (such as nested unbounded summations) that arise from modeling real-world queries. We evaluate SQLSolver with 359 equivalent query pairs derived from the SQL rewrite rules in Calcite and Spark SQL. SQLSolver successfully proves 346 pairs of them, which significantly outperforms existing provers. 

   more » « less
4. Optimal Cosmic Microwave Background Lensing Reconstruction and Parameter Estimation with SPTpol Data

   https://doi.org/10.3847/1538-4357/ac02bb  

   Millea, M.; Daley, C. M.; Chou, T-L.; Anderes, E.; Ade, P. A.; Anderson, A. J.; Austermann, J. E.; Avva, J. S.; Beall, J. A.; Bender, A. N.; et al (December 2021, The Astrophysical Journal)

   Abstract We perform the first simultaneous Bayesian parameter inference and optimal reconstruction of the gravitational lensing of the cosmic microwave background (CMB), using 100 deg 2 of polarization observations from the SPTpol receiver on the South Pole Telescope. These data reach noise levels as low as 5.8 μ K arcmin in polarization, which are low enough that the typically used quadratic estimator (QE) technique for analyzing CMB lensing is significantly suboptimal. Conversely, the Bayesian procedure extracts all lensing information from the data and is optimal at any noise level. We infer the amplitude of the gravitational lensing potential to be A ϕ = 0.949 ± 0.122 using the Bayesian pipeline, consistent with our QE pipeline result, but with 17% smaller error bars. The Bayesian analysis also provides a simple way to account for systematic uncertainties, performing a similar job as frequentist “bias hardening” or linear bias correction, and reducing the systematic uncertainty on A ϕ due to polarization calibration from almost half of the statistical error to effectively zero. Finally, we jointly constrain A ϕ along with A L , the amplitude of lensing-like effects on the CMB power spectra, demonstrating that the Bayesian method can be used to easily infer parameters both from an optimal lensing reconstruction and from the delensed CMB, while exactly accounting for the correlation between the two. These results demonstrate the feasibility of the Bayesian approach on real data, and pave the way for future analysis of deep CMB polarization measurements with SPT-3G, Simons Observatory, and CMB-S4, where improvements relative to the QE can reach 1.5 times tighter constraints on A ϕ and seven times lower effective lensing reconstruction noise. 

   more » « less
5. Lyapunov functions for first-order methods: Tight automated convergence guarantees

   Taylor, A; Van Scoy, B; Lessard, L (July 2018, Proceedings of Machine Learning Research)

   We present a novel way of generating Lyapunov functions for proving linear convergence rates of first-order optimization methods. Our approach provably obtains the fastest linear convergence rate that can be verified by a quadratic Lyapunov function (with given states), and only relies on solving a small-sized semidefinite program. Our approach combines the advantages of performance estimation problems (PEP, due to Drori & Teboulle (2014)) and integral quadratic constraints (IQC, due to Lessard et al. (2016)), and relies on convex interpolation (due to Taylor et al. (2017c;b)). 

   more » « less