Comment by addaon | Hacker News Reader

Comment by addaon | Hacker News Reader

I've been playing with related ideas recently, and can talk about them at length... but one thing that's surprised me is just how effective frontier models (ChatGPT-5.5 in particular) are at completing certain manual proofs in the Roqc (né Coq) proof assistant. The proofs aren't always pretty, but ChatGPT can often prove something in minutes and 10 - 100 iterations that would take me, a human who has limited but non-zero proof assistant experience but significant domain experience in the lemmas being proven, much much longer.

The reason I think this is relevant and interesting in the context of the (short) article is because it challenges basic assumptions about how certain formal method tooling works. Frama-C, Ada/SPARK, etc are focused on generating proof obligations that can be automatically discharged by CVC5, Z3, etc; with a relatively painful fallback of manually proving the obligation in Rocq. The most common workflow seems to be to discover that an obligation is "hard" (not automatically discharged), and to restructure the set of visible lemmas and assertions at the obligation generation point in the code to try to make it "easy"; or even restructuring the code to try to make it easy. Which, in a world where Roqc proofs are doubly expensive (first because they're a challenge for a human to write; second because they tend to require quite a bit of maintenance churn as the code and proof around them evolves), makes sense. But if Roqc proofs are "automatically discharged with AI in the loop", this cost delta goes away -- and it becomes possible to think about writing proofs the same we (usually) write code, with human readability and clarity as the first goal, and [compiler|prover] optimization a distant second.

Which I find quite exciting, although I haven't fully digested the implications yet.

How often will AI look at something that can't be proven because you change requirements and decide to change the code and your requirements to make the proof easier though? I haven't played with proofs at all, but I do know that occasionally when I say, this test failed after making a change, AI will just change the test instead of making the code pass both the old test and the new test which is most often my intent.

That's up to the harness. Right now, my harness doesn't have any tools that would allow the agent to change contracts. Also, agents working on a Rocq proof don't have write access to the C+ACSL code; they can review it, and propose structural changes to the coordinator, but all they can do is iterate on the Roqc proof or give up. The weakest part of the harness today is that the agents that do C+ACSL work can modify both C and ACSL, even though they're usually run with the explicit intent to not change the semantics of the C code (although it's totally within bounds, and often required, for them to change e.g. `foo & 3` to `foo % 4`) -- so there's weakness here, but it's bounded, and since the contracts live in header files that they can never write, it's worked so far. It's a starting point, at least; I certainly wouldn't say this is a mature, or even good, tool chain, but still learning.

This mirrors my own experience, except I went with Lean. It was more relevant to the features I wanted to build.

Exciting times ahead.

> how effective frontier models (ChatGPT-5.5 in particular) are at completing certain manual proofs in the Roqc (né Coq) proof assistant. The proofs aren't always pretty, but ChatGPT can often prove something in minutes and 10 - 100 iterations that would take me, a human who has limited but non-zero proof assistant experience but significant domain experience in the lemmas being proven, much much longer.

... How do you know that the proofs are themselves correct?

With the proof checker.

I assume your idea is, if the spec and the proof is verified the code generated is good enough as well ?

Today, I write the code. It’s trivial and takes a lot less time than writing the spec, and since I’m using conventional tooling for WCET and stack sizing it’s nice to get those right up front. The LLMs sometimes tweak the code slightly for provability, but this is usually either direct operator replacement (shift with multiplication, and with modulus, etc) or factoring out a block to a function to tie a contract onto it, both of which I trust my compiler to undo (simple arithmetic operations and inlining, respectively) with zero to minimal impact on the generated binary.

Proof checkers fuel the AI hype by outputting "valid" for a hallucinated text. /s

Reply on news.ycombinator.com