WG5 Machine Learning in Proofs

The aim of this WG is to contribute to the field of machine-learning-based methods to improve the efficiency of automated theorem proving systems in terms of further development of techniques for proof guidance and premise selection. Furthemore, the group will explore how and to what extent tasks of computer-assisted reasoning can be extended to proofs that are represented in (controlled) natural languages.

Goals 2024-2025

• Share knowledge and discuss the results and perspectives on the use of large language models in proof systems

  Deliverables

• Detailed technical report on the evaluation of techniques for learning proof search guidance and premise selection in automated theorem provers.
  • Learning Guided Automated Reasoning: A Brief Survey Lasse Blaauwbroek, David M. Cerna, Thibault Gauthier, Jan Jakubův, Cezary Kaliszyk, Martin Suda, Josef Urban, Logics and Type Systems in Theory and Practice 2024.
• White paper on including restricted natural language proof formats to existing proof libraries.

  Activities

• March-April 2025: Theorem Proving with LLMs: SoA and Future Perspectives, Edinburgh, Scotland, UK
• 24-27 June 2024: EuroProofNet Summer School on AI for Reasoning and Processing of Mathematics, Kutaisi, Georgia
• 25-26 March 2024: Workshop on Alignment of Proof Systems and Machine Learning, Vienna, Austria

• 6-8 September 2023: Joint WG4-WG5 meeting/Workshop on Natural Formal Mathematics, and on libraries of formal proofs and natural mathematical language, Cambridge, UK

• 18-20 April 2023: WG meeting co-organized with Joint Workshops (PAMLTP) and (DG4D^3), Prague (Czechia)

• 5-8 September 2022: WG meeting Machine Learning for Theorem Proving co-organized with AITP’22 conference, Aussois (France)