Jingwei Hu

Jiewen Hu, Thomas Zhu, Sean Welleck · cmu

Real-world formal theorem proving often depends on a wealth of context, including definitions, lemmas, comments, file structure, and other information. We introduce miniCTX, which tests a model's ability to prove formal mathematical theorems that depend on new context that is not seen during training. miniCTX contains theorems sourced from real Lean projects and textbooks, each associated with a context that can span tens of thousands of tokens. Models are tasked with proving a theorem given access to code from the theorem's repository, which contains context that is needed for the proof. As a baseline for miniCTX, we tested fine-tuning and prompting methods that condition theorem proving on preceding context. Both approaches substantially outperform traditional methods that rely solely on state information. We found that this ability to use context is not captured by previous benchmarks such as miniF2F. Alongside miniCTX, we offer ntp-toolkit for automatically extracting and annotating theorem proving data, making it easy to add new projects into miniCTX to ensure that contexts are not seen during training. miniCTX offers a challenging and realistic evaluation of neural theorem provers.

Irene M. Gamba, Jeffrey R. Haack, Cory D. Hauck et al.

We propose a simple fast spectral method for the Boltzmann collision operator with general collision kernels. In contrast to the direct spectral method \cite{PR00, GT09} which requires $O(N^6)$ memory to store precomputed weights and has $O(N^6)$ numerical complexity, the new method has complexity $O(MN^4\log N)$, where $N$ is the number of discretization points in each of the three velocity dimensions and $M$ is the total number of discretization points on the sphere and $M\ll N^2$. Furthermore, it requires no precomputation for the variable hard sphere (VHS) model and only $O(MN^4)$ memory to store precomputed functions for more general collision kernels. Although a faster spectral method is available \cite{MP06} (with complexity $O(MN^3\log N)$), it works only for hard sphere molecules, thus limiting its use for practical problems. Our new method, on the other hand, can apply to arbitrary collision kernels. A series of numerical tests is performed to illustrate the efficiency and accuracy of the proposed method.

Francis Filbet, Jingwei Hu, Shi Jin

Numerically solving the Boltzmann kinetic equations with the small Knudsen number is challenging due to the stiff nonlinear collision term. A class of asymptotic preserving schemes was introduced in [6] to handle this kind of problems. The idea is to penalize the stiff collision term by a BGK type operator. This method, however, encounters its own difficulty when applied to the quantum Boltzmann equation. To define the quantum Maxwellian (Bose-Einstein or Fermi- Dirac distribution) at each time step and every mesh point, one has to invert a nonlinear equation that connects the macroscopic quantity fugacity with density and internal energy. Setting a good initial guess for the iterative method is troublesome in most cases because of the complexity of the quantum functions (Bose-Einstein or Fermi-Dirac function). In this paper, we propose to penalize the quantum collision term by a 'classical' BGK operator instead of the quantum one. This is based on the observation that the classical Maxwellian, with the temperature replaced by the internal energy, has the same first five moments as the quantum Maxwellian. The scheme so designed avoids the aforementioned difficulty, and one can show that the density distribution is still driven toward the quantum equilibrium. Numerical results are present to illustrate the efficiency of the new scheme in both the hydrodynamic and kinetic regimes. We also develop a spectral method for the quantum collision operator.

Jingwei Hu, Ruiwen Shu, Xiangxiong Zhang

We develop a family of second-order implicit-explicit (IMEX) schemes for the stiff BGK kinetic equation. The method is asymptotic-preserving (can capture the Euler limit without numerically resolving the small Knudsen number) as well as positivity-preserving --- a feature that is not possessed by any of the existing second or high order IMEX schemes. The method is based on the usual IMEX Runge-Kutta framework plus a key correction step utilizing the special structure of the BGK operator. Formal analysis is presented to demonstrate the property of the method and is supported by various numerical results. Moreover, we show that the method satisfies an entropy-decay property when coupled with suitable spatial discretizations. Additionally, we discuss the generalization of the method to some hyperbolic relaxation system and provide a strategy to extend the method to third order.

