derrak

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 biggest barrier to adoption of program synthesis is writing the spec/maintaining it as the project matures. Sometimes we don’t even know what we want as the spec until we have a first draft of the program. But as you’re pointing out, LLMs could help address all of these problems.

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 were a few times where the false assumption I had to resolve was very close to the starting point. Tricky stuff.

And you designed all of these by hand? That is very impressive. How many mazes are there? The way I would start automating some of this would be to build a catalog of these visually tricky blocks that require the player to resolve a false assumption. Then I think it would be a matter of stitching these together in novel ways. Maybe the stitching procedure can be implemented by expressing a constraint system and solving for a stitching that has the properties you want.

I’m on a touch screen and I would say that the movement is a little bit sensitive. Concretely this means I found myself… going in a direction I didn’t intend to. Maybe this is a skill issue on my part. I don’t have alternative controls to suggest and I probably don’t understand the mechanics of the movement enough to even suggest which parameters to tweak.

Again, great work.

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 have downsides that can be addressed with _symbolic_ tools. But _determinism_ has very little to do with this.

LLMs by nature are non-deterministic

This is false. LLMs are functions. All appearances otherwise are an artifact of how we use them.

This fact already suggests that determinism isn’t (entirely) what you want. Because even if you _could_ use LLMs as functions (I admit you can’t always do this with frontier models), that wouldn’t make you happy.

I want the output to always be predictable based on the behavior of the program and provided configuration.

Here, I will argue that predictability here is divorced from determinism. You want an output that has a certain semantic relationship with the input. E.g., if you give a spec as input, you want a program that satisfies this spec.

Here it should be obvious that getting the same output on the same input is not very important. Who cares if the arguments to the function are renamed? Who cares if the function is implemented differently but essentially does what the spec asks?

I argue the _only_ thing that matters is that the output satisfies the intended relationship with the input. And this is orthogonal to determinism.

Edit:

It looks like the author has the same realization:

And while even this example shows how differently an LLM responds to the same query, it ends up producing a more reliable output.

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 cutting down beforehand because reducing cigarettes often makes them seem more valuable rather than less. Setting a quit date helps you prepare mentally and physically to stop smoking on that day.

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 data to be decrypted in two or more different ways, creating plausible deniability.

Doesn’t this make the whole idea of legislating this a non-starter?

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 made a python looking DSL for LLMs to convert natural language logic puzzles to. Then they converted the DSL expression to something a SAT/SMT solver could munch on.

My initial reaction was “why don’t they just have the LLM write smtlib2.” And I guess the answer is that LLMs are probably better at writing python-looking smtlib2. Probably an oversimplification of their work on my part. But I didn’t see any comparison between their work and a direct encoding into smtlib.

Makes me wonder if your idea could work along similar lines. Instead of using lisp directly, could you use a DSL that looks like more traditional languages? Would that help?

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 automated.

Question about your calculator example: is the intended use case that the user would write these L0-L2 files? Or is it expected that an LLM would write them with user intervention? And the go program, how is that obtained from L2? Is that a symbolic transformation or is the LLM doing it?

Apologies if this is written somewhere and my skimming missed it.

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 verification, but I think it is ready for formal specification and counterexample generation.

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 provide no formal relationship between their inputs and outputs.

One way to side step this is to have the LLM translate the NL into a formal language and persuade the human that the formal language captures their intent. This reduces the burden because the user only has to look at and understand the formal language spec, rather than all the code produced by the LLM.

Also once a formal spec is obtained, you can do lots of interesting computation on it. Property based testing comes to mind. Or even full-blown verification of the formal spec. Or, LLMs might be good at recognizing ambiguity. An LLM could generate two formal specs, use an SMT solver to find an input where the specs differ, and help the user use this diff to ask clarifying questions and resolve the ambiguity.

One comment I have is that layers L1 and L2 _might_ be reinventing the wheel slightly. Your ensure statements remind me of Dafny or Verus, for instance, which have a lot of tooling behind them.

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 how good the automation is in ACL2 and partially a commentary on the fact that I don’t use it for hard problems :)

I use it more for property based testing. The counterexample generator is very powerful because it leverages the knowledge base of the theorem prover (all the accumulated lemmas, etc.) among other things.

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 languages like Dafny and Lean.

An alternative that side steps all of this is to not use an external language at all. ACL2 might be a better fit in this regime than Dafny or Lean because of how close it sits to SBCL.

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: why are we using a statistical model to control this search, and not a symbolic model?

Modern SAT and SMT solvers are excellent at searching spaces. There has already been work on biasing them with machine learning. Symbolic models for control, statistical models for bias. We should be thinking about how to apply this idea to practical, industrial software engineering tasks. There is already some work on program synthesis from formal specifications, but it has yet to scale.

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 progress towards human-like intelligence is in principle possible. In reality, we do not know.

