[yaj54]

Is the theory tied to a specific llm? I'm interpreting it as, e.g., the llm writes the code, the solver verifies it, repeat until correct. In this situation the two are decoupled and the llm would be a drop in and thusly could be any local or remote llm. Is there something about your approach that doesn't allow this?

(also, +1 for OS link request)

[nextos]

Decoupling both is the simplest option, but not the one I am focusing on. Also note SAT/SMT can also be used for synthesis.

In fact, synthesis has a relatively rich history using SAT/SMT solvers.

[yaj54]

Are you using the SAT/SMT solvers to feed training data into a transformer or integrating the solver logic into the model code?