Ранжирование инвариантов циклов, сгенерированных языковыми моделями, для верификации программ

Ranking LLM-Generated Loop Invariants for Program Verification

October 13, 2023

Авторы: Saikat Chakraborty, Shuvendu K. Lahiri, Sarah Fakhoury, Madanlal Musuvathi, Akash Lal, Aseem Rastogi, Aditya Senthilnathan, Rahul Sharma, Nikhil Swamy

cs.AI

Аннотация

Синтез индуктивных инвариантов циклов является фундаментальной задачей для автоматизации верификации программ. В данной работе мы наблюдаем, что крупные языковые модели (такие как GPT-3.5 или GPT-4) способны синтезировать инварианты циклов для определенного класса программ в режиме "0-shot", однако для генерации корректных инвариантов требуется несколько попыток. Это может привести к большому количеству вызовов программы верификации для установления инварианта. Чтобы решить эту проблему, мы предлагаем подход {\it переранжирования} для сгенерированных результатов языковых моделей. Мы разработали ранкер, который может отличать корректные индуктивные инварианты от некорректных попыток на основе определения задачи. Ранкер оптимизирован как контрастный ранкер. Экспериментальные результаты показывают, что этот механизм переранжирования значительно улучшает позиционирование корректных инвариантов среди сгенерированных кандидатов, что приводит к заметному сокращению количества вызовов верификатора.

English

Synthesizing inductive loop invariants is fundamental to automating program verification. In this work, we observe that Large Language Models (such as gpt-3.5 or gpt-4) are capable of synthesizing loop invariants for a class of programs in a 0-shot setting, yet require several samples to generate the correct invariants. This can lead to a large number of calls to a program verifier to establish an invariant. To address this issue, we propose a {\it re-ranking} approach for the generated results of LLMs. We have designed a ranker that can distinguish between correct inductive invariants and incorrect attempts based on the problem definition. The ranker is optimized as a contrastive ranker. Experimental results demonstrate that this re-ranking mechanism significantly improves the ranking of correct invariants among the generated candidates, leading to a notable reduction in the number of calls to a verifier.