Can LLMs Reason Like Automated Theorem Provers for Rust Verification? VCoT-Bench: Evaluating via Verification Chain of Thought

• URL: http://arxiv.org/abs/2603.18334v1
• Date: Wed, 18 Mar 2026 22:42:20 GMT
• Title: Can LLMs Reason Like Automated Theorem Provers for Rust Verification? VCoT-Bench: Evaluating via Verification Chain of Thought
• Abstract summary: VCoT-Lift lifts low-level solver reasoning into high-level, human-readable verification steps.<n>VCoT-Bench measures performance along three dimensions: robustness to varying degrees of missing proofs, competence across different proof types, and sensitivity to the proof locations.
• Score: 1.167370706056905
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: As Large Language Models (LLMs) increasingly assist secure software development, their ability to meet the rigorous demands of Rust program verification remains unclear. Existing evaluations treat Rust verification as a black box, assessing models only by binary pass or fail outcomes for proof hints. This obscures whether models truly understand the logical deductions required for verifying nontrivial Rust code. To bridge this gap, we introduce VCoT-Lift, a framework that lifts low-level solver reasoning into high-level, human-readable verification steps. By exposing solver-level reasoning as an explicit Verification Chain-of-Thought, VCoT-Lift provides a concrete ground truth for fine-grained evaluation. Leveraging VCoT-Lift, we introduce VCoT-Bench, a comprehensive benchmark of 1,988 VCoT completion tasks for rigorously evaluating LLMs' understanding of the entire verification process. VCoT-Bench measures performance along three orthogonal dimensions: robustness to varying degrees of missing proofs, competence across different proof types, and sensitivity to the proof locations. Evaluation of ten state-of-the-art models reveals severe fragility, indicating that current LLMs fall well short of the reasoning capabilities exhibited by automated theorem provers.

Related papers

• Towards Automated Formal Verification of zkEVMs Using LLM-Guided Constraint Synthesis [14.825615940318038]
  ZkEVMs generate zero-knowledge that guarantee off-chain execution correctness.<n> subtle implementation bugs can lead to valid proofs certifying semantically faulty states.<n>Formal verification via SMT solvers can prevent this, but is bottlenecked by specification.<n>We propose Veri Synth, a framework that synthesizes executable Python/Z3 verification models from Rust.
  arXiv  Detail & Related papers  (2026-07-22T06:20:36Z)
• VeryTrace: Verifying Reasoning Traces through Compilable Formalism and Structured Verification [3.5959223920188776]
  Multi-step reasoning with Chain-of-Thought (CoT) prompting remains fragile.<n>This paper presents VeryTrace, a zero-shot verification-and-repair framework.
  arXiv  Detail & Related papers  (2026-06-23T04:15:48Z)
• 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)
• FACT-E: Causality-Inspired Evaluation for Trustworthy Chain-of-Thought Reasoning [49.65751420291115]
  Chain-of-Thought (CoT) prompting has improved LLM reasoning, but models often generate explanations that appear coherent while containing unfaithful intermediate steps.<n>We propose FACT-E, a causality-inspired framework for evaluating CoT quality.<n>We show that FACT-E improves reasoning-trajectory selection and yields stronger in-context learnings.
  arXiv  Detail & Related papers  (2026-04-12T15:35:08Z)
• Stress-Testing the Reasoning Competence of LLMs With Proofs Under Minimal Formalism [2.215655942741476]
  We introduce ProofGrid, a benchmark suite for evaluating reasoning through machine-checkable proofs.<n>ProofGrid contains 15 tasks spanning proof writing, proof checking, proof masking, and proof gap-filling.<n> Tasks are expressed in minimal formal notation, especially NDL, a compact natural-deduction language that fits in short prompts.
  arXiv  Detail & Related papers  (2026-04-07T01:19:41Z)
• Grounding the Score: Explicit Visual Premise Verification for Reliable Vision-Language Process Reward Models [8.630726904040781]
  Explicit Visual Premise Verification (EVPV) is a lightweight verification interface that conditions step scoring on the reliability of the visual premises a step depends on.<n>EVPV improves step-level verification and consistently boosts Best-of-N reranking accuracy over strong baselines.
  arXiv  Detail & Related papers  (2026-03-17T08:40:26Z)
• Execution-State-Aware LLM Reasoning for Automated Proof-of-Vulnerability Generation [36.950993500170014]
  We present DrillAgent, an agentic framework that reformulates PoV generation as an iterative hypothesis-verification-refinement process.<n>We evaluate DrillAgent on SEC-bench, a large-scale benchmark of real-world C/C++ vulnerabilities.
  arXiv  Detail & Related papers  (2026-02-14T03:17:27Z)
• VIRO: Robust and Efficient Neuro-Symbolic Reasoning with Verification for Referring Expression Comprehension [51.76841625486355]
  Referring Expression (REC) aims to localize the image region corresponding to a natural-language query.<n>Recent neuro-symbolic REC approaches leverage large language models (LLMs) and vision-language models (VLMs) to perform compositional reasoning.<n>We introduce VIRO, a neuro-symbolic framework that embeds lightweight operator-level verifiers within reasoning steps.
  arXiv  Detail & Related papers  (2026-01-19T07:21:19Z)
• Towards Comprehensive Stage-wise Benchmarking of Large Language Models in Fact-Checking [64.97768177044355]
  Large Language Models (LLMs) are increasingly deployed in real-world fact-checking systems.<n>We present FactArena, a fully automated arena-style evaluation framework.<n>Our analyses reveal significant discrepancies between static claim-verification accuracy and end-to-end fact-checking competence.
  arXiv  Detail & Related papers  (2026-01-06T02:51:56Z)
• Look As You Think: Unifying Reasoning and Visual Evidence Attribution for Verifiable Document RAG via Reinforcement Learning [55.232400251303794]
  Look As You Think (LAT) is a reinforcement learning framework that trains models to produce verifiable reasoning paths with consistent attribution.<n>LAT consistently improves the vanilla model in both single- and multi-image settings, yielding average gains of 8.23% in soft exact match (EM) and 47.0% in IoU@0.5.
  arXiv  Detail & Related papers  (2025-11-15T02:50:23Z)
• CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
  We develop CompassVerifier, an accurate and robust lightweight verifier model for evaluation and outcome reward.<n>It demonstrates multi-domain competency spanning math, knowledge, and diverse reasoning tasks, with the capability to process various answer types.<n>We introduce VerifierBench benchmark comprising model outputs collected from multiple data sources, augmented through manual analysis of metaerror patterns to enhance CompassVerifier.
  arXiv  Detail & Related papers  (2025-08-05T17:55: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)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  We introduce SAFE, a framework that overcomes the lack of human-written snippets to enable automated proof generation of Rust code.<n> SAFE re-purposes the large number of synthesized incorrect proofs to train the self-ging capability of the fine-tuned models.<n>We achieve a 52.52% accuracy rate in a benchmark crafted by human experts, a significant leap over GPT-4o's performance of 14.39%.
  arXiv  Detail & Related papers  (2024-10-21T08:15:45Z)
• A Chain-of-Thought Is as Strong as Its Weakest Link: A Benchmark for Verifiers of Reasoning Chains [33.46649770312231]
  Prompting language models to provide step-by-step answers is a prominent approach for complex reasoning tasks. No fine-grained step-level datasets are available to enable thorough evaluation of such verification methods. We introduce REVEAL: Reasoning Verification Evaluation, a dataset to benchmark automatic verifiers of complex Chain-of-Thought reasoning.
  arXiv  Detail & Related papers  (2024-02-01T12:46:45Z)

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.