Re: [isabelle] Proving Contests



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.
> > >
> > >
> >
> >
> >
>



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.