upvote

points

by Mizza2 hours ago |
comments
upvoteby viraptor2 hours ago|
[-]
The scope of what we can verify is still tiny. It worked well for "this program won't crash". It's really hard for cases like "this encryption is secure" or "this compression always decompresses to the same thing". But anything like "this GUI program that talks to an SQL database does what's expected" is basically impossible and we're not even close.

It's going to take way more than throwing a more advanced LLM at the problem to make any progress.

reply
upvoteby pmontra2 hours ago|
parent|
next
[-]
In many cases we don't even know ourselves what the program should do. There are many edge cases, business decisions, dark and not dark patterns, misunderstood requirements, etc. What can it verify, that the program is doing correctly what we actually did not want it to do? At least we could end up with no bugs in the ORM, but it's not there that my customers are making money.
reply
upvoteby sanderjd47 minutes ago|
parent|
prev|
next
[-]
Right. The paper notes that they stubbed out all the trickier crypto and system call routines with contracts. If those routines don't adhere to the modeled contracts in real execution, then the proof's guarantee won't hold. Also things like concurrency and signal handling are intentionally not modeled.

I think this is an incredible result and I hope we'll see more and more of it, but even still, it's verifying a pretty thin slice of an actually executing system!

reply
upvoteby grumbelbart22 hours ago|
parent|
prev|
next
[-]
Why? We already have formally verified microkernels in production (Apple's L4 variant in their security enclave, for example). I'd say the tools are mostly there, it's a matter of scaling, and maybe a matter of adapting code to make verification easier. Both things where LLMs can shine.

The biggest hurdle is probably the number of bugs in most code. Verification would mean fixing all of those as well.

reply
upvoteby creata1 hours ago|
parent|
[-]
Wikipedia says:

> Apple A series processors beginning with the A7 contain a Secure Enclave coprocessor running an L4 operating system called sepOS (Secure Enclave Processor OS) based on the L4-embedded kernel developed at NICTA in 2006.

Are you sure that sepOS was formally verified? seL4, also from NICTA, was formally verified, but I don't think L4-embedded or sepOS were.

reply
upvoteby vikramkr2 hours ago|
parent|
prev|
next
[-]
The thing about exponentials is that we can go from "we're not even close" to "all software in the world was getting aggressively hacked and we figured it out to stop that from happening" very very quickly. I would not be surprised if by this time next year we had some sort of nist standard for formal verification or something. It certainly changes things a lot once llms can solve millennium problems
reply
upvoteby 1122332 hours ago|
parent|
[-]
You speak as if that is a software or tech problem. People cannot even stop producing direct-to-garbage fast fashion. Who can make them completely rewrite all software, so it is tractable to prove? Please consider that there has been almost no hardware nor llm architecture progress in last few years. Apparent progress is people literally burning money to buy and power the gpus.

You (they) cannot even prove Collatz, how are you planning to prove Powerpoint?

reply
upvoteby vikramkr1 hours ago|
parent|
next
[-]
Claiming the models are not good at math at this point, especially for things like formalization where w you aren't even breaking new ground, is a very very bold claim to make. So ignoring that point for obvious reasons, why would people rewrite all software?

1. Because everything everywhere is getting hacked

2. For the same reasons people are already decomping games and rebuilding Photoshop and stuff - because they can and don't want to pay for proprietary options.

3. Because of the exact same dynamics of fast fashion? I'm not sure how fast fashion supports your point. Fast fashion is specifically not maintaining old clothes and treating all clothes as disposable slop and rotating through them. That dynamic in software is all software becomes single use throwaway and formalization as a part of the agent loop based on some set of standards is a pretty good way to make that tractable

reply
upvoteby 1122331 hours ago|
parent|
next
[-]
What do you mean "no new ground"? There is a very narrow, super constrained set of programs that we know how to formalize, some programs we kinda sorta hope we can, and absolutely everything else where we might not even bother. Check out what epic effort it took to prove 5th busy beaver. no visible abvances on collatz conjecture - and those are among simpliest things you can come up with! Any software that embeds similar behaviour is undecidable by construction. Which forces a rewrite to exclude such behaviour. Or, most likely, fabricating proof criteria that are unsound.

What is more likely, for AI agent that is trained with the goal of making user believe their problem is solved to solve exceedingly hard problem by developing novel theory, or to come up with plausible looking fake solution to the problem?

Fast fashion was mentioned as parallel to fast software — no incentives to lose profits.

reply
upvoteby creata51 minutes ago|
parent|
prev|
[-]
People (humans) have been able to verify 10k-ish line programs so far. I don't think AI has done better yet, but either way it'll probably catch up soon. But getting to the millions or billions of lines of code in real software would be breaking new ground.
reply
upvoteby auggierose1 hours ago|
parent|
prev|
[-]
> You (they) cannot even prove Collatz, how are you planning to prove Powerpoint?

No plans on that front. Instead, I write my software from the start using a methodology of formal specification and proof. And at some point (1 year from now?) that software will include something much better and cooler than Powerpoint.

reply
upvoteby pmontra8 minutes ago|
parent|
next
[-]
I don't know if you comment was sarcasm. If not, how does your methodology specifies and proves that your Powerpoint replacement will draw rectangles with the fashionable gradients of the year you release it. If gradients won't have fallen out of fashion again by then. And that's only a silly example. Programs like that have a huge number of features. I am ready to bet that some of them have been designed and informally approved in front of a coffee machine 20+ years ago.

However yes, anything formal can help and if AIs can hide it from ourselves (we won't be able to follow it) and make it their internal design language chances are that it's going to be really used.

reply
upvoteby 11223355 minutes ago|
parent|
prev|
[-]
That is actually impressive. And most likely the only way to get such software — by writing formally sound code from start. Trying to turn existing toilet pot into pot of gold "with AI" is modern alchemy.
reply
upvoteby saagarjha2 hours ago|
parent|
prev|
[-]
We're starting to get there with stuff like the compression thing.
reply