Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory

• URL: http://arxiv.org/abs/2606.06523v1
• Date: Tue, 02 Jun 2026 18:46:50 GMT
• Title: Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory
• Abstract summary: Equipping Large Language Models (LLMs) to execute reliable multistep has become a central challenge in artificial intelligence.<n>This challenge mirrors a long-standing problem in mathematics, where the ambiguity of natural languages (NLs) motivates the development of formal languages (FLs)<n>We propose **Lean4Agent**, the first framework that uses Lean4, a dependent-type FL to model and verify agent behavior.
• Score: 17.95201244576703
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Equipping Large Language Models (LLMs) to execute reliable multi-step workflows has become a central challenge in artificial intelligence. Despite recent advances in LLMs' agentic capabilities, most agent systems still lack formal methods for specifying, verifying, and debugging their workflow and execution trajectories. This challenge mirrors a long-standing problem in mathematics, where the ambiguity of natural languages (NLs) motivates the development of formal languages (FLs). Inspired by this paradigm, we propose **Lean4Agent**, to the best of our knowledge, the first framework that uses Lean4, a dependent-type FL to model and verify agent behavior. **Lean4Agent** launches **FormalAgentLib**, an extensible Lean4 library for formally modeling and verifying agent workflows' semantic consistency under explicit assumptions, and enabling localization of execution-time failures revealed by trajectories. Building on **FormalAgentLib**, we further develop **LeanEvolve**, which applies results in **FormalAgentLib** to revise workflows to enhance its capability. Extensive experiments on a hard problem subset of SWE-Bench-Verified and a subset of ELAIP-Bench across 5 leading LLMs indicate that the verification-passing workflows outperform the failing ones by an average of **11.94%**, and **LeanEvolve** further improves SWE performance by **7.47%** on average. Furthermore, **Lean4Agent** establishes a foundation for a new field of using expressive dependent-type FL to formally model and verify agent behavior.

Related papers

• A Phased Workflow for Operating LLM-Based Coding Agents [0.7874708385247353]
  We report on a phased workflow for operating coding agents developed by the AI research team at Infobip.<n> Context management is the central concern, addressed through four strategies applied at each phase to counter known failure modes.<n>We identify two open problems: the absence of metrics for workflow effectiveness and the gap between formalized context management components and the workflow-level patterns that practitioners need.
  arXiv  Detail & Related papers  (2026-08-31T12:39:26Z)
• AgentArk: Distilling Multi-Agent Intelligence into a Single LLM Agent [57.10083973844841]
  AgentArk is a novel framework to distill multi-agent dynamics into the weights of a single model.<n>We investigate three hierarchical distillation strategies across various models, tasks, scaling, and scenarios.<n>By shifting the burden of computation from inference to training, the distilled models preserve the efficiency of one agent while exhibiting strong reasoning and self-correction performance of multiple agents.
  arXiv  Detail & Related papers  (2026-02-03T19:18:28Z)
• R&D-Agent: An LLM-Agent Framework Towards Autonomous Data Science [70.1638335489284]
  High-level machine learning engineering tasks remain labor-intensive and iterative.<n>We introduce R&D-Agent, a comprehensive, decoupled, and framework that formalizes the machine learning process.<n>R&D-Agent defines the MLE into two phases and six components, turning agent design for MLE into a principled, testable process.
  arXiv  Detail & Related papers  (2025-05-20T06:07:00Z)
• FlowAgent: Achieving Compliance and Flexibility for Workflow Agents [31.088578094151178]
  FlowAgent is a novel agent framework designed to maintain both compliance and flexibility.<n>Building on PDL, we develop a comprehensive framework that empowers LLMs to manage OOW queries effectively.<n>We present a new evaluation methodology to rigorously assess an LLM agent's ability to handle OOW scenarios.
  arXiv  Detail & Related papers  (2025-02-20T07:59:31Z)
• Large Language Model Agent for Fake News Detection [33.06422916067896]
  FactAgent is an agentic approach of utilizing large language models for fake news detection. It emulates human expert behavior in verifying news claims without any model training. It offers insights into the reasoning process of fake news detection for end users.
  arXiv  Detail & Related papers  (2024-04-30T06:55:27Z)
• Enhancing the General Agent Capabilities of Low-Parameter LLMs through Tuning and Multi-Branch Reasoning [56.82041895921434]
  Open-source pre-trained Large Language Models (LLMs) exhibit strong language understanding and generation capabilities. When used as agents for dealing with complex problems in the real world, their performance is far inferior to large commercial models such as ChatGPT and GPT-4.
  arXiv  Detail & Related papers  (2024-03-29T03:48:12Z)
• Agent-FLAN: Designing Data and Methods of Effective Agent Tuning for Large Language Models [56.00992369295851]
  Open-sourced Large Language Models (LLMs) have achieved great success in various NLP tasks, however, they are still far inferior to API-based models when acting as agents. This paper delivers three key observations: (1) the current agent training corpus is entangled with both formats following and agent reasoning, which significantly shifts from the distribution of its pre-training data; (2) LLMs exhibit different learning speeds on the capabilities required by agent tasks; and (3) current approaches have side-effects when improving agent abilities by introducing hallucinations. We propose Agent-FLAN to effectively Fine-tune LANguage models for Agents.
  arXiv  Detail & Related papers  (2024-03-19T16:26:10Z)
• DS-Agent: Automated Data Science by Empowering Large Language Models with Case-Based Reasoning [56.887047551101574]
  We present DS-Agent, a novel framework that harnesses large language models (LLMs) agent and case-based reasoning (CBR) In the development stage, DS-Agent follows the CBR framework to structure an automatic iteration pipeline, which can flexibly capitalize on the expert knowledge from Kaggle. In the deployment stage, DS-Agent implements a low-resource deployment stage with a simplified CBR paradigm, significantly reducing the demand on foundational capabilities of LLMs.
  arXiv  Detail & Related papers  (2024-02-27T12:26:07Z)
• AgentBench: Evaluating LLMs as Agents [99.12825098528212]
  Large Language Model (LLM) as agents has been widely acknowledged recently.<n>We present AgentBench, a benchmark that consists of 8 distinct environments to assess LLM-as-Agent's reasoning and decision-making abilities.
  arXiv  Detail & Related papers  (2023-08-07T16:08:11Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.