4 ms·

I'd also add that AI code generation in non-formally-verifiable languages, at places with concurrency requirements like Nvidia, might end up in the short-term c

by btown 2y ago

I'd also add that AI code generation in non-formally-verifiable languages, at places with concurrency requirements like Nvidia, might end up in the short-term creating more hard-to-spot concurrency bugs than before, as developers become incentivized to tab-complete code without fully thinking through the implications as they type. But AI code generation for formally verifiable programs? And to assist in writing custom domain-specific verifiers? Now that's the sweet spot. The programming languages of the future, and the metaprogramming libraries on top of them, will look really, really cool.

erichocean 2y ago
> But AI code generation for formally verifiable programs? For verifiable domains, this really is the sweet spot. An annoying aspect of verification-in-practice is that it is just really bulky—there's a lot to type in, and it's tedious. LLMs, especially the latest crop of weak-reasoning models, are great for this.
- atiedebee 2y ago
  I tested o3-mini yesterday, having it verify a bit-hack for "vectorizing" 8x8bit integer addition using a single 64 bit int value[0]. Suffice to say, I am not impressed. I asked it to give me a counter example that would make the function fail, or to tell me that it works if it does. It mentioned problems regarding endianness which weren't present, it mentioned carries that would spill over which couldn't happen. I had given it chances to give counter examples, but the counterexamples he gave didn't fail. Only after telling it that I tested the code and that it works did it somewhat accept that the solution worked. I think a deterministic, unambiguous process is a lot more valuable for formal verification. [0] https://chatgpt.com/share/67aefb63-f60c-8002-bfc6-c7c45b452018 https://chatgpt.com/share/67aefb63-f60c-8002-bfc6-c7c45b4520...
  - hyperman1 2y ago
    A limitation I see with AI for coding is that your problem must be mainstream to get decent results. In my experience, if I ask it to do web things in PHP or Java, data things in Python, ... it gives a good enough result. If I ask it a postgis question, I get an answer with hallucinated APIs, bugs, and something that doesn't even do what I want if it works. I suspect the ADA/Spark world and the formal verification world are to small to decently train the AI.
    - amoss 2y ago
      > A limitation I see with AI for coding is that your problem must be mainstream to get decent results. Or to phrase it another way, there must examples of the technique that you want to "generate" in the training set otherwise the horrifically overfitted model cannot work. Probably a little bit too cynical but this is my experience asking LLMs "unusual" questions.
      - nottorp 2y ago
        Seems realistic. I tried asking a LLM for a full code snippet for the first time yesterday (i've been using them as search engines better than google, which isn't saying much, before). It produced code that compiled but failed to do anything because the 3rd api call it generated returned an error instead of doing what the LLM said it would do. Didn't spend time on seeing what was wrong because we already had a library that did the same thing; I was more testing what the LLM can do.
      - TheOtherHobbes 2y ago
        No, that's about where we are. Today's LLM coding is basically automated Stack Overflow copy/paste - not too bad for anything simple and mainstream, but unable to reason about code from first principles, and fond of making up random shit that looks good but doesn't work.
  - brabel 2y ago
    I thought OP was saying AI can generate the code that can then be formally verified based on your non-verifiable code, not that the AI itself is verifying it? I could be wrong, of course.
    - atiedebee 2y ago
      Perhaps I misread it then. I think that if you're at the point of using formal verification you're likely to be very meticulous in whatever you're writing, so an AI would be used quite carefully
stefan_ 2y ago
Have you tried it for Rust, arguably a much lower bar than actually fully formally verifiable? Sorry to say but AI can't figure out the borrow checker. I'd speculate it does poor on a lot of things that are sort of implicit in the code / properties of the grand structure rather than incremental text things.
- kevlar700 2y ago
  There is a podcast and blackhat? video about Nvidia choosing SPARK over Rust. Not because of formal verification at all but because it is a more developed prospect and offers better security even without any formal verification. This isn't mentioned but Ada is also far better at modelling registers or even network packets. I might consider AI if it utilised SPARKs gnat prove but I wouldn't usw AI otherwise.
  - LiamPowell 2y ago
    As an example of modelling packets, here's an example of modelling a complex packet which is a bit-packed tagged union. I don't think many other languages make such packets so easy to declare: https://gist.github.com/liampwll/abaaa1f84827a1d81bcdb2f5f1743406 https://gist.github.com/liampwll/abaaa1f84827a1d81bcdb2f5f17...
    - xxpor 2y ago
      p4? Granted, that's not something that just compiles to a usable language.
- TheOtherHobbes 2y ago
  AI means some future more rigorous system than today's Clippy++ LLMs. At least that's what it should mean. It's not clear if that's going to happen.
- steveklabnik 2y ago
  > Sorry to say but AI can't figure out the borrow checker. I'd speculate it does poor on a lot of things that are sort of implicit in the code / properties of the grand structure rather than incremental text things. I don’t really use AI tools, but in the past few weeks I’ve tried it with Rust and while it had problems, borrow checking errors were never part of them. I fully agree that LLMs don’t “understand,” but people also really oversell the amount of thinking needed to satisfy borrowing in a lot of cases.
dmix 2y ago
> as developers become incentivized to tab-complete code without fully thinking through the implications as they type. Is this true? There should always be a QA process and you should always carefully review when committing. The writing process doesn't influence that unless you're automating whole swaths you don't understand during reviews.
nostrademons 2y ago
I had a production bug (caught in canary) introduced into Google Play in just this manner. The AI code review assist suggested switching a method to a more modern alternative, both the author and code reviewer thought the AI suggestion was a good one, the new alternative was documented as not being safe to use in the onCreate() method of an Android activity, the code in question was not in onCreate but was in a method transitively called by onCreate in a different Activity, boom goes an unrelated Activity. Would've been caught trivially by an expressive type system, but the LLM doesn't know that.

