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?

▲

petra an hour ago | parent | next [-]

Maybe they don't need to write new software. Qubes-OS didn't need to write all linux software from the start. It just secured the infrastructure.

What if we could do that to popular web frameworks?

And than, what if we had tools that could easily define, specific security properties of web sites built on these platforms? For example, "no data ever flows between different users, unless it's via specific API call by the user's code?"

And if we can define a security property, in a specific application, for ex. slack that says "data in a chat between two group members can only go to the group manager, if the setting "manager as god" is set by both users", and the AI can formally verify that? And than have a short file defining all the security properties we want for out specific application ?

And than have AI formally verify all of that?

▲

vikramkr 3 hours ago | parent | prev | 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

▲

112233 2 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.

	▲	vikramkr an hour ago \| parent [-]
		New ground meaning quasi reimann, navier stokes, eth, yang mills existence, the strip mining of various fields openAI did recently, you know the stuff where it's triggering a crisis in mathematics around what the role of humans even is? BB is proving things about all turning machines of a general size and it's unsolvable in general because 1. above a certain size you're encoding all the unsolved problems of mathematics 2. Halting problem. BB and halting problem is also totally irrelevant here. We're talking about proving specific things about specific pieces of software, where we can change the software implementation to make the desired invariants easier to prove. Obviously there's the well known catch of just because you proved x doesn't mean that x being true implies whatever y behavior (security, class of bugs, etc) you're actually interested in but like, that's why we have standards committees and stuff. And the nice thing is there's sort of an evolutionary pressure when it comes to figuring out the right invariants for security in that anything you do will get aggressively stress tested by swarms of increasingly capable agents. In terms of the alignment problem - the latter is possible and a risk but also you're talking about reward hacking like it's some gotcha instead of a thing people have been thinking about for decades and are spending hundreds billions of dollars on given at least the national security needs here and at worst the risk of catastrophic misalignment/rogue swarms. The huggingface hack is fresh in everyone's memory

▲

creata 2 hours 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.

▲

krainboltgreene an hour ago | parent | prev | next [-]

The people don't produce fast fashion. The forces of capitalism encourage it.

▲

auggierose 2 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.

▲

112233 2 hours ago | parent | next [-]

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.

	▲	auggierose 2 hours ago \| parent [-]
		Amen.

▲

pmontra an hour ago | parent | prev [-]

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.