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.

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 before March 10. Notifications will be sent on March 17 maximum.

Participants selected to be reimbursed will receive a formal invitation. If they do not accept the invitation on e-cost within the 2 weeks, their invitation will be canceled and they will not be reimbursed.

After the meeting, they will have to upload on e-cost a copy of their flight/train tickets, and hotel and meal bills. The support is a flat rate of a little bit more than n*110 euros where n is the number attended workshop days, plus the travel.

COST (European Cooperation in Science and Technology) is a funding agency for research and innovation networks. Its 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.