可以仅通过测试合成正式规范吗？

正式规范提供了强有力的保证，但手动编写的成本仍然很高。最近基于 LLM 的方法通过从源代码推断规范来自动化这一过程，但由于知识产权风险和部署成本，它们对白盒访问的依赖对工业采用造成了障碍。我们的方法使用 LLM 仅从测试代码和动态执行跟踪推断候选规范：LLM 仅观察程序接口、选定的输入以及相应的输出或状态更改，而实现内部仍然隐藏。使用有界模型检查在本地验证候选规范，并通过反馈指导迭代细化。 SpecGenBench 基准测试的初步结果表明，测试可以引导 LLM 走向有意义的 Java 建模语言规范，同时还强调检查器兼容性和诊断反馈是可靠细化的关键挑战。