2025/02/03 by Samuel Teuber, Teuber, Samuel, Bernhard Beckert +1 · 1 citation
Business, Management and Accounting · Computer Science · Decision Sciences · #Artificial Intelligence (cs.AI) #Business Process Modeling and Analysis #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Machine Learning (cs.LG) #Model-Driven Software Engineering Techniques #Simulation Techniques and Applications #Software Engineering (cs.SE)
paper · pdf · doi:10.48550/arxiv.2502.01573
openalex publication_date 2025/02/03 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Recent work has shown that Large Language Models (LLMs) are not only a suitable tool for code generation but also capable of generating annotation-based code specifications. Scaling these methodologies may allow us to deduce provable correctness guarantees for large-scale software systems. In comparison to other LLM tasks, the application field of deductive verification has the notable advantage of providing a rigorous toolset to check LLM-generated solutions. This short paper provides early results on how this rigorous toolset can be used to reliably elicit correct specification annotations from an unreliable LLM oracle.