SearcharxivSearch

arXiv subjects

Thomas Chen

Publications and source records attributed to Thomas Chen.

At least 19 recordsLinked to original sources

A Theoretical Framework for Self-Play Theorem Proving Algorithms

Self-play, a type of training algorithm that enables a model to self-improve, has recently shown promising empirical results in the context of formal theorem proving using Large Language Models (LLMs). (Dong & Ma, 2025) instantiate self-play with two cooperating agents: a prover, which proves theorems, and a conjecturer, which generates new theorems as a curriculum to the prover. In this paper, we provide a theoretical framework for understanding the self-improvement capabilities of self-play algorithms for theorem proving. First, we formalize the set of theorems as a graph, with nodes as theorems and edges between pairs of theorems with similar semantics. We introduce a set of primitive assumptions that characterize the guarantees of a trained prover and how a conjecturer can access the structure of the graph. Second, we show that if the underlying graph of theorems is well-connected, then a prover-conjecturer system, where the conjecturing algorithm is based on a reversible random walk, is sufficient to grow the set of proved theorems exponentially. Third, motivated by an issue encountered empirically by self-play algorithms, where the conjecturer tends to generate artificially complex and non-fundamental theorems, we propose a diversity measure for a training distribution of theorems generated by a conjecturer and an improved conjecturing algorithm that locally maximizes this diversity measure, by computing the diffusion similarity between neighboring theorems in the theorem graph. Finally, we describe a method to compute the diffusion similarity by using contrastive learning to embed nodes into Euclidean space and then computing the inner-product between embeddings.

cs.LG

Bivariate range functions with superior convergence order

Range functions are a fundamental tool for certified computations in geometric modeling, computer graphics, and robotics, but traditional range functions have only quadratic convergence order ($m=2$). For ``superior'' convergence order (i.e., $m>2$), we exploit the Cornelius--Lohner framework in order to introduce new bivariate range functions based on Taylor, Lagrange, and Hermite interpolation. In particular, we focus on practical range functions with cubic and quartic convergence order. We implemented them in Julia and provide experimental validation of their performance in terms of efficiency and efficacy.

math.NA

Trapped bosons in mean field QED, nonlinear resonance cascades and dynamical BEC formation

In this paper, we study a system of bosons trapped in a confining potential, interacting with a quantized field of coherent photons in the mean field description of non-relativistic Quantum Electrodynamics (QED) obtained by [N. Leopold and P. Pickl , 2017]. We derive the effective nonlinear cascade equations governing the emission and absorption of coherent photons by the boson subsystem in a combined weak-coupling and macroscopic time limit. We demonstrate that solutions to this nonlinear cascade determine a monotone decreasing energy flow in the boson subsystem, and thereby describe the dynamical formation of a Bose-Einstein condensate (BEC) with full ground state occupation, under conservation of the total boson $L^2$ mass. We note that this process is crucially different from thermal relaxation to the ground state, and fundamentally depends on the nonlinear nature of the cascade dynamics.

math-ph

Non-Asymptotic Length Generalization

Length generalization is the ability of a learning algorithm to learn a hypothesis which generalizes to longer inputs than the inputs in the training set. In this paper, we provide provable guarantees of length generalization for various classes of functions in an idealized setting. First, we formalize the framework of non-asymptotic length generalization, which requires a computable upper bound for the minimum input length that guarantees length generalization, as a function of the complexity of ground-truth function under some given complexity measure. We refer to this minimum input length to length generalize as length complexity. We show the Minimum-Complexity Interpolator learning algorithm achieves optimal length complexity. We further show that whether a function class admits non-asymptotic length generalization is equivalent to the decidability of its language equivalence problem, which implies that there is no computable upper bound for the length complexity of Context-Free Grammars. On the positive side, we show that the length complexity of Deterministic Finite Automata is $2n - 2$ where $n$ is the number of states of the ground-truth automaton. Our main results are upper bounds of length complexity for a subset of a transformer-related function class called C-RASP (Yang & Chiang, 2024). We show that the length complexity of 1-layer C-RASP functions is $O(T^2)$ when the ground-truth function has precision $T$, and that the length complexity of 2-layer C-RASP functions is $O(T^{O(K)})$ when the ground-truth function has precision $T$ and $K$ heads.

