will take place at TU Wien Informatics, Vienna, Austria, March 25th-26th 2024, organised by Michael Rawson and Cezary Kaliszyk. Complaints to the former. The event is supported by the Cost Action CA20111 - European Research Network on Formal Proofs and will be co-located with a meeting of Working Group 5 of the action, “Machine Learning in Proofs”.

Aims

The symbolic and statistical approaches to artificial intelligence can be difficult to combine. The workshop will focus on the problem of aligning proof systems and machine learning techniques to reduce the “impedance mismatch” suffered by interdisciplinary researchers. This covers a wide range of topics by nature, but examples could include:

  • alignment of successful proof with loss functions
  • design of proof environments for reinforcement learning
  • machine-learning approaches to problems in proof systems
  • efficiency considerations for deployment of machine learning within proof systems
  • design of automatic proof procedures with respect to machine learning
  • proof systems for verification of machine learning

The workshop will be a forum for exchange of solutions to these problems between researchers working in different areas, and also a source of completely original ideas.

Format

The workshop solicits contributed talks supported by an extended abstract of up to 1 page, excluding references, in the EasyChair format. Abstracts will be reviewed for relevance and quality and subsequently made public on the workshop’s web page. Participants that contribute talks will be given preference when applying for travel support — see below. Workshop deadlines are as follows:

  • Abstract submission: February 25th
  • Travel support application: February 25th
  • Notification of acceptance: ASAP thereafter.

Please submit abstracts via email.

Registration and Optional Travel Support

Please email us if you plan to attend, regardless of whether you submit an abstract or apply for 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 you have not already, then fill in an application form.

As soon as possible after the meeting and certainly within two weeks, submit a copy of your flight/train tickets to e-cost. Selected participants will have 2 weeks to accept the invitation sent from e-cost. If you do not accept the invitation within 2 weeks, you will not be reimbursed. Support will be at a flat rate of approximately €160 per day.

TU Wien has facilities for attendees with children, including a dedicated parent-child room. Please e-mail the organisers for more details if you would like to make use of them.

Location

Hörsaal Zemanek

TU Wien Informatics Favoritenstraße 9-11 1040 Wien

Schedule

To be announced, but at least the following talks will be given:

  • Machine Learning for Automated Theorem Proving: an ML-side perspective (Boris Shminke)
  • Automated Proof Techniques for Assessing the Security of Chaos-Based Encryption Algorithms (Fatih Özkaynak)
  • Two Learning Operators for Clause Selection Guidance (Martin Suda)
  • Exploration of properties of differentiable logics through mechanisation (Natalia Ślusarz)
  • Learning to Rank in Automatic Theorem Proving (Filip Bártek)
  • Neural Termination Analysis (Julian Parsert)
  • Guiding Enumerative Program Synthesis with Large Language Models (Yixuan Li)
  • Neuro-Symbolic Specification Generation for C programs (George Granberry)
  • Algorithm Selection for Symbolic Integration using Machine Learning (Rashid Barket)
  • Integrating ML into SMT solvers (Jelle Piepenbrock)

Directions and Getting Around

From the airport, take a train to the city. You can buy a single ticket for around €5, cash or card, from the red ÖBB kiosks in the airport and the airport train station. Trains typically run either directly to the main train station (“Hauptbahnhof”), or with a number of stops to one of Vienna’s smaller stations. The City Airport Train (CAT), buses and taxis are other possibilities with different tradeoffs.

From the main train station, it is a 20-minute walk north along Favoritenstraße to the building. If you prefer, you can take the metro (“U-bahn”) line U1 from the main station in the direction of Leopoldau to Taubstummengasse.

From smaller stations it is also possible to walk or take the metro. If taking such a train, I recommend getting off at the central station (“Wien Mitte”/”Landstraße”), where it is a pleasant 30-minute walk through Stadtpark and Karlsplatz to the building. From the central station you can also take the metro line U4 in the direction of Hütteldorf to Karlsplatz, then a short walk.

The building spans Favoritenstraße 9-11, but the door at Favoritenstraße 11 is not often open. Therefore, starting from Favoritenstraße 9, proceed through the wooden doors into the courtyard. Turn right, through the automatic glass door into the hallway. Continue straight on, past the lift on your left into the lobby/reception area. At this point you should be met by organisers. However, in the absence of organisers, turn left after reception through the double doors, Zemanek is immediately on the right. The university map has an entry for the room.

Getting around Vienna is relatively easy: the city is walkable, and public transport functions well. You can buy paper public transport tickets from kiosks in metro stations and elsewhere, which are valid on public transport within Vienna city limits. Transport tickets have to be validated before use. NB these tickets are not valid for the train to/from the airport, as this leaves the city limits.

Event Photos

To be taken.