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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
