Programming

28500 readers

579 users here now

Welcome to the main community in programming.dev! Feel free to post anything relating to programming here!

Cross posting is strongly encouraged in the instance. If you feel your post or another person's post makes sense in another community cross post into it.

Hope you enjoy the instance!

Rules

Follow the programming.dev instance rules
Keep content related to programming in some way
If you're posting long videos try to add in some form of tldr for those who don't want to watch videos

Wormhole

Follow the wormhole through a path of communities !webdev@programming.dev

founded 3 years ago

MODERATORS

snowe@programming.dev

Ategon@programming.dev

UlrikHD@programming.dev

bugsmith@programming.dev

Spyro@programming.dev

-15

"Bend": an attempt to apply formal proofs to AI-generated code (github.com)

submitted 16 hours ago by unquietwiki@programming.dev to c/programming@programming.dev

3 comments fedilink hide all child comments

This showed up on TLDR today. Supposed to be able to loop this in with AI-assisted code development to provide guardrails on what the program is actually supposed to do.

top 3 comments

sorted by: hot top controversial new old

[–] litchralee@sh.itjust.works 12 points 12 hours ago* (last edited 12 hours ago) (1 children)

I'm deeply skeptical. If the whole premise is that natural language (which is how prompts to AI generation are given) is insufficiently precise to constrain output, and that formal specification is precise enough, then why are we bothering to use natural language generation? If this works as stated, then it's a tactic admission that the thing being checked is inherently flawed. Why not just use the formal specification to generate code then?

I suspect that two things are true: natural language is inherently insufficiently precise for nontrivial code generation, and also that formal specification is not broad enough to describe all the code which is being generated today using AI/LLMs.

Reliability of generated output was never an engineered goal for LLMs, and no amount of "reasoning by Lego" can fully compensate for this no matter how complex the mitigations in post. It's the same reason why safety (under any definition) cannot be "bolted on" to an LLM after the fact.

[–] Zarobi@aussie.zone 4 points 10 hours ago* (last edited 10 hours ago)

I read the GitHub and tried it out. It basically works by recursively testing the output. It seems very expensive, and not specific in implementation. In the example given, the LLM can still make any changes it wants, as long as it doesn't fail the test. They're also designed to be written by the LLM itself, not humans. So it's not really a replacement for natural language.

It reminds me of integration testing tools such as Cypress, except it's an LLM running the test on itself. The "laws" are only in effect when the LLM understands the laws, and understands how it's change will affect compliance with them.

In my opinion, in practice, LLMs will end up writing a 19,000 lines long impenetrable and unreadable "law handbook", get confused about the laws, burn through a ridiculous amount of time and tokens recursively testing itself at every step of the journey, and people will end up removing it. It's cool in theory though, but it has so many rough edges that seem inherit to the technology.

[–] thoughtfuldragon@lemmy.blahaj.zone 8 points 14 hours ago

And the circle of programming continues except now there's a world destruction machine in there too.