論文の概要: Validating ETCS Data with the B Mathematical Language: An Industrial Pipeline and a Blueprint for LLM Integration
- arxiv url: http://arxiv.org/abs/2607.26111v1
- Date: Tue, 28 Jul 2026 15:05:50 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-30 21:06:25.432187
- Title: Validating ETCS Data with the B Mathematical Language: An Industrial Pipeline and a Blueprint for LLM Integration
- Title（参考訳）: B数理言語によるETCSデータの検証:産業用パイプラインとLCM統合のための青写真
- Abstract要約: 本稿では, CLEARSY, ValidAItionにおける産業研究の現状について報告する。
この作業は、CLEARSYですでに使われているフレームワークと会話によるオーサリングループを組み合わせて、新しい形式的なメソッドを提案する。
論文は、これまでに集められた証拠に基づいて、Bの数学的言語の形式的な規則は真実の源であり続けなければならないと論じている。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Can large language models participate in the production and validation of ERTMS/ETCS data without undermining the certification arguments required by CENELEC EN 50128/50716? ERTMS/ETCS is a distributed safety-critical system (trackside, onboard, radio-block centre) whose behaviour is parameterised by large volumes of data drawn from the UNISIG Subsets; errors in that data propagate through the distributed architecture. This paper reports the current status of an ongoing industrial research effort at CLEARSY, ValidAItion, that bridges the ERTMS Operational Simulator to the CLEARSY Data Solver and applies rules expressed in the B mathematical language to that trackside data. During construction, a large language model (Claude) has authored the rule corpus and the parsers through a Model Context Protocol server; every proposal is adjudicated by the downstream toolchain and by systematic human review, and the toolchain has already rejected a syntactically valid but semantically illegal generated scenario. The contribution is architectural and industrial, not algorithmic: the work combines frameworks already in use at CLEARSY (CLEARSY Data Solver, ERTMS Operational Simulator) with a conversational authoring loop, rather than proposing a new formal method. It is a progress report: rule coverage is growing, the human-review campaign is underway, and the quantitative results will be published separately. The paper argues, on the evidence gathered so far, that formal rules in the mathematical language of B must remain the source of truth, while the language model serves as the fenced assistant in a distributed safety-critical railway system: AI proposes, the formal oracle disposes, the human confirms.
- Abstract（参考訳）: 大規模な言語モデルは、CENELEC EN 50128/50716の要求する認証引数を損なうことなく、RTMS/ETCSデータの生成と検証に参加できるだろうか?
ERTMS/ETCSは、UNISIGサブセットから引き出された大量のデータによって振る舞いがパラメータ化される分散安全クリティカルシステム(トラックサイド、オンボード、ラジオブロックセンター)である。
本稿では,ERTMS 操作シミュレータを CLEARSY データソルバーにブリッジし,B 数式で表される規則をトラックサイドデータに適用する CLEARSY, ValidAItion における産業研究の現状について報告する。
構築中、大規模な言語モデル(Claude)が、Model Context Protocolサーバを通じてルールコーパスとパーサを作成した。すべての提案は、下流のツールチェーンと体系的なヒューマンレビューによって調整され、ツールチェーンは、構文的に有効だがセマンティックに違法に生成されたシナリオをすでに拒否している。
この研究は、CLEARSY(CLEARSY Data Solver, ERTMS Operational Simulator)ですでに使われているフレームワークと、新しい形式的なメソッドを提案するのではなく、会話によるオーサリングループを組み合わせたものである。
ルールカバレッジが増加し、人間レビューキャンペーンが進行中であり、定量結果が別々に発表される、という進捗報告である。
論文は、これまでに収集された証拠に基づき、Bの数学的言語における公式な規則は真実の源であり続け、言語モデルは分散安全クリティカル鉄道システムにおけるフェンス付きアシスタントとして機能している、と論じている。
関連論文リスト
- Formal-Method-Guided Vibe Coding: Closing the Verification Loop on AI-Generated Safety-Critical Software Through Model-Driven Engineering [40.048798975817924]
バイブコーディングは高速で、低臨界のコンシューマソフトウェアには適しています。
DO-178C、IEC 61508、ISO 26262によって管理される安全クリティカルなシステムでは、認証への道は提供されない。
フォーマルな検証を通じてビブコーディングをガイドするクローズドループパイプラインであるForgeを紹介します。
論文 参考訳（メタデータ） (2026-06-21T10:01:45Z) - BarrierBench : Evaluating Large Language Models for Safety Verification in Dynamical Systems [4.530582224312311]
バリア証明書合成のための LLM ベースのエージェントフレームワークを提案する。
このフレームワークは自然言語推論を使用して、候補証明書を提案し、洗練し、検証する。
BarrierBenchは、線形、非線形、離散時間、連続時間設定にまたがる100の動的システムのベンチマークである。
論文 参考訳（メタデータ） (2025-11-12T14:23:49Z) - 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) - Boosting the Capabilities of Compact Models in Low-Data Contexts with Large Language Models and Retrieval-Augmented Generation [2.9921619703037274]
本稿では,形態素解析の言語タスクにおいて,より小さなモデルの出力を補正するために,大言語モデル(LLM)を基盤とした検索拡張生成(RAG)フレームワークを提案する。
データ不足や訓練可能なパラメータの不足を補うために,言語情報を活用するとともに,LLMを通して解釈・蒸留された記述文法からの入力を許容する。
コンパクトなRAG支援モデルがデータスカース設定に極めて有効であることを示し、このタスクとターゲット言語に対する新しい最先端技術を実現する。
論文 参考訳（メタデータ） (2024-10-01T04:20:14Z) - ConVerSum: A Contrastive Learning-based Approach for Data-Scarce Solution of Cross-Lingual Summarization Beyond Direct Equivalents [4.029675201787349]
言語間の要約は自然言語処理の洗練された分野である。
高品質なCLSデータがない場合、CLSには実現可能な解決策がない。
コントラスト学習のパワーを活かしたCLSのための新しいデータ効率のアプローチであるConVerSumを提案する。
論文 参考訳（メタデータ） (2024-08-17T19:03:53Z) - CELA: Cost-Efficient Language Model Alignment for CTR Prediction [70.65910069412944]
CTR(Click-Through Rate)予測は、レコメンダシステムにおいて最重要位置を占める。
最近の取り組みは、プレトレーニング言語モデル(PLM)を統合することでこれらの課題を緩和しようとしている。
CTR予測のためのtextbfCost-textbfEfficient textbfLanguage Model textbfAlignment (textbfCELA)を提案する。
論文 参考訳（メタデータ） (2024-05-17T07:43:25Z) - FLIP: Fine-grained Alignment between ID-based Models and Pretrained Language Models for CTR Prediction [49.510163437116645]
クリックスルーレート(CTR)予測は、パーソナライズされたオンラインサービスにおいてコア機能モジュールとして機能する。
CTR予測のための従来のIDベースのモデルは、表形式の1ホットエンコードされたID特徴を入力として取る。
事前訓練された言語モデル(PLM)は、テキストのモダリティの文を入力として取る別のパラダイムを生み出した。
本稿では,CTR予測のためのIDベースモデルと事前学習言語モデル(FLIP)間の細粒度特徴レベルのアライメントを提案する。
論文 参考訳（メタデータ） (2023-10-30T11:25:03Z) - SILO Language Models: Isolating Legal Risk In a Nonparametric Datastore [159.21914121143885]
推論中にこのリスクパフォーマンストレードオフを管理する新しい言語モデルであるSILOを提案する。
SILOは(1)オープンライセンスコーパス(OLC)上でパラメトリックLMをトレーニングすることで構築されます。
データストアへのアクセスはドメインのパフォーマンスを大幅に改善し、PileでトレーニングされたLMでパフォーマンスギャップの90%を閉じる。
論文 参考訳（メタデータ） (2023-08-08T17:58:15Z) - Cross-Lingual NER for Financial Transaction Data in Low-Resource
Languages [70.25418443146435]
半構造化テキストデータにおける言語間名前認識のための効率的なモデリングフレームワークを提案する。
我々は2つの独立したSMSデータセットを英語とアラビア語で使用し、それぞれが半構造化された銀行取引情報を持っている。
わずか30のラベル付きサンプルにアクセスすることで、我々のモデルは、英語からアラビア語までの商人、金額、その他の分野の認識を一般化することができる。
論文 参考訳（メタデータ） (2023-07-16T00:45:42Z) - A Unified Strategy for Multilingual Grammatical Error Correction with
Pre-trained Cross-Lingual Language Model [100.67378875773495]
本稿では,多言語文法的誤り訂正のための汎用的かつ言語に依存しない戦略を提案する。
我々の手法は言語固有の操作を使わずに多様な並列GECデータを生成する。
NLPCC 2018 Task 2のデータセット(中国語)で最先端の結果を達成し、Falko-Merlin(ドイツ語)とRULEC-GEC(ロシア語)の競合性能を得る。
論文 参考訳（メタデータ） (2022-01-26T02:10:32Z) - Unsupervised Paraphrasing with Pretrained Language Models [85.03373221588707]
教師なし環境で,事前学習した言語モデルを用いて高品質なパラフレーズを生成する訓練パイプラインを提案する。
提案手法は,タスク適応,自己スーパービジョン,動的ブロッキング(Dynamic Blocking)という新しい復号アルゴリズムから構成される。
提案手法は,Quora Question PairとParaNMTの両方のデータセット上で,最先端の性能を達成できることを示す。
論文 参考訳（メタデータ） (2020-10-24T11:55:28Z) - Cross-lingual Information Retrieval with BERT [8.052497255948046]
本稿では、人気のある双方向言語モデルBERTを用いて、英語クエリと外国語文書の関係をモデル化し、学習する。
BERTに基づく深部関係マッチングモデルを導入し,教師の弱い事前学習多言語BERTモデルを微調整して訓練する。
短い英語クエリに対するリトアニア語文書の検索実験の結果、我々のモデルは有効であり、競争ベースラインのアプローチよりも優れていることが示された。
論文 参考訳（メタデータ） (2020-04-24T23:32:13Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。