BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Tactic Prediction for Theorem Proving with Proof Context
DTSTART:20190516T114500
DTEND:20190516T124500
DTSTAMP:20260407T025910Z
UID:c6b108ca91ffc184a3f67b53bb8d26d6dfd86dc85624ee0f931b1eb8
CATEGORIES:Conferences - Seminars
DESCRIPTION:By Viktor Toman\n\nAbstract\nIn this project we consider machi
 ne learning applications in higher-order theorem proving. Given a proof st
 ate\, the crucial task in theorem proving is to select a beneficial tactic
  and optionally to parameterize the tactic by premises. We consider learni
 ng policies for this task from data in the environment of an interactive h
 igher-order theorem prover HOL Light. Given logs of successful HOL Light p
 roofs guided by mathematicians\, we learn in a supervised manner policies 
 that operate on the level of individual proof steps. Given a proof step\, 
 a policy predicts the tactic that was applied and computes relevance score
 s for premises possibly used as tactic parameters. The crucial objective o
 f the project is to explore possibilities of improving the prediction by p
 roviding more context of proof steps as input. The context can include the
  original conjecture of the proof\, the current list of assumptions\, the 
 history of goals in previous proof steps\, and the history of tactic appli
 cations. The internship project aligns well with the objective of our rese
 arch group to build an interface that automates the theorem-proving proces
 s in HOL Light. Given a statement to be proven\, the interface will repeat
 edly call a fixed policy to select a parameterized tactic for the current 
 proof state. Accurate prediction policies make the interface more powerful
 \, as they increase the chances of successfully proving statements and thu
 s obtaining more proof data.\n\nBio\nViktor Toman is a computer science Ph
 D student at the Institute of Science and Technology (IST) Austria. After 
 obtaining his Bachelor's and Master's degree at Masaryk University Brno\, 
 Czech Republic\, he has joined the research group of Krishnendu Chatterjee
  at IST Austria to pursue a PhD in formal methods. His research interests 
 include model checking\, program verification\, and machine learning in fo
 rmal methods.\n\nMore information
LOCATION:INR 331 https://plan.epfl.ch/?room=INR331
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR