一句话：Expecto 用神经符号方法从自然语言意图中自顶向下模块化合成 DSL 形式规约，作为可信赖的规约预言机。
规约驱动开发（SDD）借助大语言模型从自然语言意图生成代码，但自然语言规约本身的歧义性使正确性难以保证。本文提出 Expecto，一个自动从自然语言意图中抽取可信形式化规约的系统，采用神经符号方法融合 LLM 与程序合成技术。其核心思想是自顶向下、模块化的规约合成算法，把复杂的规约抽取任务分解为可管理的单元；规约书写在一个专门设计的 DSL 中，可简洁表达功能需求。这种模块化合成配合精简 DSL 降低了 LLM 的推理复杂度，提升了抽取规约的准确性。实验表明，与整体式、纯 LLM 的方法相比，Expecto 显著提高了抽取规约的准确性与可靠性；在 Defects4J 的真实缺陷程序上，Expecto 生成的形式规约能检出比基线更多的 bug。
Specification-Driven Development (SDD) has emerged as a promising paradigm in software development. This trend is fueled by recent advances in leveraging large language models (LLMs) to generate code from user intents expressed in natural language. However, the reliance on natural language specifications introduces ambiguity and challenges in ensuring correctness. To address these problems, we present Expecto, a system that automatically extracts trustworthy formal specifications from natural language intents. Expecto employs a neuro-symbolic approach, combining the strengths of LLMs and program synthesis techniques. Our key idea is to adopt a top-down, modular specification synthesis algorithm that breaks down the complex task of specification extraction into manageable units. The specifications are written in a domain-specific language (DSL) designed to succinctly express formal specifications of functional requirements. This modular synthesis with a concise DSL reduces the reasoning complexity for LLMs and enhances the accuracy of the extracted specifications. Our results demonstrate that Expecto significantly improves the accuracy and reliability of extracted specifications compared to a monolithic, purely LLM-based approach. Furthermore, when applied to real-world buggy programs in Defects4J, Expecto successfully generates formal specifications that detect more bugs than the baselines.
@article{LeeH26,
title = {Expecto: Extracting Formal Specifications from Natural Language Description for Trustworthy Oracles},
author = {Dongjae Lee and Kihong Heo},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808332}
}