Comment by aw1621107
2 days ago
The paper explicitly says that if you use an LLM it is prompted function-by-function.
For the SAT solver I think classification can be done function-by-function if you manually drive the solver in the single-function mode, but I think you're more right in that the whole-program mode doesn't actually do that.
I think my misunderstanding stemmed from interpreting the start of section 5.4 and figure 3 as showing that constraint generation occurred strictly before the verifier was invoked and glossing over the bit at the start of section 6 that said that the process basically works the other way around when using the solver to build the p-model.
Perhaps the LLM can infer enough context from one function.
Possibly? Though given its outputs apparently aren't completely out there I'd hazard a guess that the inferred context usually shouldn't be too far off of what can be deduced using more traditional methods.