The Workshop Theorem Proving and Machine Learning in the age of LLMs: SoA and 
Future Perspectives 
will take place in Edinburgh, Scotland, UK, April 7th-8th 2025, organised by 
Ekaterina Komendantskaya,  Elizabeth Polgreen, Michael Rawson, Christian 
Saemann, Kathrin Stark. The event is supported by the Cost Action CA20111 - 
European Research Network on Formal Proofs.
Workshop webpage: https://europroofnet.github.io/wg5-edinburgh25/

Aims

Machine learning (ML) has been shown to be very successful in programming and 
translation talks, and creates new opportunities combining AI with proofs. 
Recently, various claims have been made that large language models (LLMs) will 
revolutionise these areas. However, many questions about the details of the 
applications of LLMs and their impact on theorem proving and mathematics remain 
open. At the workshop, we want to bring together researchers from a wide range 
of communities: mathematics, automated and interactive theorem proving, machine 
learning, natural language processing, and formal methods, in order to discuss 
the state-of the-art and future directions for this new area of research.

Examples of topics that we intend to discuss include, but are not limited to:

+ ML/LLM for Advancing Proof Techniques, e.g., tailoring LLMs to 
theorem-proving datasets and benchmarks, combining neural networks and symbolic 
reasoning for robust theorem proving, enabling LLMs to learn proof techniques 
from minimal data or prior examples.
+ Applications of ML/LLM in Theorem Proving, e.g., designing co-pilot systems 
for theorem provers like Coq, Lean, or Isabelle, auto-formalising mathematical 
concepts and proofs from textbooks or research papers, human-machine 
collaboration workflows in proof construction.
+ Challenges and Limitations of ML/LLM in Theorem Proving, e.g. addressing 
hallucinations and errors in proofs generated by LLMs, handling large and 
complex proof spaces with LLM-guided tools, mitigating biases introduced during 
LLM training on specific mathematical domains.
+ Benchmarks and Evaluation for ML/LLM in Theorem Proving, e.g., creating 
datasets specifically for evaluating LLM-based theorem proving systems, 
assessing the interpretability and trustworthiness of LLM-generated proofs, 
defining success metrics for proof assistance beyond correctness, such as 
creativity and accessibility.
+ Interdisciplinary Impact of ML/LLM, e.g., leveraging LLMs to teach formal 
methods, logic, and theorem proving to students, using LLMs to explore 
conjectures and new areas of mathematical research, applications in formal 
verification for software, hardware, and systems engineering, including 
industrial applications.
+ Future Directions for ML/LLM in Theorem Proving: e.g.,  the implications of 
relying on AI systems for critical mathematical proofs, setting open standards 
for the integration of LLMs in the theorem-proving workflows, speculating on 
the evolution of LLMs and their roles in formal reasoning.
+ Cross-Domain Connections: e.g., developing user-friendly natural language 
interfaces for proof assistants, adapting LLM capabilities from general domains 
to formal logic and proofs.


Format:
 
Keynote Talks:

+ Machine Learning in Industrial Verification: Swarat Chaudhuri (University of 
Texas and Google DeepMind)
+ Machine Learning for Mathematics Research: Sergei Gukov (Caltech University 
and Dublin Institute of Advanced Studies)
+ Machine Learning in Theorem Proving: Josef Urban (CIIRC/CVUT, Czech Republic)

Call for Presentations:

The workshop solicits contributed talks supported by an extended abstract of up 
to 2 pages in LNCS format, excluding references. Abstracts will be reviewed for 
relevance and quality and subsequently made public on the workshop's web page.
All abstracts must be submitted via this Easychair page.
+ Abstract submission: January 31st 2025 (AOE).
+ Travel support application: January 31st 2025.
+ Notification of acceptance: ASAP thereafter.

Registration and Optional Travel Support:

Please fill out the following form 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 12) 
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.

Participants who contribute talks will be given preference when applying for 
travel support.

Location:

Postgraduate Centre Heriot-Watt, Heriot-Watt University, Edinburgh, EH14 4AL, 
UK. More information about the Heriot-Watt campus.
                                                                                
     
If you have any questions, please contact Kathrin Stark.



_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Reply via email to