Winter Term 2024/25
Neural Networks in Formal Verification
| Event Type: | Seminar |
|---|---|
| Target Group: | Master Computer Science |
| Scope: | 2 SWS / 3 ECTS |
| Events: |
Kickoff:
October 23rd 2024, 13:00 – 14:00 in room 201 (building 50.34) Presentations 4+6: January 23rd 2025, 15:45 – 17:15 in room 301 (building 50.34) Presentations 1+2: February 6th 2025, 15:45 – 17:15 in room 301 (building 50.34) Presentations 7+8: February 13th 2025, 15:45 – 17:15 in room 301 (building 50.34) |
| Event Number: | 2400094 |
| ILIAS Course: | Link |
| Chair: | Application-oriented Formal Verification |
| Lecturers: |
Prof. Bernhard Beckert |
| Registration: | Through Wiwi-Portal until October 21st at 11:55 p.m. |
| Allocation of Places: | Topics will be distributed at the kickoff event. Priority will be given on a FCFS basis, considering preferences from registration. |
| Prerequisites: | No formal requirements, but prior experience with program analysis, verification or automated reasoning is helpful. |
| Language: | English |
Subject Area
Our chair specializes in formal methods across a broad spectrum of modern software development. This seminar aims to provide an overview of the current research landscape in the formal verification and the scope of neural networks in this domain. Specifically, it will explore two key aspects:
- Verification of Neural Networks focuses on the techniques, methods, and tools to ensure that neural networks operate safely, reliably, and as intended. This includes verifying the accuracy, robustness, and explainability of trained models, and their safe deployment in application platforms.
- Neural Networks for Verification involves utilizing AI and machine learning techniques to enhance traditional verification methods, making them more scalable, efficient, and effective for practical systems.
Tasks
For successful participation in the seminar, each participant is expected to achieve the following:
- Reading Assignment: Independently develop the content of the research topic to be presented (usually based on 1 or 2 papers). You will receive the necessary support in regular meetings with a supervisor.
- Presentation and Discussion: Prepare a 25-min presentation on the topic. After the presentations there will be an in-class discussion (roughly around 20 mins) that every student is expected to attend and participate in.
- Postprocessing: Write a report (7-8 pages, ACM Generic Journal Manuscript format) on the motivation of the research topic, state-of-the-art approaches, identify any shortcomings, write the relevant discussions from the class and mention how this research contributes to the broader landscape.
Slides and Material
Topics:
The following list of topics is intended to provide an overview. If you have any questions about topics or organization, please contact Debasmita Lohar.
Topic 1:
- Robustness
1. Local Robustness w.r.t. L0-Attacks: Boosting Few-Pixel Robustness Verification via Covering Verification Designs, CAV 2024
2. Towards Robustness Certification Against Universal Perturbations, ICLR 2023 - Fairness
1. FETA: Fairness Enforced Verifying, Training, and Predicting Algorithms for Neural Networks, EAAMO 2023
2. Fairify: Fairness Verification of Neural Networks, ICSE 2023 - Explainability
1. VERIX: Towards Verified Explainability of Deep Neural Networks, NeurIPS 2023
2. Formally Explaining Neural Networks within Reactive Systems, FMCAD 2023 - Quantization
1. Scalable Verification of Quantized Neural Networks, AAAI 2021
2. Sound Mixed Fixed-Point Quantization of Neural Networks, EMSOFT 2023
Topic 2:
- LLMs for Theorem Proving
1. Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs, ICLR 2023
2. LEGO-Prover: Neural Theorem Proving with Growing Libraries, ICLR 2024 - Reinforcement Learning (RL) for Theorem Proving
1. Learning to Find Proofs and Theorems by Learning to Refine Search Strategies, NeurIPS 2022
2. HyperTree Proof Search for Neural Theorem Proving, NeurIPS 2022 - LLMs for Formal Specifications
1. Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification, CAV 2024
2. Lemur: Integrating Large Language Models in Automated Program Verification, ICLR 2024 - LLMs for Program Synthesis
1. Guiding Enumerative Program Synthesis with Large Language Models, CAV 2024
2. Clover: Closed-Loop Verifiable Code Generation, SAIV 2024