I want to push back against the idea that ANNs are “vectors of floating points” and therefore it’s impossible to prove things about them. Many algorithms involve continuous variables and we can prove things about them. Support vector machines are also learning algorithms that are “vectors of floating points” and we have a pretty good theory of how they work. In fact, there already is a sizable body of theoretical results about ANNs, even if it still falls significantly short of what we need.
The biggest problem is not necessarily in the “floating points”. The problem is that we still don’t have satisfactory models of what an “agent” is and what it means for an agent to be “aligned”. But, we do have some leads. And once we solve this part, there’s no reason of principle why it cannot be combined with some (hitherto unknown) theory of generalization bounds for ANNs.
For an even more extreme example, Linear Regression is a large “vector of floating points” that’s easy enough to prove things about proofs are assigned as homework questions for introductory Linear Algebra/Statistics classes.
I also think that we’ve had more significantly more theoretical progress on ANNs than I would’ve predicted ~5 years ago. For example, the theory of wide two layer neural networks has basically been worked out, as had the theory of infinitely deep neural networks, and the field has made significant progress understanding why we might expect the critical points/local minima gradient descent finds in ReLU networks to generalize. (Though none of this work is currently good enough to inform practice, I think?)
I’m uncertain about what R abstractions/models are best to use for reasoning about AI. Coq has a numberofoptions, which might imply different things about provability of different propositions and economic viability of those proofs getting anywhere near prod. Ought a type theorist or proof engineer concern themselves with IEEE754 edge cases?
We are not at the stage of formal verification, we are merely at the stage of constructing a theory from which we might be able to derive verifiable specifications. Once we have such specifications we can start discussing the engineering problem of formally verifying them. But the latter is just the icing on the cake, so to speak.
I want to push back against the idea that ANNs are “vectors of floating points” and therefore it’s impossible to prove things about them. Many algorithms involve continuous variables and we can prove things about them. Support vector machines are also learning algorithms that are “vectors of floating points” and we have a pretty good theory of how they work. In fact, there already is a sizable body of theoretical results about ANNs, even if it still falls significantly short of what we need.
The biggest problem is not necessarily in the “floating points”. The problem is that we still don’t have satisfactory models of what an “agent” is and what it means for an agent to be “aligned”. But, we do have some leads. And once we solve this part, there’s no reason of principle why it cannot be combined with some (hitherto unknown) theory of generalization bounds for ANNs.
see also
+1 to both points.
For an even more extreme example, Linear Regression is a large “vector of floating points” that’s easy enough to prove things about proofs are assigned as homework questions for introductory Linear Algebra/Statistics classes.
I also think that we’ve had more significantly more theoretical progress on ANNs than I would’ve predicted ~5 years ago. For example, the theory of wide two layer neural networks has basically been worked out, as had the theory of infinitely deep neural networks, and the field has made significant progress understanding why we might expect the critical points/local minima gradient descent finds in ReLU networks to generalize. (Though none of this work is currently good enough to inform practice, I think?)
I’m uncertain about what R abstractions/models are best to use for reasoning about AI. Coq has a number of options, which might imply different things about provability of different propositions and economic viability of those proofs getting anywhere near prod. Ought a type theorist or proof engineer concern themselves with IEEE754 edge cases?
We are not at the stage of formal verification, we are merely at the stage of constructing a theory from which we might be able to derive verifiable specifications. Once we have such specifications we can start discussing the engineering problem of formally verifying them. But the latter is just the icing on the cake, so to speak.
I personally think work on reduced precision inference (e.g. 4 bit!) is probably useful, as circuits should be easier to analyze than floats.