5 ms·

I've noticed quite a lot of Prolog content lately. I don't know if it's just a case of the Baader–Meinhof phenomenon, but it looks to me that recent article[1]

by lelag 2y ago

I've noticed quite a lot of Prolog content lately. I don't know if it's just a case of the Baader–Meinhof phenomenon, but it looks to me that recent article[1] about Prolog being able to improve LLM reasoning abilities renewed some interest in the language. [1] https://shchegrikovich.substack.com/p/use-prolog-to-improve-llms-reasoning https://shchegrikovich.substack.com/p/use-prolog-to-improve-...

worldsayshi 2y ago
Here's the hacker news post: https://news.ycombinator.com/item?id=41831735 https://news.ycombinator.com/item?id=41831735
- dang 2y ago
  Thanks! Macroexpanded: Use Prolog to improve LLM's reasoning - https://news.ycombinator.com/item?id=41831735 https://news.ycombinator.com/item?id=41831735 - Oct 2024 (155 comments)
deleted 2y ago
[deleted]
weinzierl 2y ago
Which is strange considering how old and limited Prolog in a sense is. I wonder why no superset ever gained traction and what it would look like. I imagine it fitting somewhere in the hierarchy Theorem Prover ⊃ SMT Solver ⊃ SAT Solver since Theorem Prover ⊃ Prolog
- sixfiveotwo 2y ago
  Indeed, you can get a lot more from dependent types than Damas-Hindley-Milner inference, yet does it mean that you should use the former everywhere?
- Byamarro 2y ago
  Learning curve perhaps? There doesn't have to be an overlap between people working on this and the tools you have mentioned
- knome 2y ago
  limited in what sense? prolog is turing complete.
  - Epa095 2y ago
    He might be thinking about the SLDNF resolution happening. But yes, you can implement any prover in prolog. This distinction is discussed a bit here: https://www.metalevel.at/prolog/theoremproving https://www.metalevel.at/prolog/theoremproving
- Epa095 2y ago
  The post in OP has the following hyphothesis: > Why Prolog? [...] Due to it's declarative nature it might be a bit easier for LLMs to generate code, because LLM doesn't need to generate precise control flow. This is an interesting point, and my guess is that prolog is the declarative programming language with most example code out there for it to learn on(excluding SQL). Alternatively it could try to create some problem description for an automated theorem prover. My (absolute ignorant) guess is that the prolog aproach works better for two reasons: - The amount of prolog code in the training set is higher - It is still only able to create code for problems easy enough that prolog can handle them.
- dsabanin 2y ago
  Another attractive feature of Prolog is that it’s homoiconic, like lisp.

by lelag 2y ago

worldsayshi 2y ago

Here's the hacker news post: https://news.ycombinator.com/item?id=41831735 https://news.ycombinator.com/item?id=41831735

dang 2y ago
Thanks! Macroexpanded: Use Prolog to improve LLM's reasoning - https://news.ycombinator.com/item?id=41831735 https://news.ycombinator.com/item?id=41831735 - Oct 2024 (155 comments)

deleted 2y ago

[deleted]

weinzierl 2y ago

Which is strange considering how old and limited Prolog in a sense is. I wonder why no superset ever gained traction and what it would look like. I imagine it fitting somewhere in the hierarchy Theorem Prover ⊃ SMT Solver ⊃ SAT Solver since Theorem Prover ⊃ Prolog

sixfiveotwo 2y ago
Indeed, you can get a lot more from dependent types than Damas-Hindley-Milner inference, yet does it mean that you should use the former everywhere?
Byamarro 2y ago
Learning curve perhaps? There doesn't have to be an overlap between people working on this and the tools you have mentioned
knome 2y ago
limited in what sense? prolog is turing complete.
- Epa095 2y ago
  He might be thinking about the SLDNF resolution happening. But yes, you can implement any prover in prolog. This distinction is discussed a bit here: https://www.metalevel.at/prolog/theoremproving https://www.metalevel.at/prolog/theoremproving
Epa095 2y ago
The post in OP has the following hyphothesis: > Why Prolog? [...] Due to it's declarative nature it might be a bit easier for LLMs to generate code, because LLM doesn't need to generate precise control flow. This is an interesting point, and my guess is that prolog is the declarative programming language with most example code out there for it to learn on(excluding SQL). Alternatively it could try to create some problem description for an automated theorem prover. My (absolute ignorant) guess is that the prolog aproach works better for two reasons: - The amount of prolog code in the training set is higher - It is still only able to create code for problems easy enough that prolog can handle them.
dsabanin 2y ago
Another attractive feature of Prolog is that it’s homoiconic, like lisp.