Counterfactual Regret for Reflective Agents with Lean-Verified Guarantees

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

cs.AIOct 10, 2026

Counterfactual Regret for Reflective Agents with Lean-Verified Guarantees

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

Organizations: School of Computer Science and Technology / School of Artificial Intelligence China University of Mining and Technology Xuzhou, China

Abstract

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.

Figures & tables

Proof obligation	Purpose of formal checking	Formal result
Probability coherence	Preserve native laws across couplings.	Prop. 4 , Thm. 7
Adaptive observations	Derive moments under bounded stopping.	Lem. 5 , Thm. 6
Generation reliability	Couple quality, trials and hard costs.	Thm. 11 , Cor. 13
Deployment stability	Control error propagation on actual paths.	Thms. 9 – 10
Composition and limits	Align task clocks and limit hypotheses.	Thm. 11 , Cor. 8
Benchmark consistency	Match cost and feedback conventions.	Thm. 14

Table 1: Proof obligations addressed by the Lean formalization.

Appendix figures & tables5 assets

Supplementary material from the paper’s appendix.

Appendix

Result	Formal endpoint
Proposition 4	NativeSemantics.Execution.expected_bounds , loss_integrable , and Realization.expected_total
Lemma 5	FiniteObservation.Round.estimate_mean , weighted_second , and StoppedObservation.Protocol.stopped_unbiased , stopped_second
Theorem 6	DependentSelection.expected_growing_selection
Theorem 7	NativeFamily.own_coupling_counterfactual
Corollary 8	NativeNoRegret.budget_tends_zero and NativeFamily.own_coupling_no_regret
Theorem 9	StateFeedbackStability.actual_loss , adaptive_resource_loss , and module FeedbackLocalOnly , declaration uniform_local_bound

Appendix

Table 2: Numbered results and their checked Lean endpoints. Prefix DRGPR. is omitted.

Symbol	Meaning and scope
$T,t,s,r,R,N$	Task horizon and task index, internal-operation index, reference-slot index, last padded slot, and slot cap $N=R+1$ . Defined in Sections 2 and 2.4 .
$\mathsf{U},\mathsf{O},\mathsf{U}(h),\mathsf{E}$	Operation and result spaces, legal next operations, and admissible extension relation. These describe operational legality, not resource penalties.
$\mathsf{X},\mathsf{M},\mathsf{A}$	Context, memory, and primitive-action spaces. Lowercase $x,m,a$ are their elements. The benchmark phase count $m$ is local to Section 4 .
$\mathcal{H}_{s}^{\rm op},\mathcal{H}_{t}^{\rm task}$	Operation-history and task-history spaces. Random task prefix $H_{t}=(Z_{0},\ldots,Z_{t})$ , with $Z_{t}\in\mathcal{Z}_{t}$ . Lowercase $h$ is a realized history.
$\pi_{i},\mu,A,\mu_{A},\mathcal{M}$	Execution-card action kernel, comparator meta-policy, complete native learner, its operation-selection kernel, and nonempty comparator class. $i$ is immutable executable identity, not a primitive action.
$\sigma_{t},Y_{t},L_{T},J_{T},R_{T}$	Common task scorer, scalar task loss, realized cumulative loss, expected cumulative loss, and own-history regret from equation 1 . Unqualified $R_{T}$ abbreviates $R_{T}(A,\mathcal{M})$ .

Appendix

Table 3: Semantic and algorithmic notation. Domains and probability laws are part of the definitions.

Endpoint or charge	Definition, outgoing comparison, and correspondence
$J_{A}^{\mathrm{nat}}$	Expected native learner loss $J_{T}(A)$ . Expectation of realA . Its difference from $J_{A}^{\mathrm{ref}}$ is bounded by $E_{A}$ .
$J_{A}^{\mathrm{ref}}$	Expected reference learner endpoint, expectation of refA . Its difference from $J^{\mathrm{sel}}$ is bounded by $F+\mathcal{P}_{b}+D_{A}$ .
$J^{\mathrm{sel}}$	$\sum_{r=0}^{R}\mathbb{E}_{\Gamma_{\mu}}\ell^{\mathrm{ref}}_{r}(J_{r})$ , identified with Experiment.selectedTotal . Its comparison to $J_{\mu}^{\mathrm{av}}$ is the proved selection bound.
$J_{\mu}^{\mathrm{av}}$	$\sum_{r=0}^{R}\mathbb{E}_{\Gamma_{\mu}}\ell^{\mathrm{ref}}_{r}(v_{r})$ , identified with Experiment.availableTotal . Its difference from $J_{\mu}^{\mathrm{al}}$ is bounded by $G$ .
$J_{\mu}^{\mathrm{al}}$	Aligned represented comparator score, expectation of aligned . Its difference from $J_{\mu}^{\mathrm{cl}}$ is bounded by $bS$ .
$J_{\mu}^{\mathrm{cl}}$	Score after removing alignment, expectation of clean . Its difference from $J_{\mu}^{\mathrm{path}}$ is bounded by $h_{\mathrm{resp}}(S+1)+D_{C}$ .

Appendix

Table 4: Expected endpoints, directed charges, and exact Lean field names. All expectations use

\Gamma_{\mu}

