Great points, which I take as drawing attention to the tradeoff between false positives and false negatives in automatic verification. Especially in domains not considered security-critical, we may be happy to accept that a verifier (perhaps based on an LLM) sometimes accepts a program with a bug, so long as it makes the right call most of the time.
There is a subtlety to the question of which verifiers count as “extremely limited in what they can handle.” I’m thinking most prominently of general-purpose proof assistants like Lean. They should be able to verify correctness of any program, but the catch is that someone (human, AI, a collaboration between them) needs to write a proof! However, once the proof exists, it is easy to check.
FWIW, I totally agree that we need to change the verifiers to answer the challenges of new developments in AI-assisted programming. So much effort is going into performance-optimizing ML inference, and the extent of similar effort for formal-verification tools is paltry in comparison, setting us up for formal methods as a performance bottleneck. That’s why I’m excited about building new hardware-software stacks optimized for formal verification and program synthesis, perhaps hosting symbolic and neural workloads on the same platform with fast interconnect. It’s a major thrust of my own present research, and I will return to the subject often in future articles I’m planning.
The chance to take advantage of LLM “internal languages” is a great point, whose consequences I haven’t digested yet.
Great points, which I take as drawing attention to the tradeoff between false positives and false negatives in automatic verification. Especially in domains not considered security-critical, we may be happy to accept that a verifier (perhaps based on an LLM) sometimes accepts a program with a bug, so long as it makes the right call most of the time.
There is a subtlety to the question of which verifiers count as “extremely limited in what they can handle.” I’m thinking most prominently of general-purpose proof assistants like Lean. They should be able to verify correctness of any program, but the catch is that someone (human, AI, a collaboration between them) needs to write a proof! However, once the proof exists, it is easy to check.
FWIW, I totally agree that we need to change the verifiers to answer the challenges of new developments in AI-assisted programming. So much effort is going into performance-optimizing ML inference, and the extent of similar effort for formal-verification tools is paltry in comparison, setting us up for formal methods as a performance bottleneck. That’s why I’m excited about building new hardware-software stacks optimized for formal verification and program synthesis, perhaps hosting symbolic and neural workloads on the same platform with fast interconnect. It’s a major thrust of my own present research, and I will return to the subject often in future articles I’m planning.
The chance to take advantage of LLM “internal languages” is a great point, whose consequences I haven’t digested yet.