3 ms·
Oh, I think I misunderstood the proposal there. I thought the language model was meant to be producing (only) code, not proofs. If it manages to produce succes
by schoen 3y ago
Oh, I think I misunderstood the proposal there. I thought the language model was meant to be producing (only) code, not proofs.
If it manages to produce successful proofs of pre-existing property specifications, then that's great!
- ratmice 3y agoYeah, I think the catch is the "pre-existing property specifications" part. I think you need to carefully understand both AI & Human generated propositions. While proofs once checked are just gravy.