3 ms·
> But, you can generally prompt around this sort of thing by asking the model to adopt a preferred context such as "you're an expert xxx", providing of course t
by thesz 3y ago
> But, you can generally prompt around this sort of thing by asking the model to adopt a preferred context such as "you're an expert xxx", providing of course that is did see such expert-tagged material in the training set.
So, I need LM to be an expert in SAT solving and an expert Haskell programmer. This means I need LM to be trained on the SAT solving and on vast amount of Haskell code.
I think it is already easy to see that LM should be trained in an intersection of quite fringe (yes, I am watching that TV series right now) things.
I also think that it is beyond reason to ask for this.
- p1esk 3y agoPlease get back to us when you try whatever you’re trying to do with a good model (gpt4, opus, or ultra). I recommend refraining from making (and especially from posting) any conclusions until then.
- thesz 3y ago> a good model Strongly reminds me of "no true scotsman." If you have an access to a good model, try that simple problem of blocked clause decomposition and please get back to us.
- p1esk 3y agoI do have access to good models, but you are the one making far reaching statements about LLMs. Please preface your future posts on the topic with “I’ve never tried any decent models, so I don’t know what I’m talking about”.
- thesz 3y agoI will include such disclaimer after you prove me wrong as you have means to do that.
- p1esk 3y agoSounds good. What prompt do you want me to try?
- thesz 3y ago"Please implement blocked clause decomposition in Haskell" I, actually, asked my friend to ask whatever LLM he paid for to perform this experiment. I think he uses latest or previous GPT. At least he is paying for it which I cannot do and won't do in foreseeable future. Just like I said above, not only LLM failed to properly implement the algorithm, it failed to provide even remotely correct types for clauses and blocked clauses. What happened next amused me like nothing else related to AI. The exchange that followed incorrect initial attempt, GPT clearly tried to persuade my friend to implement the correct version for it, constantly providing him with partially (and stupidly) incorrect code. This is exactly what MathCraft [1] does. [1] https://en.wikipedia.org/wiki/Cyc#MathCraft https://en.wikipedia.org/wiki/Cyc#MathCraft And this behavior is clealy counterproductive. This is not what one might expect from anything that is advertized as a good assisting measure. I can use ghci, vim and actual paper with much greater effect.
- thesz 3y agoThe LLM under test was GPT 4 turbo.
- 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.