Pipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

POMDPs and belief-state planning — Examples

1 · Prerequisites

2 · Logical flowchart

3 · Definitions, theorems and proofs

None yet.

4 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedjudge pass (gpt-6-luna)Open item page →

A two-state POMDP update changes a three-to-one prior to nine-to-one

Example

Let $S = {s_{0}, s_{1}}$ , $A = {a}$ , $Ω = {x, y}$ , reward alphabet ${0}$ , and horizon $H = 1$ with $γ = 1$ . For each $i \in {0, 1}$ , the joint next-state/reward law assigns probability one to $(s_{i}, 0)$ from $(s_{i}, a)$ , so the hidden state remains fixed and the reward is zero. Let $b_{0} (s_{0}) = 3 / 4$ , $b_{0} (s_{1}) = 1 / 4$ , and set $O (x ∣ s_{0}) = 3 / 4$ , $O (x ∣ s_{1}) = 1 / 4$ , $O (y ∣ s_{0}) = 1 / 4$ , and $O (y ∣ s_{1}) = 3 / 4$ . The probability of observing $x$ is $5 / 8$ , and after $x$ the belief is $b_{1} (s_{0}) = 9 / 10$ , $b_{1} (s_{1}) = 1 / 10$ .

Facts & Assumptions

Given: The finite POMDP model in the example and the observation $x$ .

[F1]

