Complete Interval Abstraction Training

1. Integration point: apply the method to a small deterministic RL environment, a learned world model, or an RNN dynamics predictor. Parameterize scalar outputs of Fθ with a monotone MLP using nonnegative weights, such as softplus-constrained weights. If actions have mixed effects, use separate positive and negative monotone channels and propagate their known signs. Partition the relevant state-action domain into uniform boxes of width h. 2. Pseudocode: for each cell C=[l,r] and action cell A=[a,b], compute yminus=Fθ(l,a) and yplus=Fθ(r,b); set sminus=Qh(yminus−δ) and splus=Qh(yplus+δ+h1), where δ is a coordinatewise validation residual bound. Build lower and upper transition graphs. Run reachability from initial cells for both graphs. Add λ times the upper-only volume, |Rplus minus Rminus|, to the dynamics or policy loss. 3. Computed quantities are corner evaluations, quantization, and graph reachability. The monotonicity property is guaranteed by the architecture; δ and the effective Lipschitz constant are estimated on held-out transitions. 4. First experiment: train a two-dimensional monotone MLP model on xnext=tanh(Ax+Bu) with nonnegative A and B. Compare nominal planning, ordinary interval propagation, and the paired abstraction for h=0.2, 0.1, and 0.05. The predicted signature is linear gap reduction with h until the residual floor O(δ): halving h should approximately halve the upper-lower gap before saturation. The lower abstraction should never certify a sampled unsafe trajectory as safe, and the upper abstraction should contain every held-out sampled trajectory after residual inflation.