cs.LG

Architecture independent generalization bounds for overparametrized deep ReLU networks

We prove that overparametrized neural networks are able to generalize with a test error that is independent of the level of overparametrization, and independent of the Vapnik-Chervonenkis (VC) dimension. We prove explicit bounds that only depend on the metric geometry of the test and training sets, on the regularity properties of the activation function, and on the operator norms of the weights and norms of biases. For overparametrized deep ReLU networks with a training sample size bounded by the input space dimension, we explicitly construct zero loss minimizers without use of gradient descent, and prove a uniform generalization bound that is independent of the network architecture. We perform computational experiments of our theoretical results with MNIST, and obtain agreement with the true test error within a 22 % margin on average.

cs.LG

Learning Symbolic Task Decompositions for Multi-Agent Teams

One approach for improving sample efficiency in cooperative multi-agent learning is to decompose overall tasks into sub-tasks that can be assigned to individual agents. We study this problem in the context of reward machines: symbolic tasks that can be formally decomposed into sub-tasks. In order to handle settings without a priori knowledge of the environment, we introduce a framework that can learn the optimal decomposition from model-free interactions with the environment. Our method uses a task-conditioned architecture to simultaneously learn an optimal decomposition and the corresponding agents' policies for each sub-task. In doing so, we remove the need for a human to manually design the optimal decomposition while maintaining the sample-efficiency benefits of improved credit assignment. We provide experimental results in several deep reinforcement learning settings, demonstrating the efficacy of our approach. Our results indicate that our approach succeeds even in environments with codependent agent dynamics, enabling synchronous multi-agent learning not achievable in previous works.

cs.MA

Zero loss guarantees and explicit minimizers for generic overparametrized Deep Learning networks

We determine sufficient conditions for overparametrized deep learning (DL) networks to guarantee the attainability of zero loss in the context of supervised learning, for the $\mathcal{L}^2$ cost and {\em generic} training data. We present an explicit construction of the zero loss minimizers without invoking gradient descent. On the other hand, we point out that increase of depth can deteriorate the efficiency of cost minimization using a gradient descent algorithm by analyzing the conditions for rank loss of the training Jacobian. Our results clarify key aspects on the dichotomy between zero loss reachability in underparametrized versus overparametrized DL.

cs.LG

Derivation of effective gradient flow equations and dynamical truncation of training data in Deep Learning

We derive explicit equations governing the cumulative biases and weights in Deep Learning with ReLU activation function, based on gradient descent for the Euclidean loss in the input layer, and under the assumption that the weights are, in a precise sense, adapted to the coordinate system distinguished by the activations. We show that gradient descent corresponds to a dynamical process in the input layer, whereby clusters of data are progressively reduced in complexity ("truncated") at an exponential rate that increases with the number of data points that have already been truncated. We provide a detailed discussion of several types of solutions to the gradient flow equations. A main motivation for this work is to shed light on the interpretability question in supervised learning.

cs.LG

Gradient flow in parameter space is equivalent to linear interpolation in output space

We prove that the standard gradient flow in parameter space that underlies many training algorithms in deep learning can be continuously deformed into an adapted gradient flow which yields (constrained) Euclidean gradient flow in output space. Moreover, for the $L^{2}$ loss, if the Jacobian of the outputs with respect to the parameters is full rank (for fixed training data), then the time variable can be reparametrized so that the resulting flow is simply linear interpolation, and a global minimum can be achieved. For the cross-entropy loss, under the same rank condition and assuming the labels have positive components, we derive an explicit formula for the unique global minimum.

cs.LG

Interpretable global minima of deep ReLU neural networks on sequentially separable data

We explicitly construct zero loss neural network classifiers. We write the weight matrices and bias vectors in terms of cumulative parameters, which determine truncation maps acting recursively on input space. The configurations for the training data considered are (i) sufficiently small, well separated clusters corresponding to each class, and (ii) equivalence classes which are sequentially linearly separable. In the best case, for $Q$ classes of data in $\mathbb{R}^M$, global minimizers can be described with $Q(M+2)$ parameters.

cs.LG

Derivation of renormalized Hartree-Fock-Bogoliubov and quantum Boltzmann equations in an interacting Bose gas

Our previous work [37] presented a rigorous derivation of quantum Boltzmann equations near a Bose-Einstein condensate (BEC). Here, we extend it with a complete characterization of the leading order fluctuation dynamics. For this purpose, we correct the latter via an appropriate Bogoliubov rotation, in partial analogy to the approach by Grillakis-Machedon et al. [59], in addition to the Weyl transformation applied in [37]. Based on the analysis of the third order expansion of the BEC wave function, and the second order expansions of the pair-correlations, we show that through a renormalization strategy, various contributions to the effective Hamiltonian can be iteratively eliminated by an appropriate choice of the Weyl and Bogoliubov transformations. This leads to a separation of renormalized Hartree-Fock-Bogoliubov (HFB) equations and quantum Boltzmann equations. A multitude of terms that were included in the error term in [37] are now identified as contributions to the HFB renormalization terms. Thereby, the error bound in the work at hand is improved significantly. To the given order, it is now sharp, and matches the order or magnitude expected from scaling considerations. Consequently, we extend the time of validity to $t\sim (\log N)^2$ compared to $t\sim (\log N/\log \log N)^2$ before. We expect our approach to be extensible to smaller orders in $\frac1N$.

math-ph

Global $\mathcal{L}^2$ minimization at uniform exponential rate via geometrically adapted gradient descent in Deep Learning

We consider the scenario of supervised learning in Deep Learning (DL) networks, and exploit the arbitrariness of choice in the Riemannian metric relative to which the gradient descent flow can be defined (a general fact of differential geometry). In the standard approach to DL, the gradient flow on the space of parameters (weights and biases) is defined with respect to the Euclidean metric. Here instead, we choose the gradient flow with respect to the Euclidean metric in the output layer of the DL network. This naturally induces two modified versions of the gradient descent flow in the parameter space, one adapted for the overparametrized setting, and the other for the underparametrized setting. In the overparametrized case, we prove that, provided that a rank condition holds, all orbits of the modified gradient descent drive the ${\mathcal L}^2$ cost to its global minimum at a uniform exponential convergence rate; one thereby obtains an a priori stopping time for any prescribed proximity to the global minimum. We point out relations of the latter to sub-Riemannian geometry. Moreover, we generalize the above framework to the situation in which the rank condition does not hold; in particular, we show that local equilibria can only exist if a rank loss occurs, and that generically, they are not isolated points, but elements of a critical submanifold of parameter space.

cs.LG

On non-approximability of zero loss global ${\mathcal L}^2$ minimizers by gradient descent in Deep Learning

We analyze geometric aspects of the gradient descent algorithm in Deep Learning (DL), and give a detailed discussion of the circumstance that in underparametrized DL networks, zero loss minimization can generically not be attained. As a consequence, we conclude that the distribution of training inputs must necessarily be non-generic in order to produce zero loss minimizers, both for the method constructed in [Chen-Munoz Ewald 2023, 2024], or for gradient descent [Chen 2025] (which assume clustering of training data).

cs.LG

Geometric structure of shallow neural networks and constructive ${\mathcal L}^2$ cost minimization

In this paper, we approach the problem of cost (loss) minimization in underparametrized shallow ReLU networks through the explicit construction of upper bounds which appeal to the structure of classification data, without use of gradient descent. A key focus is on elucidating the geometric structure of approximate and precise minimizers. We consider an $L^2$ cost function, input space $\mathbb{R}^M$, output space ${\mathbb R}^Q$ with $Q\leq M$, and training input sample size that can be arbitrarily large. We prove an upper bound on the minimum of the cost function of order $O(\delta_P)$ where $\delta_P$ measures the signal-to-noise ratio of training data. In the special case $M=Q$, we explicitly determine an exact degenerate local minimum of the cost function, and show that the sharp value differs from the upper bound obtained for $Q\leq M$ by a relative error $O(\delta_P^2)$. The proof of the upper bound yields a constructively trained network; we show that it metrizes a particular $Q$-dimensional subspace in the input space ${\mathbb R}^M$. We comment on the characterization of the global minimum of the cost function in the given context.