For me this isn’t an assumption, it’s a corollary that follows from the Church-Turing thesis.

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 intelligence does matter today because we’re going to kneecap ourselves if we incorrectly believe there is something special about humans. It will stop us from closing that gap.

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 capabilities in hardware and software are beyond our current abilities. It seems likely that it is possible though, even if we don’t know how to do it yet.

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 otherwise are due to how we use them

b) lots of traditional technologies which have none of the problems of LLMs are non-deterministic. E.g., symbolic non-deterministic algorithms.

Non-determinism isn’t the problem with LLMs. The problem is that there is no formal relationship between the input and output.

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 teach current LLM backed systems new tricks. But do we have reason to believe that no AI system can synthesize novel technologies. What reason do you have to believe humans are special in this regard?

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 typo. “The author didn’t care enough to proofread, why should I bother reading.”

Remember, this is important: do not look at the tests. If you let them into your context

This is a bad idea. You are trusting the LLM’s ability to follow instructions. Worse, depending on your harness the LLM might not even be able to follow these instructions. The harness may indiscriminately place code into the context in a way that is uncontrolled by the LLM.

A better idea is to modify your harness so that certain files are excluded from the context.

I asked another AI to carefully review the tests and identify those that don't make sense.

Test validation is an entire area of research and I’m yet to be convinced that this is a task for LLMs.

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 knuckle any search process. AI is not going to give us completeness, even if we can tack on a post-hoc soundness check. Moreover, AI can act as a heuristic but it is not going to automatically exploit symmetries and other symbolic contours of the space. Exploiting such contours is what makes these symbolic tools so powerful.

There has been a lot of work on combining symbolic search with machine learning as a heuristic. To me, this is the most promising route. My take is that we should use the statistical models to bias, and the symbolic models to control.

Verifying software is mathematics: the same reasoning that proves a theorem in abstract algebra proves that a cryptographic library correctly implements its specification.

I also want to push back on this. If you have written a mechanical proof about software and a mechanical proof about a mathematical object, you’ll note that they feel qualitatively different.

In my experience, proofs about software have way more case splits involving thousands or even millions of cases. Proofs about more traditional mathematical objects tend to have far fewer case splits of this nature. The obligations in proofs about software tend be easier to automatically. Mathematical objects tend to require a lot more insight and infrastructure around them.

Of course proofs about software are still mathematics and the same infrastructure can found both. I am merely suggesting that proofs about software may be amenable to more specialization than proofs about mathematics generally.

I will also say that finding a counterexample tends to be more important in software settings than finding a proof. This is because software tends to have bugs whereas mathematics tends to eliminate such bugs before we bother to mechanically formalize it.

The AI community has already made its choice.

I wonder if this is the wrong choice. Lean is great for reasoning about mathematics. I don’t think it’s the right choice for reasoning about industry scale software. I hate the ACL2 user experience, but I think it is fundamentally more fit to reason about software. I wish the AI community would take a broader look at what formal methods tools are available instead of just picking up the hottest most popular tool and shoe horning everything into it.

I think your solution is a good idea. I was just pushing back on why it’s a good idea. Determinism isn’t the crux. The crux is that you’re using a symbolic algorithm with well-defined formal semantics.

I was trying to show that determinism is not the crux by pointing out that there are ways to get a deterministic output from an LLM. And that thought experiment shows that determinism isn’t what’s essential.

And I will disagree about merely narrowing the outputs. If I download a local model and set the temperature to zero and give it the same prompt twice, I will get the same output. Not one of several outputs in a narrow set. LLMs are functions.

It's deterministic on purpose (doesn't include any Al layer)

I wouldn’t use the word deterministic here. I would use the word symbolic. Determinism, meaning that you always get the same output on the same input, isn’t what you want here. For instance, you can use an LLM without temperature, etc. and its output will be deterministic. More over, if you had a symbolic, non-deterministic algorithm you would probably also be happy to use that.

In my mind the most salient difference between code and natural language is that code has a formal semantics.

I’m still not entirely sure what people mean when they call a formal/natural language deterministic. As we’ve discussed, it can’t possibly mean that it has a single valid interpretation, since this is untrue of C code. If it means that code has a _precise set_ of interpretations, then I wouldn’t use the word deterministic for that.

All compilations do what I intended to do when I wrote the C code. But each compilation does the intended thing in a different way.

The point I’m making is that determinism isn’t the key difference between compilers and LLMs. The key difference is that LLMs do not give semantic guarantees. I don’t care if they give the same output on the same input, just as I don’t care very much which C compiler I use.

I don’t know your background, but suspect that if you were given sufficient motivation, you could solve these problems in an esoteroic language. It might be tedious, but I suspect that most anyone with an undergraduate degree in computer science and sufficient experience in a couple programming languages could meet the task.