LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation

• URL: http://arxiv.org/abs/2605.01394v1
• Date: Sat, 02 May 2026 11:31:33 GMT
• Title: LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation
• Abstract summary: Large language models (LLMs) and agents have shown promising progress, but their true capabilities and failure modes remain unclear.<n>We present the first systematic and contamination-aware study of LLM- and agent-based formal specification generation for C programs.
• Score: 75.05397479715576
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal specification is essential for rigorous program verification, yet writing correct specifications remains costly and difficult to automate. Although large language models (LLMs) and agents have shown promising progress, their true capabilities and failure modes remain unclear. We present the first systematic and contamination-aware study of LLM- and agent-based formal specification generation for C programs. We introduce LiveFMBench, a continuously evolving benchmark of 630 ACSL (ANSI/ISO C Specification Language)-annotated C programs, including 360 newly collected cases designed to mitigate data leakage. Using this benchmark, we evaluate direct prompting with different sampling sizes, reasoning-enabled (thinking mode) inference, the agentic pipeline, and perform a fine-grained failure analysis. Experimental results reveal that naive evaluation substantially overestimates performance because models under direct prompting may exhibit unfaithful behaviors, such as deceiving automated provers or ignoring code-context constraints; after excluding such cases, the true specification generation accuracy drops by approximately 20\%. We further find that both increased sampling and thinking mode significantly improve success rates, with smaller models benefiting more from thinking mode. Agentic pipelines are particularly effective under low sampling budgets and on harder datasets. Failure analysis further shows that incorrect loop invariants are the dominant error type, while agentic pipelines notably reduce assertion errors. These results expose fundamental limitations in current LLM-based approaches and suggest they remain far from replacing human-authored formal specifications. We release LiveFMBench at https://huggingface.co/datasets/fm-universe/Live-FM-Bench and all evaluation artifacts to support future research.

Related papers

• Prediction of Prediction (PoP): Inter-Layer Activation Fusion for Single-Pass Hallucination Detection in Large Language Models [0.0]
  This work evaluates whether internal hidden-state transition dynamics during generation can signal factual errors without auxiliary decoding calls.<n>We introduce Prediction of Prediction (PoP), a mechanism that captures layer-transition uncertainty.<n>PoP achieves an area under the receiver operating characteristic curve (AUROC) of 75.5% for factual-correctness classification.
  arXiv  Detail & Related papers  (2026-08-27T14:17:14Z)
• Employing Vision-Language Models for Face Image Quality Assessment [0.023141219541346198]
  Face Image Quality Assessment (FIQA) is a crucial control step in biometric pipelines.<n>State-of-the-art FIQA methods achieve high utility but typically operate as "black boxes"<n>We investigate the potential of off-the-shelf Vision-Language Models (VLMs) to bridge this gap by performing FIQA in a zero-shot setting.
  arXiv  Detail & Related papers  (2026-05-17T14:57:52Z)
• Rewarding the Scientific Process: Process-Level Reward Modeling for Agentic Data Analysis [68.28714988482703]
  Process Reward Models (PRMs) have achieved remarkable success in augmenting the reasoning capabilities of Large Language Models (LLMs)<n>We present a study revealing that general-domain PRMs struggle to supervise data analysis agents.<n>We introduce DataPRM, a novel environment-aware generative process reward model.
  arXiv  Detail & Related papers  (2026-04-27T09:00:30Z)
• How LLMs Fail and Generalize in RTL Coding for Hardware Design? [56.361436215029045]
  We introduce a new error taxonomy grounded in problem solvability, inspired by cognitive theory.<n>Our taxonomy categorizes failures into syntactic, semantic, solvable functional, and unsolvable functional types.
  arXiv  Detail & Related papers  (2026-04-26T14:34:49Z)
• SERC: LDPC-Inspired Semantic Error Correction for Retrieval-Augmented Generation [3.53018552538156]
  Large Language Models (LLMs) have demonstrated remarkable capabilities, but their reliability is significantly compromised by hallucinations.<n>We propose the LDPC-inspired semantic error correction for retrieval-augmented generation (SERC)<n>We reformulate the text generation process as a semantic noisy channel, treating generated responses as noise-corrupted codewords.
  arXiv  Detail & Related papers  (2026-04-12T09:09:46Z)
• Dynamic analysis enhances issue resolution [53.50448142467294]
  DAIRA (Dynamic Analysis-enhanced Issue Resolution Agent) is an automated repair framework that embeds dynamic analysis into the agent's reasoning cycle.<n> Driven by a Test Tracing-Driven methodology, DAIRA utilizes lightweight monitors to extract critical runtime data.<n>When powered by Gemini 3 Flash Preview, DAIRA establishes a new state-of-the-art (SOTA) performance, achieving a 79.4% resolution rate on the SWE-bench Verified dataset.
  arXiv  Detail & Related papers  (2026-03-23T14:48:54Z)
• AgentProcessBench: Diagnosing Step-Level Process Quality in Tool-Using Agents [50.481033105867205]
  We introduce AgentProcessBench, the first benchmark dedicated to evaluating step-level effectiveness in realistic, tool-augmented trajectories.<n>The benchmark comprises 1,000 diverse trajectories and 8,509 human-labeled step annotations with 89.1% inter-annotator agreement.<n>It features a ternary labeling scheme to capture exploration and an error propagation rule to reduce labeling ambiguity.
  arXiv  Detail & Related papers  (2026-03-15T16:13:58Z)
• MARS: Unleashing the Power of Speculative Decoding via Margin-Aware Verification [7.935725883885573]
  Speculative Decoding (SD) accelerates autoregressive large language model (LLM) inference by decoupling generation and verification.<n>We propose Margin-Aware Speculative Verification, a training-free and domain-agnostic verification strategy that adapts to the target model's local decisiveness.<n>Our method conditions verification on decision stability measured directly from the target logits and relaxes rejection only when strict verification provides minimal benefit.
  arXiv  Detail & Related papers  (2026-01-21T22:03:06Z)
• Stress-Testing ML Pipelines with Adversarial Data Corruption [11.91482648083998]
  Regulators now demand evidence that high-stakes systems can withstand realistic, interdependent errors.<n>We introduce SAVAGE, a framework that formally models data-quality issues through dependency graphs and flexible corruption templates.<n>Savanage employs a bi-level optimization approach to efficiently identify vulnerable data subpopulations and fine-tune corruption severity.
  arXiv  Detail & Related papers  (2025-06-02T00:41:24Z)
• VerifyThisBench: Generating Code, Specifications, and Proofs All at Once [9.383313869205628]
  We introduce a new benchmark that evaluates end-to-end program verification from natural language descriptions.<n>Our evaluation reveals that even state-of-the-art (SOTA) models, such as o3-mini, achieve a pass rate of less than 4%.
  arXiv  Detail & Related papers  (2025-05-25T19:00:52Z)
• Thinking Longer, Not Larger: Enhancing Software Engineering Agents via Scaling Test-Time Compute [61.00662702026523]
  We propose a unified Test-Time Compute scaling framework that leverages increased inference-time instead of larger models.<n>Our framework incorporates two complementary strategies: internal TTC and external TTC.<n>We demonstrate our textbf32B model achieves a 46% issue resolution rate, surpassing significantly larger models such as DeepSeek R1 671B and OpenAI o1.
  arXiv  Detail & Related papers  (2025-03-31T07:31:32Z)

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.