論文の概要: Verifiable Checks for Business Rule Consistency
- arxiv url: http://arxiv.org/abs/2608.00396v1
- Date: Sat, 01 Aug 2026 02:22:38 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-06 14:58:59.412085
- Title: Verifiable Checks for Business Rule Consistency
- Title(参考訳): ビジネスルール整合性の検証可能なチェック
- Abstract要約: SMTソルバを用いた一貫性チェックのためのツールおよびフレームワークであるSIRNAを提案する。
本稿では,大規模言語モデル(LLM)と形式的検証手法を組み合わせた3部システムについて述べる。
- 参考スコア(独自算出の注目度): 1.0439136407307046
- License: http://creativecommons.org/licenses/by-nc-nd/4.0/
- Abstract: 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.
- Abstract(参考訳): ビジネスルールの自然言語ドキュメントと内部実装の進化の間の一貫性を維持することは、大規模システムにおいて重要な課題である。
SMTソルバを用いた一貫性チェックのためのツールおよびフレームワークであるSIRNAを提案する。
税制領域におけるコスト計算のケーススタディを用いて,大規模言語モデル(LLM)と形式的検証手法を組み合わせた3部構成のシステムを実証した。
SIRNAは自然言語の文書をLSMを使って候補のSMT式に変換し、その後に翻訳の検証を行う。
そして、対応するビジネスルールを等価なSMT表現に変換し、自然言語の形式化に対して検証する。
本手法は,自然言語ドキュメンテーションとプログラム実装の両方にビジネスロジックが存在する領域に一般化可能である。
ベースライン評価と比較すると、SIRNAは偽陽性と偽陰性の数を大幅に減らし、その発見に説明可能性を与えている。
関連論文リスト
- SEDCoT: Enhancing LLM-Based COBOL Code Translation via Symbolic Execution and Delta Debugging [49.898541267264115]
古い技術や疎結合なドキュメンテーション、開発者の引退などによって、メンテナンスはますます難しくなっている。
従来のルールベースのトランスコンパイラは、読み書きが難しい出力を出力する。
本稿では,新しいC言語翻訳フレームワークであるSEDCoTを提案する。
論文 参考訳(メタデータ) (2026-07-05T03:07:10Z) - Reasoning over Grammar: Can Synthetic Linguistic Reasoning Traces Enhance Low-Resource Machine Translation? [49.7935995447581]
我々は,低リソース機械翻訳が言語解析と文法推論の中間段階の構造化の恩恵を受けるか検討する。
本稿では,Universal Dependencies Treebank,Dictionary,Gram-rule Bankから,ステップバイステップの言語推論トレースを自動的に生成するパイプラインを提案する。
その結果,言語的推論の痕跡は推論時ガイダンスとして最も有効であることが示唆された。
論文 参考訳(メタデータ) (2026-06-02T15:36:12Z) - Beyond BLEU: A Semantic Evaluation Method for Code Translation [2.3802148866231057]
本研究では,コード翻訳タスクに対する新しい評価手法を提案し,表面レベルの文字列類似性に対する意味的等価性を強調した。
正しい実行結果を生成する翻訳の割合として定義される意味的正当性スコアを導入する。
BLEUスコアは意味的正当性と無視できる相関を示した。
論文 参考訳(メタデータ) (2026-05-06T17:14:33Z) - Job Skill Extraction via LLM-Centric Multi-Module Framework [51.37063712967151]
本稿では,意味検索,文脈内学習,教師付き微調整を組み合わせたLLM中心のフレームワークであるSRICLを提案する。
SRICLは、6つの公的なスパンラベル付きジョブアド文のコーパスにおいて、GPT-3.5よりも相当なSTRICT-F1の改善を達成し、ベースラインを加速し、無効なタグと幻覚したスパンを激減する。
論文 参考訳(メタデータ) (2026-04-23T10:46:07Z) - Improving Symbolic Translation of Language Models for Logical Reasoning [14.474630644806723]
小さな言語モデル(LM)は、しばしば自然言語(NL)を一階述語論理(FOL)に変換するのに苦労する。
既存のアプローチは通常、これらのエラーを修正するために自己イテレーションに依存するが、そのような方法は基礎となるモデルの能力に大きく依存する。
本稿では,予測を述語生成とFOL翻訳の2段階に分割し,モデル動作の制御性を高めるインクリメンタル推論を提案する。
論文 参考訳(メタデータ) (2026-01-14T12:47:14Z) - PLSemanticsBench: Large Language Models As Programming Language Interpreters [31.611330217819713]
大規模言語モデル(LLMs)がコード推論に長けているため、自然な疑問が生じる: LLMはプログラム(つまり、インタプリタとして振舞う)を純粋にプログラミング言語の形式的意味論に基づいて実行できるか?
本稿では, 命令型言語IMPを用いて, 小ステップ操作意味論 (SOS) と書き直しに基づく操作意味論 (K-semantics) によって定式化されている問題について検討する。
本稿では,Human-Written,LLM-Translated,Fuzzer-Generatedの3つの評価セットを提案する。
論文 参考訳(メタデータ) (2025-10-03T18:23:26Z) - Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。
有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。
生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
論文 参考訳(メタデータ) (2025-07-22T08:13:01Z) - Verifiable Natural Language to Linear Temporal Logic Translation: A Benchmark Dataset and Evaluation Suite [8.325455397285873]
時相論理(TL)翻訳システムに対する最先端自然言語(NL)の実証評価は,既存のベンチマークにおいてほぼ完全な性能を示す。
本稿では,自動NL-to-LTL翻訳の検証と妥当性を評価する統一ベンチマークであるVerifiable Linear Temporal Logic Benchmark (VLTL-Bench)を紹介する。
論文 参考訳(メタデータ) (2025-07-01T15:41:57Z) - Lost in Literalism: How Supervised Training Shapes Translationese in LLMs [51.04435855143767]
大規模言語モデル(LLM)は機械翻訳において顕著な成功を収めた。
しかし、過度にリテラルと不自然な翻訳を特徴とする翻訳は、依然として永続的な課題である。
我々は、黄金の基準を磨き、不自然なトレーニングインスタンスをフィルタリングするなど、これらのバイアスを軽減する方法を導入する。
論文 参考訳(メタデータ) (2025-03-06T12:14:45Z) - $\forall$uto$\exists$val: Autonomous Assessment of LLMs in Formal Synthesis and Interpretation Tasks [21.12437562185667]
本稿では,形式構文を自然言語に翻訳する際のLLM評価のスケールアップ手法を提案する。
我々は、文脈自由文法(CFG)を用いて、その場で配布外のデータセットを生成する。
我々はまた、このパラダイムの実現可能性と拡張性を示すために、複数のSOTAクローズドおよびオープンソースLCMの評価を行う。
論文 参考訳(メタデータ) (2024-03-27T08:08:00Z) - How Proficient Are Large Language Models in Formal Languages? An In-Depth Insight for Knowledge Base Question Answering [52.86931192259096]
知識ベース質問回答(KBQA)は,知識ベースにおける事実に基づいた自然言語質問への回答を目的としている。
最近の研究は、論理形式生成のための大規模言語モデル(LLM)の機能を活用して性能を向上させる。
論文 参考訳(メタデータ) (2024-01-11T09:27:50Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。