Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory

Lean4Agent 用 Lean 4 形式化语言描述 agent workflow 和执行轨迹，提供 FormalAgentLib 来验证语义一致性、定位轨迹暴露的运行时失败，并用 LeanEvolve 基于验证结果修订 workflow。实验覆盖 SWE-Bench-Verified hard subset 和 ELAIP-Bench 子集、5 个主流 LLM；通过验证的 workflow 平均比失败 workflow 高 11.94%，LeanEvolve 进一步平均提升 SWE 表现 7.47%。