derrak

So do you disagree with the parent that “code is just a spec as far as the C compiler is concerned”?

Maybe it’s important to agree on what a spec is. For instance, do you agree that a spec can be just as formal as code implementing the spec? For instance, if the spec is written in a machine parseable logic do you take that to be a spec? Or are you taking a spec to be written in natural language?

I suspect some of your disagreement with the parent is about this definition. I’m just trying to understand because for me it’s uncontroversial to claim C code is a spec for assembly code, but maybe the issue is that I am not thinking of specs in the colloquial way.

My cynical take on this sort of research is that we will never use raw LLMs to solve these kinds of reasoning problems and it’s therefore unclear why we bother to test them on these kinds of benchmarks.

Modern SAT solvers are completely cracked. I think there are a lot of potential synergies between such symbolic solvers and machine learning (and maybe even LLMs). But it doesn’t seem like an LLMs ability to directly solve these tasks with no symbolic tool use is going to predict the quality of these synergies.

Are there any good systems that somehow enforce consistency between documentation and code? Maybe the problem is fundamentally ill-posed.

I see. Then we’re on the same page. My follow up question is: why do we care if the LLM is deterministic?

Hypothetically, if we could guarantee a semantic relationship between the input and output we wouldn’t care if the LLM was deterministic. For instance, if I give the LLM a lean theorem and it instantiates a program and a mechanical proof that the program conforms to the lean theorem, I just don’t care about determinism. Edit: this is equivalent to me not caring very much about which particular conformant C compiler I pick

And my understanding of LLMs is that they actually are functions and the observed randomness is an artifact of how we use them. If you had the weights and the hardware, you could run the frontier models deterministically. But I don’t think you’d be satisfied even if you could do that. Edit: this is maybe analogous to picking a particular C compiler that does not promise conformance

There are valid concerns with LLMs but I’m not convinced non-determinism is the thing we should care about.

> if we noted them down, it would have been longer than the code

If you are only noting down requirements of what the program is doing rather than how it should do that thing, I would expect that writing the requirements would necessarily be more succinct than writing the program.

It terrifies me every time I realize people are just jumping into writing code without specifying what that code is required to do. A day of hacking saves an hour of critical thought and planning.

> code is rigid and deterministic

I really wish people would start defining what they mean when they say code is deterministic. For instance, code is not deterministic in the sense that it admits a single interpretation when compiled. C code admits many assembly interpretations and the assembly you get will vary depending on your compiler and parameters.

When people say code is deterministic I think they mean it has a formal semantics. But these formal semantics may admit any one of many interpretations.

> two programs can both satisfy the same spec and have completely different

The spec should express all relevant constraints. If your spec admits two things and only one is admissible in your mind, your spec is incomplete.

> has a massive envelope

The size of the envelope is less relevant than the expressivity of the language used to express subsets of that envelope. But almost always there is some logic which is more succinct for expressing the spec than the programming language used to express the implementation.

> your security posture is now a function of how exhaustive your spec is

The alternative is that your security posture is a function of unstated intentions living in somebody’s brain. This alternative seems strictly worse.

> You'd need to enumerate what NOT to do

This is equivalent to declaring what you must do and usually there is a succinct way to do this that does not involve listing every negative example

Why is this a weird definition of determinism? Could you please define what you mean when you say deterministic?

A C program does not identify a single assembly program. It identifies a set of assembly programs. This fits the pretty standard definition of non-determinism.

A difference between natural language and C code is that natural language does not have a formal semantics. Having no formal semantics is a very different problem from having a semantics that admits a well-defined set of interpretations.

> LLMs output the average of their training data

I think it follows that if you ask it to implement something, it will implement the average thing.

But then it also follows that if you give it the average thing and ask it to improve it by doing something clever, it may identify a clever improvement if such an improvement has ever been done in an analogous setting that exists in its training set.

> Your own cleverness would have to be below average

In this case the difference between myself and the LLM is that I’ve never seen the clever thing before (or I cannot recall it as effectively), but the LLM has and the LLM is specialized to recall it

> Creating this spec is often going to be harder than writing a single compliant program.

I’m not sure if I agree. A good spec will specify what the program is supposed to do rather than how the program should do that thing. It should be easier to specify what rather than how. Moreover, it should be standard practice to express what before you start writing how.

I see some people pushing back on this by saying two programs that satisfy the same spec might have different performance or security properties. That is correct and if you care about those things, you should specify them. Writing down these properties, e.g., “the program is O(n) where n is blah” should be much easier than implementing a non-trivial linear time algorithm founded in deep ideas.