2 ms·
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 th
by yaj54 3y ago
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 3y agoDecoupling 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 3y agoAre you using the SAT/SMT solvers to feed training data into a transformer or integrating the solver logic into the model code?