European Research Network on Formal Proofs
COST action CA20111
COST logo
EU flag and COST acknowledgement
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.

took place at TU Wien Informatics, Vienna, Austria, March 25th-26th 2024, organised by Michael Rawson and Cezary Kaliszyk. Complaints to the former. The event was supported by the Cost Action CA20111 - European Research Network on Formal Proofs and 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

25th March

  • 1000–1100 Boris Shminke: Machine Learning for Automated Theorem Proving: an ML-side perspective abstracts slides
  • 1100–1130 break
  • 1130–1200 Fatih Özkaynak: Automated Proof Techniques for Assessing the Security of Chaos-Based Encryption Algorithms abstract
  • 1200–1230 Rashid Barket: Algorithm Selection for Symbolic Integration using Machine Learning abstract slides
  • 1230–1400 lunch (not provided)
  • 1400–1430 Natalia Ślusarz: Exploration of properties of differentiable logics through mechanisation abstract
  • 1430–1500 Filip Bártek: Learning to Rank in Automatic Theorem Proving abstract slides
  • 1500–1530 break
  • 1530 WG5 meeting slides

26th March

  • 0930–1000 Alessandro Bruni: Yet another formal theory of probabilities (with an application to random sampling) abstract
  • 1000–1030 Yixuan Li: Guiding Enumerative Program Synthesis with Large Language Models abstract
  • 1030–1100 George Granberry: Neuro-Symbolic Specification Generation for C programs abstract
  • 1100–1130 break
  • 1130–1200 Jelle Piepenbrock: Integrating ML into SMT solvers
  • 1200–1230 Julian Parsert: Neural Termination Analysis abstract
  • 1230–1400 lunch (not provided)
  • 1400–1410 Clemens Eisenhofer: CheeZ3: using LLMs to predict SMT models
  • 1410–1430 Robin Coutelier: A practical application of machine learning in Vampire
  • 1430–1500 coffee
  • 1500–1530 Martin Suda: Two Learning Operators for Clause Selection Guidance abstract slides

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.

Local Information

Refer to the excellent guide produced for the WG6 meeting here. Please note that the location is different this time.

Event Photos

all participants seated, taken from the front of the room the invited speaker from the back of the room David Cerna presenting at the WG5 meeting Martin Suda explaining saturation-based proof search with a large diagram