7 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…
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…
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…
A Neural Score-Based Particle Method for the Vlasov-Maxwell-Landau System
Vasily Ilin, Jingwei Hu
Plasma modeling is central to the design of nuclear fusion reactors, yet simulating collisional plasma kinetics from first principles remains a formidable computational challenge:…
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 metho…
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…