A Verified Neural Network Model Builder
One of the most exciting discoveries of my PhD work is that it is possible to algorithmically build neural networks that obey logical constraints on their inference before, after, and throughout their training. This is a brand new angle to AI alignment: rather than take an existing neural network and somehow guide it in the direction of the intended behavior through interventions, we can instead synthesize a neural network in advance that already has the intended behavior!
But my PhD work was just a simple proof-of-concept; there’s lots to do to make it useful in practice. My goal is to have a neural network model builder that
1. Allows the user to give constraints in full first-order logic
2. Builds nets that continue to obey rules after update
3. Includes updates for gradient descent and Hebbian learning
4. Is fully formalized and proven correct in Lean
5. The user can run the Lean code as a program to get the neural network output
Bookmark this page in order to keep tabs on progress! If you would like to contribute / collaborate, you can start either by making a pull request on github (currently empty while I migrate this code) or just shooting me an email, cckisby ☆ gmail ♧ com.
Update Log
Update 9/4/2026
I’m officially launching the project! I am not starting from nothing: I have some Lean code from a previous conference paper, which I have chipped away at and modified over the last two years whenever I had time. This code includes
- a formal, general, definition of recurrent neural networks that don’t oscillate
- proofs of various closure properties of neural networks
- the model-building algorithm, but for a modal logic rather than a first-order logic, and for Hebbian learning (no gradient descent)
There are many TODO items left before this software is ready to be used. Some of these things (indicated by 📚) involve open-ended research and conjectures; these will likely take a significant amount of time to get right (and I need to be prepared for the possibility that they cannot be done).
Other items () don’t require new theory, but are necessary to make this practically computable on almost anybody’s laptop. For example, all proofs must be constructive, and certain constructions have to be made more efficient (to curb against things like exponential blowup).
Finally, there are things () that are Nice to Have’s, that would help others adopt this model-building algorithm into their own work.
Here’s the TODO list at the moment, as far as I can tell:
- 📚 Lift the underlying logic from modal to first-order. There is a trick I have in mind for doing this, but it may not be straightforward.
- 📚 Adapt the model building algorithm to work for first-order logic constraints. And the most important thing: prove that it’s correct! This is a scary + fun step.
- 📚 Adapt the model building algorithm to work for gradient descent. Another scary + fun step, I have to think “in advance” about backprop’s effects.
- 💻 Make all nonconstructive proofs constructive! There are a few places where it would have been annoying to give the explicit construction, so I lazily “hacked” the proofs. I’ve got to iron all those out.
- 💻 Test run the process on larger and larger inputs. Make efficiency and space usage cuts wherever I can. This program should not be slower than it absolutely has to be.
- 📝 Add unit testing and other property guarantees
- 📝 Make nice terminal pretty printing & console error logs.
- 📝 Make the terminal user interface nice, and also write up a quick GUI / web interface
- 📝 Write in examples of properties that I have in mind, with files that show the whole process from constraints -> trained neural net
- 📝 Have hooks into Tensorflow + Pytorch. This may be as simple as exporting files that these libraries can then import. Or it may be as complicated as interfacing Lean with Python, and importing certain public functions.