Research
On-device research index

arXiv research

A locally-built, LLM-digested index of recent arXiv papers in quant finance, geometry/topology, and statistical ML — keyword search served straight from SQLite on this machine.

168,878 papers · 148 categories

Trend · papers per month

2795598381,117 · Jun 202019922001200920172026
48 results for Neural Theorem Proving

This paper studies neural network operators and their convergence properties.

problem Understanding the approximation and convergence of neural network operators.
method Proves density results, convergence estimates, and Voronovskaya-type theorems.
result Establishes quantitative convergence estimates and derives Voronovskaya-type theorems.

The paper proves deep neural networks with analytic activation can approximate any function.

problem Approximating functions with neural networks using analytic activation functions.
method Elementary proofs for real and complex networks, Stone-Weierstrass theorem, Mergelyan's theorem.
result Closure of neural network classes equals space of polynomials for analytic activation.

Lean Copilot uses LLMs to assist theorem proving in Lean, improving efficiency and automation.

problem Challenges in using existing neural theorem provers to prove novel theorems autonomously.
method Introduces Lean Copilot, a framework for integrating LLMs into Lean's theorem proving process.
result Lean Copilot automates 74.2% of proof steps on average, significantly improving over existing methods.

The study proves a quantitative functional CLT for neural networks with smooth activation functions.

problem Understanding the convergence rates of neural networks with different activation functions.
method Functional versions of the Stein-Malliavin approach and a quantitative functional central limit theorem.
result Rates of convergence depend on the smoothness of the activation function, ranging from logarithmic to sqrt(n).

We rigorously prove a central limit theorem for neural network models with a single hidden layer. The central limit theorem is proven in the asymptotic regime of simultaneously (A) large numbers of hidden units and (B) large numbers of stochastic gradient descent training iterations. Our result describes the neural net…

2018-08-28abs ↗pdf ↗

The paper defines new spaces for neural networks and proves approximation theorems.

problem Identifying the appropriate function space and norm for neural network models.
method Defining the Barron space and flow-induced function space, proving approximation theorems.
result Optimal approximation theorems hold for functions in the Barron space for two-layer neural networks and the flow-induced space for residual neural networks.

TVS-FNNs can approximate any continuous function on expanded input spaces.

problem Processing a broader range of inputs like sequences and matrices.
method Proving a universal approximation theorem for TVS-FNNs.
result TVS-FNNs can approximate any continuous function on expanded input spaces.

NTP struggles to learn relationships without increased exploration.

problem NTP's performance in extracting true relationships among data is poor.
method Created synthetic logical datasets with injected relationships to test NTP's performance and identify algorithmic issues.
result Increasing exploration in NTP's algorithm improves its performance in recovering relationships.

Unified geometric flows improve deep learning efficiency and simplify neural network topologies.

problem Improving deep learning performance and simplifying neural network structures.
method Proposes a thermodynamically coupled Ricci flow that dynamically adapts parameter space geometry to loss landscape topology, enabling automated singularity resolution and providing entanglement entropy bounds.
result Demonstrates 2.1× convergence acceleration and 63% topological simplification while maintaining O(NlogN)\mathcal{O}(N\log N) complexity, outperforming Riemannian baselines by 15.2% in few-shot accuracy.

Generalizes neural network approximation to infinite-dimensional manifolds and derivatives.

problem Approximating differentiable maps on infinite-dimensional manifolds.
method Proves a weighted Nachbin theorem to establish universal approximation for differentiable maps, including derivatives.
result Linear functions of the signature can approximate path space functionals including their derivatives.

Paper connects neural network score approximation to reverse diffusion model distribution approximation.

problem Quantifying the relationship between neural network score approximation and the distribution generated by reverse diffusion models.
method Combines Hornik's universal approximation theorem, Girsanov's theorem, and data processing inequality.
result Neural network score approximation guarantees distribution approximation in reverse diffusion models.

Functional input neural networks approximate continuous functions on weighted spaces.

problem Approximating continuous functions on infinite-dimensional weighted spaces.
method Additive family mapping, non-linear activation, linear readouts, Stone-Weierstrass theorem.
result Global universal approximation of continuous functions on weighted spaces.

Mixtures of neural operators reduce active complexity in operator learning.

problem Reduction of active complexity in operator learning models.
method Constructive comparison between routed mixtures of neural operators (MoNOs) and a fixed single-neural-operator construction.
result Every scalar uniformly continuous nonlinear operator can be approximated by a MoNO whose active expert has smaller depth, width, and rank scaling.

Neural networks can approximate functions uniformly across various measures.

problem Universal approximation of functions across different probability measures.
method Proving neural networks are dense in Orlicz spaces, extending classical theorems.
result Neural networks uniformly approximate functions for weakly compact families of measures.

The neural tangent kernel equivalence theorem fails in practice.

problem Does the neural tangent kernel (NTK) equivalence theorem hold in practical neural network training?
method Rigorously derived NTK and conducted numerical experiments to evaluate the equivalence theorem.
result Adding a layer to a neural network and the corresponding updated NTK do not yield matching changes in predictor error.

Neural networks can approximate gradient of smooth functions, but with limitations.

problem Approximating gradient of smooth functions using neural networks.
method Proving limitations of neural networks with more than one hidden layer and introducing implicit parametrization.
result Neural networks with more than one hidden layer can only represent one feature in their first hidden layer.

This paper presents the first use of graph neural networks (GNNs) for higher-order proof search and demonstrates that GNNs can improve upon state-of-the-art results in this domain. Interactive, higher-order theorem provers allow for the formalization of most mathematical theories and have been shown to pose a significa…

2019-05-24abs ↗pdf ↗

Neural network implementation of Brenier's polar factorization for vector fields.

