We're posting lots of papers written with GPT-6 Astra on generalization properties of bayesian neural net learning.[1] The following picture emerges:
For variousreasonablepriors on MLP weights,[2] the induced prior on functions is a circuit prior: for fixed depth, the ordering of functions by negative log prior is roughly their ordering by minimal circuit width. From a quantitative version of this statement, one gets the following sample complexity bound: if the function is implemented by a circuit of width , then conditioning on train data points is sufficient to get test accuracy.[3]
These results hold as long as is realizable; in particular, for arbitrarily overparametrized NN-bayes.
For various other reasonable priors on MLP weights,[5], one gets bad sample complexity when very overparametrized: when learning some functions , even after seeing train data points, the learner is still likely to have at least some constant test error rate.
GPT-6 Astra has produced Lean formalizations corresponding to each of the 5 papers individually referenced above.[6] The folder contains 30+ more manuscripts which have not been formalized yet[7]; our guess is that each manuscript is correct[8].
If you want to understand this research program, we recommend starting from these slides to understand the setup and some key ideas, and then reading the FAQ to get a sense of the current state of the agenda, including its many open problems.
specifically, the "mean field" prior and priors which are "stronger" than it; you can think of these as priors that care a bunch about minimizing norm ↩︎
except for exponentially small probability in the choice of , and this assumes no distribution shift between train and test ↩︎
There is a host of possible conditions here; there are open research directions of understanding how reasonable our candidate conditions are, coming up with more natural alternative conditions, or arguing that there isn't any very natural condition. For some cases, it is open if a robustness assumption is needed at all. ↩︎
specifically, certain priors that care about norm less than the mean field prior ↩︎
Opus 5.5 reviewed these formalizations and said all theorem statements were formalized correctly. ↩︎
because we didn't want to throw more money into tokens at this time ↩︎
possibly modulo minor errors that don't kill the result or the proof strategy, as usual in math ↩︎
We're posting lots of papers written with GPT-6 Astra on generalization properties of bayesian neural net learning. [1] The following picture emerges:
GPT-6 Astra has produced Lean formalizations corresponding to each of the 5 papers individually referenced above. [6] The folder contains 30+ more manuscripts which have not been formalized yet [7] ; our guess is that each manuscript is correct [8] .
If you want to understand this research program, we recommend starting from these slides to understand the setup and some key ideas, and then reading the FAQ to get a sense of the current state of the agenda, including its many open problems.
prior work ↩︎
specifically, the "mean field" prior and priors which are "stronger" than it; you can think of these as priors that care a bunch about minimizing
except for exponentially small probability in the choice of
There is a host of possible conditions here; there are open research directions of understanding how reasonable our candidate conditions are, coming up with more natural alternative conditions, or arguing that there isn't any very natural condition. For some cases, it is open if a robustness assumption is needed at all. ↩︎
specifically, certain priors that care about
Opus 5.5 reviewed these formalizations and said all theorem statements were formalized correctly. ↩︎
because we didn't want to throw more money into tokens at this time ↩︎
possibly modulo minor errors that don't kill the result or the proof strategy, as usual in math ↩︎