Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Automating AI Away

replicated.live

Post reply on HN
Print view View original

21–30 of 69 posts

Re: Automating AI Away

#21

Post by gritzko »

Animats wrote: post #12

This makes sense, although it's not well described here. Formal methods, as in proof of correctness, have been around for decades (I was doing that stuff in the 1980s) but pushing the proofs through was too laborious. The seL4 verification effort reportedly used over a decade of people time. The idea is that if you have a formal specification of what you want to happen, you can get a LLM to do the struggling with the…

might be relevant: https://martin.kleppmann.com/2025/12/08/ai-formal-verificati...

Re: Automating AI Away

#22

Post by derdi »

hadi121 wrote: post #14
derdi wrote: post #7

Earlier quoted context omitted.

Humans aren't deterministic. Determinism is a red herring. There are lots of other problems with agentic programming, but this is not at the top of the list.

I agree with the humans aren't deterministic, but I feel like that wasn't the scope of the original commentator. Humans are not deterministic, yes. Neither are LLMs. Both should be phased out of processes that need to be deterministic. What do you think?

I don't think processes have to be deterministic. Results should be, in the following sense: Both humans and LLMs should write software that is well-written, well-tested, well-documented, and that meets the spec. But this still leaves a lot of room for creativity (or rolling dice).

Re: Automating AI Away

#23

Post by dofm »

gritzko wrote: post #8
derdi wrote: post #6

This is a very interesting introduction to a blog post, but... I'm somehow missing the actual blog post. How does this stuff work in practice? What are some concrete examples? How does one get from JavaScript tokenizing things in a commit hook to validating that the LLM didn't disable tests it didn't agree with, or any other helpful property?

I am the author. I am trying to limit one post to one page. Most people here are reading reasoning all day, I am afraid. Might get tired. I also aspire to make one post a day. To be continued.

> Most people here are reading reasoning all day, I am afraid. Might get tired.

This is well-observed.

Re: Automating AI Away

#24

Post by Animats »

oulipo2 wrote: post #18
Animats wrote: post #12

This makes sense, although it's not well described here. Formal methods, as in proof of correctness, have been around for decades (I was doing that stuff in the 1980s) but pushing the proofs through was too laborious. The seL4 verification effort reportedly used over a decade of people time. The idea is that if you have a formal specification of what you want to happen, you can get a LLM to do the struggling with the…

Problem is, usually describing the problem you want to solve *correctly* using formal tool is a task as hard (and often, equivalent to) the implementation. That said, having a formal description is useful

For some problems, yes. Formal specification is particularly useful in two cases. 1) The problem is simple but an efficient implementation is hard or bug-prone. Examples are garbage collection, file systems, sorts, databases, and tree updating. 2) The inverse of the problem is simpler than the forward operation. Examples include matrix inversion and parsing.

Re: Automating AI Away

#25

Post by Animats »

gritzko wrote: post #21
Animats wrote: post #12

This makes sense, although it's not well described here. Formal methods, as in proof of correctness, have been around for decades (I was doing that stuff in the 1980s) but pushing the proofs through was too laborious. The seL4 verification effort reportedly used over a decade of people time. The idea is that if you have a formal specification of what you want to happen, you can get a LLM to do the struggling with the…

might be relevant: https://martin.kleppmann.com/2025/12/08/ai-formal-verificati...

Yes. I should have cited that. He has this right.

Re: Automating AI Away

#26

Post by inspectorSlap »

lubujackson wrote: post #2

Makes sense, I have had the biggest wins with AI by attacking nondeterminism whenever possible. BTW, you should probably fix the Beagle link on your homepage: https://replicated.live/beagle/

I find some of the most interesting, and catastrophic failures in my agent fine-tuning come from the clamping down of non-determinism. It is totally the correct approach, but must be handled delicately. The non-deterministic core remains, but now under bimodal pressure.

Re: Automating AI Away

#27

Post by inspectorSlap »

stego-tech wrote: post #4

Basically what I’ve been saying since OldJob forced LLMs down our throats and pegging performance to usage metrics: why the fuck are we handing deterministic processes to probabilistic systems when it should be the other way around (using probabilistic systems to design deterministic ones)? LLMS should be abstracted out of a process as soon as practicable, replaced with deterministic processes or procedures. Otherwis…

This is exactly right. Abstracted out of the process, or to a point of most optimal application.

Re: Automating AI Away

#28

Post by auggierose »

Animats wrote: post #24
oulipo2 wrote: post #18

Earlier quoted context omitted.

Problem is, usually describing the problem you want to solve *correctly* using formal tool is a task as hard (and often, equivalent to) the implementation. That said, having a formal description is useful

For some problems, yes. Formal specification is particularly useful in two cases. 1) The problem is simple but an efficient implementation is hard or bug-prone. Examples are garbage collection, file systems, sorts, databases, and tree updating. 2) The inverse of the problem is simpler than the forward operation. Examples include matrix inversion and parsing.

I wouldn’t split it like that. Formal verification is useful in the case that the spec is simpler than the implementation. That’s it.

Coming up with simple specs is not necessarily easy. You could say that is kind of what math is about. That’s how we actually make progress: find those cases where simple specs are possible and build upon them. That’s the kind of library made for eternity.

Re: Automating AI Away

#29

Post by x3haloed »

stego-tech wrote: post #4

Basically what I’ve been saying since OldJob forced LLMs down our throats and pegging performance to usage metrics: why the fuck are we handing deterministic processes to probabilistic systems when it should be the other way around (using probabilistic systems to design deterministic ones)? LLMS should be abstracted out of a process as soon as practicable, replaced with deterministic processes or procedures. Otherwis…

Actually... yes. I was bracing to be very annoyed with your comment starting with "why is everyone using AI so stupid?!" (I know those weren't your words, but it felt like that kind of post)

And then... yeah. You got it exactly right. Once a problem or process is deterministic, that's the wrong application of an LLM.

But I had never quite thought of it in these exact terms. The way I've been thinking about it up until now is that the very best way to use LLMs is to have them produce tools. The tools get to stay reliable and predictable. They boost your performance. But I think you found the more general abstraction of the same idea. Tool-making is not deterministic. But the tools themselves can be. That's why it fits. Trying to stuff LLMs into what's otherwise a deterministic process is an absurd waste and error-prone.

Smart. I like it.

Re: Automating AI Away

#30

Post by verdverm »

Second this, following Cloudflare's post on how they do agentic PR review, I'm working on a script that renders the conext and diff to disk before passing it off to the agent, which generates a jsonl file of comment add/update, which another script will process. Way better than handing it bash and clis so it can fumble about non deterministically
Post reply on HN