← All papers
First page of Counterfactual Regret for Reflective Agents with Lean-Verified Guarantees

Counterfactual Regret for Reflective Agents with Lean-Verified Guarantees

Zhongnian Li, Shi Xu, Mengting Xu, Peng Ying, Xinzheng Xu

cs.AI Oct 10, 2026 · v1
All thirteen numbered regret results and a concrete native instance are formalized in Lean 4 with Mathlib, with a public proof repository.
Reflective language agents reuse feedback and memory to adapt across tasks without updating model weights. However, existing guarantees for policy selection and action generation do not by themselves establish when local reflection yields long-term performance guarantees for the complete agent under resource constraints. In this paper, we address this gap by deriving sufficient conditions for sublinear counterfactual regret from local generation and deployment guarantees, while retaining the native controller. Specifically, we establish a resource-sensitive transfer that bounds full-state deployment discrepancies along actual execution paths and preserves the own-history laws of both learner and comparator. Besides, local generation reliability yields a cumulative generation opportunity bound, linking policy acquisition to long-term performance through an explicit quality, coverage, and hard-budget tradeoff. To verify these guarantees, we formalize the conditional proof chain for all thirteen numbered theoretical results in Lean, including a native instance with repeated policy growth and imperfect validation.

Existing guarantees for policy selection and action generation in reflective language agents do not establish when local reflection yields long-term performance guarantees for the complete agent under resource constraints.

The authors derive sufficient conditions for sublinear counterfactual regret against resource-feasible comparators while retaining the native controller. They do this through a resource-sensitive transfer bounding deployment discrepancies along actual execution paths, and through a cumulative generation opportunity bound derived from local reliability. The conditional proof chain for all thirteen numbered results is formalized in Lean 4 with Mathlib. The formalization covers probability coherence, adaptive observation moments, deployment stability, and a concrete native instance.

The authors obtain a conditional sublinear regret guarantee with an explicit quality, coverage, and hard-budget tradeoff. They prove near-matching upper and lower bounds for a paid-growth sparse-feedback benchmark. All thirteen results are machine-checked in Lean, and the proofs are released in a public repository.

Proof obligationPurpose of formal checkingFormal result
Probability coherencePreserve native laws across couplingsProp. 4, Thm. 7
Generation reliabilityCouple quality, trials and hard costsThm. 11, Cor. 13
Deployment stabilityControl error propagation on actual pathsThms. 9–10
Benchmark consistencyMatch cost and feedback conventionsThm. 14
Concrete instantiationDerive interfaces from native executionCor. 12, Prop. 16
Proof obligations addressed by the Lean formalization (excerpt)