Formal Verification is truly needed especially on this.
What he calls formal verification is what we would call regular math in machine learning. Deep learning is sorely lacking hard bounds for all sorts of things (generalization, etc.). It's something that's gotten substantially better over the past year, but is something that needs a lot of work.
PAC guarantees are very different. They generally rely on:
- Data proportional to 1/eps^2
- Only reduce the “variance” component of the “bias + variance” (you’ll never fit a linear model perfectly to a nonlinear dataset, regardless of PAC)
- Get worse as you decrease bias
- Assume your data is IID and identically distributed to the test data. In TFA, several of the examples of bad behavior come from data which is distributed differently from training data (adversarial examples or automated cars not moving out of the way)
What I initially meant by "hard bounds" was any kind of mathematical proof more rigorous than "well, dropout kinda makes your neural network not rely on one feature so that's why it generalizes".
As for your points, I don't think they're really criticisms of PAC bounds.
I'm not familiar with the first point, but it'd be surprising to me if most PAC bounds had that, considering PAC is a framework and not a specific technique...
Your second point is irrelevant to generalization. You're looking for theory about capacity I think? I think learnability also comes into play.
3rd: that is indeed what the bias variance trade-off would imply. It's also why most classic PAC bounds are vacuous for neural networks.
4th: I think that's a fair assumption to make for any meaningful study of generalization.
For the common case of "The model misclassified a data point, no idea why.", formal verification doesn't help, but that doesn't make it completely useless. Probably not worth the effort, though.