Comment by tlringer | Hacker News Reader

Comment by tlringer | Hacker News Reader

Parent Full thread

There has been a lot of work like this popping up in the past year. I think it's somewhat promising, but for ML for ITPs to really become useful, I think the models need to better take into account semantic information about terms and types and not just tactics. And this is not easy, because Coq's logic is higher-order and dependently typed, and most work in ML for PL deals with much simpler logics. Still, anything that helps with the tedium is welcome.

Another problem is that you will very rarely find examples of failing proofs, since users rarely commit them. I'm working on a joint UW-UCSD project on collecting and analyzing development data, and this is one of the goals. But our dataset is not very large, since it is hard to get users to agree to something so invasive, and there are still only 1000 or so active Coq users in total in the world right now.

Another big problem is that it is very, very difficult to define what it means for a proof to be "almost" correct. This makes it difficult to apply many existing techniques fruitfully.

Nonetheless, I think the general spirit is right. The biggest gains in proof automation in ITPs this decade are going to come from automation that makes use in some way of existing proofs, rather than starting from scratch and "blindly" (often very effectively or even decideably for certain fragments of the logic or certain domains if the user knows the right tactic to call) searching for some term with a given type.

As an example of using semantic information, you might define a bunch of functions that take two natural numbers and return some result. Then you might write some proofs about those functions.

Let's say you write those proofs via induction over the natural numbers. You can choose between arguments to induct over if your functions take multiple inputs. The most effective choice often depends on the definitions of your functions. This means to pick the best argument, already you need to unfold your definition. Chances are you do that unfolding in your head, not using a tactic, or at least not one that you keep in your final proof.

So already, an ML technique for ITPs that does not unfold definitions in goals for more information is missing out on the essential piece that makes a user choose one argument for induction over another, even when syntactically the hypotheses and goals may look identical (I can define "add" to break down the first argument or the second argument, my call).

In general, I think the ITP community likes to pretend that we are using tactics to interact with a black box, but in practice, most of us have internalized heuristics that involve introspecting on the structures of terms and types. So any model that lacks the information to internalize those heuristics is missing out.

Have you thought an interactive site where people could learn coq writing proofs? Something very similar to https://projecteuler.net/. You could get thousands of failed proofs very fast.

That's a neat idea. It would mostly help for gathering data from beginners, which would be very skewed, but I'm sure it could still be useful, especially for developing tools to help beginners.

Yeah skewing would be definitely problematic, it might be better if it would be similar to Kaggle where people would compete with each other.

This is a great idea. As I interested novice I'd certainly be a early adopter.

Idea for getting "almost correct" proofs: Take a big Coq project like CompCert or whatever. Search the version control history for commits with small changes to definitions. These very likely come with corresponding changes to proofs as well. Now apply only the code changes but not the proof changes: You get a state with "almost correct" proofs and as a bonus known "ground truth" proofs as well.

This is a really interesting idea. In some sense, you can say a proof script is "almost correct" if it proves a slightly different theorem.

I suspect the one difficulty there would be finding such incremental changes on Github. It was surprisingly difficult to find small changes to specifications in Git history for a different project that I did. Too many large commits and too much history revision, so you often lose the incremental changes. Still, it is worth trying.

Good point about the difficulty of finding incremental changes. Maybe it's better the other way round: Pick an arbitrary commit and only roll back the changes it introduces to one proof. This would model the situation where a programmer has just changed the code and is now setting out to adjust the proof.

Reply on news.ycombinator.com