Can Large Language Models Model Programs Formally?

• URL: http://arxiv.org/abs/2604.01851v1
• Date: Thu, 02 Apr 2026 10:06:05 GMT
• Title: Can Large Language Models Model Programs Formally?
• Abstract summary: Model-Bench is a benchmark and pipeline for evaluating and improving LLMs' program modeling capability.<n>It comprises 400 Python programs derived from three well-known benchmarks.<n>Our experiments reveal significant limitations in LLMs' program modeling.
• Score: 26.12584614197935
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: In the digital age, ensuring the correctness, safety, and reliability of software through formal verification is paramount, particularly as software increasingly underpins critical infrastructure. Formal verification, split into theorem proving and model checking, provides a feasible and reliable path. Unlike theorem proving, which yields notable advances, model checking has been less focused due to the difficulty of automatic program modeling. To fill this gap, we introduce Model-Bench, a benchmark and an accompanying pipeline for evaluating and improving LLMs' program modeling capability by modeling Python programs into verification-ready model checking specifications checkable by its accompanying model checker. Model-Bench comprises 400 Python programs derived from three well-known benchmarks (HumanEval, MBPP, and LiveCodeBench). Our extensive experiments reveal significant limitations in LLMs' program modeling and further provide inspiring directions.

Related papers

• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  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.
  arXiv  Detail & Related papers  (2026-05-02T11:31:33Z)
• Can Large Language Models Implement Agent-Based Models? An ODD-based Replication Study [0.6821122205224714]
  Large language models (LLMs) can now synthesize non-trivial executable code from textual descriptions.<n>Can LLMs reliably implement agent-based models from standardized specifications in a way that supports replication, verification, and validation?<n>We evaluate 17 contemporary LLMs on a controlled ODD-to-code translation task.
  arXiv  Detail & Related papers  (2026-02-08T19:56:20Z)
• Every Step Counts: Decoding Trajectories as Authorship Fingerprints of dLLMs [63.82840470917859]
  We show that the decoding mechanism of dLLMs can be used as a powerful tool for model attribution.<n>We propose a novel information extraction scheme called the Directed Decoding Map (DDM), which captures structural relationships between decoding steps and better reveals model-specific behaviors.
  arXiv  Detail & Related papers  (2025-10-02T06:25:10Z)
• PAT-Agent: Autoformalization for Model Checking [17.082027022913998]
  PAT-Agent is an end-to-end framework for natural language autoformalization and formal model repair.<n>It combines the generative capabilities of large language models with the rigor of formal verification.
  arXiv  Detail & Related papers  (2025-09-28T06:32:14Z)
• Can large language models assist choice modelling? Insights into prompting strategies and current models capabilities [0.0]
  Large Language Models (LLMs) are widely used to support various disciplines, yet their potential in choice modelling remains relatively unexplored.<n>This work examines the potential of LLMs as assistive agents in the specification and, where technically feasible, estimation of Multinomial Logit models.
  arXiv  Detail & Related papers  (2025-07-29T13:24:44Z)
• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
  Large Language Models (LLMs) trained with Reinforcement Learning (RL) face a significant challenge: their verification processes are neither reliable nor scalable.<n>A promising yet largely uncharted alternative is formal language-based reasoning.<n>Grounding LLMs in rigorous formal systems where generative models operate in formal language spaces (e.g., Dafny) enables the automatic and mathematically provable verification of their reasoning processes and outcomes.
  arXiv  Detail & Related papers  (2025-07-22T08:13:01Z)
• 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)
• Learning Program Behavioral Models from Synthesized Input-Output Pairs [70.9524884086882]
  We introduce Modelizer, a framework that learns a model from its input/output behavior using neural machine translation algorithms.<n>Modelizer mocks the original program, achieving up to 95.4% accuracy and a BLEU score of 0.98 with standard error 0.04 in mocking real-world applications.<n>We foresee several applications of these models, especially as the output of the program can be any aspect of program behavior.
  arXiv  Detail & Related papers  (2024-07-11T15:25:02Z)
• Arithmetic in Transformers Explained [1.8434042562191815]
  We analyze 44 autoregressive transformer models trained on addition, subtraction, or both.<n>We show that the addition models converge on a common logical algorithm, with most models achieving >99.999% prediction accuracy.<n>We introduce a reusable library of mechanistic interpretability tools to define, locate, and visualize these algorithmic circuits.
  arXiv  Detail & Related papers  (2024-02-04T21:33:18Z)
• Formal Verification Of A Shopping Basket Application Model Using PRISM [0.0]
  We present the results of a simulation using Prism Model Checker for a Shopping Basket Application Model. The objective is to simulate the behavior of shoppers as they go through a number of defined states of the shopping process.
  arXiv  Detail & Related papers  (2023-07-16T00:14:40Z)
• Self-Checker: Plug-and-Play Modules for Fact-Checking with Large Language Models [75.75038268227554]
  Self-Checker is a framework comprising a set of plug-and-play modules that facilitate fact-checking. This framework provides a fast and efficient way to construct fact-checking systems in low-resource environments.
  arXiv  Detail & Related papers  (2023-05-24T01:46:07Z)
• CodeGen2: Lessons for Training LLMs on Programming and Natural Languages [116.74407069443895]
  We unify encoder and decoder-based models into a single prefix-LM. For learning methods, we explore the claim of a "free lunch" hypothesis. For data distributions, the effect of a mixture distribution and multi-epoch training of programming and natural languages on model performance is explored.
  arXiv  Detail & Related papers  (2023-05-03T17:55:25Z)

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.