{"id":"0db21131-4898-49af-bedb-d747770bfe3a","arxiv_id":"2412.00906","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A sound forward-reasoning proof system for probabilistic dynamic logic is presented, with a prototype implementation and a Monty Hall verification example.","lead":"The authors introduce a proof system for probabilistic dynamic logic, a way to verify properties of programs that make random choices. The system works by symbolically executing the program and collecting constraints on probabilities, then solving them with an SMT solver.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 1's soundness claim is only meaningful for almost-surely terminating programs, a condition the proof system never checks; derivability may outrun the semantic domain.","rationale":"Stress-testing Theorem 1, I find the reader's weakest assumption is indeed the load-bearing one. The soundness argument for each rule is plausible: the proof uses Proposition 1 from [25], and the MDP semantics of Figure 2 are standard. Given the a.s.-termination assumption, the equations in the proofs of demonChoice and probChoice go through. However, the theorem overstates the domain: the semantics of [s]_p φ (Definition 2) is only defined for programs whose MDPs reach final states with probability 1 under all policies, yet the derivation relation Γ ⊢ φ imposes no corresponding condition. loopUnroll is purely an unfold; it does not certify termination. Thus, unless one proves (or the calculus enforces) that derivability implies a.s. termination, the theorem's conclusion is not well-formed for every derivable judgment. This is not a fatal soundness error — the paper transparently declares the assumption — but it is a precision gap that supports the CONDITIONAL verdict. The paper's own limiting statements (work in progress, loop rules only sketched, state-dependent probabilities assumed away) corroborate that the system is not yet a complete proof system. A concrete test is to check whether any non-a.s.-terminating program admits a finite proof; if none does, the concern is reduced to a documentation issue. I agree with the reader and leave the verdict unchanged.","tokens_in":13779,"tokens_out":19539,"duration_ms":166871,"concrete_test":"Attempt to derive a judgment for a non-a.s.-terminating program using the rules of Figure 3, e.g., Γ ⊢ [while true {skip}]_0 φ or Γ ⊢ [(while true {skip}) 1/2 ⊕ skip]_0 φ. If a finite proof tree with satisfiable side conditions exists, Theorem 1 is ill-formed for that derivation. If no such proof exists, then prove by induction on proof trees that every derivable judgment's program terminates on all paths under every policy; such a proof would show the semantic domain is automatically respected and the concern is mitigated. A simpler empirical check: extend the Crowbar prototype (Section 6) with a while loop and confirm the proof obligation fails to close.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is Theorem 1, soundness of the Figure 3 calculus. The pDL semantics in Definition 2 defines satisfaction of [s]_p φ via E_ε([[φ]]), which is only well-defined because Section 3.1 assumes all programs reach final states with probability 1 under all policies (Eq. 3). Without that assumption, the expectation over paths is undefined and |= (hence Theorem 1) has no meaning. However, the proof system has no rule or side condition that enforces almost-sure termination: the only loop rule is loopUnroll, which merely unfolds a while into an if, and there is no termination check or well-foundedness argument. Consequently, the statement 'if Γ ⊢ φ then |= (∧Γ) → φ' is not formally restricted to the domain in which |= is defined. The paper states the assumption in Section 3.1, but does not prove that every derivable judgment involves an a.s.-terminating program, nor does the theorem include it as an explicit hypothesis. This is a gap between the derivation relation and the semantic domain: a proof tree could in principle be constructed for a program outside the domain, making the theorem's conclusion ill-formed. The implementation (Section 6) exercises only the loop-free Monty Hall program, so it does not reveal whether the gap is reachable.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces a deductive proof system for Pardo et al.'s probabilistic dynamic logic (pDL) over the probabilistic guarded command language pGCL. The proof system follows KeY-style forward symbolic execution: judgments of the form Γ ⊢ U[s]_p φ are proved by syntax-driven rules (Figure 3) that accumulate side constraints on probability variables, and a proof tree is closed when the resulting constraint set is satisfiable. The main formal result is Theorem 1, which claims soundness of the Figure 3 calculus: every derivable judgment is valid in the pDL semantics. The paper illustrates the approach on the Monty Hall program and reports on a prototype implementation built on Crowbar and Z3.","tokens_in":13947,"tokens_out":19766,"duration_ms":189326,"significance":"If the formal gaps are repaired, the paper would provide a forward-reasoning proof system for pDL, complementing the backward weakest-precondition style of Katoen and collaborators and exploiting the expressive strength of dynamic logic. The manuscript's strengths include an explicit soundness proof organized rule-by-rule, a nontrivial worked example, and a publicly available prototype implementation. The paper is honest in labeling itself work in progress, and the authors clearly identify the loop-handling problem as an open issue. However, the soundness theorem is not yet stated at the required level of rigor: the almost-sure termination assumption is not integrated into the theorem, and the probability-variable machinery used by the rules is not formally part of the pDL syntax. These issues are local and fixable, but they currently undermine the central claim.","major_comments":[{"comment":"Theorem 1 states that for all Γ and φ, if Γ ⊢ φ then |= (∧Γ) → φ, with no side condition restricting φ to programs that satisfy the almost-sure termination assumption introduced in Section 3.1. The expectation in Eq. (3) is only defined when every policy reaches a final state with probability 1, and the text explicitly says that pDL 'can only talk about properties of almost surely terminating programs.' The calculus in Figure 3 contains no rule or side condition that checks almost-sure termination; loopUnroll merely unfolds a while-loop into a conditional. Consequently, the validity relation in the theorem's conclusion is undefined for any derivable judgment whose program violates the assumption, and the theorem is formally ill-posed as written. The theorem should be restated with an explicit hypothesis that all programs occurring in φ are almost surely terminating under all policies, or the calculus should be restricted to such programs.","section":"§3.1, Theorem 1, Eq. (3), Figure 3"},{"comment":"The proof rules in Figure 3 use p, p1, and p2 as syntactic probability variables in constraints such as ⟨p ≤ min(p1, p2)⟩, and the surrounding text speaks of solving these constraints. However, the pDL syntax in Section 4.1 has no category for probability terms or probability variables: p is introduced as a semantic object p : State → [0,1]. The paper never defines the syntax of judgments with free probability variables, nor the satisfaction of a formula [s]_p φ when p is a variable rather than an expectation function. This makes both the constraint-satisfiability condition and the quantification 'for all Γ and φ' in Theorem 1 undefined. The authors should add a formal language of probability parameters/terms, their interpretation, and the semantics of judgments relative to assignments of those parameters.","section":"§4.1, §5 (Judgments), Figure 3"}],"minor_comments":[{"comment":"The sentence 'for x, y ∈ {0, 1, 2}, the expression z = (2x − y) mod 3 simply returns z ∈ {0, 1, 2} such that z ≠ x and z ≠ y' is false when x = y; it should be stated with the side condition x ≠ y, which is the case in the else-branch where the expression is used.","section":"§2"},{"comment":"The text 'We use |= [s]_p φ to denote that a formula is valid' conflates the satisfaction relation with the validity relation; a metalinguistic symbol such as ⊨ should be used for validity.","section":"§4.2"},{"comment":"In the loopUnroll rule, the premise contains an unbalanced closing bracket: 'U[if (e) {sb; while (e) {sb}; s} else s}]p φ' should read 'U[if (e) {sb; while (e) {sb}; s} else s]_p φ'.","section":"Figure 3"},{"comment":"The sentence defining judgments uses 'V Γ' where the conjunction symbol is intended, and the 'Probabilistic constraints' paragraph contains a doubled 'that that'; both need correction.","section":"§5"},{"comment":"The assertion 'Γ ⊢ φ expresses existence of a proof tree' should specify that proof trees are finite and define the height used in the induction for Theorem 1; otherwise the induction over proof-tree height is not formally grounded.","section":"§5"},{"comment":"The paper should state explicitly which rules of Figure 3 are supported by the Crowbar prototype; the reported example is loop-free, and it is unclear whether the loopUnroll rule has been implemented or tested.","section":"§6"}],"recommendation":"major_revision","confidential_remarks":"The manuscript is a work-in-progress report. The main soundness theorem is not yet stated at the rigor expected for a journal: the almost-sure termination assumption needs to be made an explicit hypothesis of Theorem 1, and the probability-variable syntax used by the proof rules needs to be formalized. The prototype implementation is a useful complement but does not replace these formal fixes. I would support resubmission after these points are addressed."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"First thing to know: this is an honest work-in-progress paper. The core contribution is a forward-reasoning proof system for probabilistic dynamic logic, built on symbolic updates and SMT-resolved probability constraints. The soundness proof for the rules in Figure 3 is self-contained and each rule is checked; I found no circularity. The self-citation to [25] is legitimate, since the pDL semantics is established there and Proposition 1 is reused, not assumed as a target.\n\nThe authors are also clear about what is missing: loop reasoning is only sketched (loopUnroll is the only loop rule in the calculus; the invariant-based rules appear in the discussion), state-dependent probability expressions are assumed away, and the prototype is a small demo on Monty Hall with no machine-checked artifact. Given the paper says 'work in progress' in the abstract, these are acceptable limitations for a workshop-level or conference submission, but they do bound the paper's current reach.\n\nThe soft spot that bothers me most is a gap between the derivation relation and the semantic domain. The pDL semantics in Definition 2 is only defined for MDPs that reach final states with probability 1 under all policies; the paper states this in Section 3.1. But the proof system has no rule or side condition enforcing almost-sure termination. Theorem 1 says 'if Γ ⊢ φ then |= (∧Γ)→φ' without restricting Γ or the program to a.s.-terminating programs. So a proof could in principle be built for a program outside the semantic domain, making the theorem's conclusion ill-formed. This is not a deep flaw in the calculus itself, but it is a real gap in the theorem statement. The authors should either restrict the theorem to a.s.-terminating programs explicitly or add a syntactic termination check. The stress-test note is correct that the implementation only exercises a loop-free program, so the gap is not revealed.\n\nThe soundness argument for the demonic choice rule is the most delicate part; it uses a policy-based contradiction and seems to go through, but I would want a careful reader to double-check the step where 'p > E in the combined MDP' is transferred to a single branch.\n\nWho this is for: people working on deductive verification of probabilistic programs, especially those interested in forward symbolic execution as an alternative to weakest-precondition methods like Caesar. The paper deserves a serious referee; it is not a desk reject. My recommendation would be conditional acceptance: ask the authors to formalize the loop rules (at least one invariant-based rule), fix the a.s.-termination hypothesis in Theorem 1, and provide a reproducible artifact or at least more details on the implementation.","headline":"A soundness proof for a forward symbolic-execution calculus for pDL, credible but with a domain gap around almost-sure termination and loop rules still sketched.","tokens_in":14542,"tokens_out":4121,"would_cite":true,"duration_ms":34683,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B70","68Q60"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper establishes a sound forward symbolic-execution proof system for probabilistic dynamic logic.","keywords":["probabilistic dynamic logic","pGCL","symbolic execution","deductive verification","probabilistic programs","Markov decision processes","soundness","probabilistic constraints"],"falsifier":"Exhibit one pGCL program that is almost surely terminating and one closed proof tree in the calculus whose root judgment $\\Gamma \\vdash \\varphi$ is false in the pDL semantics for some valuation satisfying $\\Gamma$; Theorem 1 would then be false. Concretely, one could instrument the prototype to output every closed proof and independently compute the minimal reachability probability of the program by MDP model checking, looking for a mismatch.","tokens_in":13551,"feed_emoji":"🎲","tokens_out":5271,"duration_ms":47818,"temperature":0.7,"pith_summary":"This paper reports work in progress on a deductive proof system for probabilistic dynamic logic (pDL), a specification logic for programs in the probabilistic guarded command language pGCL. The paper's central claim is that the proposed proof system is sound: every judgment derivable by its symbolic-execution rules is valid in the pDL semantics, so the rules produce only correct probabilistic specifications. The proof system works forward, symbolically executing the program and collecting constraints on probability lower bounds as side conditions; closing a proof then reduces to checking those constraints. A prototype built on an existing symbolic execution engine and an SMT solver is used to verify a pDL specification of the Monty Hall game, showing the approach in action.","feed_headline":"Forward symbolic execution soundly proves probabilistic specs","feed_subtitle":"pDL's box modality turns reachability bounds into constraints an SMT solver can close.","key_machinery":"The central object is the symbolic-execution judgment $\\Gamma \\vdash U\\,[s]_p\\,\\varphi$ together with the pDL-constraints attached to the branching rules. Symbolic updates $U$ are syntactic substitutions that record state changes without evaluating them, a technique taken from dynamic-logic verification; pDL-constraints are inequalities over probability variables that must hold under the current update and assumptions. The rules for demonic and probabilistic choice generate the constraints $p \\leq \\min(p_1,p_2)$ and $p \\leq e\\cdot p_1 + (1-e)\\cdot p_2$, respectively, and these constraints are what carry the probabilistic content of the proof. The soundness argument connects each rule to the corresponding MDP semantics of pGCL through the properties of pDL listed in Proposition 1.","core_discovery":"On the paper's own terms, the discovery is that forward symbolic execution can be organized into a sound deductive calculus for pDL. The calculus operates on judgments $\\Gamma \\vdash U\\,[s]_p\\,\\varphi$, where $U$ is a symbolic update describing the current abstract state, $s$ is the remaining program, and $p$ is a lower bound on the probability that $\\varphi$ holds after $s$. Each rule in the rule set corresponds to one pGCL construct: assignment is turned into an update, demonic choice takes the minimum of branch probabilities, probabilistic choice takes the probability-weighted sum, and while loops are unfolded once. The side conditions are pDL-constraints on the probability variables, and a proof closes when the accumulated constraints are satisfiable. Theorem 1 states that any closed proof tree yields a valid pDL formula; the proof goes by induction on proof-tree height using the pDL properties collected in the paper's Proposition 1.","pith_inferences":["If soundness extends to richer loop rules, the same constraint-accumulation scheme could provide a forward counterpart to weakest-precondition calculi for expected values and expected runtimes.","Because the semantics assumes almost-sure termination, the proof system cannot by itself establish termination; a termination certificate would need to be supplied separately.","The approach could be compared against weakest-precondition engines on a benchmark of pGCL programs to measure proof size and automation, though the paper does not report such a comparison.","Adding observe-statements to pGCL and encoding conditioning as probabilistic constraints could connect this deductive style to verification of Bayesian inference programs."],"forward_implications":["Any specification proved with the calculus is guaranteed to be a valid pDL formula, so verified lower bounds on reachability probabilities are trustworthy.","The calculus supports forward reasoning, meaning proofs can be automated by symbolic execution and the remaining arithmetic sent to an SMT solver.","Because pDL is closed under logical operators, the proof system can express properties beyond Hoare logic, such as program equivalence relative to state formulae.","The current loop handling is a single unrolling rule, so general reasoning about probabilistic loops remains an explicitly open problem for this forward framework.","The Monty Hall example demonstrates that the method can handle nested nondeterministic and probabilistic choices and produce a closed proof with satisfiable probability constraints."],"supporting_citations":[{"why":"defines pDL and its model-theoretic semantics, including the properties in Proposition 1 used throughout the soundness proof.","marker":"[25]"},{"why":"defines pGCL, the guarded command language whose programs the proof system symbolically executes.","marker":"[21]"},{"why":"supplies dynamic logic, the modal framework that pDL builds on and extends with probabilistic reachability.","marker":"[13]"},{"why":"introduces symbolic updates, the mechanism the calculus uses to track state changes during forward execution.","marker":"[8]"},{"why":"provides the KeY-style forward reasoning setting and the proof-system formulation that this work follows.","marker":"[1]"},{"why":"supplies the modular symbolic execution engine used in the prototype implementation.","marker":"[17]"},{"why":"supplies the SMT solver used to discharge the accumulated probability constraints.","marker":"[23]"}],"fun_headline_variants":["Forward symbolic execution yields sound pDL proofs","Probabilistic dynamic logic gets a sound proof system","Symbolic execution proves probabilistic specifications","Sound calculus for probabilistic reachability proofs","Deductive proof system for pDL via forward reasoning"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The semantics and the proof system apply only to programs that terminate with probability 1 under every policy; if a program can loop forever with nonzero probability, the expected rewards in the pDL semantics are undefined and soundness no longer applies.","fun_headline_variants_meta":{"raw":{"variants":["Forward symbolic execution yields sound pDL proofs","Probabilistic dynamic logic gets a sound proof system","Symbolic execution proves probabilistic specifications","Sound calculus for probabilistic reachability proofs","Deductive proof system for pDL via forward reasoning"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000185,"raw_usage":{"total_tokens":1273,"prompt_tokens":846,"completion_tokens":427,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":462,"completion_tokens_details":{"reasoning_tokens":359}},"tokens_in":462,"tokens_out":427,"duration_ms":4317,"temperature":1.0,"reasoning_tokens":359,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T04:52:14.157761+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Exhibit one pGCL program that is almost surely terminating and one closed proof tree in the calculus whose root judgment $\\Gamma \\vdash \\varphi$ is false in the pDL semantics for some valuation satisfying $\\Gamma$; Theorem 1 would then be false. Concretely, one could instrument the prototype to output every closed proof and independently compute the minimal reachability probability of the program by MDP model checking, looking for a mismatch.","supporting_citations":[{"cited_title":"In: Proc","cited_arxiv_id":null,"evidence_quote":"defines pDL and its model-theoretic semantics, including the properties in Proposition 1 used throughout the soundness proof."},{"cited_title":"Monographs in Computer Science, Springer (2005),https://doi.org/10.1007/ b138392","cited_arxiv_id":null,"evidence_quote":"defines pGCL, the guarded command language whose programs the proof system symbolically executes."},{"cited_title":"Foundations of Computing, MIT Press (Oct 2000)","cited_arxiv_id":null,"evidence_quote":"supplies dynamic logic, the modal framework that pDL builds on and extends with probabilistic reachability."},{"cited_title":"In: Ahrendt et al","cited_arxiv_id":null,"evidence_quote":"introduces symbolic updates, the mechanism the calculus uses to track state changes during forward execution."},{"cited_title":"(eds.): Deductive Software Verification - The KeY Book - From Theory to Practice, Lecture Notes in Computer Science, vol","cited_arxiv_id":null,"evidence_quote":"provides the KeY-style forward reasoning setting and the proof-system formulation that this work follows."}],"review_version":1}