Counterfactual Regret for Reflective Agents with Lean-Verified Guarantees
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 obligation | Purpose of formal checking | Formal result |
|---|---|---|
| Probability coherence | Preserve native laws across couplings | Prop. 4, Thm. 7 |
| Generation reliability | Couple quality, trials and hard costs | Thm. 11, Cor. 13 |
| Deployment stability | Control error propagation on actual paths | Thms. 9–10 |
| Benchmark consistency | Match cost and feedback conventions | Thm. 14 |
| Concrete instantiation | Derive interfaces from native execution | Cor. 12, Prop. 16 |
