Hacker News Reader

Comment by foota | Hacker News Reader

In theory, an AI that wrote proofs for their code (ala coq) could be used to validate preconditions specified by the developer, right?

View on HN

I don't know to what extent you can self-verify your own system based on proof code you also write yourself. However I do know this topic of merging AI, Deep Learning, and proof assistants is an up and coming research area. I mainly follow publications from Talia Ringer [1] and collaborators on this topic.

[1] https://dependenttyp.es/

Maybe I misunderstand, but my understanding is that (at least some languages) can be given proofs of correctness for some pre and post conditions. See e.g., https://arxiv.org/pdf/2303.05491.pdf

Conceptually, you tell the computer how to validate that the conditions you state are correct with your proof, and it checks that each step follows.

To me, it seems like there will be a finite set of pre and post conditions ever needed for 99% of future programming, and eventually everything will be a catalog of the conditions to working code.

One just needs a language to write those conditions in.

I'm not sure how to phrase this, but it seems like there's some trade off between how easy it is to express a condition, and how easy it is to verify that it holds in an imperative language.

One the one hand you have declarative languages, and on the other imperative languages.

Not sure where I'm going with this, but I think there's something there.

Reflexion can serve as good reference here:

https://arxiv.org/abs/2303.11366

Essentially, AI’s output is fed into a checker, whose output is fed back into the AI for “reflexion”. Then the AI often corrects (leading to noticeable improvement in GPT-4 perf).

Reply on news.ycombinator.com