{"id":"f2b461f1-3107-4952-869e-f79efac78a37","arxiv_id":"2608.12762","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":6,"one_line_summary":"PROVE-RT, a retrieval-augmented, staged LLM pipeline, mechanizes 44.7% of a new 300-sketch benchmark of real-time scheduling analyses in the PROSA/Rocq library, far above direct LLM prompting.","lead":"This paper builds PROVE-RT, a pipeline that uses large language models with retrieval and staged code generation to create machine-checkable Rocq proofs of real-time scheduling analyses. On a 300-case benchmark it compiles 44.7% of cases, while direct prompting of frontier models compiles almost none.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The 44.7% success rate is dominated by definition-only sketches; combined with the lack of human validation of LLM-extracted sketches, compilation may only certify the LLM's restatement, not the paper's analysis.","rationale":"The reader's weakest assumption identifies exactly the load-bearing concern: the evaluation presumes the LLM-generated informal sketches faithfully represent the source schedulability analyses. The paper's own evidence strengthens this concern. Section VII-A describes extraction with Gemini-2.5-Flash and a deterministic structural filter, with no human validation step; Section IV's problem statement explicitly requires that each generated code block 'correctly represent the corresponding extracted invariant,' but nothing checks that the extracted invariant matches the paper. Table IV reveals that the 300-case evaluation set is dominated by definitions (278/300), so the reported 44.7% success rate mostly reflects definitional formalizations that carry no proof burden. The paper's Section IX limitation statement concedes that proof-bearing constructs and deeper dependency chains remain difficult, which is consistent with the low counts in Table IV. The most plausible alternative concern, that the proof-integrity checker might be bypassed, is addressed partially by the checker's design, but the deeper issue is that the checker cannot compare generated statements against the source paper because the source semantics exist only in the unvalidated sketch. The direct-baseline comparison is also confounded: baselines receive the original paper text while PROVE-RT receives LLM-extracted sketches, so part of the gap could be due to simplification in extraction rather than the staged pipeline. These considerations support the reader's CONDITIONAL verdict; no verdict change is needed, but the conditional should insist on human-verified ground truth, separate reporting for proof-bearing constructs, and released artifacts.","tokens_in":28931,"tokens_out":3246,"duration_ms":31763,"concrete_test":"Select a stratified random sample of 50 of the 300 evaluation sketches, including all 22 proof-bearing sketches. Have two independent RTS/formalization experts compare each informal sketch against the corresponding passage in the source paper and label it 'faithful', 'weakened claim', 'missing assumptions', or 'altered construct'. Recompute the success rate using only sketches labeled faithful by both experts, and also report success separately for proof-bearing constructs. If the faithful-sketch success rate falls substantially below 44.7%, or proof-bearing success is near zero, the headline claim must be weakened. A companion check: independently inspect the 134 compiling scripts to confirm that the formal statements are not tautological restatements of definitions.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The headline claim requires that the 300 evaluation sketches faithfully represent the schedulability analyses in the source papers. That condition is not established. The sketches were produced by Gemini-2.5-Flash and passed only a deterministic structural filter (Section VII-A), with no human validation against the source papers. Moreover, Table IV shows the evaluation set is overwhelmingly definitions: 278/300 (92.7%) are definitions, and only 19 lemmas plus 3 theorems are proof-bearing. For a definition there is no proof obligation; the skeleton stage declares a Definition and the proof-completion stage is vacuous, so such 'successes' do not demonstrate mechanization of a schedulability analysis. Even among the 22 proof-bearing constructs, success is around 40-54%, and Section IX explicitly concedes that 'deeper dependency chains and proof-bearing constructs that require precise PROSA context' remain difficult. Because the skeleton statement and proof are both generated from the LLM-extracted sketch, a compiling script only establishes that the sketch is internally consistent; the proof-integrity checker cannot detect a weakened statement or missing assumption, since it has no access to the original paper. The direct-prompting baselines use the paper text, so the large gap between 0% and 44.7% may partly reflect simplification introduced by the extraction stage rather than the value of the pipeline itself. Thus the central claim is not yet supported by evidence that the generated scripts correspond to the real analyses.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper presents PROVE-RT, an LLM-assisted pipeline that generates PROSA/Rocq mechanizations of schedulability analyses from real-time systems papers. The pipeline comprises five stages: LLM-based extraction of system invariants, informal sketches, and dependency graphs; processing of PROSA documentation into retrieval-ready chunks; retrieval-augmented context construction with a syntax-aware dependency-recovery step; staged skeleton generation in which proof obligations are deferred with Admitted; and batched proof completion with compiler-guided repair plus a proof-integrity checker. The authors contribute a corpus of 13,134 informal sketches extracted from 1,191 papers and evaluate the framework on 300 curated sketches, reporting a 44.7% end-to-end success rate with dense retrieval versus 0% and 0.33% for direct-prompting baselines using GPT-5 and Claude-Opus-4.6. They also report a dependency-depth analysis (RQ2) and a comparison of BM25, dense, and hybrid retrieval (RQ3), with per-construct results in Table IV and a limitations discussion in Section IX.","tokens_in":29205,"tokens_out":17823,"duration_ms":159810,"significance":"The contribution is timely: to my knowledge this is the first LLM-assisted framework aimed at PROSA/Rocq mechanization of schedulability analyses, and the corpus and evaluation support future work. The paper's strengths are substantial: correctness of generated scripts is grounded by the Rocq compiler rather than by the LLM; the direct-prompting baselines are genuine and fairly described; per-construct results are reported transparently in Table IV; and Section IX states clear limitations. If the central claim were fully supported, the framework would reduce the documented proof-engineering burden of PROSA-based verification. However, the headline success rate is dominated by definition formalization (278 of 300 evaluation sketches), and the fidelity of the LLM-extracted sketches to the source papers is not validated, so the evidence supports a narrower claim than the abstract makes. These issues are addressable within the manuscript's scope, which is why I recommend major revision rather than rejection.","major_comments":[{"comment":"Table IV shows that 278 of the 300 evaluation sketches (92.7%) are definitions, and the headline success rate of 44.7% (Dense) is dominated by them: for a definition there is no proof obligation, so a 'success' requires only that the generated skeleton and definition body type-check, and the proof-completion stage contributes nothing. For the 22 proof-bearing sketches, the Dense configuration succeeds on only 9 (40.9%), including just 1 of 3 theorems, while BM25 succeeds on 12 of 22 (54.5%). The abstract's claim that PROVE-RT 'achieves a success rate of 44.7%' at mechanizing schedulability analyses therefore overstates the demonstrated capability. The paper should report the success rate separately for definition-only and proof-bearing sketches and should lead the quantitative claims with the proof-bearing rates.","section":"Table IV; Section VIII-A"},{"comment":"The evaluation assumes that the 300 informal sketches are faithful, nontrivial representations of the schedulability analyses in the source papers, and this assumption is load-bearing but not established. The sketches were produced by Gemini-2.5-Flash and passed only a deterministic structural filter based on dependency resolution (exact, normalized, and fuzzy matching with a 0.88 threshold, and an unresolved-dependency rejection ratio of 0.15); no human validation against the source papers is reported, and the human-in-the-loop curation described in Section VIII is a category-level selection step rather than a sketch-fidelity check. Because both the skeleton statement and the completed proof are generated from the sketch, a compiling script establishes only that the sketch is internally consistent: neither the Rocq compiler nor the proof-integrity checker can detect a weakened statement or a missing assumption, since neither has access to the original paper. I recommend adding a human-validated fidelity sample with agreement rates, or explicitly reframing the contribution as the mechanization of LLM-extracted sketches rather than of the papers' analyses.","section":"Section VII-A; Section VIII"},{"comment":"The comparison between PROVE-RT and the direct-prompting baselines is input-asymmetric in a way that can inflate the reported gap. The baselines are given the original paper text or the raw informal sketch, whereas the end-to-end PROVE-RT run also includes the extraction stage; if extraction simplifies the analysis, part of the difference between 0% and 44.7% may reflect input simplification rather than the value of the retrieval, skeleton, and repair components. The near-absence of Hypothesis constructs in the corpus (8 of 13,134 in Table I) is one indication that the extractor may systematically omit assumptions. To separate these effects, the paper should quantify the simplification introduced by the extraction stage, for example by running the PROVE-RT pipeline on the original paper text as input or by measuring the complexity reduction between the papers and their extracted sketches.","section":"Section VIII; Table II"},{"comment":"The paper's own evidence and examples delimit the central claim more sharply than the abstract. Section IX concedes that 'deeper dependency chains and proof-bearing constructs that require precise PROSA context' remain difficult, and Table IV shows that the best overall configuration proves only 1 of 3 theorem sketches. The worked example in Section VI is a definitional identity discharged by unfold followed by lia, and the Appendix F example discharges its theorem by applying PROSA's pre-existing EDF_optimality result; neither demonstrates that the framework mechanizes a substantive schedulability analysis whose proof must be synthesized. The conclusions should be calibrated to the proof-bearing results and should state what fraction of the proof-bearing successes consist of direct application of existing PROSA theorems rather than multi-step proof synthesis.","section":"Section IX; Section VI"}],"minor_comments":[{"comment":"References [14] and [44] are the same paper, as are [16] and [45]; the duplicate entries should be removed and the citations consolidated.","section":"References"},{"comment":"Reference [6] cites the ROCQ 9.2.0 reference manual, while Section VII-D reports the evaluation used ROCQ version 9.1.0; please reconcile this inconsistency.","section":"Reference [6]"},{"comment":"Figure 5 restricts the plot to sketches with at most 10 sections, which excludes 30 of the 300 evaluation sketches; the caption should state this count explicitly and the text should confirm that the decreasing trend holds for the excluded group.","section":"Figure 5"},{"comment":"The evaluation depends on closed commercial models (Gemini-2.5-Flash, Claude-Opus-4.6, GPT-5) but the exact prompts, model temperatures, and decoding settings are not given; including these, together with the full prompt templates, in an appendix would materially improve reproducibility.","section":"Section VII-D"},{"comment":"The fuzzy-matching threshold (0.88), the unresolved-dependency rejection ratio (0.15), the retrieval top-K (K=5), and the weight ordering alpha > beta > gamma are introduced without sensitivity analysis; a short ablation study would clarify how sensitive the reported rates are to these choices.","section":"Section V-C"},{"comment":"The assumptions listed in the extracted sketch for the motivating example (for example, 'faults are detected immediately upon occurrence') do not appear anywhere in the generated skeleton or proof; please clarify how sketch assumptions are intended to be mapped into the formal development.","section":"Section VI; Appendix A"},{"comment":"Listing 6 contains 'tsk \\ints -> respects_sporadic_task_model arr_seq tsk', which appears to be a rendering artifact for 'tsk \\in ts'; please check all listing renderings in the final version.","section":"Listing 6"}],"recommendation":"major_revision","confidential_remarks":"The manuscript has a genuine contribution: the first LLM-assisted PROSA/Rocq pipeline, a reusable 13k-sketch corpus, and credible direct-prompting baselines. My main concern is that the 44.7% figure may be quoted without the Table IV qualification (92.7% definitions), so I recommend requiring the authors to lead with per-construct success rates and to add at least a small human-validated fidelity check of the extracted sketches. A second concern is reproducibility: the pipeline relies on closed commercial models and the exact prompts are not provided; I would treat a commitment to release the evaluation set, prompts, and generated scripts as a condition for acceptance."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Read it. The genuinely new thing is the target, not the machinery: nobody has tried LLM-assisted PROSA/ROCQ mechanization, and the 1,191-paper corpus with 13,134 dependency-tagged informal sketches is a real artifact. The pipeline stages (RAG, skeleton, proof completion, compiler-guided repair) are assembled from known techniques, but applying them to PROSA is new, and the observation that off-the-shelf LLMs produce compilable Rocq scripts that silently avoid PROSA is worth having on record.\n\nWhat is good: the design is sensible. Skeleton generation separates type structure from proof bodies; the Rocq compiler is the correctness ground truth; the proof-integrity checker tries to prevent the model from smuggling the goal into an Axiom or a new helper lemma. The comparison to direct prompting is the right baseline, and the direct failures are credible. The limitations section is honest.\n\nWhere it is soft: the headline number is oversold. Table IV shows 278 of 300 evaluation targets are definitions. Definitions carry no proof obligation, so 45% success on them is a formalization rate, not a mechanization rate. The proof-bearing count is 19 lemmas plus 3 theorems; on those, all retrieval variants land between 41% and 55%, which at n=22 is within noise of each other. The second soft spot is the extraction stage: Gemini-2.5-Flash produces the informal sketches, and validation is only structural. No human checked a sample against the source papers. So a compiling script demonstrates internal consistency with the LLM's restatement, not fidelity to the paper's analysis. Because the direct baselines start from paper text, part of the 0% vs 44.7% gap may be extraction simplifying the problem, not the pipeline adding power. Section IX concedes exactly the hard cases, deeper chains and proof-bearing constructs.\n\nI would not call the central claim false. It is unproven in the current form. The framework is plausible, the corpus has standalone value, and the citation pattern is appropriate. But the paper is not yet evidence that schedulability theorems are being mechanized, and the code/data are not released.\n\nFor a journal or conference, I would send this to a serious referee, not desk reject. The problem is real, the corpus is reusable, and the method deserves engagement. Expect the referee to ask for human-validated sketches, construct-stratified success rates, error bars over seeds, and released artifacts before the central claim can be taken at face value.","headline":"PROVE-RT is a genuinely new target and a reusable corpus, but the 44.7% headline is mostly definitions and the sketches are unvalidated, so the central mechanization claim is not yet established; send to review, expect revision.","tokens_in":29769,"tokens_out":2646,"would_cite":false,"duration_ms":28859,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"PROVE-RT is an LLM-assisted framework that claims to be the first to automatically generate machine-checked PROSA/Rocq proof scripts for real-time schedulability analyses, succeeding on 44.7% of a 300-case curated evaluation where direct…","keywords":["mechanized verification","schedulability analysis","real-time systems","LLM-assisted theorem proving","PROSA","Rocq/Coq scripts","retrieval-augmented generation","informal sketches"],"falsifier":"Take a random sample of the 300 evaluated sketches, compare each sketch's assumptions against the source paper's stated hypotheses, and recompile the generated scripts with any omitted hypotheses reinstated; if a substantial fraction of scripts then fail, the success rate measures fidelity to the sketch rather than mechanization of the original analyses.","tokens_in":28676,"feed_emoji":"🤖","tokens_out":6316,"duration_ms":53788,"temperature":0.7,"pith_summary":"PROVE-RT sets out to do what has not been done before: take schedulability analyses from real-time systems papers and turn them, automatically, into proof scripts that the PROSA/Rocq mechanized-verification library accepts. The paper's central claim is that this is achievable with LLM assistance if generation is guided by dependency-aware informal sketches, retrieval from PROSA documentation, and a two-stage skeleton-then-proof pipeline. On a curated evaluation of 300 informal sketches, the framework mechanizes 134 (44.7%), while direct prompting of frontier LLMs produces essentially no valid PROSA scripts. If the claim holds, it means the expensive, error-prone step of hand-writing mechanized schedulability proofs can be substantially automated, and the same pipeline can later serve as a verification layer for AI-generated scheduling results.","feed_headline":"LLM pipeline mechanizes schedulability proofs 44.7% of the time","feed_subtitle":"Direct prompting of frontier models gets near zero; retrieval plus staged proofs carries the result.","key_machinery":"The load-bearing object is the dependency-aware informal sketch. For each extracted invariant—definition, lemma, theorem, corollary, fixpoint, or hypothesis—the sketch records the statement, the intuition, the proof outline, and the identifiers it depends on, and these dependencies form a directed acyclic graph that fixes the order in which code blocks must appear. Because Rocq is forward-referencing, the DAG ordering is what makes the generated script compilable at all. Around that object, the pipeline has three further mechanisms: retrieval over a processed PROSA documentation corpus (chunked proof-oriented vs section-level, with syntax-based dependency recovery), skeleton generation that forces every proof obligation to remain an \"Admitted\" placeholder while definitions and type-class contexts are fully elaborated, and a proof-completion stage that fills the placeholders in batch and repairs failures from compiler error messages under a proof-integrity checker.","core_discovery":"The paper claims that the reason LLMs fail at PROSA/ROCQ script generation is not lack of proof ability but lack of the recovered formal structure: schedulability analyses in the literature are written for human readers, with assumptions, definitions, and dependencies left implicit. PROVE-RT's contribution is an intermediate representation that makes that structure explicit—each extracted invariant is paired with an informal sketch and a dependency edge, ordered into a DAG, and then fed into retrieval-augmented skeleton generation in which proof bodies are deferred with \"Admitted\", followed by batch proof completion with compiler-guided repair. Against direct prompting (0/300 for one tested frontier model, 1/300 for another), PROVE-RT with dense retrieval succeeds on 134/300 sampled sketches (44.7%). The paper takes this as evidence that retrieval-guided, staged LLM assistance is the right route to automated mechanization of real-time schedulability analysis in PROSA/Rocq.","pith_inferences":["Because the evaluation set was curated to categories well aligned with existing PROSA abstractions, the 44.7% figure is best read as an upper bound for current capability; an uncurated corpus would likely score lower.","The same staged skeleton-and-repair pattern should transfer to other domain-specific proof libraries that enforce forward referencing, so the method is not inherently tied to PROSA.","The framework's most consequential use may be the one the paper mentions in passing: serving as a mechanical check on schedulability claims produced by generative AI, turning the LLM from author of an analysis into author of a candidate that a trusted kernel verifies.","A natural stress test is to apply the pipeline to the integration-style proofs that dominate PROSA's real-world cost, such as translation interfaces to verified kernels, where the recovered formal structure is the hard part."],"forward_implications":["Direct prompting is not a viable route: on the 300-sketch evaluation, the tested frontier models produced no usable PROSA mechanizations (0/300 and 1/300), while PROVE-RT's best variant succeeded on 134/300.","Dependency depth is the main difficulty: success rates drop as sketches contain more sections, yet multi-section chains are still mechanized, so the framework handles nontrivial dependency structures, not just isolated definitions.","Retrieval method matters in a task-specific way: dense retrieval wins end-to-end (44.7%), while sparse and hybrid retrieval are stronger on proof-bearing lemmas and theorems that need exact PROSA identifiers.","The corpus of 1,191 papers and 13,134 dependency-annotated informal sketches becomes a reusable benchmark for future work on LLM-assisted formalization in real-time systems.","If the claim holds, PROVE-RT offers a path to reduce the proof-engineering burden documented in prior PROSA-based efforts, such as the thousands of lines of Rocq code needed to connect analyses to certified operating-system kernels."],"supporting_citations":[{"why":"Supplies PROSA, the Rocq library of mechanized schedulability theory that the generated scripts must use.","marker":"[5]"},{"why":"Defines the Rocq prover whose compiler is the acceptance oracle for every generated script.","marker":"[6]"},{"why":"Documents the 18,852-line CertiCAN mechanization that motivates the need for automation.","marker":"[7]"},{"why":"Shows how model changes invalidate existing mechanized proofs, motivating automated maintenance.","marker":"[9]"},{"why":"Provides the Rango retrieval-augmented proving baseline whose success-rate context frames PROVE-RT's 44.7%.","marker":"[42]"},{"why":"Provides the GPass neural-theorem-proving baseline cited as comparison context for difficulty.","marker":"[19]"},{"why":"Supplies the worst-case timing-requirement analysis used as the end-to-end illustrative example.","marker":"[43]"}],"fun_headline_variants":["LLM proof generation jumps from ~0% to 44.7% with retrieval","Retrieval-guided LLM writes PROSA proofs: 44.7% success","Staged LLM generation fixes PROSA proof gaps, hits 44.7%","LLM + dependency sketches: PROSA proof success 44.7%","From 0 to 44.7%: retrieval unlocks LLM PROSA proofs"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The measured success rate stands or falls with the informal sketches: they are produced by an LLM and filtered only by a deterministic structural check, with no human validation, so if a sketch silently weakens or omits an assumption from the original paper, a script that compiles proves the sketch, not the published analysis.","fun_headline_variants_meta":{"raw":{"variants":["LLM proof generation jumps from ~0% to 44.7% with retrieval","Retrieval-guided LLM writes PROSA proofs: 44.7% success","Staged LLM generation fixes PROSA proof gaps, hits 44.7%","LLM + dependency sketches: PROSA proof success 44.7%","From 0 to 44.7%: retrieval unlocks LLM PROSA proofs"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000693,"raw_usage":{"total_tokens":3160,"prompt_tokens":997,"completion_tokens":2163,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":613,"completion_tokens_details":{"reasoning_tokens":2054}},"tokens_in":613,"tokens_out":2163,"duration_ms":14573,"temperature":1.0,"reasoning_tokens":2054,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T23:52:14.016799+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a random sample of the 300 evaluated sketches, compare each sketch's assumptions against the source paper's stated hypotheses, and recompile the generated scripts with any omitted hypotheses reinstated; if a substantial fraction of scripts then fail, the success rate measures fidelity to the sketch rather than mechanization of the original analyses.","supporting_citations":[{"cited_title":"Intuition for generating code: Each sporadic task can release jobs at arbitrary times, but not too frequently","cited_arxiv_id":null,"evidence_quote":"Defines the Rocq prover whose compiler is the acceptance oracle for every generated script."},{"cited_title":"Certican certifying can analyses and their results,","cited_arxiv_id":null,"evidence_quote":"Documents the 18,852-line CertiCAN mechanization that motivates the need for automation."}],"review_version":1}