A gentle introduction to automated reasoning

https://www.amazon.science/blog/a-gentle-introduction-to-automated-reasoning

by yathaid • 2 years ago

79 21 2 years ago

amazon.science

some_furry• 2 years ago

This should have [2021] in the title.

cubefox4• 2 years ago

Or [pre-ChatGPT]. Nowadays most people would associate "automated reasoning" with language models fine-tuned for chat.

xyzelement3• 2 years ago

I enjoyed this bit:

// When we show this program to industry professionals, they usually figure out the right answer quickly. * A few, especially those who are aware of results in theoretical computer science, sometimes mistakenly think that we can't answer this question, with the rationale “This is an example of the halting problem, which has been proved insoluble”. * In fact, we can reason about the halting behavior for specific programs, including this one.

In other words, where a mid-wit would step through the code (and be right), a high-brow might deems the problem impossible because it fits to a generic class of which this particular instance is trivial.

It's kinda "word thinking" concept where you substitute actual understanding by being able to slap a familiar label on something and then use the label to decide how to feel about it (kinda like feeling differently about a topic based on whether you call it "social justice" which sounds good or "letting criminals roam your city" which sounds bad - whereas in reality it's probably more nuanced and different than either of these labels suggests.)

cubefox4• 2 years ago

Eliezer Yudkowsky once wrote an excellent analysis of this fallacy:

https://www.lesswrong.com/posts/NMoLJuDJEms7Ku9XS/guessing-t...

xyzelement3• 2 years ago

This is spot on and a great articulation of this concept.

Modified3019• 2 years ago

For those confused by the warm plate thing, it’s a reference to this trick the author had posted the previous day https://www.lesswrong.com/posts/fysgqk4CjAwhBgNYT/fake-expla... where the reason the plate it warmer farther away from the radiator, is because the instructor spun it around prior to the students entering the room.

didntcheck• 2 years ago

Yep, it's a sort of accidental form of making perfect the enemy of better, forgetting that while a problem may be undecidable in general, there may still be a useful semi-/decidable subset. E.g. my IDE can still tell me that my program won't halt when I've been an idiot and forgot to update the `while` variable in a loop, halting problem notwithstanding

And similarly with regards to tractability and approximations. The travelling salesman problem is hard, and yet Google Maps works very well. And even when not using an approximation, sometimes n really is small enough to be tractable

denotational2• 2 years ago

there may still be a useful semi-/decidable subset.

Yes, but note that the entire language HALT is semi-decidable (or Turing-recognisable if you use Sipser’s terminology); in this case it’s only the (strictly) decidable subset that is useful.

denotational2• 2 years ago

In other words, where a mid-wit would step through the code (and be right), a high-brow might deems the problem impossible because it fits to a generic class of which this particular instance is trivial.

In this situation, “mid-wit” might best apply to the person who studies theoretical computer science, but never manages to understand when this result is applicable: these people will fall into the second category. But see my comment at the end about whether this terminology is really appropriate.

Someone who quotes the undecidability of HALT in reference to the question of whether that specific program halts is probably not a “high-brow” (whatever that means). It’s a perfect example of “a little knowledge being a dangerous thing”: those who actually understand the theory will know when it applies; it’s those who don’t have a good internalised model of the theory, but who have a vague recollection of something along the lines “it’s impossible to tell if programs halt or not”, who are going to get it wrong.

As a side note, I don’t think “mid-wit” vs. “high-brow” is a good distinction here: whether or not you remember (or were taught) about the halting problem is not a matter of intelligence, and I suspect most people who get it wrong aren’t doing so because they never understood theoretical computer science, but rather because they haven’t been practicing academia, but rather the craft/art of software engineering, and have just forgotten it.

nerdponx• 2 years ago

This situation is portrayed in the "bell curve" meme format, a ternary extension of the "go brr" meme format.

Dimwit at the far left side of the bell curve (somewhat offensively portrayed as a disfigured drooling person) does a simple/stupid thing that works.

Expert at the far right side of the bell curve (portrayed in a Jedi robe) does the same simple/stupid thing as the dimwit.

Person at the middle of the bell curve (with the late-'10s side-buzz hipster haircut) doing some complicated thing based on principle, theory, textbook-correct procedure, etc. This person is in tears, presumably upset that the expert is doing it the simple or stupid way, and believing themselves superior to the dimwit,

nyrikki• 2 years ago

The ints being a total ordered set is why the example will terminate.

Change that to a float, where -0,0,+0 don't have a successor and it could be problematic.

Effectively the example was an existential quantifier, but will universal quantification, termination analysis would be less optimistic.

While it doesn't cover special cases like Ackerman functions, the time complexity is fairly easy to build intuition about with loops being forms of recusion for me.

While is Turning complete or a general recursive functions

For loops are primitive recursive functions

The reason c make choices it made as an example is shown in this paper. For those who haven't seen it.

https://people.csail.mit.edu/meyer/meyer-ritchie.pdf

Almondsetat• 2 years ago

Seems to me a case of people vaguely remembering long gone concepts from their university years.

The halting problem stipulates that it's impossible to have an algorithm that takes any program and decides if it halts. It doesn't say that there could be certain subclasses of programs for which such a procedure could exist.

nickpsecurity• 2 years ago

I’ll also note that the humans aren’t reasoning in their sense. We use a combination of intuition and reasoning which feed into each other. Sometimes on the whole problem, sometimes pieces. That has implications for what to expect out of reasoning tools trying to do what people do.

A solution similar to us would probably train classical analyzers and NN’s side by side on many things. They could use the traditional tools for all the analyses computers can handle. Feed the source and analysis results to NN’s to train them. Then, use them to assist in harder, contextual analyses or probabilistic predictions.

There’s a lot of unexplored territory, with potential gains, if we can mix intuition and reasoning in computers more like people do.

rhelz2• 2 years ago

Interesting that Amazon still thinks there is a place for symbolic, logic-based reasoning, in this era of LLMs.

KuriousCat• 2 years ago

How and why do LLMs get to eliminate symbolic/logic based reasoning?

rhelz2• 2 years ago

I'm thinking about how LLMs like chatGPT did a complete end-run around the more historical attempts of formulating a grammar, translating English into some kind of logical form, using that to query a database, etc etc.

lgas• 2 years ago

Interesting that so many people are still interested in fishing rods in this era of guns.

cubefox4• 2 years ago

I somewhat doubt they still think that. This post is from 2021, before ChatGPT came out.

A gentle introduction to automated reasoning

Related Stories