The gap between formal and informal has been pointed out as an Achilles' heel of formal methods from the dawn of the field, so critique is not particularly new. The standard reference is Social processes and proofs of theorems and programs (1979), which is worth reading.
No. Did you even read the article? It talks about the "specification gap", which is the difference between the formalized semantics and the intended semantics.
Every formal method has that problem (including the mentioned trivial ones like SAT and SMT).
There are ways to partially improve or at least quantify the specification gap using LLMs, by analyzing variance in the output formal specification when given a natural language specification (by eg. generating many formal specs from an input description).
See eg. "Draft-and-Prune: Improving the Reliability of Auto-formalization for Logical Reasoning" [1].
4 comments
[ 2.8 ms ] story [ 22.1 ms ] threadEvery formal method has that problem (including the mentioned trivial ones like SAT and SMT).
See eg. "Draft-and-Prune: Improving the Reliability of Auto-formalization for Logical Reasoning" [1].
[1]: https://arxiv.org/abs/2603.17233