⚠️ 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.
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.
List of Accepted Contributions
We are pleased to announce the following contributions accepted for AIPV 2026.
- Yosuke Ito. Formalizing Actuarial Mathematics in Proof Assistants
- Chengsong Tan, Jonathan Julian Huerta Y Munive, John Wickerson and Alastair Donaldson. Automated Sketching and Repairing of Large Mechanised Proofs
- Hyojae Lim. Toward Textbook-Scale Autoformalization with Large Language Models
- Grigory Neustroev, Mirco Giacobbe and Anna Lukina. Neural Continuous-Time Supermartingale Certificates
- Alcino Cunha and Nuno Macedo. Validating Formal Specifications with LLM-generated Test Cases
- Saki Hasegawa, Naoyasu Ubayashi and Hironori Washizaki. Diagnostic Evidence Levels for LLM-Assisted Fault Localization in SPIN
- Kaito Baba, Chaoran Liu, Shuhei Kurita and Akiyoshi Sannai. Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs
- Minghao Liu, Chia-Hsuan Lu and Marta Kwiatkowska. Exact Verification of Graph Neural Networks with Incremental Constraint Solving
- Holly Hendry, Pedro Ribeiro and Frank Soboczenski. Large Language Models for Verification of Reactive Programs
- Raik Hipler and Martin Leucker. Machine Learning for Stream-Based Diagnosis
- Cheng-Hui Weng. Inverting the Formalization Workflow: Prototyping an MPC Protocol in Rocq with an LLM Agent
- Mohammad Afzal, S. Akshay, Blaise Genest and Ashutosh Gupta. Formal Reasoning About Confidence and Automated Verification of Neural Networks
- Sho Sonoda. Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Models
- Xinyuan Tu, Thomas Hildebrandt and Thiago Rocha Silva. From BDD Scenarios to Formally Verifiable Behavioural Models via Dynamic Condition Response Graphs
- 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
- Martin Berger. Experience report: I’ve always been wrong about AI
- Banri Yanahama and Akiyoshi Sannai. Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization
- Qiyuan Xu, Renxi Wang, Peixin Wang, Haonan Li and Conrad Watt. A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL
- Alberto Tagliaferro, Bruno Guindani, Livia Lestingi and Matteo Giovanni Rossi. Towards an Agentic LLM-based Approach to Requirement Formalization from Unstructured Specifications
- Borja Requena, Austin Letson, Krystian Nowakowski, Izan Beltran Ferreiro and Leopoldo Sarra. A Minimal Agent for Automated Theorem Proving
- 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?
- Vasily Ilin. Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium