5 ms·
Just add a GPT natural language to language proof assistant translator as a front end (with appropriate audio device permissions) Change the need to be really
by sargstuff 3y ago
Just add a GPT natural language to language proof assistant translator as a front end (with appropriate audio device permissions)
Change the need to be really good at proglog to just need to distinctly describe what want/need.
- schoen 3y agoAdding a large language model is going to move you in the exact opposite direction from ease of formal verification.
- epgui 3y agoI mean... Not necessarily? It depends how you use it or what part of the process you delegate to it, no? Whether AI produces Lean code or a human produces Lean code... The Lean code should speak for itself. Both humans and AI are the weak link in either case, and it's unclear to me which of the two is the weaker.
- schoen 3y agoOh, 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.