[gpm]

I do... I want a chatbot that can automatically magic up proofs that all my code is correct for instance. I don't care if I understand the proofs. I care if some tool that checks proofs understands them, and that's a mechanical game just like go or chess.

[sebastiennight]

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.

[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.

[krisoft]

> I want a chatbot that can automatically magic up proofs that all my code is correct for instance.

How could the AI know what you wanted to program? If it was trained only with self play it won’t understand the language where you describe the purpose of the code because it only speaks its own idiosyncratic language. (At best.)

And if it doesn’t know what you wanted to do then all it can prove is that the program does what the program does.

[gpm]

You tell it what you want it to prove. Or the tooling surrounding it does.

The tooling surrounding it might want to prove that "this main function never invokes undefined behavior", or something more local like "for all possible inputs to the public interface to this module, no undefined behavior is invoked".

Or you might want to specify constraints by hand. For examples, you might do that by writing normal tests except you can use magical variables that take on any value [1], or you might do that by annotating functions with contracts that they obey [2]. Or at a simpler level you might just annotate functions that should never panic.

Ultimately once you can prove things about your code, it's a tool in the toolbox for querying how your code works. You can use that to write correct code from the start, or to debug incorrect code, or various other things. The problem is that right now the state of the art (non-ai) can't reason about very complex code without a lot of human help - making it a fairly impractical tool. I think AI might mange to fix that.

[1] This is how kani works in rust, here's an example: https://github.com/model-checking/verify-rust-std/pull/112/f...

[2] Creusot takes this route, here's an example https://github.com/sarsko/CreuSAT/blob/master/CreuSAT/src/so...

[Yoric]

I think that there is a strong limit to that: if you don't understand the proofs, you're going to have a hard time understanding when the model explains to you why your code is not correct.

[gpm]

In most cases I expect saying "<this> assertion fires with <this> input" is enough to be useful. Or "I can't prove <this> assertion doesn't fire, but I don't have a counter example either". Assertion used broadly to include things like rules for avoiding undefined behavior.

Better explanations would be nice of course, but not obviously practical. I wouldn't actually trust the AIs reasoning much in the first place, only that it can't trick the proof checking tool.