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