problem Implementing Brenier's polar factorization theorem for vector fields using neural networks.
method Parameterizing the convex function uu as an input convex neural network and estimating the measure-preserving map MM.
result Practical neural implementation of Brenier's polar factorization theorem.

We study the approximation properties of random ReLU features through their reproducing kernel Hilbert space (RKHS). We first prove a universality theorem for the RKHS induced by random features whose feature maps are of the form of nodes in neural networks. The universality result implies that the random ReLU features…

2018-10-10abs ↗pdf ↗

The paper analyzes Bayesian neural networks trained with VI, proving a law of large numbers for different schemes.

problem Training Bayesian neural networks with variational inference.
method Analyzes three training schemes: exact estimation, Bayes by Backprop, and Minimal VI.
result All training schemes converge to the same mean-field limit.

The paper analyzes neural networks for solving high-dimensional Schrödinger eigenvalue problems.

problem Analyzing generalization error of neural networks for high-dimensional Schrödinger eigenvalue problems.
method Proves convergence rate of generalization error independent of dimension dd under spectral Barron space assumption. Verifies assumption by proving regularity estimate.
result Generalization error rate is independent of dimension dd under spectral Barron space assumption.

Proves the existence of accurate, certifiably robust neural networks.

problem Training neural networks to be robust against adversarial attacks.
method Proves the existence of networks that approximate continuous functions and ensure robustness through interval-bound propagation.
result Proves the existence of accurate, interval-certified ReLU networks.

Gradient descent dynamics in wide neural networks are analyzed using a dynamical CLT.

problem Understanding the fluctuations in wide shallow neural networks trained via gradient descent.
method Dynamical Central Limit Theorem (CLT) applied to neural network dynamics.
result Asymptotic fluctuations remain bounded in mean square throughout training.

With the growth of deep learning, how to describe deep neural networks unifiedly is becoming an important issue. We first formalize neural networks mathematically with their directed graph representations, and prove a generation theorem about the induced networks of connected directed acyclic graphs. Then, we set up a …

2018-05-09abs ↗pdf ↗

Paper proves CFlows can approximate any diffeomorphism and applies it in Bayesian optimization.

problem Proving the universality of CFlows in approximating diffeomorphisms.
method Deriving the universality of Para-CFlows through affine coupling layers and invertible linear transforms.
result Para-CFlows can approximate any diffeomorphism in C^k-norm.

Despite the fact that generative models are extremely successful in practice, the theory underlying this phenomenon is only starting to catch up with practice. In this work we address the question of the universality of generative models: is it true that neural networks can approximate any data manifold arbitrarily wel…

2019-05-27abs ↗pdf ↗

This paper classifies GG-invariant shallow neural networks.

problem Designing optimal GG-invariant neural architectures for GG-invariant target functions.
method Proving theorems about the classification and morphisms of GG-invariant single-hidden-layer neural networks.
result Classification of GG-invariant shallow neural networks and characterization of morphisms.

Introduces Neural-Brownian Motion for modeling dynamics under learned uncertainty.

problem Modeling dynamics under uncertainty with learned parameters.
method Defines NBM using a neural network to replace classical martingale property with a non-linear expectation operator.
result Proves existence and uniqueness of canonical NBM as a continuous εθ\varepsilon^θ-martingale.

Paper proves neural networks can be approximated using interval bounds.

problem Verifying safety and robustness of neural networks.
method Introduces interval universal approximation (IUA) theorem for neural networks.
result Neural networks can be approximated using interval bounds for any continuous function and squashable activation functions.

This work extends GNNs to handle multiple graphs with non-commuting operators, proving transferability.

problem Handling multiple graphs with non-commuting operators in graph neural networks.
method Developed a mathematical theory for graph-tuple neural networks (GtNNs) with non-commuting non-expansive operators.
result Proved universal transferability of GtNNs, ensuring no non-transferable energy under convergence.

This thesis builds theoretical foundations for deep learning, proving complexity theorems and training algorithms.

problem Rigorous explanation of deep learning's success and mathematical challenges.
method Developed circuit complexity theorems, classification theorems, and training algorithms for neural nets.
result Established the existence of high-complexity neural functions and provided rigorous proofs for training algorithms.

New method stabilizes deep neural networks by setting Lyapunov exponent to zero.

problem Stability issues in deep neural networks with low width.
method Lyapunov initialization method to set Lyapunov exponent to zero.
result Lyapunov exponent governs stability of deep networks; standard methods fail for low width.

We show how the success of deep learning could depend not only on mathematics but also on physics: although well-known mathematical theorems guarantee that neural networks can approximate arbitrary functions well, the class of functions of practical interest can frequently be approximated through "cheap learning" with …

2016-08-29abs ↗pdf ↗

Paper approximates BV functions using neural networks with ReLU activation.

problem Approximating BV functions with neural networks.
method Studied convergence of stochastic gradient flow and proved Poincaré inequality for penalized cost function.
result Localization theorem: Error of constrained problem is of order R1/9R^{-1/9} with respect to unconstrained problem.

INT benchmark tests theorem proving agents' ability to generalize to unseen theorems.

problem Evaluating theorem proving agents' ability to generalize to unseen theorems.
method INT benchmark based on a theorem generation and proof procedure with adjustable knobs for measuring 6 types of generalization.
result MCTS can help agents prove new theorems.

Revisits the connection between neural networks and the Kolmogorov-Arnold theorem.

problem Explains the limitations of using the Kolmogorov-Arnold theorem to explain neural networks with multiple hidden layers.
method Derives modifications of the Kolmogorov-Arnold representation that transfer smoothness properties to the outer function and can be well approximated by ReLU networks.
result Shows that a deep neural network with most layers approximating the interior function is a more natural interpretation of the Kolmogorov-Arnold representation.