The state transition is the marginal of the specified finite joint reward-transition law, and each $O (\cdot ∣ s^{'})$ is a probability distribution. Finite partially observable Markov decision process

[F2]

The predicted belief is $\overset{ˉ}{b} (s^{'}) = \sum_{s} T (s^{'} ∣ s, a) b (s)$ , the observation probability is $q (o ∣ b, a) = \sum_{s^{'}} O (o ∣ s^{'}) \overset{ˉ}{b} (s^{'})$ , and the positive-probability update is $τ (b, a, o) (s^{'}) = O (o ∣ s^{'}) \overset{ˉ}{b} (s^{'}) / q (o ∣ b, a)$ . Belief states and the finite Bayes filter

[F3]

The predicted law and observation probabilities normalize, and $τ$ is a probability vector when $q > 0$ . The finite POMDP Bayes filter is a probability kernel

[F4]

Finite sums over finite index sets are well defined and enumeration-independent. The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form

Verification

1.1givenF1F2

The transition marginal is the identity on $S$ , so the predicted law after action $a$ is ${\overset{ˉ}{b}}_{1} (s_{0}) = 3 / 4$ and ${\overset{ˉ}{b}}_{1} (s_{1}) = 1 / 4$ .

2.1step 1.1F2F4algebra

The observation normalizer is $q (x ∣ b_{0}, a) = (3 / 4) (3 / 4) + (1 / 4) (1 / 4) = 9 / 16 + 1 / 16 = 5 / 8 > 0$ .

3.1step 1.1step 2.1F2F3algebra∎

The update gives $b_{1} (s_{0}) = (3 / 4) (3 / 4) / (5 / 8) = (9 / 16) / (10 / 16) = 9 / 10$ and $b_{1} (s_{1}) = (1 / 4) (1 / 4) / (5 / 8) = (1 / 16) / (10 / 16) = 1 / 10$ . Both coordinates are nonnegative and sum to one, in agreement with [F3].

ExampleConstruction: AI-generatedVerification: AI-generatedOpen item page →

An observation with identical state likelihoods leaves the belief unchanged

Example

Let $S = {s_{0}, s_{1}}$ , $A = {a}$ , $Ω = {x}$ , reward alphabet ${0}$ , horizon $H = 1$ , and discount $γ = 1$ . From each state, the joint next-state/reward law assigns probability one to the same state with reward zero. Let $b_{0} (s_{0}) = 2 / 3$ , $b_{0} (s_{1}) = 1 / 3$ , and let $O (x ∣ s_{0}) = O (x ∣ s_{1}) = 1$ . Then $q (x ∣ b_{0}, a) = 1$ and the posterior after $x$ is again $(2 / 3, 1 / 3)$ ; the observation does not distinguish the two hidden states.

Facts & Assumptions

Given: The finite POMDP model in the example and the observation $x$ .

[F1]

The finite POMDP transition is the marginal of its joint reward-transition law, and each observation law is normalized. Finite partially observable Markov decision process

[F2]

The predicted state distribution, observation normalizer, and positive-probability Bayes update are the finite sums and quotient in the belief-filter definition. Belief states and the finite Bayes filter

[F3]

A positive-normalizer update is a probability vector and the induced belief transition is a probability kernel. The finite POMDP Bayes filter is a probability kernel

[F4]

Finite sums over a finite index set are well defined and enumeration-independent. The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form

Verification

1.1givenF1F2

The hidden-state transition is the identity, so the predicted distribution is $\overset{ˉ}{b} (s_{0}) = 2 / 3$ and $\overset{ˉ}{b} (s_{1}) = 1 / 3$ .

2.1step 1.1F2F4algebra

The normalizer is $q (x ∣ b_{0}, a) = 1 \cdot (2 / 3) + 1 \cdot (1 / 3) = 1 > 0$ .

3.1step 1.1step 2.1F2F3algebra∎

The posterior coordinates are $τ (b_{0}, a, x) (s_{0}) = 1 \cdot (2 / 3) / 1 = 2 / 3$ and $τ (b_{0}, a, x) (s_{1}) = 1 \cdot (1 / 3) / 1 = 1 / 3$ . They sum to one as required by [F3], so the observation leaves the belief unchanged.

ExampleConstruction: AI-generatedVerification: AI-generatedjudge pass (gpt-6-luna)Open item page →

A zero-likelihood observation has no posterior update

Example

Let $S = {s_{0}, s_{1}}$ , $A = {a}$ , $Ω = {x, y}$ , reward alphabet ${0}$ , horizon $H = 1$ , and discount $γ = 1$ . From each state, the joint next-state/reward law assigns probability one to that same state with reward zero. Put $b_{0} (s_{0}) = 1$ , $b_{0} (s_{1}) = 0$ , and let $O (x ∣ s_{0}) = 1$ , $O (y ∣ s_{0}) = 0$ , $O (x ∣ s_{1}) = 0$ , and $O (y ∣ s_{1}) = 1$ . Then the observation distribution has $q (y ∣ b_{0}, a) = 0$ and $q (x ∣ b_{0}, a) = 1$ , so $τ (b_{0}, a, y)$ is undefined and the belief transition uses only the positive-mass $x$ branch.

Facts & Assumptions

Given: The finite POMDP model in the example, the prior $b_{0} = δ_{s_{0}}$ , and the action $a$ .

[F1]

The finite POMDP uses probability transition and observation laws; the reward is not part of the observed history. Finite partially observable Markov decision process

[F2]

The predicted state distribution, observation normalizer, positive-domain Bayes update, and omission of zero-normalizer observations are defined by the finite belief filter. Belief states and the finite Bayes filter

[F3]

Observation probabilities sum to one, and the induced belief transition is a probability kernel using only positive-probability branches. The finite POMDP Bayes filter is a probability kernel

[F4]

Finite sums over a finite index set are well defined. The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form

Verification

1.1givenF1F2

The hidden-state transition is the identity, so the predicted state distribution after $a$ is $\overset{ˉ}{b} (s_{0}) = 1$ and $\overset{ˉ}{b} (s_{1}) = 0$ .

2.1step 1.1F2F4algebra

The normalizers are $q (y ∣ b_{0}, a) = O (y ∣ s_{0}) \overset{ˉ}{b} (s_{0}) + O (y ∣ s_{1}) \overset{ˉ}{b} (s_{1}) = 0$ and $q (x ∣ b_{0}, a) = 1$ .

3.1step 2.1F2F3∎

Since $q (y ∣ b_{0}, a) = 0$ , the definition makes $τ (b_{0}, a, y)$ undefined and omits the $y$ term from $K$ . The only positive observation branch is $x$ with mass one by step 2.1, so $K$ assigns total mass one to $τ (b_{0}, a, x)$ and no mass to an impossible $y$ update, as required by [F3].

ExampleConstruction: AI-generatedVerification: AI-generatedjudge pass (gpt-6-luna)Open item page →

A finite POMDP family has exponentially many witnessed alpha vectors

Example

For each $n \in N$ with $0 < n$ , let $I_{n} = {t \in N : t < n}$ be a clock set and let a hidden binary string be a function $x : I_{n} \to {0, 1}$ . Write $σ (t)$ for the natural successor. Put $S = {(x, t) : x \in {0, 1}^{I_{n}}, t \in I_{n}}$ , $A = {0, 1}$ , $Ω = {o}$ , and reward alphabet $R = {0, 1}$ . For $t \in I_{n}$ , define $t^{+} = σ (t)$ if $σ (t) \in I_{n}$ , and $t^{+} = t$ otherwise. Under action $a$ at $(x, t)$ , the joint next-state/reward law assigns probability one to next state $(x, t^{+})$ and reward $1_{{a = x (t)}}$ ; the sole observation $o$ occurs with probability one. Let $x^{\circ} : I_{n} \to {0, 1}$ be the constant-zero string, take $b_{0} = δ_{(x^{\circ}, 0)}$ , and set horizon $H = n$ and $γ = 1$ . There are exactly $2^{n}$ depth- $n$ policy trees, one for each binary action string $y : I_{n} \to {0, 1}$ . The alpha vector of tree $y$ , evaluated at state $(x, 0)$ , is $\sum_{t < n} 1_{{x (t) = y (t)}}$ . At the point-mass belief $δ_{(y, 0)}$ this vector has value $n$ , while every distinct action string has value strictly less than $n$ . Therefore all $2^{n}$ alpha vectors are distinct and each has a witness belief in $Δ (S)$ , which need not be reachable from the specified initial belief; the family has state count $n 2^{n}$ .

Facts & Assumptions

Given: A natural number $n$ with $0 < n$ and the finite POMDP described in the example, with initial belief $δ_{(x^{\circ}, 0)}$ , horizon $n$ , and discount $1$ .

[F1]

A finite POMDP has finite state, action, and observation sets, transition and observation probability laws, an initial belief, and a finite-horizon objective. Finite partially observable Markov decision process

[F2]

A depth-zero tree has vector $0$ ; a depth- $(h + 1)$ tree consists of a root action and one subtree per observation, with vector given by the finite transition-observation backup. Exhaustive finite-horizon POMDP alpha-vector backup

[F3]

The value at horizon $H$ is the maximum of $b \cdot α$ over the backup's vectors, and a vector is witnessed when it attains that maximum at some belief. Finite-horizon POMDP values are piecewise-linear and convex

[F4]

For finite sets, the function set $X^{Y}$ is finite of cardinality $∣ X ∣^{∣ Y ∣}$ . The set $A^{B}$ of functions $B \to A$ between finite sets is finite, with $∣ A^{B} ∣ = ∣ A ∣^{∣ B ∣}$

[F5]

Finite Cartesian products are finite and their cardinalities multiply; cardinality is the natural number equinumerous with the set. The product rule: $∣ A \times B ∣ = ∣ A ∣ ∣ B ∣$ , and $∣ \prod_{i < m} A_{i} ∣ = \prod_{i < m} ∣ A_{i} ∣$ , The cardinality $∣ A ∣$ of a finite set

[F6]

Natural powers start at $m^{0} = 1$ and satisfy $m^{h + 1} = m^{h} m$ . Exponentiation of natural numbers, $m^{n}$ , and its agreement with the integer power in $R$

[F7]

Finite sums over an initial segment are recursively defined and preserve termwise inequalities. Finite sums and finite products, by recursion, Laws of finite sums and finite products

[F8]

A belief is a probability vector on $S$ , so the point mass at any state of $S$ is a belief. Belief states and the finite Bayes filter

[F9]

In the von Neumann naturals, $0 \in n$ when $n \neq 0$ , $k \in σ (k)$ , every natural number is transitive, and $σ$ is the successor used by the clock. The natural numbers $N$ (von Neumann), On $N$ the order is membership: $m < n ⟺ m \in n$ , Every natural number is a transitive set and is not a member of itself

[F10]

The clock set $I_{n} = {t \in N : t < n}$ equals the von Neumann natural $n$ , so it is finite and has cardinality $n$ . A finite initial segment of the naturals has its index as cardinality

[F11]

If a property holds at $0$ and its truth at $k$ implies its truth at $σ (k)$ for every $k \in N$ , it holds for every natural number. The principle of mathematical induction

Verification

1.1givenF1F4F5F6F9F10

By [F10], $I_{n}$ is finite with cardinality $n$ . Hence the function set ${0, 1}^{I_{n}}$ has cardinality $2^{n}$ by [F4] and [F6], and the product rule [F5] gives $∣ S ∣ = n 2^{n}$ . Since $0 < n$ , [F9] gives $0 \in I_{n}$ , so $(x^{\circ}, 0) \in S$ and its point mass is a probability distribution. The action, observation, and reward sets are finite and nonempty. For each state and action the specified joint mass assigns one next-state/reward pair probability one, and the singleton observation law has total mass one; thus the data satisfy [F1].

1.2givenF3

With one observation, the tree-count recurrence in [F3] gives $N_{0} = 1$ and $N_{h + 1} = 2 N_{h}$ : each tree is determined by its root action and its unique observation continuation.

2.1step 1.2F4F6F11inductionalgebra

Induction using [F11] and the recursion for powers [F6] gives $N_{h} = 2^{h}$ for every $h$ : the base is $N_{0} = 1 = 2^{0}$ , and $N_{h + 1} = 2 N_{h} = 2 \cdot 2^{h} = 2^{h + 1}$ . A depth- $n$ tree with one observation is exactly an action string $y : I_{n} \to {0, 1}$ , so there are exactly $2^{n}$ such trees by [F4].

2.2givenstep 1.1F9F10F11induction

Let $c_{k}$ be the clock coordinate after $k$ transitions from the initial clock $0$ . We prove by induction that $k \in I_{n}$ implies $c_{k} = k$ . At $k = 0$ this holds. If $σ (k) \in I_{n}$ , then $k \in σ (k)$ by [F9], and transitivity of the natural $n = I_{n}$ from [F10] gives $k \in I_{n}$ ; the induction hypothesis gives $c_{k} = k$ . Since $σ (k) \in I_{n}$ , the transition rule advances to $c_{σ (k)} = σ (k)$ . If $σ (k) \notin I_{n}$ , the successor case of the implication is vacuous. The induction principle [F11] proves the claim for every $k$ .

3.1givenstep 2.2F1F2F7

Therefore, at each decision time $t \in I_{n}$ from initial state $(x, 0)$ , the hidden state is $(x, t)$ . Under the tree $y$ its reward at that time is $1_{{x (t) = y (t)}}$ , and the finite horizon sum with $γ = 1$ gives $α_{y} (x, 0) = \sum_{t < n} 1_{{x (t) = y (t)}}$ .

4.1givenstep 2.1step 3.1F3F7F8algebra∎

For each string $y$ , the point mass $δ_{(y, 0)}$ is a belief by [F8], and [F3] evaluates its tree there as $α_{y} (y, 0) = n$ . If $z \neq y$ , some coordinate $t$ differs, so the sum for $α_{z} (y, 0)$ has at least one zero term and all other terms at most one; its value is strictly less than $n$ . Thus $y$ is the unique maximizing tree at $δ_{(y, 0)}$ , so its vector is witnessed. If $y \neq z$ , their values at $δ_{(y, 0)}$ differ, so their vectors are distinct. By step 2.1 there are $2^{n}$ strings; hence the example has exactly $2^{n}$ distinct witnessed vectors.