形式仕様変換2026/8/5arXiv:2608.05439v1

SCP-NL2TL: 自然言語から時相論理仕様への選択的適合予測と意味検証

SCP-NL2TL: Selective Conformal Prediction with Semantic Verification for Natural Language to Temporal Logic Specifications

シェア:X Threads Facebook LINE はてブ Bluesky

自然言語の指示を形式仕様に変換する際、信頼できない翻訳を拒否する選択的翻訳フレームワークを提案。逆翻訳の忠実度と翻訳の分散を組み合わせたスコアで信頼性を評価し、適合予測で誤受理率を制御する。

詳しい要約

1. どんなもの？

自然言語命令をロボットや自律システムが計画・推論・形式検証に利用可能な形式仕様（Temporal Logic）へ翻訳する際に、翻訳結果の信頼性を判定し、不確実な場合には翻訳を棄権（abstain）する選択的翻訳フレームワークを提案する。

2. 先行研究と比べてどこがすごい？

既存の翻訳モデルは入力に対して常に仕様を生成するが、本手法は選択的予測（selective conformal prediction）に着想を得て、生成だけでなく信頼性の判定も行う点が新しい。また、信頼性スコアとして、仕様を自然言語に逆翻訳した際の忠実度と、意味的に等価な繰り返し翻訳の分散という2つの相補的なブラックボックス信号を用いる点が独自性。

3. 技術・手法の肝は？

信頼性スコアは、逆翻訳の忠実度と、意味的等価性を考慮した繰り返し翻訳の分散の2信号を組み合わせて計算する。Conformal risk controlにより、誤った仕様を受け入れる率に分布フリーの上限を保証しつつ、受け入れか棄権かを決定する。さらに、命令埋め込みに対するconformal anomaly detectorを用いて、分布外入力（out-of-distribution）を翻訳前に検出する。

4. どうやって有効だと検証した？

Signal Temporal Logic (STL)、Linear Temporal Logic (LTL)、geometric Spatio-Temporal Logic (SpaTiaL)の3つの形式仕様言語で実験し、翻訳の信頼性向上、評価したcross-tier shifts下でのロバスト性、不確実性を考慮した棄権の有効性を実証した。

5. 議論はある？

要旨からは、提案手法の限界や特定の条件下での性能低下などについての議論は不明。ただし、分布フリーの保証があるものの、実際の適用にはスコア関数の設計やconformal calibrationのデータ依存性などが影響する可能性が考えられるが、要旨には明記されていない。

6. 次に読むべき論文は？

要旨で参照されている研究は明示されていないが、関連手法としてselective conformal prediction、conformal risk control、および自然言語から形式仕様への翻訳（NL2TL）に関する既存研究が挙げられる。具体的には、Temporal Logicへの翻訳モデルや、conformal predictionの基礎論文が該当する。

※ AIが要旨から生成した要約です。正確性は原文をご確認ください。

著者: Yixuan Wang, Licheng Luo, Yu Fu, Kaidi Xu, Yue Dong, Mingyu Cai

分類: cs.AI, cs.LG

原文アブストラクト

Translating natural language instructions into machine-interpretable formal specifications enables robots and autonomous systems to plan, reason, and formally verify their behavior. However, existing translation models typically generate a specification for every input, even when the result is unreliable or fails to capture the user's intent, creating risks in safety-critical applications. Inspired by selective conformal prediction, we propose a selective translation framework that not only generates formal specifications but also determines when they can be trusted. Reliability is scored by two complementary black-box signals, the fidelity of the specification back-translated into natural language and the dispersion of repeated translations under exact semantic equivalence, which fail on different errors and jointly separate incorrect translations more sharply than either alone. Conformal risk control calibrates this score into a decision that accepts a specification or abstains, with a distribution-free bound on the rate at which incorrect specifications are accepted for execution, and a conformal anomaly detector on instruction embeddings screens out-of-distribution inputs before any translation is attempted. The proposed framework is general across formal specification languages, with experiments on Signal Temporal Logic (STL), Linear Temporal Logic (LTL), and geometric Spatio-Temporal Logic (SpaTiaL) demonstrating improved translation reliability, robustness under the evaluated cross-tier shifts, and effective uncertainty-aware abstention. This work establishes a foundation for trustworthy natural language interfaces by enabling AI systems to recognize when generated specifications may not be reliable.

arXivで原文を読む →arXiv概要ページ

← 論文一覧