[Club2] Talk by Daniel Kühlwein: Wednesday, August 21, 14:00, Room Turing (00.09.38)

[Andrei Popescu]

Dear All,  

Tomorrow, at our usual Club2 time, Daniel Kühlwein will talk about his joint 
work with Jasmin and others on the higher education of Sledgehammer.   
Details and clarifications below.

Cheers, 
   Andrei   

Verbatim note from Jasmin: 

Daniel is going to hold his ITP 2013 talk for our benefit. Those who have
already seen the talk in Rennes are of course welcome to join again but will not
be missed. ;)

Daniel Kühlwein -- MaSh: Machine Learning for Sledgehammer
(joint work with Jasmin Christian Blanchette, Cezary Kaliszyk and Josef Urban)
==============================================================================
Wednesday, August 21, 14:00, Room Turing (00.09.38)

Sledgehammer integrates automatic theorem provers in the proof assistant
Isabelle/HOL. A key component, the relevance filter, heuristically ranks the
thousands of facts available and selects a subset, based on syntactic similarity
to the current goal. We introduce MaSh, an alternative that learns from
successful proofs. New challenges arose from our "zero-click" vision: MaSh
should integrate seamlessly with the users' workflow, so that they benefit from
machine learning without having to install software, set up servers, or guide
the learning. The underlying machinery draws on recent research in the context
of Mizar and HOL Light, with a number of enhancements. MaSh outperforms the old
relevance filter on large formalizations, and a particularly strong filter is
obtained by combining the two filters.

Bio:
Daniel studied mathematics in Tuebingen, Birmingham and Bonn. He did his Diplom
on the Naproche project, a natural language proof checker. For his PhD, he's
developing machine learning algorithms and tools for formal methods. Josef Urban
and Daniel created MaLeS, a learning based automatic tuning framework for
automated theorem provers. Together with Jasmin Blanchette, Cezary Kaliszyk and
Josef Urban, he is currently working on integrating learning into Isabelle.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20130820/093073a4/attachment.html>