Category: Non classé

Great news came yesterday, the paper by Marco Casadio and co-authors about LLM and verification has been accepted to the Journal of Applied Mathematics. Congratulations to Marco and all the co-authors!!!! Here is the draft if you are curious: https://arxiv.org/abs/2403.10144

Happy to announce that 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/

We are opening the seminar series SAIR: Safe and Secure AI for Robotics. The inaugural lecture will be given by Prof Ram Ramamoorthy, Edinburgh University, on “Safety and Trustworthiness of Human-Centred Autonomous Systems”. More details are available here: https://laiv.uk/sair-safe-and-secure-ai-for-robotics/

In the next 2 weeks, we are hosting two great talks on applications of formal methods in Robotics: https://laiv.uk/laiv-seminars/. If you are in Edinburgh area, join us at HWU or Edinburgh Universities. Otherwise, join on-line!

The LAIV group has started to teach an AI Safety Course in the New DAIR CDT: the Center for Doctoral training in Dependable and Deployable AI for Robotics. Ekaterina, Colin and Marco teach relevant aspects of verification for Robotics and AI PhD students within this CDT.

We submitted a new NLP benchmark to the International Competition on Neural Network Verification (VNN COMP), and we won a popular VNN COMP community vote (2^nd place) to have our new benchmark included in the Competition. This is the first ever NLP benchmark at VNNCOMP. It is considered to be prestigious to contribute to the selected list of benchmarks there! The benchmark comes as a result of the below research paper:
Marco Casadio, Tanvi Dinkar, Ekaterina Komendantskaya, Luca Arnaboldi, Omri Isac, Matthew L. Daggitt, Guy Katz, Verena Rieser, Oliver Lemon:
NLP Verification: Towards a General Methodology for Certifying Robustness.

Many congratulations to all co-authors!

Many congratulations to Natalia Slusarz, and supporting collaborators/supervisors, for having the following paper accepted at ITP’24:

Taming Differentiable Logics with Coq Formalisation
Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Ślusarz, Kathrin Stark https://arxiv.org/abs/2403.13700

Katya and Marco gave a talk “Mind Your Language: How to Make LLM Applications Trustworthy” at TAS Governance node at Edinburgh university. The pre-print related to the talk can be found here.

A team of Robotics, AI and Verification experts at Heriot-Watt and Edinburgh Universities has secured funding for training a cohort of PhD students in “Dependable and Deployable AI for Robotics”. Press release can be found here. It is an honour for LAIV to be part of this new chapter in the development of the Edinburgh Centre for Robotics!

Many congratulations to Remi Desmartin and Omri Isac (and their team of co-authors) for receiving the “Best Short Paper” award at LOPSTR’2023 this week, for the paper:
Remi Desmartin, Omri Isac, Grant O. Passmore, Kathrin Stark, Ekaterina Komendantskaya, Guy Katz:
Towards a Certified Proof Checker for Deep Neural Network Verification. LOPSTR 2023: 198-209