Large language models (LLMs) have shown proficiency in various software engineering tasks, such as code generation and translation. However, a key limitation in their performance may be their (lack of) understanding of programming-language semantics. Even when explicit semantics are given, it remains unclear whether LLMs apply those rules or lean on priors learned during pre-training instead. We study if LLMs lean on priors or given semantics with a novel task--Program Executability Prediction (PrEx)--that asks models to predict whether a program is semantically valid or invalid (and, if invalid, which formal rule it violates) given the program's syntax and operational semantics. Because PrEx requires both valid and invalid programs, we build a dataset with systematically generated invalid transformations derived from valid programs. We evaluate open-source coding LLMs under two semantic formalisms and two semantic shifts across Human-Written, LLM-Translated, and Fuzzer-Generated program splits. Our findings show that LLMs lean on pre-training priors rather than systematically applying the given rules, performing especially poorly on modified semantics and degrading further as program complexity increases. PrEx is available at https://github.com/EngineeringSoftware/prex.
Lara Marinov, Aditya Thimmaiah, Jayanth Srinivasa et al.· 0 citations
Smack improves on ExLi by extending the reach and fault-detection ability of inline-test generation, and is also complementary to ExLi on target statements that ExLi can handle.
Pengyue Jiang, Yu Liu, An Guo et al.· European Conference on Objec...· 1 citation
MGQL is presented, the first mechanized, small-step operational semantics for a substantial read-only fragment of GQL that is grounded in the ISO/IEC 39075 standard, and it is proved that the type system is sound, ensuring an end-to-end guarantee of well-formed queries yielding results that conform to their declared schemas.