A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants

• URL: http://arxiv.org/abs/2508.18587v1
• Date: Tue, 26 Aug 2025 01:39:50 GMT
• Title: A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
• Abstract summary: We perform a case study based on two mature Rocq projects: the hs-to-coq tool and Verdi.<n>We evaluate the effectiveness of LLMs in generating proofs by both quantitative and qualitative analysis.
• Score: 9.022905966514717
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large language models (LLMs) can potentially help with verification using proof assistants by automating proofs. However, it is unclear how effective LLMs are in this task. In this paper, we perform a case study based on two mature Rocq projects: the hs-to-coq tool and Verdi. We evaluate the effectiveness of LLMs in generating proofs by both quantitative and qualitative analysis. Our study finds that: (1) external dependencies and context in the same source file can significantly help proof generation; (2) LLMs perform great on small proofs but can also generate large proofs; (3) LLMs perform differently on different verification projects; and (4) LLMs can generate concise and smart proofs, apply classical techniques to new definitions, but can also make odd mistakes.

Related papers

• On Reasoning-Centric LLM-based Automated Theorem Proving [1.8002666661892468]
  We introduce ReCent-Prover, a reasoning-centric proof agent for Rocq.<n>We show that ReCent-Prover achieves a 22.58% relative improvement in the number of proved theorems over the previous state-of-the-art.
  arXiv  Detail & Related papers  (2026-04-21T15:11:42Z)
• Proof-RM: A Scalable and Generalizable Reward Model for Math Proof [67.53066972145183]
  Large Language Models (LLMs) have demonstrated strong math reasoning abilities through Reinforcement Learning with *Verifiable Rewards* (RLVR)<n>Many advanced mathematical problems are proof-based, with no guaranteed way to determine the authenticity of a proof by simple answer matching.<n>To enable automatic verification, a Reward Model (RM) capable of reliably evaluating full proof processes is required.
  arXiv  Detail & Related papers  (2026-02-02T17:42:53Z)
• LLM4VV: Evaluating Cutting-Edge LLMs for Generation and Evaluation of Directive-Based Parallel Programming Model Compiler Tests [7.6818904666624395]
  This paper proposes a dual-LLM system and experiments with the usage of LLMs for the generation of compiler tests.<n>It is evident that LLMs possess the promising potential to generate quality compiler tests and verify them automatically.
  arXiv  Detail & Related papers  (2025-07-29T02:34:28Z)
• Towards Reliable Proof Generation with LLMs: A Neuro-Symbolic Approach [14.213719696233934]
  Large language models (LLMs) struggle with formal domains that require rigorous logical deduction and symbolic reasoning.<n>We propose a neuro-symbolic approach that combines LLMs' generative strengths with structured components to overcome this challenge.
  arXiv  Detail & Related papers  (2025-05-20T15:13:32Z)
• "I know myself better, but not really greatly": How Well Can LLMs Detect and Explain LLM-Generated Texts? [10.454446545249096]
  This paper investigates detection and explanation capabilities of current LLMs across two settings: binary (human vs. LLM-generated) and ternary classification (including an undecided'' class)<n>We evaluate 6 close- and open-source LLMs of varying sizes and find that self-detection (LLMs identifying their own outputs) consistently outperforms cross-detection (identifying outputs from other LLMs)<n>Our findings underscore the limitations of current LLMs in self-detection and self-explanation, highlighting the need for further research to address overfitting and enhance generalizability.
  arXiv  Detail & Related papers  (2025-02-18T11:00:28Z)
• Satori: Reinforcement Learning with Chain-of-Action-Thought Enhances LLM Reasoning via Autoregressive Search [57.28671084993782]
  Large language models (LLMs) have demonstrated remarkable reasoning capabilities across diverse domains.<n>Recent studies have shown that increasing test-time computation enhances LLMs' reasoning capabilities.<n>We propose a two-stage training paradigm: 1) a small-scale format tuning stage to internalize the COAT reasoning format and 2) a large-scale self-improvement stage leveraging reinforcement learning.
  arXiv  Detail & Related papers  (2025-02-04T17:26:58Z)
• Proof Automation with Large Language Models [6.587933406842906]
  Large Language Models (LLMs) have shown promise in automatically generating informal proofs in natural language. We propose PALM, a novel generate-then-repair approach that first prompts an LLM to generate an initial proof and then leverages targeted symbolic methods to iteratively repair low-level problems. Our results show that PALM significantly outperforms other state-of-the-art approaches, successfully proving 76.6% to 180.4% more theorems.
  arXiv  Detail & Related papers  (2024-09-22T00:19:27Z)
• Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean [81.94024084598598]
  We introduce Lean Copilot, a framework for running LLM inference in Lean.<n>We build tools that suggest proof steps, complete proof goals, and select relevant premises.<n>When assisting humans, Lean Copilot requires only 2.08 manually-entered proof steps on average (3.86 required by aesop)<n>When automating the theorem proving process, Lean Copilot 74.2% proof steps on average, 85% better than aesop (40.1%).
  arXiv  Detail & Related papers  (2024-04-18T22:54:08Z)
• Supervised Knowledge Makes Large Language Models Better In-context Learners [94.89301696512776]
  Large Language Models (LLMs) exhibit emerging in-context learning abilities through prompt engineering. The challenge of improving the generalizability and factuality of LLMs in natural language understanding and question answering remains under-explored. We propose a framework that enhances the reliability of LLMs as it: 1) generalizes out-of-distribution data, 2) elucidates how LLMs benefit from discriminative models, and 3) minimizes hallucinations in generative tasks.
  arXiv  Detail & Related papers  (2023-12-26T07:24:46Z)
• LLatrieval: LLM-Verified Retrieval for Verifiable Generation [67.93134176912477]
  Verifiable generation aims to let the large language model (LLM) generate text with supporting documents. We propose LLatrieval (Large Language Model Verified Retrieval), where the LLM updates the retrieval result until it verifies that the retrieved documents can sufficiently support answering the question. Experiments show that LLatrieval significantly outperforms extensive baselines and achieves state-of-the-art results.
  arXiv  Detail & Related papers  (2023-11-14T01:38:02Z)
• Rephrase and Respond: Let Large Language Models Ask Better Questions for Themselves [57.974103113675795]
  We present a method named Rephrase and Respond' (RaR) which allows Large Language Models to rephrase and expand questions posed by humans. RaR serves as a simple yet effective prompting method for improving performance. We show that RaR is complementary to the popular Chain-of-Thought (CoT) methods, both theoretically and empirically.
  arXiv  Detail & Related papers  (2023-11-07T18:43:34Z)
• Knowing What LLMs DO NOT Know: A Simple Yet Effective Self-Detection Method [36.24876571343749]
  Large Language Models (LLMs) have shown great potential in Natural Language Processing (NLP) tasks. Recent literature reveals that LLMs generate nonfactual responses intermittently. We propose a novel self-detection method to detect which questions that a LLM does not know that are prone to generate nonfactual results.
  arXiv  Detail & Related papers  (2023-10-27T06:22:14Z)
• Assessing the Reliability of Large Language Model Knowledge [78.38870272050106]
  Large language models (LLMs) have been treated as knowledge bases due to their strong performance in knowledge probing tasks. How do we evaluate the capabilities of LLMs to consistently produce factually correct answers? We propose MOdel kNowledge relIabiliTy scORe (MONITOR), a novel metric designed to directly measure LLMs' factual reliability.
  arXiv  Detail & Related papers  (2023-10-15T12:40:30Z)

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.