Re:AI and the Problem of Knowledge Collapse
by thesz on Saturday April 06, 2024 @05:58PM
(#39955995)
Blocked 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.
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.