4 ms·
>This means I need LM to be trained on the SAT solving and on vast amount of Haskell code. Essentially why the current batch of top-tier LLMs are trained on a
by freeone3000 3y ago
>This means I need LM to be trained on the SAT solving and on vast amount of Haskell code.
Essentially why the current batch of top-tier LLMs are trained on a pile of text amounting to “the internet”, containing every haskell q&a on stackoverflow, every sat implementation on github, and every explaination of those terms on wikipedia. It might seem unreasonable without the sense of scale and expense of building these things; but yes, it has those input data in its training set.
- thesz 3y agoBlocked clause decomposition is implemented in, I think, two SAT preprocessors in SAT solvers, both are C++. There are about three to five different articles on the topic. For LLM to implement BCD in Haskell it needs to be able to translate between Haskell and C++ and it is well beyond trivial.