Descripción actualizada lista para pegar en Zenodo: HADD: Extending the BDI Abstract Interpreter for Stochastic Sensors presents a conservative formal extension of the classical Belief–Desire–Intention abstract interpreter proposed by Rao and Georgeff in "BDI Agents: From Theory to Practice" (ICMAS 1995). The paper does not propose to replace the BDI interpreter. It proposes to evolve it along a specific axis: the epistemic nature of its sensors. The original BDI interpreter was designed for deterministic sensors — radar, altimeters, flight data — where the assumption that sensor output represents the likely state of the environment holds reliably enough that no formal verification mechanism was necessary. Rao and Georgeff acknowledged this assumption explicitly in footnote 1 of their 1995 paper, marking the boundary of their own model. Thirty years later, large language models are routinely used as the perceptual front-end of autonomous agents. An LLM is a sensor of a kind that did not exist in 1995: it produces fluent, high-confidence output that may not correspond to reality. The sensor-accuracy assumption that footnote 1 identified as occasionally violated is, for LLM sensors, violated systematically. HADD is the natural continuation of the reasoning Rao and Georgeff left at the edge of that footnote. The paper introduces three components inserted at precisely identified points in the original loop, without modifying any existing component. An EVR gate Φ sits between perception and belief commitment, intercepting belief deltas that fail epistemic verification before they can contaminate the belief store. EMRE, an epistemically calibrated adapter, adjusts the declared confidence of LLM output per tenant and per document type, operating in three data-maturity modes and feeding the result to Φ. A Verification Tribunal verifies plan epistemic grounding and operational legality before any action executes. The resulting cycle is: perceive → verify → update beliefs → deliberate → validate → execute → audit. The central formal result is the Learning Boundary Theorem (T1): EMRE modifies exclusively the confidence field of perception output, leaving every other field immutable and therefore preserving all original BDI invariants — including downstream determinism, tenant isolation, the single belief-entry path, pre-execution verification, and the append-only audit trail. A Coverage Proposition (P2) establishes that, when the verifier and judge sets are complete, every executed action carries a recorded verdict against the declared set of verifiers, retrievable through the audit trail before execution. A Holonic Compositional Theorem (T3) proves that certifiability scales: if a single HADD agent satisfies the invariants, any holonic composition of HADD agents satisfies them too. The paper is explicit about what it does not claim. The verifier taxonomy is declared and finite; its exhaustiveness with respect to all possible hallucination phenomena is left as an open conjecture. MINERVA, the reference implementation, was benchmarked over 30 documents confirming end-to-end realizability across twelve desire types, with Epistemic Capture Rate ECR = 1 (TPR = 1.0, FPR = 0.0), BDI desire selection at ~1μs and O(1) in the number of agents, and Tribunal verification at <3μs per plan. The lexical-grounding verifiers currently produce false positives on common vocabulary; calibrating them toward semantic entailment is identified as a prerequisite for any meaningful quantitative evaluation, and is the subject of a dedicated forthcoming paper. The primary contribution is architectural and formal: the BDI interpreter can be evolved conservatively as the epistemic character of its sensors changes, and T1 is the form such an evolution's correctness proof should take. HADD is the first instance of that pattern, not its endpoint.
Alejandro Jaime (Sat,) studied this question.