{"id":"2d123d13-58bb-4f54-866b-e106d93e9937","arxiv_id":"2607.12532","paper_version":1,"verdict":"UNVERDICTED","confidence":"LOW","novelty_score":6.0,"correctness_risk":"unknown","formal_verification":"none","parameter_count":0,"one_line_summary":"A novel quantum pre-expectation calculus reasons about expected runtime without upper bounds, via rewards and a program transformation that encodes runtime in weakest pre-expectations.","lead":"The paper introduces a pre-expectation framework for quantum programs that analyzes expected runtime without requiring an upper bound, including for programs that may run forever. It matters for verifying quantum software with rewards and unbounded loops, where classical weakest-precondition tools fall short.","discovery_kind":"new_method","skeptic_critique":{"model":"grok-4.5","headline":"No significant objection identified beyond the abstract-only limitation already noted by the reader; the load-bearing preservation claim cannot be checked without definitions and proofs.","rationale":"The reader’s UNVERDICTED / LOW-confidence assessment is the only defensible stance given an abstract-only review. The weakest assumption they isolate—preservation of expected runtime (including the infinite case) under the reward-encoding transformation—is exactly the condition that must hold for the central claim to be true. Because the full text is unavailable, that condition cannot be verified or refuted; manufacturing a more specific technical objection would violate the good-faith rule. The recommended concrete test simply operationalizes the missing check: inspect the actual theorem and its proof for the extended-real case. No adjustment to the verdict is warranted.","tokens_in":1920,"tokens_out":425,"duration_ms":3662,"concrete_test":"Obtain the full paper (or arXiv source) and check whether the main theorem relating the weakest pre-expectation of the transformed program to the expected runtime of the original program is stated for the extended reals (including +∞) and proved without an a-priori upper bound; if the proof only covers the finite case or silently assumes boundedness, the headline claim fails.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper is available only as an abstract. The central claim is that a novel pre-expectation framework (and a program transformation encoding runtime via rewards) lets one reason about quantum preconditions without an upper bound, so that expected runtime—including infinite expected runtime—can be obtained from weakest pre-expectation calculus. The reader correctly flags that this rests on the transformation preserving expected runtime even when the expectation is infinite. Without the body there are no definitions of the pre-expectation operators, no statement of the transformation, and no theorems establishing soundness or preservation. That is an information gap, not an internal inconsistency or a concrete technical flaw that can be isolated and attacked. No further load-bearing concern can be substantiated from the given material.","agreement_with_reader":"agree"},"referee_report":{"model":"grok-4.5","summary":"The manuscript (available only as an abstract) revisits quantum weakest preconditions for expected-runtime analysis of quantum programs. It claims a novel pre-expectation framework that reasons about preconditions without requiring an upper bound, motivated by programs with reward statements and by the need to handle potentially infinite expected runtime. Several approaches are announced, including a program transformation that encodes expected runtime so that it can be recovered from a weakest pre-expectation calculus with rewards.","tokens_in":2070,"tokens_out":547,"duration_ms":9762,"significance":"If the framework is sound and the announced transformation correctly preserves expected runtime (including the infinite case), the work would extend classical pre-expectation techniques to quantum programs without artificial upper bounds and would give a usable tool for runtime analysis of non-terminating or infinite-expectation quantum programs. That would be a solid contribution to quantum program verification. The abstract alone, however, supplies no definitions, theorems, or examples with which to assess whether those claims hold.","major_comments":[{"comment":"Only the abstract is available for review. The central load-bearing claim—that a program transformation encodes expected runtime into rewards so that the weakest pre-expectation of the transformed program equals the true expected runtime even when that expectation is infinite—cannot be checked: there are no definitions of the pre-expectation operators, no statement of the transformation, and no soundness or preservation theorems. Assessment of correctness is therefore impossible on the supplied material.","section":null},{"comment":"The abstract asserts that the framework works “without the need of an upper bound” and handles “potentially infinite expected runtime.” Without the body it is impossible to verify whether the operators are well-defined on unbounded or infinite expectations, whether the fixed-point characterizations remain valid, or whether the reward encoding is faithful in the infinite case. These points are essential to the paper’s main contribution and must be established formally before acceptance can be considered.","section":null}],"minor_comments":[{"comment":"The abstract is clear on motivation but does not name the concrete quantum programming language, the precise form of reward statements, or the relationship to existing quantum weakest-precondition calculi; those details should appear early in the full manuscript for positioning.","section":null}],"recommendation":"uncertain","confidential_remarks":"Full text was not provided; this is an abstract-only review. I cannot responsibly recommend accept, minor_revision, major_revision, or reject without the body. Please supply the complete manuscript for a proper technical assessment. Scope (cs.LO / quantum program verification) appears appropriate if the claims hold."},"author_rebuttal":null,"desk_editor":{"model":"grok-4.5","letter":"The one thing you need to know: this paper claims a novel pre-expectation framework for quantum programs that drops the usual upper-bound requirement, so you can reason about expected runtime—including cases where it may be infinite—especially with reward statements. The main technical vehicle is a program transformation that encodes runtime via rewards and then reuses weakest pre-expectation calculus.\n\nWhat looks new and useful is exactly that removal of the bound. Existing quantum wp variants often force you to supply an a-priori upper bound; for loops or reward-carrying programs that may not terminate almost-surely, that is a real obstacle. Framing expected runtime as a special case of wp-with-rewards via a transformation is a clean idea if it works. The authors (Katoen et al.) know the classical and quantum wp literature well, so the survey/revisit part is likely careful.\n\nSoft spots are almost entirely information gaps, not visible flaws. We have only the abstract: no definitions of the pre-expectation operators, no statement of the transformation, no theorems. The load-bearing claim is that the transformed program’s weakest pre-expectation equals the true expected runtime of the original even when that expectation is infinite. That preservation has to be proved carefully (domains, measures, continuity at infinity). Nothing in the abstract contradicts itself or smells like circularity; it is simply unverifiable from what we have. “Several ways” to do the analysis is also left vague.\n\nThis is for people already working on quantum program logics or probabilistic resource analysis. A reader who cares about quantum wp or expected runtime of quantum loops will get value from the full development. It is coherent enough and important enough inside the subfield to deserve a serious referee rather than a desk reject. I would not cite or bring it to reading group on the abstract alone, but I would send it out for review and then decide.","headline":"Abstract-only claim of a bound-free quantum pre-expectation calculus for expected runtime (incl. infinite); useful if the preservation theorems hold, but we cannot check them yet.","tokens_in":2679,"tokens_out":478,"would_cite":false,"duration_ms":13133,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"grok-4.5","headline":"A pre-expectation framework reasons about quantum program preconditions without upper bounds, so expected runtime can be analyzed even when it may be infinite.","keywords":["quantum weakest preconditions","pre-expectations","expected runtime","quantum programs","reward statements","program transformation","runtime analysis"],"falsifier":"Exhibit a concrete quantum program whose true expected runtime (computed by other means) differs from the weakest pre-expectation obtained after the proposed reward transformation, especially on an instance with infinite expected runtime.","tokens_in":2771,"feed_emoji":"⏱️","tokens_out":618,"duration_ms":5075,"temperature":0.7,"pith_summary":"This paper revisits quantum weakest preconditions with the goal of analyzing the expected runtime of quantum programs, including cases where that expectation may be infinite. Standard approaches often require an a priori upper bound on the quantities being reasoned about; the authors introduce a novel pre-expectation framework that removes that requirement. The framework is especially useful for programs that contain reward statements, which can encode runtime cost. One concrete route they develop is a program transformation that rewrites a quantum program so that its expected runtime becomes expressible as a weakest pre-expectation with rewards. The result is a calculus that can certify runtime behavior without presupposing that the expectation is finite.","feed_headline":"Quantum runtime analyzed without upper bounds","feed_subtitle":"A pre-expectation calculus and reward transformation handle expected runtime even when it may be infinite.","key_machinery":"The novel pre-expectation framework for quantum programs (together with a program transformation that encodes expected runtime via reward statements so that weakest pre-expectation calculus applies directly).","core_discovery":"Quantum weakest preconditions can be recast as a pre-expectation calculus that does not demand an upper bound on the quantities of interest, thereby supporting expected-runtime analysis of quantum programs (including those with rewards and those whose expected runtime may be infinite) via transformations that reduce runtime questions to weakest pre-expectation calculations.","pith_inferences":["The same bound-free pre-expectation style may transfer to other quantitative properties of quantum programs (energy, entanglement cost) that can be encoded as rewards.","Classical expected-runtime calculi that already use rewards may serve as a template for verifying soundness of the quantum transformation.","Tool builders could implement the transformation as a front-end that reuses existing quantum weakest-precondition engines for runtime queries."],"forward_implications":["Expected runtime of quantum programs can be stated and reasoned about inside a weakest pre-expectation calculus without first proving finiteness.","Reward statements become a systematic device for turning runtime questions into pre-expectation questions.","Programs whose expected runtime diverges can still be analyzed rather than excluded by an upper-bound hypothesis.","Several alternative routes to the same analysis become available once the pre-expectation framework is in place."],"fun_headline_variants":["Pre-expectation calculus for quantum runtime without upper bounds","Quantum programs: expected runtime via unbounded pre-expectations","Transform quantum rewards to weakest pre-expectation runtime checks","Analyzing possibly infinite quantum runtime with pre-expectations","Recast quantum weakest preconditions as unbounded pre-expectations"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The program transformation and reward encoding must preserve the true expected runtime of the original quantum program, including when that expectation is infinite.","fun_headline_variants_meta":{"raw":{"variants":["Pre-expectation calculus for quantum runtime without upper bounds","Quantum programs: expected runtime via unbounded pre-expectations","Transform quantum rewards to weakest pre-expectation runtime checks","Analyzing possibly infinite quantum runtime with pre-expectations","Recast quantum weakest preconditions as unbounded pre-expectations"]},"model":"grok-4.5","effort":"low","cost_usd":0.00375,"raw_usage":{"total_tokens":1083,"prompt_tokens":639,"num_sources_used":0,"completion_tokens":79,"cost_in_usd_ticks":37500000,"prompt_tokens_details":{"text_tokens":639,"audio_tokens":0,"image_tokens":0,"cached_tokens":128},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":365,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":639,"tokens_out":79,"duration_ms":3288,"temperature":1.0,"reasoning_tokens":365,"cache_read_input_tokens":128,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-15T05:21:20.722061+00:00","model_set":{"reader":"grok-4.5"},"falsifier":"Exhibit a concrete quantum program whose true expected runtime (computed by other means) differs from the weakest pre-expectation obtained after the proposed reward transformation, especially on an instance with infinite expected runtime.","supporting_citations":[],"review_version":1}