⚠️ Travel Advisory:
Due to the strong number of contributions received, AIPV is now planned as a two-day event, taking place from May 18 to May 19.
Please take this into account when making your travel and accommodation arrangements.
⚠️ Regarding Participation:
AIPV is planned as an in-person workshop. Remote presentations are not a standard option and will only be considered in exceptional cases upon prior agreement with the organisers.
Thank you for your understanding.
Program
Tentative program — subject to change.
Contents
Day 1 (May 18)
Session-1 09:00–10:30 (Theme: Verification, Chair: TBA)
| Time |
Type |
Speaker |
Title |
| 09:00–09:10 |
Opening |
AIPV organising team |
|
| 09:10–09:50 |
Keynote |
Conrad Watt |
TBA |
| 09:50–10:10 |
Contributed |
Raik Hipler and Martin Leucker |
Machine Learning for Stream-Based Diagnosis |
| 10:10–10:30 |
Contributed |
Borja Requena, Austin Letson, Krystian Nowakowski, Izan Beltran Ferreiro and Leopoldo Sarra |
A Minimal Agent for Automated Theorem Proving |
↑ Back to top
Coffee Break and Poster 10:30–11:00
| Time |
Type |
Note |
| 10:30–11:00 |
Coffee Break |
Poster |
Session-2 11:00–12:30 (Theme: Isabelle & Rocq, Chair: TBA)
| Time |
Type |
Speaker |
Title |
| 11:00–11:10 |
TBA |
TBA |
TBA |
| 11:10–11:30 |
Contributed |
Cheng-Hui Weng |
Inverting the Formalization Workflow: Prototyping an MPC Protocol in Rocq with an LLM Agent |
| 11:30–11:50 |
Contributed |
Yusuke Ito |
Formalizing Actuarial Mathematics in Proof Assistants |
| 11:50–12:10 |
Contributed |
Qiyuan Xu, Renxi Wang, Peixin Wang, Haonan Li and Conrad Watt |
A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL |
| 12:10–12:30 |
Contributed |
Chengsong Tan, Jonathan Julian Huerta Y Munive, John Wickerson and Alastair Donaldson |
Automated Sketching and Repairing of Large Mechanised Proofs |
↑ Back to top
Lunch 12:30–14:00
| Time |
Type |
Note |
| 12:30–14:00 |
Lunch Break |
Poster |
Session-3 14:00–15:30 (Theme: Mathematics, Chair: TBA)
| Time |
Type |
Speaker |
Title |
| 14:00–14:40 |
Keynote |
Christian Szegedy |
TBA |
| 14:40–15:00 |
Contributed |
Hyojae Lim |
Toward Textbook-Scale Autoformalization with Large Language Models |
| 15:00–15:30 |
Contributed |
Kaito Baba, Chaoran Liu, Shuhei Kurita and Akiyoshi Sannai |
Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs |
↑ Back to top
Coffee Break and Poster 15:30–16:00
| Time |
Type |
Note |
| 15:30–16:00 |
Coffee Break |
Poster |
Session 4 16:00-17:40 (Theme: Application, Chair: TBA)
| Time |
Type |
Speaker |
Title |
| 16:00–16:20 |
Sponsor |
Axiom Math |
TBA |
| 16:20–16:40 |
Contributed |
Alcino Cunha and Nuno Macedo |
Validating Formal Specifications with LLM-generated Test Cases |
| 16:40–17:00 |
Contributed |
Martin Berger |
Experience report: I’ve always been wrong about AI |
| 17:00–17:40 |
Round Table |
TBA |
Panel Discussion |
| 17:40–17:50 |
Closing |
AIPV organising team |
|
↑ Back to top
Reception 18:30-20:40
| Time |
Type |
Note |
| 17:50–18:30 |
Sightseeing |
|
| 18:30–20:40 |
Reception |
Poster |
Day 2 (May 19)
Session-1 09:00–10:30 (Theme: Theory, Chair: Martin Berger)
| Time |
Type |
Speaker |
Title |
| 09:00–09:10 |
Opening |
AIPV organising team |
|
| 09:10–09:30 |
Sponsor |
Harmonic |
TBA |
| 09:30–10:10 |
Keynote |
Nobuko Yoshida |
TBA |
| 10:10–10:30 |
Contributed |
Grigory Neustroev, Mirco Giacobbe and Anna Lukina |
Neural Continuous-Time Supermartingale Certificates |
↑ Back to top
Coffee Break and Poster 10:30–11:00
| Time |
Type |
Note |
| 10:30–11:00 |
Coffee Break |
Poster |
Session-2 11:00–12:30 (Theme: Lean, Chair: TBA)
| Time |
Type |
Speaker |
Title |
| 11:00–11:10 |
Short Talk |
Balaji Rao, John Harrison, Soonho Kong, Juneyoung Lee and Carlo Lipizzi |
s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs |
| 11:10–11:30 |
Contributed |
Banri Yanahama and Akiyoshi Sannai |
Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization |
| 11:30–11:50 |
Contributed |
Austin Letson, Leopoldo Sarra, Auguste Poiroux, Oliver Dressler, Paul Lezeau, Dhyan Aranha, Frederik Pu, Aaron Hill, Miguel Corredera Hidalgo, Julian Berman, George Tsoukalas and Lenny Taelman |
SorryDB: Can AI Provers Complete Real-World Lean Theorems? |
| 11:50–12:10 |
Contributed |
Vasily Ilin |
Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium |
| 12:10–12:30 |
Contributed |
Xinyuan Tu, Thomas Hildebrandt and Thiago Rocha Silva |
From BDD Scenarios to Formaly Verifiable Behavioural Models via Dynamic Condition Response Graphs |
↑ Back to top
Lunch 12:30–14:00
| Time |
Type |
Note |
| 12:30–14:00 |
Lunch Break |
Poster |
Session-3 14:00–15:30 (Theme: Neueral Network, Chiar: TBA)
| Time |
Type |
Speaker |
Title |
| 14:00–14:30 |
Keynote |
TBA |
TBA |
| 14:30–14:50 |
Contributed |
Minghao Liu, Chia-Hsuan Lu and Marta Kwiatkowska |
Exact Verification of Graph Neural Networks with Incremental Constraint Solving |
| 14:50–15:10 |
Contributed |
Mohammad Afzal, S. Akshay, Blaise Genest and Ashutosh G |
Formal Reasoning About Confidence and Automated Verification of Neural Networks |
| 15:10–15:30 |
Contributed |
Sho Sonoda |
Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Models |
↑ Back to top
Coffee Break and Poster 15:30–16:00
| Time |
Type |
Note |
| 15:30–16:00 |
Coffee Break |
Poster |
Session-4 16:00-17:40 (Theme: LLM, Chair: TBA)
| Time |
Type |
Speaker |
Title |
| 16:00–16:20 |
Contributed |
Holly Hendry, Pedro Ribeiro and Frank Soboczenski |
Large Language Models for Verification of Reactive Programs |
| 16:20–16:40 |
Contributed |
Alberto Tagliaferro, Bruno Guindani, Livia Lestingi and Matteo Giovanni Rossi |
Towards an Agentic LLM-based Approach to Requirement Formalization from Unstructured Specifications |
| 16:40–17:00 |
Sponsor |
Noeon Research |
TBA |
| 17:00–17:40 |
Round Table |
TBA |
Panel Discussion |
| 17:40–17:50 |
Closing |
AIPV organising team |
|
↑ Back to top
![Random Image]()