Ido Pinto

Not All Invariants Are Equal: Curating Training Data to Accelerate Program Verification with SLMs

The synthesis of inductive loop invariants is a critical bottleneck in automated program verification. While Large Language Models (LLMs) show promise in mitigating this issue, they often fail on hard instances, generating invariants that are invalid or computationally ineffective. While fine-tuning…