3 ms·

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 i

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

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