AIMACS — PROGRAM
Days: Saturday, 25 July 2026
Saturday, 25 July 2026
09:00-10:30
Morning session
AIMACS
Session Chair:
Location:
C2.05
| 09:00-10:00 |
LLM-aided theorem-proving (abstract) 60 min
1 Apodex
|
| 10:00-10:30 |
Constrained decoding (abstract) 30 min
1 UCSD
|
10:30-11:00
Coffee Break
AIMACS
Location:
C2.05
11:00-12:00
Second morning session
AIMACS
Session Chair:
Location:
C2.05
| 11:00-12:00 |
CSLib: The Lean Computer Science Library (abstract) 60 min
1 Stanford University
2 ETH Zurich
|
12:00-14:00
Lunch
AIMACS
Location:
C2.05
14:00-14:30
Poster Lightning Session #1
AIMACS
Session Chair:
Location:
C2.05
| 14:00-14:10 |
Typing Tensor Calculus in 2-Categories (abstract) 10 min
1 Oxford University
|
| 14:10-14:20 |
Transformers are Inherently Succinct (abstract) 10 min
1 RPTU Kaiserslautern-Landau
|
| 14:20-14:30 |
Fast and principled equation discovery from chaos to climate (abstract) 10 min
1 Durham University
|
14:30-15:00
Afternoon session
AIMACS
Session Chair:
Location:
C2.05
| 14:30-15:00 |
TBD (abstract) 30 min
1 Chalmers University
|
15:00-15:30
Poster Lightning session
AIMACS
Session Chair:
Location:
C2.05
| 15:00-15:10 |
Neurosymbolic Auditing of Natural-Language Software Requirements (abstract) 10 min
1 Stevens Institute of Technology
|
| 15:10-15:20 |
Improved Upper Bounds for Slicing the Hypercube (abstract) 10 min
1 TTM Technologies
|
| 15:20-15:30 |
Bisimulation-based reduction of neural network controllers (abstract) 10 min
1 The University of New Mexico
|
15:30-16:00
Coffee Break
AIMACS
Location:
C2.05
16:00-16:30
Afternoon Session #2
AIMACS
Session Chair:
Location:
C2.05
| 16:00-16:30 |
Advancing Mathematics Research with AI-Powered Formal Proof Search (abstract) 30 min
1 Google DeepMind
|
16:30-17:10
Poster Lightning Session #3
AIMACS
Session Chair:
Location:
C2.05
| 16:30-16:40 |
A Rust-to-Lean Verification Pipeline with AI Provers: An Experience Report (abstract) 10 min
1 Runtime Verification
|
| 16:40-16:50 |
CovCal: Risk-Controlled Lean-as-Judge for Natural-Language Mathematical Reasoning (abstract) 10 min
1 Imperial College
|
| 16:50-17:00 |
LeanPolish: A Kernel-Verified Dataset and Symbolic Compression Framework for Lean 4 Proofs (abstract) 10 min
1 Imperial College
|
| 17:00-17:10 |
ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings (abstract) 10 min
1 Georgia Tech
|
17:10-18:00
Panel
AIMACS
Session Chair:
Location:
C2.05
| 17:10-18:00 |
Panel: How should CAV researchers respond to AI progress? (abstract) 50 min
1 Brown University
2 Rice University
3 MIT
4 UT Austin
|