Hacker News new | ask | show | jobs
by YeGoblynQueenne 217 days ago
The reason why you can write parsers with Prolog is because you can cast the problem of determining whether a string belongs to a language or not as a proof, and, in Prolog, express it as a set of Definite Clauses, particularly with the syntactic sugar of Definite Clause Grammars that give you an executable grammar that acts as both acceptor and generator and is equivalent to a left-corner parser.

Now, with that in mind, I'd like to understand how you and the OP reconcile the ability to carry out a formal proof with the inability to do reasoning. How is it not reasoning, if you're doing a proof? If a proof is not reasoning, then what is?

1 comments

Clearly people write parsers in C and C++ and Pascal and OCAML, etc. What does it mean to come in with "the reason you can write parsers with Prolog..."? I'm not claiming that reason is incorrect, I'm handwaving it away as irrelevant and academic. Like saying that Lisp map() is better than Python map() because Lisp map is based on formal Lambda Calculus and Python map is an inferior imitation for blub programmers. When a programmer maps a function over a list and gets a result, it's a distinction without a difference. When a programmer writes a getchar() peek() and goto state machine parser with no formalism, it works, what difference does the formalism behind the implementation practically make?

Yes maybe the Prolog way means concise code is easier for a human to tell whether the code is a correct expression of the intent, but an LLM won't look at it like that. Whatever the formalism brings, it isn't enough that every parser task is done in Prolog in the last 50 years. Therefore it isn't any particular interest or benefit, except academic.

> both acceptor and generator

Also academically interesting but practically useless due to the combinatorial explosion of "all possible valid grammars" after the utterly basic "aaaaabbbbbbbbbbbb" examples.

> "how you and the OP reconcile the ability to carry out a formal proof with the inability to do reasoning. How is it not reasoning, if you're doing a proof? If a proof is not reasoning, then what is?"

If drawing a painting is art, is it art if a computer pulls up a picture of a painting and shows it on screen? No. If a human coded the proof into a computer, the human is reasoning, the computer isn't. If the computer comes up with the proof, the computer is reasoning. Otherwise you're in a situation where dominos falling over is "doing reasoning" because it can be expressed formally as a chain of connected events where the last one only falls if the whole chain is built properly, and that's absurdum.

> If a human coded the proof into a computer, the human is reasoning, the computer isn't. ... If the computer comes up with the proof, the computer is reasoning.

That is exactly what "formal logic programming" is all about. The machine is coming up with the proof for your query based on the facts/rules given by you. Therefore it is a form of reasoning.

Reasoning (cognitive thinking) is expressed as Arguments (verbal/written premises-to-conclusions) a subset of which are called Proofs (step-by-step valid arguments). Using Formalization techniques we have just pushed some of those proof derivations to a machine.

I pointed this out in my other comment here https://news.ycombinator.com/item?id=45911177 with some relevant links/papers/books.

See also Logical Formalizations of Commonsense Reasoning: A Survey (from the Journal of Artificial Intelligence Research) - https://jair.org/index.php/jair/article/view/11076

With Prolog, the proof is carried out by the computer, not a human. A human writes up a theory and a theorem and the computer proves the theorem with respect to the theory. So I ask again, how is carrying out a proof not reasoning?

>> I'm not claiming that reason is incorrect, I'm handwaving it away as irrelevant and academic.

That's not a great way to have a discussion.

The word "reason" came into this thread with the original comment:

    3. LLMs are bad at solving reasoning problems.

    4. Prolog is good at solving reasoning problems.
I agree with you. In Prolog "?- 1=1." is reasoning by definition. Then 4. becomes "LLMs should emit Prolog because Prolog is good at executing Prolog code".

I think that's not a useful place to be, so I was trying to head off going there. But now I'll go with you - I agree it IS reasoning - can you please support your case that "executing Prolog code is reasoning" makes Prolog more useful for LLMs to emit than Python?

This is not my claim:

