8 papers
Evaluation of LLMs for Mathematical Formalization in Lean
Tyson Klingner, Drew Bladek, Escher Crawford +6
Within the past few years, the ability of Large Language Models (LLMs) to generate formal mathematical proofs has improved drastically. We provide a comparison of various LLMs' eff…
Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium
Vasily Ilin
We present a complete Lean 4 formalization of the equilibrium characterization in the Vlasov-Maxwell-Landau (VML) system, which describes the motion of charged plasma. The project…
Theory of (Co)homological Invariants on Quantum LDPC Codes
Zimu Li, Yuguo Shao, Fuchuan Wei +2
We establish a systematic mathematical framework for constructing and computing (co)homological invariants that induce logical gates on quantum low-density parity-check (qLDPC) cod…
DiScoFormer: Plug-In Density and Score Estimation with Transformers
Vasily Ilin, Peter Sushko, Ranjay Krishna
Estimating probability density and its score from samples remains a core problem in generative modeling, Bayesian inference, and kinetic theory. Existing methods are bifurcated: cl…
Stability of the spatially homogeneous Landau equation in relative entropy and applications to score-based numerical methods
Vasily Ilin
We give a short and elementary proof of stability for strong solutions of the spatially homogeneous Landau equation with Coulomb collisions, measured in relative entropy. The argum…
Score-based deterministic density sampling
Vasily Ilin, Peter Sushko, Jingwei Hu
We propose a deterministic sampling framework using Score-Based Transport Modeling for sampling an unnormalized target density given only its score . Our method…
REALEDIT: Reddit Edits As a Large-scale Empirical Dataset for Image Transformations
Peter Sushko, Ayana Bharadwaj, Zhi Yang Lim +6
Existing image editing models struggle to meet real-world demands. Despite excelling in academic benchmarks, they have yet to be widely adopted for real user needs. Datasets that p…
Transport based particle methods for the Fokker-Planck-Landau equation
Vasily Ilin, Jingwei Hu, Zhenfu Wang
We propose a particle method for numerically solving the Landau equation, inspired by the score-based transport modeling (SBTM) method for the Fokker-Planck equation. This method c…