Trimmed abstract: “ Evolutionary algorithms, known to be flexible and versatile, have been successfully applied to handle a variety of scientific and engineering problems in numerous disciplines for also several decades… In the article, we describe in detail our first, ad-hoc attempt to [use them to] fully automatically prove theorems as well as the preliminary results. Ten simple theorems from various branches of mathematics were proven, and most of these theorems cannot be proven by using the tactic auto alone in Coq, the adopted proof assistant. The implication and potential influence of this study are discussed, and the developed source code with the obtained experimental results are released as open source.”
Note: when linking to an arXiv article, I think that it is better to link to the online abstract (the
/abs/url, in the present case https://arxiv.org/abs/1602.07455) rather than the PDF: the PDF is just one click away, the abstract gives the abstract (instead of you having to repeat it), the author and the year.The evaluation in this article is extremely weak: it claims to do better than the
autotactic of Coq, but people with Coq experience know thatautois an extremely limited form of automation (it does the “obvious” things only, unless you enlarge it with large collections of hints). Generic automation tactics have been written (by hand) for Coq, such as thecrushtactic, that would be a much better base to compare against. Evaluating an automated prover by comparing withautodoes not give any useful information.I think that simple evolutionary approaches like the one presented here have been tried many time (it’s basically a master internship topic that any research would have in mind, and it has certainly tried countless time since the eighties), and it doesn’t really work. Much more powerful approaches are available today, for example using a translation into first-order goals that SMT solvers can check (CVC4 or Z3 would eat the examples in this paper alive). There is a growing litterature on “Hammers” for proof assistants, that delegate the hard proving work to automated theorem provers; Isabelle has the very nice sledgehammer tool, and there is recent work in the Coq space, CoqHammer. It’s not quite as good as Isabelle’s sledgehammer yet (or automated provers for other assistants), but it’s already much stronger than the tool described in its article, and potential descendants of it using genetic search only.
re Coq evolutionary algorithms
Well, that’s what I thought far as someone had to have tried it. The GA’s/EA’s are one of those general-purpose methods so effective at so many things that I’d have tried it on about every angle of theorem proving if I had a chance and was in that field. They don’t always do that, though. Thanks for chiming in about that weakness in the paper and those alternatives.
re arXiv
What I did is specific to this site. I normally include the title, name(s), and year. IIRC I was asked not to put names on some time ago by an admin. Got a damaged memory so that may or may not have been here. It does clutter the front page with long titles, though, with info that’s usually first thing you see in CompSci papers. I was definitely asked by pushcx not to put year on it when it’s current but otherwise OK. And in metas most Lobsters liked that some of us put abstracts, Github, etc in text field to help them avoid wasted time. With all that, I just submit the article, its year, and a trimmed abstract. If they need the citation, they can always Google it. They should anyway as part of due diligence in case there’s more recent work or my citation was wrong. Academics here have caught me screwing up on dates or other stuff on occasion.
re. arXiv, my point was that you could have submitted the URL https://arxiv.org/abs/1602.07455 instead of https://arxiv.org/pdf/1602.07455, and that I think in general it’s good hygiene for articles in an open-access archive. (I agree with your preference on citing authors and publication year when you cite a work, and I apply them in in-text citations, although I understand that lobster has a policy on titles that suggests only including the title. If you link to the arxiv web abstract instead of the pdf documentations, the terse title is never an issue as the metadata is all available on the landing page.)
For arXiv, I’ve mainly just been trying to save people a click taking them right to the PDF. I might experiment with doing it that way, though.