cs.LG

Geometric structure of Deep Learning networks and construction of global ${\mathcal L}^2$ minimizers

In this paper, we explicitly determine local and global minimizers of the $\mathcal{L}^2$ cost function in underparametrized Deep Learning (DL) networks; our main goal is to shed light on their geometric structure and properties. We accomplish this by a direct construction, without invoking the gradient descent flow at any point of this work. We specifically consider $L$ hidden layers, a ReLU ramp activation function, an $\mathcal{L}^2$ Schatten class (or Hilbert-Schmidt) cost function, input and output spaces $\mathbb{R}^Q$ with equal dimension $Q\geq1$, and hidden layers also defined on $\mathbb{R}^{Q}$; the training inputs are assumed to be sufficiently clustered. The training input size $N$ can be arbitrarily large - thus, we are considering the underparametrized regime. More general settings are left to future work. We construct an explicit family of minimizers for the global minimum of the cost function in the case $L\geq Q$, which we show to be degenerate. Moreover, we determine a set of $2^Q-1$ distinct degenerate local minima of the cost function. In the context presented here, the concatenation of hidden layers of the DL network is reinterpreted as a recursive application of a {\em truncation map} which "curates" the training inputs by minimizing their noise to signal ratio.

cs.LG

The Focusing Optics X-ray Solar Imager (FOXSI)

FOXSI is a direct-imaging, hard X-ray (HXR) telescope optimized for solar flare observations. It detects hot plasma and energetic electrons in and near energy release sites in the solar corona via bremsstrahlung emission, measuring both spatial structure and particle energy distributions. It provides two orders of magnitude faster imaging spectroscopy than previously available, probing physically relevant timescales (<1s) never before accessible to address fundamental questions of energy release and efficient particle acceleration that have importance far beyond their solar application (e.g., planetary magnetospheres, flaring stars, accretion disks). FOXSI measures not only the bright chromospheric X-ray emission where electrons lose most of their energy, but also simultaneous emission from electrons as they are accelerated in the corona and propagate along magnetic field lines. FOXSI detects emission from high in the tenuous corona, where previous instruments have been blinded by nearby bright features and will fully characterizes the accelerated electrons and hottest plasmas as they evolve in energy, space, and time to solve the mystery of how impulsive energy release leads to solar eruptions, the primary drivers of space weather at Earth, and how those eruptions are energized and evolve.

astro-ph.IM

Quantum Boltzmann dynamics and bosonized particle-hole interactions in fermion gases

In this paper, we study a cold gas of $N \gg 1$ weakly interacting fermions. We describe the time evolution of states that are perturbations of the Fermi ball, and analyze the dynamics in particle-hole variables. Our main result states that, for small values of the coupling constant and for appropriate initial data, the effective dynamics of the momentum distribution is determined by a discrete collision operator of quantum Boltzmann form.

math-ph

Recommending Low-Cost Compact Space Environment and Space Weather Effects Sensor Suites for NASA Missions

As miniaturized spacecraft (e.g., cubesats and smallsats) and instrumentation become an increasingly indispensable part of space exploration and scientific investigations, it is important to understand their potential susceptibility to space weather impacts resulting from the sometimes volatile space environment. There are multitude of complexities involved in how space environment interacts with different space hardware/electronics. Measurements of such impacts, however, have been lacking. Therefore, we recommend developing and/or procuring low-cost, low-power consumption, and compact sensor suites (mainly for space weather and impact purposes) and flying them on all future NASA (and U.S in general) missions in order to measure and quantify space weather impacts, in addition to the main instrumentation.

astro-ph.IM