Hacker News

points by lilbigdoot 3 days ago | 0 comments

> The only way to do that is to make your code provable. That again is only realistically doable using AI.

I think that LLMs actually cannot do this right now while people can?

Also there is a lot of defensive programming that has been left to application and runtime layers because of dated security models in our OS and permissions that are way too coarse. It's a lot easier to write a correct program when you don't have to check every path and do that perfectly when the permission system can ensure that no files that haven't been whitelisted cannot be read

[–] adastra22 3 days ago

My intuition is the opposite? The math results we are seeing lately are done with theorem provers. LLMs are getting very good at this and surpassing what humans have been able to prove. Verified code is traditionally very expensive and only applicable in niche areas when done by humans.

[–] foopod 3 days ago

> LLMs are getting very good at this and surpassing what humans have been able to prove.

But if the reverse were true it would be impossible to prove. AI is trained on all of humanities solutions - LLMs stand on the shoulders of giants, not the other way around.

[–] adastra22 3 days ago

As of today, the training data the originates from humans represents a vanishingly small portion of the total training. The vast majority of training - how many 9’s is a trade secret - of a frontier model is synthetic RLVR data. That’s how they got good at this.

[–] drdeca 3 days ago

I thought only like a third (maybe 2/3?) of the training was RLVR?

[–] adastra22 2 days ago

It’s an increasing portion of training month by month. As of this last summer, pretty much all new GPU hardware is going to a combination of inference and post-training model tuning, generally RLVR.

[–] gfosco 3 days ago

We do, too, as we have also been trained from the same prior solutions.

[–] Loquebantur 3 days ago

LLMs can, in principle, do everything humans can. And arguably more. "Right now" is how long? People are slow.

"Provable" essentially means, you have explicit operators acting on explicit states in an exhaustively defined way that preserves "truth", explicitly defined invariants.

A finite thing you can argue over deterministically.

Obviously, "you" there is an LLM, the machine your code is run on has to be defined in that very same exacting manner and so on.

That still isn't enough, you need abstraction, a hierarchy of categories that preserve your intent and accurately describe the problem space.

"Programming" then is solving an inverse problem over that hierarchy, filling in the blanks sensibly on your way down through the model hierarchy, all the way to atomic instructions your (proven) hardware understands.

Those layers of proper abstraction is what's largely missing currently. Or rather, is merely vaguely approximated.

All of which is to say: yes, the current state is a mess. Resolving that is far from easy.

But you really have no choice, that mess is transparent to large-enough LLMs. Security by obscurity only goes so far.

[–] AnthonyMouse 3 days ago

> But you really have no choice, that mess is transparent to large-enough LLMs.

It's transparent to large-enough LLMs given enough resources. Which is the thing that was always true. The difference now is that the level of resources is lower, so we're finding a bunch of things it wasn't previously economical to find.

But the cost still isn't zero. On top of that, the same LLMs are now generating enormous volumes of new code, which both nobody has verified to that level of exaction and nobody has even considered how it interacts with existing and other new code.

[–] lilbigdoot 3 days ago

> Those layers of proper abstraction is what's largely missing currently. Or rather, is merely vaguely approximated.

This I can agree with, and my perspective would be that we have theoretical solutions with no ergonomics, and rely on unproven (as in formally proven/validated) mechanisms. WASM + capability passing is enough, but the WASM layer is still built on an OS or runtime that is not proven and you'll have a heck of a time trying to build a product on it

[–] boston_clone 3 days ago

> LLMs can, in principle, do everything humans can.

I think narrowing the scope of this statement would better support your argument, as it is easily disproved in its current form.

[–] freecodeio 3 days ago

LLMs can't do a backflip. I can.

[–] solyin 3 days ago

Unitree's H2-X can.

https://youtu.be/Y3zb4o47yqA

[–] deadfoxygrandpa 3 days ago

is unitree h2-x an llm?

[–] braj0 2 days ago

why not? I'm sure you could bolt one onto it...

[–] drivebyhooting 3 days ago

I can’t do a backflip. I guess I’m subservient to LLMs then.

[–] combinebeatsai 3 days ago

> LLMs can, in principle, do everything humans can.

Oh yeah? slides baton Pick up that can, Clanker.

Jokes aside, I do want to see the first news of AI going out of its way to acquire and make use of actual currency and hiring a meat proxy. I don't even care what for, can be making paperclips.

[–] khafra 2 days ago

The first such news is pretty old: In ARC's 2023 eval of GPT-4, it hired a TaskRabbit worker to bypass a CAPTCHA out of the small research budget allocated to the agent. Even the rentahuman.ai site which forms a market for meat puppets is kinda old now.

[–] xanderbookface 2 days ago

What do you think would b e a good experiment to run? At this point it could be interesting to just give AI some money, connect it to rentahuman, and see what it does.

[–] criley2 3 days ago

https://bend-lang.com/

Folks are creating some interesting stuff in this space