Verifiable Checks for Business Rule Consistency
SIRNA 可自动核对自然语言业务规则与 DSL 代码是否同义,并给出反例:账单、税务、合规系统常同时维护自然语言文档和可执行 DSL;两者一旦语义跑偏,人工审查很难系统发现。SIRNA 的做法是:用 LLM 把 NL 文档转成 SMT 公式并先校验翻译,再把 DSL 等价编码成 SMT,最后交给 SMT 求解器判一致、列反例。
NL 文档与 DSL 代码的语义对齐过去主要靠人工,特殊例外很容易漏掉;SIRNA 把 NL 经 LLM 转成受校验的 SMT 公式,把 DSL 等价编码成 SMT,再由求解器判定并生成反例。在加拿大联邦所得税案例中,它定位到 DSL 对 SIN≥900000000 的零税逻辑未写入 NL 文档,反例为 income=−200/29 时两侧输出 −1 与 0。
核心判断:把“受校验的 NL→SMT 翻译”和“DSL 的等价 SMT 编码”交给同一个 SMT 求解器比较,能把文档与代码的语义不一致变成可判定问题,并用反例说明偏差条件;在税务案例中作者报告假阳性与假阴性较基线显著减少。
1. 老问题:NL 文档与 DSL 实现靠人工对齐,账单、税务等场景覆盖不全;基线假阳性/假阴性偏高,且缺少反例。 2. 方法与受控检查:LLM 译 NL 成 SMT-LIB 后先过自动推理校验器;DSL 做等价 SMT 编码;求解器判等价,θ 默认 23。 3. 决定性结果与动作:加拿大所得税例中检出 SIN≥900000000 零税例外;income=−200/29 时 −1 对 0;按反例改文档、改代码或标记例外。
评估场景是加拿大联邦所得税成本计算:NL 描述渐进五档税率,DSL 另有 SIN 条件逻辑。系统把结果分成四类:欠规范导致的虚假不一致、需要修的真实偏差、有意差异、一致。定位案例为 DSL 中 special 变量触发 SIN≥900000000 时税额归零,NL 未声明;反例 income=−200/29,NL FinalTaxes=−1,DSL final_tax=0。比较结论只到“较基线显著减少假阳性与假阴性”,未给数值。
- 它要解决什么
- 实际问题是:NL 业务规则文档和 DSL 实现长期并存,如何不靠人工逐条比对,自动发现“文档没说但代码做了”或“文档要求但代码没做”的语义偏差?
- 研究路径
- 机制分五步:LLM 先把 NL 规则译成候选 SMT-LIB;自动推理校验器检查这步翻译;DSL 经可靠等价变换得到语义相同的 SMT-LIB;SMT 求解器比较两侧公式是否等价;若不等价,输出具体变量赋值和两侧输出差,并枚举发散条件,让用户决定修文档、修代码或承认为有意例外。
- 这对工程意味着什么
- 第一步:挑一个账单或税务规则对,补齐变量规格和取值范围,用默认 θ=23 跑一次 SIRNA,看反例能否复现。要避开的捷径:不要拿 LLM 生成的 SMT 公式直接当标准答案;未校验翻译会把误报或漏报带进最终结论。
- 证据定位
- 在加拿大联邦所得税案例中,DSL 用 special 变量让 SIN≥900000000 时税额归零,但 NL 文档没有写这个例外。SIRNA 给出反例:income=−200/29 时,NL 输出 FinalTaxes=−1,DSL 输出 final_tax=0。作者称相较基线假阳性与假阴性显著减少;具体数值未在摘录中提供。(筛选维度:形式化验证、可复核评测)
- 适用边界
- 边界要说明白:摘录只给加拿大联邦税务单一领域,泛化未量化;变量规格和取值范围需要人工配置,是前置领域成本;θ 对结果影响未量化;假阳性、假阴性的具体数值未在供给文本中给出。
方法与英文摘要
输入是(NL 文档,DSL 代码)对、变量规格、取值范围和置信阈值 θ,默认 23。配置阶段由 LLM 生成候选 SMT-LIB 公式,再经自动推理校验器检查翻译质量;评估阶段把 DSL 等价变换为 SMT-LIB,由 SMT 求解器比较两侧语义。发现不一致时输出反例,并枚举实现偏离文档的条件。示例领域是加拿大联邦所得税。
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.