Research map / Large language models / AI and society

Position: Trustworthy AI Agents Require the Integration of Large Language Models and Formal Methods

ICML 2025 · Large language models › AI and society · approach: Critiques of LLM claims and judging · 0 citations (OpenAlex)

Read the paperCheck your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

Position paper arguing that trustworthy AI agents need bidirectional integration of LLMs and formal methods, illustrated with a PAT model-checking agent prototype and conceptual designs for theorem proving, SMT, and LLM testing/monitoring.

Problem

LLMs hallucinate and lack formal correctness guarantees, while formal methods are rigorous but hard to scale and adopt; the paper argues that trustworthy AI agents require combining the two.

Approach

Proposes a bidirectional fusion: LLMs automate and broaden formal methods (autoformalization, model checking, theorem proving, premise selection), while formal tools (model checkers, SMT solvers, logic-based test generation, runtime monitoring) certify and constrain LLM agent behavior.

Key results

• In a car key-lock case study, GPT-4o's directly generated PAT model allowed the key to be locked inside the car; PAT counterexample traces let the LLM repair the model so it passes verification.
• The paper reports no quantitative benchmark results for the proposed PAT agent prototype.

Limitations

• Evidence is limited to case studies and conceptual explorations without systematic quantitative evaluation.
• Generalization to other formal tools (Alloy, PRISM, UPPAAL) is asserted but not demonstrated.
• Formal verification of LLMs faces non-determinism, high input dimensionality, and lack of formal specification.

Experimental setup

Baselines: GPT-4o direct formal model generation

Builds on: PAT Sledgehammer Chain-of-thought

Closest papers by meaning

• Position: TrustLLM: Trustworthiness in Large Language Models (ICML 2024 · similarity 0.87)
• Do as We Do, Not as You Think: the Conformity of Large Language Models (ICLR 2025 · similarity 0.86)
• Can Large Language Model Agents Simulate Human Trust Behavior? (NeurIPS 2024 · similarity 0.86)
• To trust or not to trust: Attention-based Trust Management for LLM Multi-Agent Systems (NeurIPS 2026 · similarity 0.86)
• AgentBench: Evaluating LLMs as Agents (ICLR 2024 · similarity 0.85)
• Bridging the Knowledge Gap: Understanding User Expectations for Trustworthy LLM Standards (AAAI 2025 · similarity 0.85)