技術的概要：REASONSTL

問題定義

シグナル時相論理（STL）は、サイバーフィジカルシステム（CPS）および自律システムにおける実数値シグナル上の時空間要件を指定するために不可欠な形式言語である。STL は厳密な検証と合成を可能にするが、実務者は通常、要件を自然言語（NL）で表現する。これらの NL 記述を実行可能な STL 数式に変換することは、重要なボトルネックとなっている。

既存のアプローチは重大な限界に直面している：

• 手動仕様定義： 専門知識を必要とし、労働集約的であり、拡張性が低い。
• 商用 LLM API： 能力は高いものの、高いトークンコストを伴い、第三者へ機密性の高いシステム要件を送信することによるプライバシー上の懸念が生じる。
• 従来の自動化手法：
  • DeepSTL はゼロから訓練されたニューラル機械翻訳に依存しており、汎化能力が制限される。
  • KGST はプロプライエタリな API を含むハイブリッドパイプラインを使用しており、プライバシーおよびコスト上の問題が生じる。
  • RESTL はローカルで動作するが、中間推論なしに直接数式を生成するため、解釈可能性と正確性が損なわれる。
• 技術的課題： NL から STL への翻訳には、構文上の妥当性だけでなく、意味的グラウンディング、計算を考慮した推論（例：単位変換、算術計算）、および時相区間とドメイン固有のシグナルの正確な処理が必要である。閾値や演算子における微小な誤りは、誤った意味論につながる可能性がある。

手法：REASONSTL

著者らは、計算を考慮した NL から STL への生成のために設計された、ローカルかつツール拡張型のフレームワークであるREASONSTLを提案する。中核となる哲学は、単一のステップによるシーケンス予測に依存するのではなく、翻訳プロセスを明示的な推論、決定論的ツール呼び出し、構造化された数式構築に分解することである。

1. ツール拡張型生成

生テキストを生成する代わりに、モデルは推論セグメント、ツール呼び出し、およびツールの出力からなる構造化されたロールアウトを生成し、構造化された STL JSON ツリーで終わる。

• ツールセット： フレームワークは、コンパクトで型付けされた決定論的ツールのセットを利用する：
  • parse_duration：時間表現を正規化する（例：「30 分」→ 1800）。
  • convert_unit：物理単位を変換する（例：ft → m）。
  • eval_math_expr：閾値の算術式を評価する。
  • calc_time_diff：タイムスタンプから時間差を計算する。
• デカップリング： この設計は、言語的解釈と構造的推論を正確な数値計算から分離し、プロセスを検査可能かつ検証可能にする。

2. 結果境界付きプロセス報酬最適化

REASONSTL は、中間のツール使用軌道と最終的な数式構築の両方を監督する新しい訓練戦略を導入する。

• プロセス報酬： 中間段階（ツール呼び出し、推論）には、局所的な正しさ（引数の妥当性、実行可能性、一貫性）に基づいて報酬が割り当てられる。
• 結果境界設定： 重要なのは、中間報酬が最終 STL 数式の正しさによって上限設定される点である。最終数式が誤っている場合、中間ステップで達成可能な最大報酬は減少する。これにより、誤った最終結果につながる「もっともらしいが意味的に無効な」推論痕跡が強化されるのを防ぐ。
• プレフィックスマスキング： 中間ステップが失敗した場合、それに依存する後続の段階は後方更新からマスクされ、モデルが早期にエラーを停止または修正することを学習する。
• 最適化： フレームワークは、これらの境界付き報酬に基づいてモデルを最適化するために、グループ相対方策目的（PPO に類似するが、尤度比クリッピングを伴わない）を使用する。

3. STL-BENCH：新しいベンチマーク

計算を考慮した NL から STL への生成を評価するために、著者らは実世界の CPS シグナルに基づいたバイリンガル（英語/中国語）ベンチマークであるSTL-BENCHを導入する。

• 特徴： 6 つの工学ドメイン、33 のシナリオ、および 41 のドメインに根ざしたシグナル変数を網羅する。
• 複雑性： サンプルの 73% が中間計算（ツール使用）を必要とする。ツール使用軌道、時相正規化、および単位変換の明示的な注釈が含まれる。
• 構造： STL 数式は、スキーマ検証と再帰的構造的マッチングを可能にする JSON ツリーとして表現され、単純な文字列マッチングを超えている。
• 検証： データセットは、テンプレートにアンカーされた生成、ルールベースの検証、および層化された人間による監査を通じて構築され、高品質なラベルを確保している。

主要な貢献

1. ローカルツール拡張型フレームワーク： REASONSTL は、多段階推論と決定論的ツール呼び出しを通じて NL を STL に変換するローカルかつオープンソースのフレームワークであり、時相正規化、単位変換、および算術評価を明示的に処理する。
2. 結果境界付きプロセス監督： 中間のツール使用軌道と最終的な数式構築を共同で監督する訓練戦略であり、最終的な正しさで中間報酬を境界設定することで、無効な推論経路が強化されるリスクを低減する。
3. 計算を考慮したベンチマーク（STL-BENCH）： ドメインに根ざしたシグナル、物理単位、算術的制約、および明示的なツール使用注釈を備えたバイリンガルベンチマークであり、計算を考慮した生成の厳密な評価を可能にする。

実験結果

実験は、確立されたDeepSTLベンチマークと新しいSTL-BENCHの両方で行われた。

• DeepSTL における性能： REASONSTL-DIRECT（直接生成バリアント）で訓練された 4B パラメータモデル（Qwen3-4B）は、81.43% の数式精度と82.57% のフォーマット精度を達成した。これは、最強のブラックボックス API ベースライン（Claude-Opus-4.7）を 15 ポイント以上上回り、以前の最先端（RESTL）を約 21 ポイント改善した。
• STL-BENCH における性能：
  • 完全な REASONSTL モデル（推論とツールを備えた）は、英語で51.0%、中国語で**47.0%**の数式精度を達成し、ベースモデルおよび慎重にプロンプトされた API ベースライン（例：GPT-5.4、Kimi-K2.6）の両方を上回った。
  • 人間による検証： 言語あたり 100 サンプルのサブセットにおいて、REASONSTL はプロプライエタリモデルの性能と同等かそれ以上であり、英語で53%、中国語で**51%**の精度を達成した。
  • 汎化： 手書きでテンプレートフリーのテストセットにおいて、REASONSTL は最高水準の数式精度（54%）を達成し、強力な API ベースラインをわずかに上回りながら、一部の商用モデルよりも高い推論スループットを維持した。
• アブレーション研究： 結果は、教師あり微調整（SFT）がフォーマットの初期化に寄与する一方で、プロセス報酬とツール拡張型推論を伴う強化学習（RL）が性能向上の主要な駆動力であることを確認した。

意義と主張

本論文は、REASONSTL が形式仕様策定のための透明性が高く、低コストでプライバシーを保護する代替手段を提供すると主張している。パイプライン全体をローカルかつオープンソースに維持することで、商用 LLM API に伴うプライバシーとコストの障壁に対処している。

著者らは、フレームワークがタスクを決定論的計算と構造化された推論に分解する能力により、生成プロセスが検査可能かつ検証に適していることを強調している。これは、安全クリティカルな CPS アプリケーションにとって重要な特徴である。システムは最先端の性能を達成しているが、著者らは控えめに、特に残存する意味論的誤りをドメインの専門家がレビューする必要がある安全クリティカルな文脈においては、現在、完全自律的な専門仕様設計の代替手段というよりも、人間がループ内に入るドラフティングアシスタントとして最も適していると指摘している。