undefined | Better HN

0 pointssebastiennight1y ago0 comments

In the specific example you're quoting, this would in theory be possible : train a model to just output random code in a specific language, then run it to provide feedback of whether the code was correct or not.

In the end you might be able to get a model very highly capable of outputting or validating correct code without ever having seen human code.

One issue I'm seeing with this is that the space of possible harmful code that you'd need to run on the training machine is quite vast, even in a VM. I wouldn't touch that with a 10-foot pole, or plug it to the Internet.

0 comments

gpm1y ago

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.

j / k navigate · click thread line to collapse