It seems like a lot of the trouble with making this plan work is the trouble of making formal verification scale to very large and messy systems, which has been an open problem for a long time, and is the big place this class of idea might turn out to be effectively impossible. It may be that noise pressure is too high, so learning the real world unavoidably forces mess beyond the reach of any formal verification based approach.
I’ve bumped into various folks who tried formal verification for neural networks before and the thing they’ve said consistently is, “well, you can do it at all, but the most complex properties are still things like not crashing an aircraft in a simplified flight simulator for a low-millions-of-parameters model, and that’s primarily possible because of the low dimensional input/output space.”
formally verifying huge, combinatorial spaces (eg, llm/image/physics model IO) seems potentially very far beyond tractability, even with the help of a deep learning approach specifically designed for scaling formal verification to huge messy things. if it’s possible to make this work, it’d look like figuring that out.
It seems like a lot of the trouble with making this plan work is the trouble of making formal verification scale to very large and messy systems, which has been an open problem for a long time, and is the big place this class of idea might turn out to be effectively impossible. It may be that noise pressure is too high, so learning the real world unavoidably forces mess beyond the reach of any formal verification based approach.
I’ve bumped into various folks who tried formal verification for neural networks before and the thing they’ve said consistently is, “well, you can do it at all, but the most complex properties are still things like not crashing an aircraft in a simplified flight simulator for a low-millions-of-parameters model, and that’s primarily possible because of the low dimensional input/output space.”
formally verifying huge, combinatorial spaces (eg, llm/image/physics model IO) seems potentially very far beyond tractability, even with the help of a deep learning approach specifically designed for scaling formal verification to huge messy things. if it’s possible to make this work, it’d look like figuring that out.