Symbol	Meaning and scope
$S_{t},s,K_{t},L_{t},p^{\rm init}$	Complete finite state, its realization, native and reference state-transition kernels, and common initial distribution in Section 3.2 . The capital switch bound $S$ is not a state.
$c_{t},V^{L}_{t,n},h_{t},\bar{H}$	Common immediate state score, $n$ -step continuation value from state-time $t$ , local continuation-range envelope, and its uniform bound. $\bar{H}$ is distinct from the response scale $h_{\mathrm{resp}}$ .
$\operatorname{TV},D_{\mathrm{KL}},\varepsilon_{t},\bar{\varepsilon}$	Total variation, relative entropy, local full-state TV envelope, and uniform activity-scaled TV factor. Relative entropy uses natural logarithms and the common support in Appendix F .
$\chi_{t},r_{t},c_{\min},B_{A},B_{C}$	Nonnegative update activity, actual-path resource charge, strictly positive cost per unit activity, and learner/comparator resource envelopes. Here $r_{t}(s)$ is a resource function, not a slot number.
$\zeta_{t},\mathcal{D}_{t,n},\kappa$	Local product $h_{t}\varepsilon_{t}$ , its accumulated $K$ -Bellman charge, and $\bar{H}\bar{\varepsilon}/c_{\min}$ . The proof integrates along the native $K$ law.
$e,k,k_{e},\mathcal{H}_{e,k}^{\rm gen}$	Generation episode, trial index, number of trials, and episode-specific completed-trial space. Trials and task rounds need not coincide.

Appendix

Table 5: Notation specific to stability, generation, and the paid binary benchmark.

Component	Role and scope of the contribution
Growing selection	Classical exponential weights and sharing, checked on history-dependent finite types.
Native transfer	Directed own-law composition, with application-dependent interface certificates.
Local stability	Range-sensitive TV telescoping, specialized to actual-path adaptive resource charging.
Local generation	Conditional coverage and per-task quality bound the generation opportunity gap.
Paid benchmark	Explicit common-model information lower and primitive upper, near matching only under equation 28 .
Lean artifact	Reproducible verification of the conditional mathematical chain and its explicit interfaces.

Appendix

Table 6: Roles of the results in the conditional native-transfer analysis.

Self-Reflection in Language Model Agents

See all 36 papers

LoongReflect: Boosting Long-Horizon Reflection in Search Agents via Global Perspective Distillation
Aug 12, 2026Zhixin Zhang, Xinke Jiang, Zhibang Yang +5LLM-Guided RL LLM Agents
School of Computer Science, Peking University, Beijing, China · National Engineering Research Center for Software Engineering, Peking University, Beijing, China · Key Laboratory of High Confidence Software Technologies, Ministry of Education, Beijing, China +2
COUNTERMEM: World-Model Verified Counter-Factual Memory for Language Agents
Sep 25, 2026Hongji Pu, Ruixiang Tang, Yongfeng ZhangMemory-Augmented Language Model Agents Persistent Memory for Language Models
University of Illinois Urbana–Champaign · Department of Computer Science, Rutgers University
Honest Lying: Understanding Memory Confabulation in Reflexive Agents
May 28, 2026Prakhar Dixit, Sadia Kamal, Tim OatesAI Agent Reliability LLM Self-Refinement
Department of Computer Science, University of Maryland Baltimore County, Baltimore, MD, USA.

Aug 12, 2026J/K move · Enter open · S save

LoongReflect: Boosting Long-Horizon Reflection in Search Agents via Global Perspective Distillation

Zhixin Zhang, Xinke Jiang, Zhibang Yang, Weixuan Xu+4

School of Computer Science, Peking University, Beijing, China · National Engineering Research Center for Software Engineering, Peking University, Beijing, China · Key Laboratory of High Confidence Software Technologies, Ministry of Education, Beijing, China+2

LLM-Guided RL LLM Agents Long-Horizon LLM Agents RL for LLM Agents Memory-Augmented Language Model Agents Self-Reflection in Language Model Agents

Open paper AskPDF arXiv

Large language model agents increasingly rely on long-horizon reasoning to solve complex tasks involving planning, tool use, and memory. A critical capability in such settings is reflection: assessing trajectory progress, identifying missing evidence and unreliable intermediate states, and deciding whether to continue, revise, or abandon the current branch. Learning effective reflection, however, is challenging because reflection is performed locally within the current branch, whereas its utility can only be determined by its contribution to the final trajectory outcome. This local-global mismatch makes outcome-based reinforcement learning provide only local, sparse and delayed supervision for reflective decisions. To solve these, we propose LoongReflect, a training framework that formulates reflection as a memory-control policy. The agent operates over a reversible trajectory tree using explicit reflect and backtrack actions. Reflection consolidates verified facts, missing evidence, and branch-specific risks into working memory, while backtracking removes an unreliable branch from the active context and preserves a concise corrective lesson. To learn this policy, LoongReflect combines two complementary signals through a look-ahead, extragradient-style coordination mechanism. A fast channel distills globally informed reflective behavior from a privileged teacher, with supervision restricted to reflection and backtracking tokens. A slow channel optimizes complete trajectories using outcome-based GRPO, aligning local control decisions with final task success. Experiments on multi-hop retrieval-augmented generation and mathematical reasoning benchmarks demonstrate consistent improvements over outcome-only reinforcement learning and self-distillation baselines.

Abstract

Self-Reflection in Language Model Agents

Explore similar work

LoongReflect: Boosting Long-Horizon Reflection in Search Agents via Global Perspective Distillation

COUNTERMEM: World-Model Verified Counter-Factual Memory for Language Agents

Honest Lying: Understanding Memory Confabulation in Reflexive Agents