>> "executing Prolog code is reasoning" makes Prolog more useful for LLMs to emit than Python?

I said what I think about LLMs generating Prolog here:

https://news.ycombinator.com/item?id=45914587

But I was mainly asking why you say that Prolog's execution is "not reasoning". I don't understand what you mean that '"?- 1=1." is reasoning by definition' and how that ties-in with our discussion about Prolog reasoning or not.

"?- 1=1." is Prolog code. Executing Prolog code is reasoning. Therefore that is reasoning. Q.E.D. This is the point you refused to move on from until I agreed. So I agreed. So we could get back to the interesting topic.

A topic you had no interest in, only interest dragging onto a trangent and grinding it down to make ... what point, exactly? If "executing Prolog code" is reasoning, then what? I say it isn't useful to call it reasoning (in the context of this thread) because it's too broad to be a helpful definition, basically everything is reasoning, and almost nothing is not. When I tried to say in advance that this wouldn't be a useful direction and I didn't want to go here, you said it was " not a great way to have a discussion". And now having dragged me off onto this academic tangent, you dismiss it as "I wasn't interested in that other topic anyway". Annoying.

> "?- 1=1." is Prolog code. Executing Prolog code is reasoning. Therefore that is reasoning. Q.E.D.

This is the dumbest thing i have read yet on HN. You are absolutely clueless about this topic and are merely arguing for argument's sake.

> If "executing Prolog code" is reasoning, then what? I say it isn't useful to call it reasoning (in the context of this thread) because it's too broad to be a helpful definition, basically everything is reasoning, and almost nothing is not.

What does this even mean? It has already been pointed out that Prolog does a specific type of formalized reasoning which is well understood. The fact that there are other formalized models to tackle subdomains of "Commonsense Reasoning" does not detract from the above. That is why folks are trying to marry Prolog (predicate logic) to LLMs (mainly statistical approaches) to get the best of both worlds.

User "YeGoblynQueenne" was being polite in his comments but for some reason you willfully don't want to understand and have come up with ridiculous examples and comments which only reflect badly on you.

I'm sorry you find my contribution to the discussion annoying, but how should I feel if you just "agree" with me as a way to get me to stop arguing?

But I think your annoyance may be caused by misunderstanding my argument. For example:

>> If "executing Prolog code" is reasoning, then what? I say it isn't useful to call it reasoning (in the context of this thread) because it's too broad to be a helpful definition, basically everything is reasoning, and almost nothing is not.

Everything is not reasoning, nor is executing any code reasoning, but "executing Prolog code" is, because executing Prolog code is a special case of executing code. The reason for that is that Prolog's interpreter is an automated theorem prover, therefore executing Prolog code is carrying out a proof; in an entirely literal and practical sense, and not in any theoretical or abstract sense. And it is very hard to see how carrying out a proof automatically is "not reasoning".

I made this point in my first comment under yours, here:

https://news.ycombinator.com/item?id=45909159

The same clearly does not apply to Python, because its interpreter is not an automated theorem prover; it doesn't apply to javascript because its interpreter is not an automated theorem prover; it doesn't apply to C because its compiler is not an automated theorem prover; and so on, and so forth. Executing code in any of those languages is not reasoning, except in the most abstract and, well, academic, sense, e.g. in the context of the Curry-Howard correspondence. But not in the practical, down-to-brass-tacks way it is in Prolog. Calling what Prolog does reasoning is not a definition of reasoning that's too broad to be useful, as you say. On the contrary, it's a very precise definition of reasoning that applies to Prolog but not to most other programming languages.

I think you misunderstand this argument and as a consequence fail to engage with it and then dismiss it as irrelevant because you misunderstand it. I think you should really try to understand it, because it's obvious you have some strong views on Prolog which are not correct, and you might have the chance to correct them.

I absolutely have an interest in any claim that generating Prolog code with LLMs will fix LLMs' inability to reason. Prolog is a major part of my programming work and research.