Ada

58 readers

3 users here now

Ada programming language. For memory safe multi task programming, elegant embedded bit fiddling and everything else in a readable way

founded 4 months ago

MODERATORS

cm0002@programming.dev

cm0002@lemmy.world

Verifying LLM-Generated Code in the Context of Software Verification with Ada/SPARK (arxiv.org)

submitted 1 week ago by cm0002@lemmy.world to c/adalang@programming.dev

2 comments fedilink hide all child comments

you are viewing a single comment's thread
view the rest of the comments

[–] gnufuu@infosec.pub 1 points 1 week ago

The performance of Marmaragan with GPT-4o on the benchmark is promising, with correct annotations having been generated for 50.7% of the benchmark cases. The results establish a foundation for future work on combining the power of LLMs with the reliability of formal software verification.

That's basically a coin flip. Even if you made it less successful a user would have higher chances of guessing correctly whether an annotation is true of false.