一句话：用 LLM 仅从测试代码与动态执行轨迹（黑盒）推断 JML 形式规约，并以有界模型检验迭代精化。
形式规约能提供强保证，但手工编写代价高昂。已有基于 LLM 的方法多依赖源码（白盒）推断规约，这在工业落地时因知识产权风险与部署成本而受阻。本文提出仅从测试代码与动态执行轨迹中推断候选规约：LLM 只能观察到程序接口、选定输入以及对应的输出或状态变化，实现内部细节完全隐藏。候选规约随后在本地用有界模型检验进行验证，验证反馈用于引导迭代精化。在 SpecGenBench 基准上的初步结果显示，测试足以引导 LLM 生成有意义的 Java 建模语言（JML）规约，同时也暴露出检验器兼容性与诊断反馈质量是可靠精化的关键挑战。
Formal specifications offer strong guarantees, but remain costly to write manually. Recent LLM-based approaches automate this by inferring specifications from source code, yet their reliance on white-box access poses barriers to industrial adoption due to intellectual property risks and deployment costs. Our approach uses LLMs to infer candidate specifications solely from test code and dynamic execution traces: the LLM observes only the program interface, selected inputs, and corresponding outputs or state changes, while the implementation internals remain hidden. Candidate specifications are validated locally using bounded model checking, with feedback guiding iterative refinement. Initial results on the SpecGenBench benchmark suggest that tests can guide LLMs towards meaningful Java Modeling Language specifications, while also highlighting checker compatibility and diagnostic feedback as key challenges for reliable refinement.
@inproceedings{paperbot12318,
title = {Can Formal Specifications Be Synthesized from Tests Alone?},
author = {Tianhai Liu and Maximilian Müller and Tobias Hey and Vitus Lüntzel and Muhammad Minhas and Anne Koziolek and Bernhard Beckert},
booktitle = {ASE},
year = {2026},
doi = {10.1145/3832783.3834549}
}