論文の概要: PROVE-RT: Generating Mechanized Theorem Prover Scripts for Real-Time Systems using LLMs

• arxiv url: http://arxiv.org/abs/2608.12762v1
• Date: Thu, 13 Aug 2026 03:12:17 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-08-14 18:29:38.377523
• Title: PROVE-RT: Generating Mechanized Theorem Prover Scripts for Real-Time Systems using LLMs
• Title（参考訳）: PROVE-RT:LLMを用いたリアルタイムシステムのための機械的理論証明スクリプトの生成
• Abstract要約: 本稿では, PROSA/ROCQ スクリプトを生成する LLM 支援フレームワーク PROVE-RT を紹介する。 我々は,1,191のリアルタイムシステム論文から機械化指向コーパスを構築し,134の非公式スケッチと依存関係情報を含む。 キュレートされた評価セットでは、最先端のLLMの直接的なプロンプトは有効なPROSA機構を確実に生成することができず、PROVE-RTは44.7%の成功率を達成する。
• 参考スコア（独自算出の注目度）: 2.6015820133532137
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Schedulability analysis is essential for certifying real-time systems, but existing tests are often developed through pen-and-paper proofs that are difficult to scale, validate, and maintain. Mechanized verification in PROSA/ROCQ offers a rigorous alternative, yet manually constructing such proofs requires substantial domain expertise and proof-engineering effort. Recent successes of large language models (LLMs) across a wide range of tasks make them promising candidates for generating PROSA/ROCQ scripts for mechanized theorem provers. However, state-of-the-art LLMs often lack the PROSA-specific knowledge required to correctly use its modeling abstractions and proof patterns. This paper introduces PROVE-RT, an LLM-assisted framework for generating PROSA/ROCQ scripts to mechanize schedulability analyses in real-time systems literature. PROVE-RT guides generation through dependency-aware informal sketches, retrieval from processed PROSA documentation, staged skeleton generation, and proof completion. We construct a mechanization-oriented corpus from 1, 191 real-time systems papers, containing 13, 134 informal sketches with dependency information. On a curated evaluation set, direct prompting of state-of-the-art LLMs fails to reliably generate valid PROSA mechanizations, whereas PROVE-RT achieves a success rate of 44.7%. These results show that retrieval-guided and staged LLM assistance can improve automated mechanization of schedulability analysis in PROSA/ROCQ.
• Abstract（参考訳）: スケジューリング可能性分析は、リアルタイムシステムの認証に不可欠であるが、既存のテストは、スケール、検証、保守が難しいペンと紙の証明によって開発されることが多い。 PROSA/ROCQの機械的検証は厳密な代替手段を提供するが、そのような証明を手作業で構築するには相当な専門知識と証明工学の努力が必要である。 近年の大規模言語モデル (LLM) の成功により、機械化された定理プローバー用の PROSA/ROCQ スクリプトを生成する候補候補が期待できる。 しかしながら、最先端のLLMは、そのモデリング抽象化と証明パターンを正しく使用するのに必要な、PRSA固有の知識を欠いていることが多い。 本稿では,PLA/ROCQ スクリプトを生成するための LLM 支援フレームワーク PROVE-RT について紹介する。 PROVE-RT は、依存関係を意識した非公式スケッチ、処理された PROSA ドキュメントからの検索、ステージ化されたスケルトン生成、証明完了を通じて生成をガイドする。 我々は,1,191のリアルタイムシステム論文から機械化指向コーパスを構築し,134の非公式スケッチと依存関係情報を含む。 キュレートされた評価セットでは、最先端のLLMの直接的なプロンプトは有効なPROSA機構を確実に生成することができず、PROVE-RTは44.7%の成功率を達成する。 これらの結果から, PROSA/ROCQにおける検索誘導型および段階的LCM支援により,スケジューリング可能性解析の自動機械化が向上することが示唆された。

関連論文リスト

• Automatic Translation of Unstructured Requirements into Linear Temporal Logic through Large Language Models [46.28810845443601]
  本稿では,LTL(Linear Temporal Logic)式を非構造的要求から直接生成することにより,現代市販のLarge Language Models (LLMs) がこのギャップを埋めることができるかどうかを評価する。 本研究は, 構造的に異なる15の異種ベンチマークを用いて, 数発のプロンプト戦略を用いて, 近代LLMの6点について検討した。 その結果,現在の汎用LLMはタスク固有の微調整を伴わずに非構造化NLto-LTLタスクにおいて実質的に有意な性能を達成できることが示唆された。
  論文  参考訳（メタデータ） (2026-08-06T17:13:07Z)
• Beyond the Syntax: Do Security Experts Trust LLMs for NIDS Rule Engineering? [70.17374586573033]
  本稿では,Large Language Models(LLMs)に基づくNIDSルールエンジニアリングを人間中心で調査する。 LLMは構文的に正しい規則を生成するが、専門家は部分的にしか展開できないと考えている。 大規模モデルは構文的に有効な規則を一貫して生成するが、小型モデルはIDSルールの生成にはほとんど効果がない。
  論文  参考訳（メタデータ） (2026-07-07T07:09:56Z)
