LLM-Augmented Proof Search for Domain-Specific Compiler Verification

Xu et al. (2025) and Qian et al. (2025) show that LLMs can automate significant portions of verification tasks in software engineering and interactive theorem proving, respectively. Building on this, the proposed research would design a system where LLMs serve as first-line proof searchers for domain-specific transformations (e.g., MLIR dialects, hardware description languages), tightly integrated into proof assistants like Lean or Coq. The LLM would generate candidate invariants, proof sketches, or even counterexamples for failed transformations, with fallback to human-guided steps only as necessary. This is distinct from traditional “hammer” approaches by tailoring the LLM’s training and interaction for compiler IR semantics and transformation patterns. Such a system could dramatically accelerate the verification of new optimizations, especially for fast-moving domains like AI hardware or cryptography.

References:

1. Lean-auto: An Interface between Lean 4 and Automated Theorem Provers. Yicheng Qian, Joshua Clune, Clark Barrett, Jeremy Avigad (2025). International Conference on Computer Aided Verification.
2. Towards Automated Formal Verification of Backend Systems with LLMs. Kangping Xu, Yifan Luo, Yang Yuan, A. C. Yao (2025). arXiv.org.