Program
Tentative program — subject to change.
Contents
Day 1 (May 18)
Session-1 09:00–10:30 (Theme: Verification, Chair: Yutaka Nagashima)
| Time |
Type |
Speaker |
Title |
Material |
| 09:15 |
Opening |
AIPV organising team |
|
slide |
| 09:20 |
Keynote |
Conrad Watt |
The Bright Future of Verification Slop |
slide |
| 10:00 |
Contributed |
Raik Hipler and Martin Leucker |
Machine Learning for Stream-Based Diagnosis |
ID10 slide paper |
| 10:20 |
Contributed |
Borja Requena, Austin Letson, Krystian Nowakowski, Izan Beltran Ferreiro and Leopoldo Sarra |
A Minimal Agent for Automated Theorem Proving |
ID20 poster |
↑ Back to top
Coffee Break and Poster 10:40–11:00
| Time |
Type |
Note |
| 10:40 |
Coffee Break |
Poster |
Session-2 11:00–12:40 (Theme: Isabelle & Rocq, Chair: Jonathan Julián Huerta y Munive)
| Time |
Type |
Speaker |
Title |
Material |
| 11:00 |
Sponsor |
Harmonic |
Automatically Formally Verified Software using Aristotle |
|
| 11:20 |
Contributed |
Cheng-Hui Weng |
Inverting the Formalization Workflow: Prototyping an MPC Protocol in Rocq with an LLM Agent |
ID11 poster paper |
| 11:40 |
Contributed |
Yosuke Ito |
Formalizing Actuarial Mathematics in Proof Assistants |
ID01 slide poster paper GitHub |
| 12:00 |
Contributed |
Qiyuan Xu, Renxi Wang, Peixin Wang, Haonan Li and Conrad Watt |
A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL |
ID18 poster GitHub |
| 12:20 |
Contributed |
Chengsong Tan, Jonathan Julián Huerta y Munive, John Wickerson and Alastair F. Donaldson |
Automated Sketching and Repairing of Large Mechanised Proofs |
ID02 slide poster paper |
↑ Back to top
Lunch 12:40–14:00
| Time |
Type |
Note |
| 12:40 |
Lunch Break |
Poster |
Session-3 14:00–15:30 (Theme: Mathematics, Chair: Minchao Wu)
| Time |
Type |
Speaker |
Title |
Material |
| 14:00 |
Keynote |
Cezary Kaliszyk |
Autoformalization Across Proof Assistants: Languages, Proof Styles, and Automation |
slide |
| 14:40 |
Contributed |
Hyojae Lim |
Toward Textbook-Scale Autoformalization with Large Language Models |
ID03 |
| 15:00 |
Contributed |
Kaito Baba, Chaoran Liu, Shuhei Kurita and Akiyoshi Sannai |
Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs |
ID07 slide poster paper GitHub Paper |
↑ Back to top
Coffee Break and Poster 15:30–16:00
| Time |
Type |
Note |
| 15:30 |
Coffee Break |
Poster |
Session 4 16:00–17:40 (Theme: Application, Chair: Chengsong Tan)
| Time |
Type |
Speaker |
Title |
Material |
| 16:00 |
Sponsor |
Hendrik Skubch (Noeon Research) |
Towards Trustable Machine Reasoning — A case study using variant Sudoku |
|
| 16:20 |
Contributed |
Alcino Cunha and Nuno Macedo |
Validating Formal Specifications with LLM-generated Test Cases |
ID05 slide Paper |
| 16:40 |
Workshop |
Everyone |
Research Ideas |
guiding slides and resulting slides |
| 17:20 |
Closing |
AIPV organising team |
|
|
↑ Back to top
Reception 18:00–20:00 in Room 201-203
Participants from other FM 2026 workshops are also warmly welcome to join the reception, especially if they take the opportunity to have a look at the AIPV posters and interact with the presenters.
| Time |
Type |
Note |
| 17:21 |
Short guided walking tour |
This is an optional informal event strictly outside the scope of AIPV itself. Participation is therefore entirely at your own discretion and responsibility. |
| 18:00 |
Reception |
Poster (Room 201-203). |
Day 2 (May 19)
Session-1 09:00–10:30 (Theme: Theory, Chair: Martin Berger)
| Time |
Type |
Speaker |
Title |
Material |
| 09:00 |
Opening |
AIPV organising team |
|
|
| 09:10 |
Keynote |
Nobuko Yoshida |
Resilient Distributed Intelligent Swarms and Safeguarded AI: Programming Models and Runtime Guarantees |
|
| 09:50 |
Contributed |
Grigory Neustroev, Mirco Giacobbe and Anna Lukina |
Neural Continuous-Time Supermartingale Certificates |
ID04 slide poster Paper |
| 10:10 |
Contributed |
Xinyuan Tu, Thomas Hildebrandt and Thiago Rocha Silva |
From BDD Scenarios to Formally Verifiable Behavioural Models via Dynamic Condition Response Graphs |
ID14 poster paper slide |
↑ Back to top
Coffee Break and Poster 10:30–11:00
| Time |
Type |
Note |
| 10:30 |
Coffee Break |
Poster |
Session-2 11:00–12:30 (Theme: Lean, Chair: Kensho Tsurusaki)
| Time |
Type |
Speaker |
Title |
Material |
| 11:00 |
Contributed |
Vasily Ilin |
Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium |
ID22 poster |
| 11:20 |
Contributed |
Banri Yanahama and Akiyoshi Sannai |
Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization |
ID17 |
| 11:40 |
Contributed |
Austin Letson, Leopoldo Sarra, Auguste Poiroux, Oliver Dressler, Paul Lezeau, Dhyan Aranha, Frederick Pu, Aaron Hill, Miguel Corredera Hidalgo, Julian Berman, George Tsoukalas and Lenny Taelman |
SorryDB: Can AI Provers Complete Real-World Lean Theorems? |
ID21 poster |
| 12:00 |
Sponsored |
Jimmy Shin (AxiomMath.ai) |
AXLE: Free, Public Lean 4 Tooling for AI-Driven Mathematics |
|
↑ Back to top
Lunch 12:30–14:00
| Time |
Type |
Note |
| 12:30 |
Lunch Break |
Poster |
Session-3 14:00–15:30 (Theme: Neural Network, Chair: TBA)
| Time |
Type |
Speaker |
Title |
Material |
| 14:00 |
Contributed |
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 |
ID15 slide Project LinkedIn Leaderboard YouTube |
| 14:20 |
Contributed |
Minghao Liu, Chia-Hsuan Lu and Marta Kwiatkowska |
Exact Verification of Graph Neural Networks with Incremental Constraint Solving |
ID08 slide poster paper paper |
| 14:40 |
Contributed |
Mohammad Afzal, S. Akshay, Blaise Genest and Ashutosh Gupta |
Formal Reasoning About Confidence and Automated Verification of Neural Networks |
ID12 poster |
| 15:00 |
Contributed |
Sho Sonoda |
Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Models |
ID13 paper1 paper2 |
↑ Back to top
Coffee Break and Poster 15:30–16:00
| Time |
Type |
Note |
| 15:30 |
Coffee Break |
Poster |
Session-4 16:00–17:40 (Theme: LLM, Chair: TBA)
| Time |
Type |
Speaker |
Title |
Material |
| 16:00 |
Contributed |
Holly Hendry, Pedro Ribeiro and Frank Soboczenski |
Large Language Models for Verification of Reactive Programs |
ID09 |
| 16:20 |
Contributed |
Alberto Tagliaferro, Bruno Guindani, Livia Lestingi and Matteo Giovanni Rossi |
Towards an Agentic LLM-based Approach to Requirement Formalization from Unstructured Specifications |
ID19 slide poster paper Paper |
| 16:40 |
Contributed |
Liao Zhang |
Signal Shot: End-to-End Formal Verification of Signal’s Cryptographic Stack |
ID23 slide poster paper |
| 17:00 |
Round Table |
10 Questions about AIPV |
Panel Discussion |
questions |
| 17:40 |
Business Meeting |
AIPV organising team |
|
questionnaire |
↑ Back to top
![Random Image]()