*To*: Dominique Unruh <unruh at ut.ee>*Subject*: Re: [isabelle] Proving Contests*From*: Simon Wimmer <wimmersimon at gmail.com>*Date*: Wed, 7 Nov 2018 10:41:40 +0100*Cc*: gidon.ernst at unimelb.edu.au, José Manuel Rodriguez Caballero <josephcmac at gmail.com>, cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <CAPFfTE4EjW8YW61EpBfp3mM=H6ZoYVuiMs0w6PiDoToPz=idFA@mail.gmail.com>*References*: <CANQq8HWwTaAOppm7rKGbDJVuu-mzP15RCkKHxDsPZwydL7Uy=A@mail.gmail.com> <CAA8xVUhm=WwPsCEfwgrzGwdxcoN7hhV2metf0mYK+c2yDGdMYQ@mail.gmail.com> <SYBPR01MB3579A5983FFE6323448E7ED4D5C40@SYBPR01MB3579.ausprd01.prod.outlook.com> <CAA8xVUhE24imYTNni3QfFhmNWY-onmoR6kHcLjGipfF6D1L4bw@mail.gmail.com> <SYBPR01MB3579AE64CDD65C94F6346710D5C40@SYBPR01MB3579.ausprd01.prod.outlook.com> <CAPFfTE4EjW8YW61EpBfp3mM=H6ZoYVuiMs0w6PiDoToPz=idFA@mail.gmail.com>

