The Joint EuroProofNet Workshops on Practical Aspects of Machine Learning in Theorem Proving (PAMLTP) and Datasets Generation for Data-Deficient Domains (DG4D^3)
will take place at the Czech Institute of Informatics, Robotics and Cybernetics (CIIRC CTU), Prague, Czech Republic on April 18-19 (PAMLTP) and April 19-20 (DG4D^3) organized by Martin Suda (CTU) and David Cerna (CAS ICS), respectively.
The events are supported by the Cost Action CA20111 - European Research Network on Formal Proofs and will be co-located with a meeting of WG5 of the action, on Machine Learning in Proofs running through April 18-20.
** Directions From CIIRC To Room Below** More Pictures after Directions
Aims:
Practical Aspects of Machine Learning in Theorem Proving: Efficient implementation is the key to practical deployment of ML-based techniques, especially in highly tuned systems like theorem provers, yet practical aspects are only rarely discussed. The workshop will provide an opportunity for practitioners in the area to share experiences with libraries, support tools, implementation tricks and discovered solutions.
We assume theorem proving to cover logics ranging from SAT and SMT, to first-order or even higher-order, including temporal, modal, or non-classical flavors, relying on saturation, the tableau methods, or tactical search in the ITP context among others, and with the ML part including supervised as well as reinforcement learning, not limited to deep learning.
Datasets Generation for Data-Deficient Domains: Investigations exploiting statistical guidance to advance SOTA performance in domains typically approached using purely symbolic methods are more prevalent than ever. Consider the recent advancements in clause selection for Automated Theorem Proving. Impressive as these results are, they strongly depend on the existence of a large corpus of theorem-proving tasks built by the community over the last few decades. Domains without this unified community effort cannot directly exploit current advancement without first developing datasets for the task. For example, guiding modern inductive synthesis systems. The workshop will provide an opportunity for researchers who developed, are currently developing, or planning to develop training data for a particular problem to present their work and discuss approaches, methodologies, and pitfalls.
Format:
Both workshops solicit contributed talks backed up by an extended abstract of up to 1 page (excluding references) in the Easychair format. The abstracts will be reviewed for relevance and quality and made public on the workshops’ web page. (The abstracts are considered non-archival.) Participants with accepted abstracts will be given preference when applying for reimbursement (see below). The workshop deadlines are as follows:
Abstract submission: March 10 AoE
Travel support application: March 10 AoE
Notification of acceptance: March 17
Please submit your abstract via email to the organizers:
PAMLTP: Martin Suda (martin.suda@cvut.cz)
DG4D^3: David Cerna (dcerna@cs.cas.cz)
Optional Travel Support:
The travel and accommodation of a number of participants (approximately 15) will be supported by the Cost Action CA20111 - European Research Network on Formal Proofs. If you want to be funded, please check the eligibility and reimbursement rules to know whether you can be funded. Register to EuroProofNet if not already done. Fill in the following form. Notifications will be sent on March 17.
After the meeting (within 2 weeks), upload on e-cost a copy of your flight/train tickets. Note, that the selected participants will have 2 weeks to accept the invitation sent from e-cost. If you do not accept the invitation on e-cost within the 2 weeks, you will not be able to be reimbursed. The support will be a flat rate of a little bit more than n*110 where n <= 4 is the number of nights.
COST (European Cooperation in Science and Technology) is a funding agency for research and innovation networks. Our Actions help connect research initiatives across Europe and enable scientists to grow their ideas by sharing them with their peers. This boosts their research, career and innovation.
Location :
Room 571 in Building B
Czech Institute of Informatics, Robotics and Cybernetics (CIIRC) Jugoslávských partyzánů 1580/3 160 00 Dejvice, Prague
Schedule:
| Time | Tuesday April 18th, 2023 | Wednesday April 19th, 2023 | Thursday April 20th, 2023 |
|---|---|---|---|
| 9:45 | Introduction | – | – |
| 10:00 | Johannson (invited) | Rawson (invited) | Hula (invited) |
| 10:30 | Johannson (invited) | Rawson (invited) | Hula (invited) |
| X min | coffee | coffee | coffee |
| 11:00+X | Zombori | Schulz | del Rio |
| 11:30+X | Petkovic | Parsert | Barket |
| 12:00+X | Lunch | Lunch | Lunch |
| 12:30 | Lunch | Lunch | Lunch |
| 13:00 | Lunch | Lunch | Lunch |
| 13:30 | Lunch | Lunch | Lunch |
| 14:00 | Kaliszyk (about WG5) | Doré / Bartek | Hozzova /Hajdu |
| 14:30 | Kaliszyk (about WG5) | Purgal / Ratschan | Ulbrich/???? |
| 15:00 | WG5 discussion & deliverables | WG5 discussion & deliverables | WG5 discussion & deliverables |
| 15:30 | WG5 discussion & deliverables | WG5 discussion & deliverables | WG5 discussion & deliverables |
| 16:00 | WG5 discussion & deliverables | WG5 discussion & deliverables | WG5 discussion & deliverables |
| 16:30 | WG5 discussion & deliverables | WG5 discussion & deliverables | WG5 discussion & deliverables |
- Moa Johannson: Exploring Mathematical Conjecturing with Large Language Models (joint work with Nicholas Smallbone) Abstract Slides
- Zsolt Zombori: Training Data Extraction for Identifying Useful Lemmas (join work with Michael Rawson, Christoph Wernhard) Abstract Slides
- Matej Petković: Machine Learning for Context-Sensitive Search in Agda (joint work with Andrej Bauer and Ljupco Todorovski) Abstract Slides
- Cezary Kaliszyk: Working Group 5, Machine Learning in Proofs
- Michael Rawson: Takin’ Off: Deploying Neural Models for Theorem Proving Abstract Slides
- Stephan Schulz: Proof generation and challenges Slides
- Julian Parsert: Data Generation for SyGuS Problems (joint work with Elizabeth Polgreen) Abstract
- Maximilian Doré: Correct-by-construction programming with generative language models Slides
- Filip Bartek: Learning Symbol Weights for Clause Selection Slides
- Stanislaw Purgal: Splitting large models across multiple machines
- Stefan Ratschan: Executing Formal Specifications by Enumeration with Bounds Learning
- Jan Hula: ML 2.0 - sketches of the horizon Abstract Slides
- Tereso del Río: Data augmentation in mathematical objects Abstract
- Rashid Barket: Generating Rational Elementary Integrable Expressions Abstract Slides
- Petra Hozzova: Program Synthesis in Saturation Slides
- Marton Hajdu: Breaking the Diamond in Superposition Slides
- Mattias Ulbrich: Experience Report: Reinforcement Learning for Deductive Program Verification
Directions From CIIRC:
- Step One
- Step Two
- Step Three
- Step Four
- Step Five
- Step Six
- Step Seven
- Step Eight
- Step Nine
- Step Ten
Event Photos:
- First Day
- Coffee Break
- WG5 meeting
- Czech Dinner
- Last Day
