The Coq mailing list

[geoff AT tptp.org]

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.