[gpm]

Just generating code might be interesting too, but in the above comment I was actually thinking of generating formal proofs of correctness.

The process I'm thinking of for using the model is

    Program
    ---(compiler)---> SMT definition + SMT statements for assertions
    ---(z3)---> Proof, Disproof, or "IDK" for assertions
    ↑--(proof-system)--> Filter for "IDK" assertions
    |--(ai)--> A proof of the assertion in the form of simpler assertions
    ⌞---------⌟ back to z3 step

I haven't really thought deeply about training a model off of this, but provided the compiler and z3 are robust against hostile inputs it seems fine even with randomly/AI generated programs. A less pure reinforcement learning technique, where you take code off the internet and only use re-enforcement learning to make it produce useful simpler assertions might work better.

I've started doodling with implementing this loop on top of the rust compiler, but I'm not yet at the point where I can say whether or not it works as well as I hope.