• PROMISE: Proof Automation as Structural Imitation of Human Reasoning [15.113069562646302]
  ProMISEは,証明状態遷移に対するステートフルな探索として,証明生成を再構成する構造認識フレームワークである。 複数のLLMバックエンドにまたがるSEL4ベンチマークのPROMISEを評価し,SeleneやRangoといった先行システムと比較した。
  論文  参考訳（メタデータ） (2026-04-07T03:49:12Z)
• Assessing Large Language Models in Generating RTL Design Specifications [2.4125580419022477]
  エンジニアは現在、既存のRTLコードを手動で解釈し、仕様書を書く必要がある。 提案手法がRTL-to-specificationの品質にどのように影響するかを考察し、生成した仕様を忠実に評価するための指標を導入する。
  論文  参考訳（メタデータ） (2025-11-17T10:06:24Z)
• SSR: Socratic Self-Refine for Large Language Model Reasoning [78.62319252287938]
  Socratic Self-Refine (SSR)は、大規模言語モデル(LLM)のきめ細かい評価と精度向上のための新しいフレームワークである。 提案したSSRはモデル応答を検証可能な(サブクエスト,サブサブアンサー)ペアに分解し,ステップレベルの信頼度推定を可能にする。 5つの推論ベンチマークと3つのLCMによる実証的な結果から、SSRは一貫して最先端の反復的自己修正ベースラインを上回っていることが分かる。
  論文  参考訳（メタデータ） (2025-11-13T18:47:07Z)
• Compiling Prompts, Not Crafting Them: A Reproducible Workflow for AI-Assisted Evidence Synthesis [1.624454100511275]
  大規模言語モデル(LLM)は、体系的な文献レビューを加速する大きな可能性を秘めている。 現在のアプローチは、しばしば信頼性と厳密さを損なう、不安定で手作業によるプロンプトに依存している。 本研究では、タスク宣言、テストスイート、自動プロンプトチューニングを再現可能なSLRに組み込む、構造化されたドメイン固有フレームワークを提案する。
  論文  参考訳（メタデータ） (2025-08-22T21:37:49Z)
• Forecasting Time Series with LLMs via Patch-Based Prompting and Decomposition [48.50019311384125]
  我々は、LLMが広範囲のトレーニングを伴わずに時系列予測を行うことのできる、シンプルで柔軟なプロンプトベースの戦略を探求する。 我々は,LLMが正確かつ効果的に予測できるPatchInstructを提案する。
  論文  参考訳（メタデータ） (2025-06-15T19:42:58Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。 実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
  論文  参考訳（メタデータ） (2025-05-28T17:57:47Z)
• APE-Bench I: Towards File-level Automated Proof Engineering of Formal Math Libraries [5.227446378450704]
  APE-Bench Iは、Mathlib4の実際のコミット履歴から構築された最初の現実的なベンチマークである。 Eleansticはスケーラブルな並列検証インフラストラクチャで、Mathlibの複数バージョンにわたる検証に最適化されている。
  論文  参考訳（メタデータ） (2025-04-27T05:04:02Z)
• Complex LLM Planning via Automated Heuristics Discovery [48.07520536415374]
  複雑な計画タスクのための大規模言語モデル(LLM)の強化を検討する。 我々は,LLMがガイドタイム検索の関数を明示的に生成できる新しい手法である自動推論発見(AutoHD)を提案する。 提案手法はモデルトレーニングや微調整を必要とせず,LLMが生成する関数の明示的な定義は推論過程の解釈可能性と洞察を与える。
  論文  参考訳（メタデータ） (2025-02-26T16:52:31Z)
• Benchmarking Uncertainty Quantification Methods for Large Language Models with LM-Polygraph [83.90988015005934]
  不確実性定量化は機械学習アプリケーションにおいて重要な要素である。 最新のUQベースラインの集合を実装した新しいベンチマークを導入する。 我々は、11タスクにわたるUQと正規化技術に関する大規模な実証的研究を行い、最も効果的なアプローチを特定した。
  論文  参考訳（メタデータ） (2024-06-21T20:06:31Z)
• ChIRAAG: ChatGPT Informed Rapid and Automated Assertion Generation [10.503097140635374]
  ChIRAAGはOpenAI GPT4をベースとして、設計の自然言語仕様からSystem Verilog Assertion (SVA)を生成する。 実験では、LSM生成した生のアサーションの27%に誤りがあり、数回の反復で修正された。 以上の結果から,LLMはアサーション生成プロセスにおいて技術者を合理化し,支援し,検証を再構築できることが示唆された。
  論文  参考訳（メタデータ） (2024-01-31T12:41:27Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。