parallel computing developers

Abstract: Modern statistical model development begins with a high-level specification in an automatic differentiation framework such as PyTorch, JAX, or TensorFlow, which is then lowered to a target backend by a compiler or implemented manually by a research engineer. In this paper, we study whether frontier language models can correctly perform the latter task by generating GPU kernels from high-level benchmark specifications. We introduce a framework in which a language-model agent uses Velvet, a program verifier for imperative programs embedded in Lean, to prove semantic equivalence between a high-level specification and a generated CUDA kernel under an explicit set of assumptions. It also asks the LLM to prove thread safety and data race freedom of the generated kernel in VerCors, a deductive verifier for parallel code. Our main contribution to the formal verification of LLM- generated GPU kernels is showing that a combination of Lean automation and language-model-guided proof construction can verify a broad set of basic neural- network building blocks over floating-point values, allowing LLMs to implement semantically correct and safe kernels. In our framework, floating-point verifications never rely on compiled code and are always checked via the Lean kernel.

Abstract: For every fixed activity $λ>0$, we establish three results for the monomer--dimer model on an $n$-vertex simple graph $G$ with $m\ge1$ edges and maximum degree $Δ$. 1. Near-linear mixing and sampling. Single-edge Glauber dynamics has mixing time $O_λ(m[\log^2 n+\log(1/\varepsilon)])$, giving a near-linear-time approximate sampler. 2. Work-efficient parallel sampling. We simulate the same Glauber dynamics in parallel using $\tilde{O}_λ(m+n)$ work and $\tilde{O}_λ(\min\{Δ,m^{1/3},\sqrt n\})$ depth with high probability. 3. Fast approximate counting. We estimate the partition function within relative error $\varepsilon$ in $\tilde{O}_λ(n^2/\varepsilon^2)$ work. For dense graphs with $m=Θ(n^2)$, this is near-linear in the input size. For the mixing theorem, we establish a general log--Sobolev criterion based on field-dynamics spectral stability, with only logarithmic dependence on the inverse occupied-marginal lower bound. Parallelism uses a matching-specific analysis of occupation-interval dependencies. Counting uses monomer-preconditioned Jerrum--Sinclair dynamics, whose parameters are learned efficiently by Glauber dynamics.