[nextos]

Not yet, it's a bit rough. The LLM I am using requires a bit of extra fine-tuning to be really smooth, I need to rent a bigger GPU. Besides, I am working on some novel integration between transformers and SAT/SMT that will take me some time to finish.

[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?

[obeavs]

Our product (phosphor) is built end-to-end in F# so this stuff is close to my heart. You might find Moonbit's approach to functional AI interesting as well https://www.moonbitlang.com/blog/moonbit-ai.