365 citations · 654 across the 11 of their papers we have counts for
11 papers
Visored: A Controlled-Natural-Language Prover for LLM-Generated Mathematics
Xiyu Zhai, Xinyi Chen, Yiping Wang +3
We present a dependent-type-based prover designed around the way LLMs (and humans) tend to write mathematics, complementing existing systems such as Lean and Rocq. Its core design…
Neuro-Symbolic Generation and Validation of Memory-Aware Formal Function Specifications
Liao Zhang, Tong Chen, Xiwei Wu +4
Formal verification of memory-manipulating programs critically depends on precise function specifications that capture memory states written by experts. This requirement has become…
Transformers are Efficient Compilers, Provably
Xiyu Zhai, Runlong Zhou, Liao Zhang +1
Transformer-based large language models (LLMs) have demonstrated surprisingly robust performance across a wide range of language-related tasks, including programming language under…
SceneGen: Generative Contextual Scene Augmentation using Scene Graph Priors
Mohammad Keshavarzi, Aakash Parikh, Xiyu Zhai +3
Spatial computing experiences are constrained by the real-world surroundings of the user. In such experiences, augmenting virtual objects to existing scenes require a contextual ap…
On the Multiple Descent of Minimum-Norm Interpolants and Restricted Lower Isometry of Kernels
Tengyuan Liang, Alexander Rakhlin, Xiyu Zhai
We study the risk of minimum-norm interpolants of data in Reproducing Kernel Hilbert Spaces. Our upper bounds on the risk are of a multiple-descent shape for the various scalings o…
Near Optimal Stratified Sampling
Tiancheng Yu, Xiyu Zhai, Suvrit Sra
The performance of a machine learning system is usually evaluated by using i.i.d.\ observations with true labels. However, acquiring ground truth labels is expensive, while obtaini…
Consistency of Interpolation with Laplace Kernels is a High-Dimensional Phenomenon
Alexander Rakhlin, Xiyu Zhai
We show that minimum-norm interpolation in the Reproducing Kernel Hilbert Space corresponding to the Laplace kernel is not consistent if input dimension is constant. The lower boun…
Gradient Descent Finds Global Minima of Deep Neural Networks
Simon S. Du, Jason D. Lee, Haochuan Li +2
Gradient descent finds a global minimum in training deep neural networks despite the objective function being non-convex. The current paper proves gradient descent achieves zero tr…
Gradient Descent Provably Optimizes Over-parameterized Neural Networks
Simon S. Du, Xiyu Zhai, Barnabas Poczos +1
One of the mysteries in the success of neural networks is randomly initialized first order methods like gradient descent can achieve zero training loss even though the objective fu…
How Many Samples are Needed to Estimate a Convolutional or Recurrent Neural Network?
Simon S. Du, Yining Wang, Xiyu Zhai +3
It is widely believed that the practical success of Convolutional Neural Networks (CNNs) and Recurrent Neural Networks (RNNs) owes to the fact that CNNs and RNNs use a more compact…
Generalization Bounds of SGLD for Non-convex Learning: Two Theoretical Viewpoints
Wenlong Mou, Liwei Wang, Xiyu Zhai +1
Algorithm-dependent generalization error bounds are central to statistical learning theory. A learning algorithm may use a large hypothesis space, but the limited number of iterati…