by btown 2y ago

erichocean 2y ago

> But AI code generation for formally verifiable programs? For verifiable domains, this really is the sweet spot. An annoying aspect of verification-in-practice is that it is just really bulky—there's a lot to type in, and it's tedious. LLMs, especially the latest crop of weak-reasoning models, are great for this.

atiedebee 2y ago
I tested o3-mini yesterday, having it verify a bit-hack for "vectorizing" 8x8bit integer addition using a single 64 bit int value[0]. Suffice to say, I am not impressed. I asked it to give me a counter example that would make the function fail, or to tell me that it works if it does. It mentioned problems regarding endianness which weren't present, it mentioned carries that would spill over which couldn't happen. I had given it chances to give counter examples, but the counterexamples he gave didn't fail. Only after telling it that I tested the code and that it works did it somewhat accept that the solution worked. I think a deterministic, unambiguous process is a lot more valuable for formal verification. [0] https://chatgpt.com/share/67aefb63-f60c-8002-bfc6-c7c45b452018 https://chatgpt.com/share/67aefb63-f60c-8002-bfc6-c7c45b4520...
- hyperman1 2y ago
  A limitation I see with AI for coding is that your problem must be mainstream to get decent results. In my experience, if I ask it to do web things in PHP or Java, data things in Python, ... it gives a good enough result. If I ask it a postgis question, I get an answer with hallucinated APIs, bugs, and something that doesn't even do what I want if it works. I suspect the ADA/Spark world and the formal verification world are to small to decently train the AI.
  - amoss 2y ago
    > A limitation I see with AI for coding is that your problem must be mainstream to get decent results. Or to phrase it another way, there must examples of the technique that you want to "generate" in the training set otherwise the horrifically overfitted model cannot work. Probably a little bit too cynical but this is my experience asking LLMs "unusual" questions.
    - nottorp 2y ago
      Seems realistic. I tried asking a LLM for a full code snippet for the first time yesterday (i've been using them as search engines better than google, which isn't saying much, before). It produced code that compiled but failed to do anything because the 3rd api call it generated returned an error instead of doing what the LLM said it would do. Didn't spend time on seeing what was wrong because we already had a library that did the same thing; I was more testing what the LLM can do.
    - TheOtherHobbes 2y ago
      No, that's about where we are. Today's LLM coding is basically automated Stack Overflow copy/paste - not too bad for anything simple and mainstream, but unable to reason about code from first principles, and fond of making up random shit that looks good but doesn't work.
- brabel 2y ago
  I thought OP was saying AI can generate the code that can then be formally verified based on your non-verifiable code, not that the AI itself is verifying it? I could be wrong, of course.
  - atiedebee 2y ago
    Perhaps I misread it then. I think that if you're at the point of using formal verification you're likely to be very meticulous in whatever you're writing, so an AI would be used quite carefully

stefan_ 2y ago

Have you tried it for Rust, arguably a much lower bar than actually fully formally verifiable? Sorry to say but AI can't figure out the borrow checker. I'd speculate it does poor on a lot of things that are sort of implicit in the code / properties of the grand structure rather than incremental text things.

kevlar700 2y ago
There is a podcast and blackhat? video about Nvidia choosing SPARK over Rust. Not because of formal verification at all but because it is a more developed prospect and offers better security even without any formal verification. This isn't mentioned but Ada is also far better at modelling registers or even network packets. I might consider AI if it utilised SPARKs gnat prove but I wouldn't usw AI otherwise.
- LiamPowell 2y ago
  As an example of modelling packets, here's an example of modelling a complex packet which is a bit-packed tagged union. I don't think many other languages make such packets so easy to declare: https://gist.github.com/liampwll/abaaa1f84827a1d81bcdb2f5f1743406 https://gist.github.com/liampwll/abaaa1f84827a1d81bcdb2f5f17...
  - xxpor 2y ago
    p4? Granted, that's not something that just compiles to a usable language.
TheOtherHobbes 2y ago
AI means some future more rigorous system than today's Clippy++ LLMs. At least that's what it should mean. It's not clear if that's going to happen.
steveklabnik 2y ago
> Sorry to say but AI can't figure out the borrow checker. I'd speculate it does poor on a lot of things that are sort of implicit in the code / properties of the grand structure rather than incremental text things. I don’t really use AI tools, but in the past few weeks I’ve tried it with Rust and while it had problems, borrow checking errors were never part of them. I fully agree that LLMs don’t “understand,” but people also really oversell the amount of thinking needed to satisfy borrowing in a lot of cases.

dmix 2y ago

> as developers become incentivized to tab-complete code without fully thinking through the implications as they type. Is this true? There should always be a QA process and you should always carefully review when committing. The writing process doesn't influence that unless you're automating whole swaths you don't understand during reviews.

nostrademons 2y ago

I had a production bug (caught in canary) introduced into Google Play in just this manner. The AI code review assist suggested switching a method to a more modern alternative, both the author and code reviewer thought the AI suggestion was a good one, the new alternative was documented as not being safe to use in the onCreate() method of an Android activity, the code in question was not in onCreate but was in a method transitively called by onCreate in a different Activity, boom goes an unrelated Activity. Would've been caught trivially by an expressive type system, but the LLM doesn't know that.