alt Hacker NewsI'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"?).
Replies
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...
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.