4 ms·
I wonder if AI systems like ChatGPT will be helpful in this area. Something that’s able to track all requirements of a system and understands the code enough to
by rqtwteye 4y ago
I wonder if AI systems like ChatGPT will be helpful in this area. Something that’s able to track all requirements of a system and understands the code enough to validate it against the requirements.
- stfutechbros 4y agoChatGPT is basically the opposite of formal verification... It itself is not verified, and its results are so inaccurate that you need to verify them anyway.
- cartoonfoxes 4y agoMost definitely. I've been playing with using ChatGPT to generate proof texts in Isabelle/HOL, since it lets me verify the correctness of the output before code generation.
- Taikonerd 4y agoI've had the same thought. Formally proven code can give powerful security assurances (cf. Project Everest[1]), but it's also very, very labor-intensive. I've heard rules of thumb like, "100x as much time to prove the software correct as to write it in the first place." If LLM systems are going to give us a virtual army of programmers, I think formally proving more systems software (device drivers, browser engines, etc.) would be a great use of their time. [1]: https://www.microsoft.com/en-us/research/blog/project-everest-advancing-the-science-of-program-proof/ https://www.microsoft.com/en-us/research/blog/project-everes...
- deterministic 4y agoCompCert is a proven correct C compiler proven correct by a very small team in a few years. Used by Airbus for avionics software. GCC after 25 years of work still has bugs.
- AlotOfReading 4y agoI've had extremely poor results attempting to get current LLMs to generate proofs, for code or otherwise.
- ogogmad 4y agoCombining it with AutoGPT (or the ideas it's based on) and a formal prover like Lean might be the answer. Have you tried? Basically, if you don't allow GPT to iteratively write, execute, criticise and then correct its code, you won't get good results.
- rqtwteye 4y agoI think it probably needs to be a specialized combination of LLM and hardcoded knowledge.
- markusde 4y agoYeah, I'm cautiously excited about how AI and FM might work together. I don't think LLM's can ever be trusted to verify programs itself, but anything which can reduce the annotation overhead for programmers is a super useful thing!
- rqtwteye 4y agoI don't think a pure LLM approach will work (or maybe it will, who knows?). I am more thinking of a hybrid that combines LLM or other AI with some hardcoded knowledge for this domain