In case you’re not familiar, I will point you to the classical program synthesis literature. There the task is to take a spec written in say first-order logic, and output a program that satisfies this spec. I think the…
Wow! I really enjoyed this. The 2.5D rendering gives a lot of opportunities to visually obscure the insight that’s necessary to solve the maze. It makes me think that a good maze should have a “oh, duh” moment. There…
Makes me think of academic papers that overhype their contribution. Also makes me think about AI hype.
How do you define determinism?
Lets solidify definitions. A procedure is deterministic iff for all inputs, it always produces the same output on that input. Now, I am going to be pedantic because words matter here. I agree with the author that LLMs…
This app runs contrary to one of the most prolific stop smoking guides. https://www.allencarr.com/easyway-stop-smoking/top-tips-to-s... > You’re going to stop naturally so carry on smoking as usual until then. > Avoid…
> As a countermeasure to key disclosure laws, some personal privacy products such as BestCrypt, FreeOTFE, and TrueCrypt have begun incorporating deniable encryption technology, which enable a single piece of encrypted…
I like. On the issue of “are LLMs good at lisp” I have a bit of a tangential response/observation. I saw this [paper](https://ai.meta.com/research/publications/logic-py-bridging-...) awhile ago. Long story short they…
> I also thought about pushing more toward Lean and theorem proving instead of a lighter SMT-style direction I think your intuition here is good. For these settings I think you want formal methods that are highly…
Happy to help. In general, I think counterexample generation is more important than proofs when it comes to software (most of our software is “trivially” wrong). The world might not be ready for full-blown formal…
This looks very interesting. I think the translation from L0 to L1 is going to become more and more important. There have been a lot of discussions here on HN about how natural language specs “aren’t code” and how LLMs…
I do use ACL2, although I don’t do many proofs. When I do, the proofs usually go through automatically or require me to state only a few lemmas or tell the tool how to do the induction. This is partially a commentary on…
Noted, thanks. I don’t know what non-computational intelligence would look like but I guess I’ll keep my mind open.
> The proofs stop at the language boundary. The bugs don’t. In formal verification, you have to model everything you care about. I suspect we’ll see large fragments of popular languages being more thoroughly modeled in…
Looks interesting. Anything in particular from it that you think relates to my comment?
> Certainly it is much closer to a brick than to a human. I disagree with this premise. A computer approximates a Turing Machine, which puts it far above a brick.
> Recently I’ve been thinking about coding with AI in terms of it being a process of navigating a tree of probabilistic outcomes. I think this is the correct way to think about automated coding. The natural question is:…
We can keep our discussion about church turing here if you want. I will argue that the following capacities: 1. creating rules and 2. deciding to follow rules (or not) are themselves controlled by rules.
As long as agnosticism is the attitude, that’s fine. But we shouldn’t let mythology about human intelligence/computational capacity stop us from making progress toward that end. > unstated assumption that technological…
Note that I prefaced my comment by saying the parent might be right about LLMs. > That's irrelevant. My comment was relevant, if a bit tangential. Edit: I also want to say that our attitude toward machine vs. human…
The Church-Turing thesis comes to mind. It would at least suggest that humans aren’t capable of doing anything computationally beyond what can be instantiated in software and hardware. But sure, instantiating these…
> non-deterministic printer. I interpret non-deterministic here as “an LLM will not produce the same output on the same input.” This is a) not true and b) not actually a problem. a) LLMs are functions and appearances…
Maybe you’re right about modern LLMs. But you seem to be making an unstated assumption: “there is something special about humans that allow them to create new things and computers don’t have this thing.” Maybe you can’t…
First, I have some advice if you are open to it. Apply a spell/grammar checker to your post before sharing it with other people. Your post has several typos and many people will stop reading after the first or second…
> AI must control the proof search, not delegate to a black box. Cannot disagree more. Take a look at modern SAT solvers, SMT solvers, and automated theorem provers like ACL2. We should _not_ be letting the AI’s white…
In case you’re not familiar, I will point you to the classical program synthesis literature. There the task is to take a spec written in say first-order logic, and output a program that satisfies this spec. I think the…
Wow! I really enjoyed this. The 2.5D rendering gives a lot of opportunities to visually obscure the insight that’s necessary to solve the maze. It makes me think that a good maze should have a “oh, duh” moment. There…
Makes me think of academic papers that overhype their contribution. Also makes me think about AI hype.
How do you define determinism?
Lets solidify definitions. A procedure is deterministic iff for all inputs, it always produces the same output on that input. Now, I am going to be pedantic because words matter here. I agree with the author that LLMs…
This app runs contrary to one of the most prolific stop smoking guides. https://www.allencarr.com/easyway-stop-smoking/top-tips-to-s... > You’re going to stop naturally so carry on smoking as usual until then. > Avoid…
> As a countermeasure to key disclosure laws, some personal privacy products such as BestCrypt, FreeOTFE, and TrueCrypt have begun incorporating deniable encryption technology, which enable a single piece of encrypted…
I like. On the issue of “are LLMs good at lisp” I have a bit of a tangential response/observation. I saw this [paper](https://ai.meta.com/research/publications/logic-py-bridging-...) awhile ago. Long story short they…
> I also thought about pushing more toward Lean and theorem proving instead of a lighter SMT-style direction I think your intuition here is good. For these settings I think you want formal methods that are highly…
Happy to help. In general, I think counterexample generation is more important than proofs when it comes to software (most of our software is “trivially” wrong). The world might not be ready for full-blown formal…
This looks very interesting. I think the translation from L0 to L1 is going to become more and more important. There have been a lot of discussions here on HN about how natural language specs “aren’t code” and how LLMs…
I do use ACL2, although I don’t do many proofs. When I do, the proofs usually go through automatically or require me to state only a few lemmas or tell the tool how to do the induction. This is partially a commentary on…
Noted, thanks. I don’t know what non-computational intelligence would look like but I guess I’ll keep my mind open.
> The proofs stop at the language boundary. The bugs don’t. In formal verification, you have to model everything you care about. I suspect we’ll see large fragments of popular languages being more thoroughly modeled in…
Looks interesting. Anything in particular from it that you think relates to my comment?
> Certainly it is much closer to a brick than to a human. I disagree with this premise. A computer approximates a Turing Machine, which puts it far above a brick.
> Recently I’ve been thinking about coding with AI in terms of it being a process of navigating a tree of probabilistic outcomes. I think this is the correct way to think about automated coding. The natural question is:…
We can keep our discussion about church turing here if you want. I will argue that the following capacities: 1. creating rules and 2. deciding to follow rules (or not) are themselves controlled by rules.
As long as agnosticism is the attitude, that’s fine. But we shouldn’t let mythology about human intelligence/computational capacity stop us from making progress toward that end. > unstated assumption that technological…
Note that I prefaced my comment by saying the parent might be right about LLMs. > That's irrelevant. My comment was relevant, if a bit tangential. Edit: I also want to say that our attitude toward machine vs. human…
The Church-Turing thesis comes to mind. It would at least suggest that humans aren’t capable of doing anything computationally beyond what can be instantiated in software and hardware. But sure, instantiating these…
> non-deterministic printer. I interpret non-deterministic here as “an LLM will not produce the same output on the same input.” This is a) not true and b) not actually a problem. a) LLMs are functions and appearances…
Maybe you’re right about modern LLMs. But you seem to be making an unstated assumption: “there is something special about humans that allow them to create new things and computers don’t have this thing.” Maybe you can’t…
First, I have some advice if you are open to it. Apply a spell/grammar checker to your post before sharing it with other people. Your post has several typos and many people will stop reading after the first or second…
> AI must control the proof search, not delegate to a black box. Cannot disagree more. Take a look at modern SAT solvers, SMT solvers, and automated theorem provers like ACL2. We should _not_ be letting the AI’s white…