用AI+形式化验证，自动检查业务规则文档与代码的一致性。
Verifiable Checks for Business Rule Consistency
- 用大模型将自然语言规则转为SMT公式，再验证转换正确性。
- 在税务成本计算场景中，误报率和漏报率显著降低。
- 适合需要高可信度的金融、税务等合规性系统开发者。
在大规模系统中，保持业务规则的自然语言文档与其内部实现的一致性是一项重大挑战。本文提出SIRNA工具框架，利用SMT求解器实现一致性检查。以税务领域的成本计算为例，构建了三部分系统：首先使用大语言模型（LLMs）将自然语言文档转化为候选SMT公式，并进行翻译验证；随后将实际业务规则转化为等价的SMT表示，并与自然语言形式化结果进行比对。该方法适用于业务逻辑同时存在于自然语言文档和程序实现的领域。相较于基线方法，SIRNA显著降低了误报与漏报数量，并提供可解释的验证结果。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。