Théo Zimmermann (Aug 08 2020 at 10:30): Théo Zimmermann (Aug 08 2020 at 10:30):@Lasse recently presented his work on Tactician at CICM 2020, which triggered questions from @brando90 (Gitter import) in the CICM 2020 Slack and now on Discourse. Looking at these discussions and also the comparisons with all the other ML works like CoqGym and the other related works on hammers (CoqHammer), I was thinking that it might make sense to start a Zulip stream on these topics (tentatively titled "AI and hammers devs & users") so that the informal discussion can continue. What do you think @Lasse (and also @Emilio Jesús Gallego Arias, @Karl Palmskog, @Łukasz Czajka...)?
Karl Palmskog (Aug 08 2020 at 10:32):I agree something like this would be useful. But I personally don't like the "AI" label (it's short, but "machine learning" is better)
Bas Spitters (Aug 08 2020 at 10:36):ML ?
Karl Palmskog (Aug 08 2020 at 11:00):maybe: "machine learning and (proof) automation". ML bound to be confused with OCaml/SML
Bas Spitters (Aug 08 2020 at 15:06):I was joking :-)
Pierre-Marie Pédrot (Aug 08 2020 at 15:17):We should set up an elaborate scam to convince venture capitalists that "ML" meant meta-language all along, and extract as much money as possible from it for PLT research...
Lasse Blaauwbroek (Aug 08 2020 at 16:22):Sounds good! I also prefer the term machine learning over AI :-) Regarding my tool: Tactician is not quite ready for mass adoption by end-users yet (I've not made a 1.0 release and it's not yet in the opam repo). That being said, if there are people who would like to give some feedback, that would be appreciated. That mainly regards the user experience, such as installation and learning from libraries (standard libraries and others). Regarding its strength: My guess is that the current learner is not yet good enough to be massively useful. I'm currently working on improvements, which I expect will land in a couple of weeks. Installation instructions can be found at coq-tactician.github.io
Notification Bot (Aug 09 2020 at 06:16):This topic was moved by Théo Zimmermann to #Machine learning and automation > Comparative evaluation
Last updated: Jun 01 2023 at 13:01 UTC