AI 如何应对验证软件的组合爆炸
AI 导读
一个朴素的问题：我看到很多人说 AI 将帮助构建形式验证的软件，就像 AI 帮助形式化数学一样。 但验证软件的瓶颈不就是证明*每一个*程序执行都安全的组合爆炸吗？ AI 如何帮助解决这个问题？
正文
Naive Q: I see many people say that AI will help build formal verified software, similarly to how AI helps formalize math
But isn't the bottleneck for verified software the combinatorial explosion of proving that *every* program execution is safe?
How does AI help with that?