一句话：提出神经符号 agent LHC，用 LLM 自动生成整包精化类型标注并由 LiquidHaskell 验证，大幅降低形式验证标注成本。
精化类型是 Floyd-Hoare 逻辑的类型化推广，能以模块化方式静态保证软件的正确性、安全性与安全性属性。然而其表达力与模块化要求开发者手工为每个函数编写可能很复杂的类型规范，成本极高。本文提出 LHC，一个神经符号 agent：它利用 LLM 为整个包或模块中的所有函数自动生成精化类型标注，并以精化类型检查器 LiquidHaskell 作为 oracle 验证生成规范的正确性。作者构建了三个使用精化类型强制数据结构不变式到低级内存安全等性质的真实 Haskell 包数据集，用于评估 LHC。这些包此前需要专家数天到数周才能完成标注。实验表明，即使使用 30 亿参数的 StarCoder 等相对较小的模型，通过微调与精心选择的上下文，该神经符号 agent 能在数小时内自动为整个库中最多 94% 的函数生成精化类型，说明 LLM 可显著减少使用形式验证所需的人力。
Refinement types, a type-based generalization of Floyd-Hoare logics, are an expressive and modular means of statically ensuring a wide variety of correctness, safety, and security properties of software. However, their expressiveness and modularity means that to use them, a developer must laboriously annotate all the functions in their code with potentially complex type specifications that specify the contract for that function. We present LHC, a neurosymbolic agent that uses LLMs to automatically generate refinement type annotations for all the functions in an entire package or module, using the refinement type checker LiquidHaskell as an oracle to verify the correctness of the generated specifications. We curate a dataset of three Haskell packages where refinement types are used to enforce a variety of correctness properties from data structure invariants to low-level memory safety and use this dataset to evaluate LHC. Previously these packages required expert users several days to weeks to annotate with refinement types. Our evaluation shows that even when using relatively smaller models like the 3 billion parameter StarCoder LLM, by using fine-tuning and carefully chosen contexts, our neurosymbolic agent generates refinement types for up to 94% of the functions across entire libraries automatically in just a few hours, thereby showing that LLMs can drastically shrink the human effort needed to use formal verification.
DOI 原文 ·
@inproceedings{paperbot8896,
title = {Neurosymbolic Modular Refinement Type Inference},
author = {Georgios Sakkas and Pratyush Sahu and Kyeling Ong and Ranjit Jhala},
booktitle = {ICSE},
year = {2025},
doi = {10.1109/icse55347.2025.00090}
}