Dear all, currently we use the following scheme. Each sub-task is worth a certain number of points. We first rank by highest total score, and then lowest sum of submission time stamps to break the ties. Simon On Wed, Nov 7, 2018, 10:24 AM Dominique Unruh <unruh at ut.ee> wrote: > Instead of judging by proof by runtime (which does not seem like a very > useful criterion) or by beauty (which needs big human effort), an option > would be percentage of completion. By giving out several problems of > differing hardness one could make sure that basically no-one will get 100% > of the solutions. (And even for a given problem one might have different > options. E.g., prove this for integers vs. for any ring. Or prove this with > the following additional simplifying assumption vs. prove it without > assumption, etc.) > > Then checking can be automated. (And to look for cheaters, it will not be > enough to manually scan the source for for "sorry". Instead, the only > reliable way as far as I know is to extract the proof term and replay it in > a separate instance of Isabelle. But the infrastructure for that is mostly > there, so it's mainly a question of filling in some "plumbing".) > > Best wishes, > Dominique. > > > > > > On Wed, 7 Nov 2018 at 10:14, Gidon Ernst <gidon.ernst at unimelb.edu.au> > wrote: > > > Hi José, > > > > indeed, judging the solutions in those competitions was always a > > tremendous effort. > > The reason why at these events humans had to be involved in the judging > > was the diversity of tools and the fact that specifications were given in > > natural language. > > > > Your idea is quite different and very intriguing! I hope it will be > > realized eventually :) > > > > Best, > > Gidon > > > > ________________________________________ > > From: cl-isabelle-users-bounces at lists.cam.ac.uk < > > cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of José Manuel > > Rodriguez Caballero <josephcmac at gmail.com> > > Sent: Wednesday, November 7, 2018 4:54:25 PM > > To: cl-isabelle-users at lists.cam.ac.uk > > Subject: Re: [isabelle] Proving Contests > > > > Hi Gidon, > > > > Interesting Proving Contests in your links, thank you ! Nevertheless, I > > took a look at the Geographical distribution of the participants (page 3 > in > > the following link): > > > > > http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.362.2877&rep=rep1&type=pdf > > > > I think that it is important to open a competition for millions of > > participants at the same time, including participants from less > > economically developed countries. This is the reason why I suggested a > > software in order to do the ordering of the solutions in virtue of the > > running time: human cannot handle such a huge data. > > > > In the same way that alphabetization was extended from an elite to the > > whole world, proof assistants are a second alphabetization that the world > > need in order to get update: https://www.youtube.com/watch?v=7Pq-S557XQU > > > > Kind Regards, > > José Manuel Rodriguez Caballero > > > > > > El mar., 6 nov. 2018 a las 21:26, Gidon Ernst (< > gidon.ernst at unimelb.edu.au > > >) > > escribió: > > > > > Hi all, > > > two similar competitions come to mind: > > > > > > 1st and 2nd VSComp, see > > > The 1st verified software competition: Experience report, FM2011 > > > The 2nd verified software competition: Experience report, COMPARE 2012 > > > > > > VerifyThis (yearly at ETAPS) > > > http://www.pm.inf.ethz.ch/research/verifythis.html > > > This year, the Isabelle Team from TUM took the gold medal :) > > > Huisman, Klebanov, Monahan: On the organisation of program verification > > > competitions, COMPARE 2012 > > > the yearly competition reports, and the STTT 17(6) special issue: > > > https://link.springer.com/journal/10009/17/6/page/1 > > > > > > Hope you find this information useful :) > > > > > > Best, > > > Gidon > > > > > > ________________________________________ > > > From: cl-isabelle-users-bounces at lists.cam.ac.uk < > > > cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of José Manuel > > > Rodriguez Caballero <josephcmac at gmail.com> > > > Sent: Wednesday, November 7, 2018 10:59:06 AM > > > To: cl-isabelle-users at lists.cam.ac.uk > > > Subject: [isabelle] Proving Contests > > > > > > > > > > > max wrote: > > > > Just now we anounced the contest system, > > > > which we are using for managing homework submissions for > > > > the current Semantics course here at TUM, as well as providing > > > > a (short) tutorial to Isabelle and the system. > > > > Also, we host monthly contests with relatively easy but hopefully > > > > fun problems. I'm already looking for problems for the month of > > > > December. I think the goal should be that experienced Isabelle > > > > users can solve them within 30 minutes. > > > > > > > > > Nice project. My idea of an International Olympiad in Isabelle are a > > little > > > bit different. Indeed, I can summarize my vision as follows: > > > > > > 1) There will be some publicity about the International Olympiad some > > > months before its date. The publicity should be mainly addressed to > > > undergraduate and high school students. People interested in the > Olympiad > > > should summit their email addresses in a website. People working with > > > Isabelle in an official research project, e.g., a Master, a PhD, a > > > professor or a professional programmer, are not allowed to apply in > order > > > to guarantee more space for beginners. > > > > > > 2) The day of the Olympiad, a thy-file with a theorem followed by sorry > > > will be sent to each one of the email addresses. > > > > > > 3) People can submit their solutions until 6 hours after their received > > the > > > email with the problem (5 hours to solve the problem and 1 hour to > make > > a > > > break, I guess). Solutions sent after the deadline will be > automatically > > > ignored. > > > > > > 4) An automatic system (software) will discriminate the invalid > > solutions, > > > e.g., using sorry somewhere, from the valid solutions. After that, it > > will > > > make an ordering according to the running time of each valid solution. > > > > > > 5) Finally, an email with the ranking of his/her solution will be > > > automatically sent to each participant. The participants having ranking > > 1, > > > 2, 3 will receive a prize. > > > > > > When I think about such an international project, I am mainly concerned > > > with people living in economically less developed countries. The idea > is > > > that a person from such countries, having the dream of winning an > > > International Olympiad in Isabelle will have a motivation to improve > > > himself/herself in this field. Of course, classification by countries > > > should be avoided and people from highly developed countries should be > > > allowed to participate as well. > > > > > > This is just a dream, I have not enough free time to do something about > > it. > > > My inspiration are the IOI: https://ioinformatics.org/ > > > > > > Kind Regards, > > > José M. > > > > > > > > > > > > >

**Follow-Ups**:**Re: [isabelle] Proving Contests***From:*José Manuel Rodriguez Caballero

**References**:**[isabelle] Proving Contests***From:*José Manuel Rodriguez Caballero

**Re: [isabelle] Proving Contests***From:*Gidon Ernst

**Re: [isabelle] Proving Contests***From:*José Manuel Rodriguez Caballero

**Re: [isabelle] Proving Contests***From:*Gidon Ernst

**Re: [isabelle] Proving Contests***From:*Dominique Unruh

- Previous by Date: Re: [isabelle] Proving Contests
- Next by Date: Re: [isabelle] Proving Contests
- Previous by Thread: Re: [isabelle] Proving Contests
- Next by Thread: Re: [isabelle] Proving Contests
- Cl-isabelle-users November 2018 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list