论文库

Lightweight methods like QuickCheck have proven to be successful in functional languages and beyond, as they let users specify properties as Boolean functions directly in code. We can replicate some of their benefits for (bounded) proofs via symbolic execution. If we can execute arbitrary functions symbolically, we can specify properties just as easily. Unfortunately, existing symbolic execution tools for Haskell are restricted to a subset of the language that excludes many real-world applications like IO; they also have a hard time scaling to larger programs, making them a poor fit for general purpose lightweight verification. One reason behind these limitations is that existing techniques only offer fixed symbolic semantics for SMT base types. This makes it hard to cover more programming constructs and libraries; it also makes it difficult to fine-tune symbolic representations for better performance. We present SymFC, a new symbolic execution method for Haskell that offers configurable semantics via embeddings. An embedding of a function in SymFC is just another Haskell function that can use arbitrary code, as well as SMT primitives. Embeddings make it easy to support new programming constructs and fine-tune symbolic representations for speed. To integrate embeddings into Haskell's type system, we make use of Haskell's coercions, which let us transparently convert between a Haskell type and the type of its embedding. We realize embeddings in SymFC, an all-paths symbolic execution engine for Haskell, which lets us symbolically represent arbitrary types and values in GHC core. We implement SymFC as a GHC plugin, and evaluate it by checking properties of Haskell's container library, and the iproute library. We build embeddings for IORef, Haskell's Ptr/ForeignPtr interface, and the hardware library Clash, and our evaluation reports a 6.25x speedup on G2's own benchmarks.

The timeline by which quantum computers can solve breakthrough problems in science depends on improved quantum algorithms as much as on better hardware. Such algorithmic advances are typically achieved through many years of expert human collaboration. In mathematics and computer science, large language models have accelerated progress through automated discovery loops. However, quantum algorithms can only be evaluated by classical computers on restricted or small instances. Here we demonstrate automated discovery of quantum programs beyond these regimes including order-of-magnitude improvements on scientific applications. To achieve this, we build a quantum program library in the Lean theorem prover in which Gemini 4 agents synthesize novel programs against formal problem specifications and verify their correctness and cost. Agent teams collaborate, sharing results and knowledge through wikis and discussing ideas at organized conferences. Our results improve on prior baselines for parallel search (up to 2.55x), quantum arithmetic (290x), and simulations relevant to fusion, photochemistry and drug-metabolism by 11x, 8x and 2.5x respectively. Combining human and artificial intelligence at scale, under the rigor of mathematical proof, lets researchers design algorithms that today's classical and quantum computers cannot test, shortening the path to practical quantum computation.

We present a systematic comparison between arbitrary precise arithmetic and integration, IEEE-754 compliant floating point arithmetic (fp16, bfp16, fp32, double precision fp64, and quadruple precision fp128), and two implementations of Posits (type III unum) for solving Newton's chaotic N-body problem. Each implementation is benchmarked with arbitrary precise calculations to objectively evaluate their performance in precision as well as speed. We rely on hardware and compiler implementations for fp64, and software implementations for arbitrary-precision arithmetic and Posits. Half precision arithmetic (fp16, bfp16, and Posits$<16,1>$) are insufficiently precise for solving Newton's equations of motion. Single precision (fp32, and Posits$<32,2>$) could be used for statistical ensemble calculations, but lead to relatively large errors in any individual strong encounter. All 64-bit implementations fp64 as well as Posits (Posits$<64,3>$) experience difficulty in our tests. One of the implementations of Posits (Universal) gives precision comparable to fp64 but is slow (by at least an orders of magnitude compared to fp64 after correcting for the more efficient hardware support for the latter). The other (CPPPosits) has a speed comparable to fp64 but has systematically larger errors (by about an order of magnitude compared to fp64 with excesses exceeding two orders of magnitude). As a consequence, this implementation leads to a systematic drift in the result space and has difficulty resolving close encounters. Posits and fp64 have difficulty when integrating a dynamical system in a moving reference frame; testing Galileo invariancy. In their current implementation, Posits do not seem to be the ideal alternative for fp64 when integrating chaotic or stiff ordinary differential equations, such as Newton's equations of motion.

Programming language researchers have developed a wide array of tools to reason about probabilistic programs, but it remains unclear how to apply these proof techniques to continuous-time stochastic processes. To bridge this gap, we propose a verification method for properties of continuous-time stochastic processes by reasoning about them as standard programs. To demonstrate our approach, we define a continuous semantics for a probabilistic imperative language $\mathrm{pWhile}^{\mathrm{dt}}$ by taking the Kuratowski limit of the standard semantics, which collects limit points of the standard program semantics as the time-step approaches zero. Then, we present a Hoare-style logic that uses loop invariants and decreasing functions to verify properties of continuous programs. To establish soundness, we identify a broad class of assertions that are preserved from the standard semantics to the continuous semantics. To demonstrate our approach, we verify properties of ten continuous-time stochastic processes modeled in $\mathrm{pWhile}^{\mathrm{dt}}$, including variants of Brownian motion and a stochastic hybrid system.