Wouldn't it be more productive spending the tokens on adding ACSL annotations to verify CPython with Frama-C? You'd verify the actual runtime instead of an AI translation of it, and fixes could be contributed upstream directly.
One advantage of this approach is that it can be done both on the C implementation code and the Python standard library. It's a bit approximate -- automatic retrofitting of formal specification maybe it helps to think of it as a stepping stone for simple automated testing and property based testing.
I think this approach to bug hunting is super promising (obviously - it finds a ton of bugs). The long-term problem is how this kind of bug-hunting can be done routinely, e.g. as part of a test suite. The approach taken by these people, the same approach as when the Julia folks did it, isn't really automatable, because it requires a lot of both human and AI agent work.
I guess longer term it needs to be built into the language, to prevent code and lean proofs from drifting. I.e. it could be opt-in properties that are written along the code, and which is then checked in the test suite. So very similar to ordinary compiler checks, except more expressive and expensive, and done only at test time.
You can writer solvers for bits of code and make them part of your test runs, I do that for gnarly bits, especially gnarly bits written by AI where the drift would not be obvious to me.
I often “oh, this is going to be an interesting article written by someone about how they use an LLM to do X” and then start and discover that the person wrote the article via prompting. I guess if you think LLMs are amazing and that you’ve gotten into a rhythm of offloading all the labour to them, you see writing your own posts as a waste of time. I just wish those posts came with disclaimers telling the reader that reading it is a waste of time too and the reader should just point an agent at it or whatever.
That reminds me of what you see in some Issues on AI-related GitHub repos. A 'conversation' where people are just pasting big walls of text with way too much formatting back and forth to each other.
The way I understand it, the two implementations can only differ in the result if the lean translation was done incorrectly; that's the point, you don't want to use those to prove invariants in the next step.
For the next step, I have the same question. It's the crux of the approach and the article is surprisingly light on detail:
> The hardest part wasn't getting AI agents to write proofs. It was getting proofs that actually mean something
So it was done by AI but they don't make entirely clear how the interesting proof statements were chosen.
They describe it later. Essentially, they are asking the AI for each function to give them a property that basically means "this function is correct", and then they let it prove that property.
yes, one can say it is "guessing" but taking in these into account:
> Source, in order of preference: (a) the implementation disagreeing with itself (C vs Python twin, fast vs slow path, method vs equivalent method, round-trips, str vs bytes); (b) undisputed invariants (no crash, no internal error leaking, results in range, no hang); (c) explicit doc sentences read in context.[...]
I am not a lean expert, but I imagine that python primitives like dicts, ints, functions, etc., have been defined in lean. So if you add a way to annotate python code with a proof, you should as well be able to automatically translate it to Lean completely.
it's a matter of how much of a modeling gap do you choose to accept.
for full, honest to god, end to end verification this would be insufficient. but you don't need that in order to reap benefits.
just gotta make sure you actually bound the triage process with some sort of automated verification process. like comparative test cases or similar. otherwise it's just a particularly expensive way of agentic hallucination.
Because in order for the proof to succeed, Lean needs "strange" assumptions about the code. This rare assumptions are the conditions to trigger the bug.
Imagine a proof that needs the axiom that all numbers are below 2^32. What happens if my system is expected to handle numbers greater than 2^32?? There you have the bug... Also it could mean that the system is not validating the boundness of the input, and 2^32 is the maximum that allows for coherent execution downstream of the execution. In both cases, it needs to be checked :)
Wouldn't it be more productive spending the tokens on adding ACSL annotations to verify CPython with Frama-C? You'd verify the actual runtime instead of an AI translation of it, and fixes could be contributed upstream directly.
One advantage of this approach is that it can be done both on the C implementation code and the Python standard library. It's a bit approximate -- automatic retrofitting of formal specification maybe it helps to think of it as a stepping stone for simple automated testing and property based testing.
Same approach for Julias stdlib: https://discourse.julialang.org/t/formalizing-julia-in-lean-...
Interesting also the prompt of the python formalization (and the blog post) mentions the julia-in-lean:
https://github.com/Broyojo/python-formalization/blob/main/AG...
I think this approach to bug hunting is super promising (obviously - it finds a ton of bugs). The long-term problem is how this kind of bug-hunting can be done routinely, e.g. as part of a test suite. The approach taken by these people, the same approach as when the Julia folks did it, isn't really automatable, because it requires a lot of both human and AI agent work.
I guess longer term it needs to be built into the language, to prevent code and lean proofs from drifting. I.e. it could be opt-in properties that are written along the code, and which is then checked in the test suite. So very similar to ordinary compiler checks, except more expressive and expensive, and done only at test time.
At that point you might as well use Lean?
It would solve the two language problem :-)
yep
You can writer solvers for bits of code and make them part of your test runs, I do that for gnarly bits, especially gnarly bits written by AI where the drift would not be obvious to me.
bend programming language already solved this problem: https://bend-lang.com/
Interesting. Now I have an idea to extend my tooling flow, thanks.
Does anyone read articles written by AI? This is a serious question.
Does anyone use code written by AI? Just as serious question.
Because I honestly can't understand how we celebrate being pushed into not writing code, but get grumpy about everything else.
Next generation AI when they eventually get in the corps?
I often “oh, this is going to be an interesting article written by someone about how they use an LLM to do X” and then start and discover that the person wrote the article via prompting. I guess if you think LLMs are amazing and that you’ve gotten into a rhythm of offloading all the labour to them, you see writing your own posts as a waste of time. I just wish those posts came with disclaimers telling the reader that reading it is a waste of time too and the reader should just point an agent at it or whatever.
I start from the assumption that anything written coming from AI enthusiasts is also written by AI and skip it by default.
That reminds me of what you see in some Issues on AI-related GitHub repos. A 'conversation' where people are just pasting big walls of text with way too much formatting back and forth to each other.
I think AI output is like your own farts. We all smell our own but others don't want to be subject to it.
I'm confused about a few points, would love it if someone could help clear it up!
- if the rewrite in Lean happens line-by-line, how can the two implementations differ in their result (Step 2)?
- how does this approach know "something that should always be true" in Step 3 (is it the intelligence of the LLM "guessing"?).
The way I understand it, the two implementations can only differ in the result if the lean translation was done incorrectly; that's the point, you don't want to use those to prove invariants in the next step.
For the next step, I have the same question. It's the crux of the approach and the article is surprisingly light on detail:
> The hardest part wasn't getting AI agents to write proofs. It was getting proofs that actually mean something
So it was done by AI but they don't make entirely clear how the interesting proof statements were chosen.
They describe it later. Essentially, they are asking the AI for each function to give them a property that basically means "this function is correct", and then they let it prove that property.
yes, one can say it is "guessing" but taking in these into account:
> Source, in order of preference: (a) the implementation disagreeing with itself (C vs Python twin, fast vs slow path, method vs equivalent method, round-trips, str vs bytes); (b) undisputed invariants (no crash, no internal error leaking, results in range, no hang); (c) explicit doc sentences read in context.[...]
https://github.com/Broyojo/python-formalization/blob/main/AG...
Only 418?
I would have expected around 10k.
Edit: Professional python programmer.
they don't have full coverage yet
Is there a way to avoid the translation or replace it with normal parsing?
In principle, yes.
I am not a lean expert, but I imagine that python primitives like dicts, ints, functions, etc., have been defined in lean. So if you add a way to annotate python code with a proof, you should as well be able to automatically translate it to Lean completely.
it's a matter of how much of a modeling gap do you choose to accept.
for full, honest to god, end to end verification this would be insufficient. but you don't need that in order to reap benefits.
just gotta make sure you actually bound the triage process with some sort of automated verification process. like comparative test cases or similar. otherwise it's just a particularly expensive way of agentic hallucination.
Stupid question: if the lean4 code is a copy of the C code, how does "it" know which code is a bug and which code is working as intended?
Because in order for the proof to succeed, Lean needs "strange" assumptions about the code. This rare assumptions are the conditions to trigger the bug.
Imagine a proof that needs the axiom that all numbers are below 2^32. What happens if my system is expected to handle numbers greater than 2^32?? There you have the bug... Also it could mean that the system is not validating the boundness of the input, and 2^32 is the maximum that allows for coherent execution downstream of the execution. In both cases, it needs to be checked :)
Can we just develop in Lean and compile to something else for speed?
Lean is actually pretty speedy as is, and it enables much harder optimizations[1]
[1] https://github.com/kim-em/lean-zip#verification-enables-perf...
Of course.
Cite an AI-written document? Hell no.