Jingwei Hu, Ruiwen Shu

We introduce a second-order time discretization method for stiff kinetic equations. The method is asymptotic-preserving (AP) -- can capture the Euler limit without numerically resolving the small Knudsen number; and positivity-preserving -- can preserve the non-negativity of the solution which is a probability density function for arbitrary Knudsen numbers. The method is based on a new formulation of the exponential Runge-Kutta method and can be applied to a large class of stiff kinetic equations including the BGK equation (relaxation type), the Fokker-Planck equation (diffusion type), and even the full Boltzmann equation (nonlinear integral type). Furthermore, we show that when coupled with suitable spatial discretizations the fully discrete scheme satisfies an entropy-decay property. Various numerical results are provided to demonstrate the theoretical properties of the method.

Shiheng Zhang, Jingwei Hu

We study the stability of a class of dynamical low-rank methods--the projector-splitting integrator (PSI)--applied to linear hyperbolic and parabolic equations. Using a von Neumann-type analysis, we investigate the stability of such low-rank time integrator coupled with standard spatial discretizations, including upwind and central finite difference schemes, under two commonly used formulations: discretize-then-project (DtP) and project-then-discretize (PtD). For hyperbolic equations, we show that the stability conditions for DtP and PtD are the same under Lie-Trotter splitting, and that the stability region can be significantly enlarged by using Strang splitting. For parabolic equations, despite the presence of a negative S-step, unconditional stability can still be achieved by employing Crank-Nicolson or a hybrid forward-backward Euler scheme in time stepping. While our analysis focuses on simplified model problems, it offers insight into the stability behavior of PSI for more complex systems, such as those arising in kinetic theory.

Lee Ricketson, Jingwei Hu

We extend the recently-developed explicit, energy-conserving particle-in-cell (PIC) scheme of [1] to the relativistic Vlasov-Maxwell system. As in the non-relativistic case, the method is built on an optimization problem that is analytically solvable, local to each particle, and designed to enforce exact energy conservation. Although the solution to this optimization problem is not guaranteed to be real, we show that such instances are rare enough for practical simulation parameters to permit dramatic improvements in energy conservation over traditional explicit PIC schemes. We show that, as in the non-relativistic case, the scheme is compatible with popular field-solvers for electromagnetic PIC schemes, including the Yee/FDTD and pseudo-spectral analytic time-domain (PSATD) methods. The scheme is verified on standard relativistic test problems, where its conservation properties are confirmed.

Vasily Ilin, Jingwei Hu, Zhenfu Wang · pku

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 can preserve some important physical properties of the Landau equation, such as the conservation of mass, momentum, and energy, and decay of estimated entropy. We prove that matching the gradient of the logarithm of the approximate solution is enough to recover the true solution to the Landau equation with Maxwellian molecules. Several numerical experiments in low and moderately high dimensions are performed, with particular emphasis on comparing the proposed method with the traditional particle or blob method.

Vasily Ilin, Peter Sushko, Jingwei Hu · allen-ai, uw

We propose a deterministic sampling framework using Score-Based Transport Modeling for sampling an unnormalized target density $π$ given only its score $\nabla \log π$. Our method approximates the Wasserstein gradient flow on $\mathrm{KL}(f_t\|π)$ by learning the time-varying score $\nabla \log f_t$ on the fly using score matching. While having the same marginal distribution as Langevin dynamics, our method produces smooth deterministic trajectories, resulting in monotone noise-free convergence. We prove that our method dissipates relative entropy at the same rate as the exact gradient flow, provided sufficient training. Numerical experiments validate our theoretical findings: our method converges at the optimal rate, has smooth trajectories, and is often more sample efficient than its stochastic counterpart. Experiments on high-dimensional image data show that our method produces high-quality generations in as few as 15 steps and exhibits natural exploratory behavior. The memory and runtime scale linearly in the sample size.