发表机构
University of Waterloo（滑铁卢大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对大型系统中业务规则自然语言文档与内部实现的一致性检查难题，提出结合LLMs与形式化验证的SIRNA框架，经税务成本计算案例验证，其可减少误报漏报并具备可解释性。
AI 中文摘要
在大型系统中，维护业务规则的自然语言文档与其不断演进的内部实现之间的一致性是一项重大挑战。我们提出SIRNA，一款用于检查此类一致性的工具与框架，它使用SMT求解器实现。以税务领域的成本计算为案例研究，我们展示了一个由三部分构成的系统，该系统将大语言模型（LLMs）与形式化验证方法相结合。SIRNA借助LLMs将自然语言文档转换为候选SMT公式，随后执行检查以验证这些转换结果；接着，将对应的业务规则转换为等效的SMT表示形式，并对照自然语言形式化结果进行验证。我们的方法可推广至业务逻辑同时存在于自然语言文档与程序化实现的领域。与基线评估相比，SIRNA显著减少了误报和漏报的数量，同时为其发现结果提供可解释性。
英文摘要
Maintaining consistency between natural language documentation of business rules and their evolving internal implementations is a significant challenge in large-scale systems. We present SIRNA, a tool and framework for checking such consistency using SMT solvers. Using the case study of cost calculations in tax domains, we demonstrate a three-part system that combines large language models (LLMs) with formal verification methods. SIRNA translates natural language documentation into candidate SMT formulas using LLMs, followed by checks to validate the translations. Then, corresponding business rules are converted into equivalent SMT representations and validated against the natural language formalizations. Our method is generalizable to domains where business logic exists in both natural language documentation and programmatic implementation. Compared to baseline evaluations, SIRNA significantly reduces the number of false positives and false negatives while offering explainability for its findings.
CommentsFormal Methods in Computer-Aided Design 2026
