PROVE-RT: Generating Mechanized Theorem Prover Scripts for Real-Time Systems using LLMs

• URL: http://arxiv.org/abs/2608.12762v1
• Date: Thu, 13 Aug 2026 03:12:17 GMT
• Title: PROVE-RT: Generating Mechanized Theorem Prover Scripts for Real-Time Systems using LLMs
• Abstract summary: This paper introduces PROVE-RT, an LLM-assisted framework for generating PROSA/ROCQ scripts.<n>We construct a mechanization-oriented corpus from 1, 191 real-time systems papers, containing 13, 134 informal sketches with dependency information.<n>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%.
• Score: 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.

Related papers

• Automatic Translation of Unstructured Requirements into Linear Temporal Logic through Large Language Models [46.28810845443601]
  This paper evaluates whether contemporary off-the-shelf Large Language Models (LLMs) can help bridge this gap by generating Linear Temporal Logic (LTL) formulas directly from unstructured requirements.<n>The study examines six modern LLMs using a few-shot prompting strategy on a heterogeneous benchmark of 15 structurally varied requirements.<n>The results indicate that current general-purpose LLMs can achieve practically significant performance on the unstructured NLto-LTL task without task-specific fine-tuning.
  arXiv  Detail & Related papers  (2026-08-06T17:13:07Z)
• Beyond the Syntax: Do Security Experts Trust LLMs for NIDS Rule Engineering? [70.17374586573033]
  This paper presents a human-centered investigation into Large Language Models (LLMs)-based NIDS rule engineering.<n>Our evaluation reveals a syntax-semantics paradox: although LLMs generate syntactically correct rules, experts find them only partially deployable.<n>While large-scale models consistently produce syntactically valid rules, small models are largely ineffective for IDS rule generation.
  arXiv  Detail & Related papers  (2026-07-07T07:09:56Z)
• PROMISE: Proof Automation as Structural Imitation of Human Reasoning [15.113069562646302]
  We present PROMISE, a structure-aware framework that reframes proof generation as a stateful search over proof-state transitions.<n>We evaluate PROMISE on the seL4 benchmark across multiple LLM backends and compare it with prior systems such as Selene and Rango.
  arXiv  Detail & Related papers  (2026-04-07T03:49:12Z)
• Assessing Large Language Models in Generating RTL Design Specifications [2.4125580419022477]
  Engineers currently should manually interpret existing RTL code and write specifications, a slow and error-prone process.<n>We investigate how prompting strategies affect RTL-to-specification quality and introduce metrics for faithfully evaluating generated specs.
  arXiv  Detail & Related papers  (2025-11-17T10:06:24Z)
• SSR: Socratic Self-Refine for Large Language Model Reasoning [78.62319252287938]
  Socratic Self-Refine (SSR) is a novel framework for fine-grained evaluation and precise refinement of Large Language Models (LLMs)<n>Our proposed SSR decomposes model responses into verifiable (sub-question, sub-answer) pairs, enabling step-level confidence estimation.<n> Empirical results across five reasoning benchmarks and three LLMs show that SSR consistently outperforms state-of-the-art iterative self-refinement baselines.
  arXiv  Detail & Related papers  (2025-11-13T18:47:07Z)
• Compiling Prompts, Not Crafting Them: A Reproducible Workflow for AI-Assisted Evidence Synthesis [1.624454100511275]
  Large language models (LLMs) offer significant potential to accelerate systematic literature reviews.<n>Current approaches often rely on brittle, manually crafted prompts that compromise reliability and rigour.<n>This research proposes a structured, domain-specific framework that embeds task declarations, test suites, and automated prompt tuning into a reproducible SLR.
  arXiv  Detail & Related papers  (2025-08-22T21:37:49Z)
• Forecasting Time Series with LLMs via Patch-Based Prompting and Decomposition [48.50019311384125]
  We explore simple and flexible prompt-based strategies that enable LLMs to perform time series forecasting without extensive retraining.<n>We propose our own method, PatchInstruct, which enables LLMs to make precise and effective predictions.
  arXiv  Detail & Related papers  (2025-06-15T19:42:58Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  Code generation with large language models (LLMs) is increasingly adopted in production but fails to ensure code quality.<n>We propose REAL, a reinforcement learning framework that incentivizes LLMs to generate production-quality code.
  arXiv  Detail & Related papers  (2025-05-28T17:57:47Z)
• APE-Bench I: Towards File-level Automated Proof Engineering of Formal Math Libraries [5.227446378450704]
  APE-Bench I is the first realistic benchmark built from real-world commit histories of Mathlib4.<n>Eleanstic is a scalable parallel verification infrastructure optimized for proof checking across multiple versions of Mathlib.
  arXiv  Detail & Related papers  (2025-04-27T05:04:02Z)
• Complex LLM Planning via Automated Heuristics Discovery [48.07520536415374]
  We consider enhancing large language models (LLMs) for complex planning tasks.<n>We propose automated inferences discovery (AutoHD), a novel approach that enables LLMs to explicitly generate functions to guide-time search.<n>Our proposed method requires no additional model training or finetuning--and the explicit definition of functions generated by the LLMs provides interpretability and insights into the reasoning process.
  arXiv  Detail & Related papers  (2025-02-26T16:52:31Z)
• Benchmarking Uncertainty Quantification Methods for Large Language Models with LM-Polygraph [83.90988015005934]
  Uncertainty quantification is a key element of machine learning applications.<n>We introduce a novel benchmark that implements a collection of state-of-the-art UQ baselines.<n>We conduct a large-scale empirical investigation of UQ and normalization techniques across eleven tasks, identifying the most effective approaches.
  arXiv  Detail & Related papers  (2024-06-21T20:06:31Z)
• ChIRAAG: ChatGPT Informed Rapid and Automated Assertion Generation [10.503097140635374]
  ChIRAAG, based on OpenAI GPT4, generates System Verilog Assertion (SVA) from natural language specifications of a design. In experiments, only 27% of LLM-generated raw assertions had errors, which was rectified in few iterations. Our results show that LLMs can streamline and assist engineers in the assertion generation process, reshaping verification.
  arXiv  Detail & Related papers  (2024-01-31T12:41:27Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.