Comment by ogogmad
3 years ago
> The existence of seL4 and its ability to be used in real projects certainly proves that formal methods has been effectively used to improve safety and security in shipping products, which was the question you asked if I understood it correctly...
No, I would expect evidence that seL4 actually gets used. Otherwise it's yet another purely academic proof of concept.
> GPT-4 ... closer to Eliza ... over-hyped ... "Stochastic Parrots" paper
You might want to look at this YouTube channel here, to see that LLMs are capable of imagination and complex logical reasoning: https://www.youtube.com/@aiexplained-official
Who knows what the future holds? ¯\_(ツ)_/¯
Anyway, it would be interesting to know a bit more about your field experience using formal methods - if possible. Thanks.
seL4 has seen use in military projects, including UAVs and drones. It's been endorsed by the Linux Foundation. I wouldn't really call it an academic proof of concept at this point.
Regarding logic problems, I've tested GPT-4 and Bard. Both fail some pretty typical logic problems, because that's not what they were designed to solve. They match patterns. This is great for story telling, summarizing, and replication of plausible prose based on its training. But, these systems break down in subtle ways when prompted to perform logical reasoning. Don't take my word for it though.
https://arxiv.org/abs/2205.11502
Even logical reasoning we take for granted, like variable substitution, is difficult for an LLM.
https://paperswithcode.com/paper/the-reversal-curse-llms-tra...
I will agree with you, however, that making any predictions about where this technology will go in the future is difficult. My experience tells me that the current modeling of LLMs are on the wrong track, but a lot of money is being invested in this technology. If there is a way to improve it incrementally, and if these incremental improvements can cause a significant paradigm shift, then perhaps I'll be proven wrong.
As for my field experience using formal methods, I currently build system software and firmware. I use model checking daily. I have built up abstract machine models using Coq and Lean 4 to constructively build data structures and algorithms that I can extract to C and machine code. Typically, these would include software cryptographic primitives, graph algorithms, data structures like binary trees, and file systems. I'd say that model checking covers about 95% of my usage of formal methods, and constructive proofs cover the remaining 5%. I use a combination of CBMC and Z3 to model check the software and firmware that I write. CBMC is used to model check software in C. Z3 is used to model check assembler and machine code.
Even logical reasoning we take for granted, like variable substitution, is difficult for an LLM.
https://paperswithcode.com/paper/the-reversal-curse-llms-tra...
This was a retrieval from training issue, not an inference one. and people have this issue too.
Variable substitution is just not a thing for natural language. sometimes it rings true, most of the time it makes no sense to assume it.