Cover Image

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

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Bayazıt, Barış, Li, Yao, Si, Xujie
Format:	Preprint
Published:	2025
Subjects:	Programming Languages Artificial Intelligence
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Towards Repository-Level Program Verification with Large Language Models
by: Zhong, Si Cheng, et al.
Published: (2025)

Code Repair with LLMs gives an Exploration-Exploitation Tradeoff
by: Tang, Hao, et al.
Published: (2024)

Chronosymbolic Learning: Efficient CHC Solving with Symbolic Reasoning and Inductive Learning
by: Luo, Ziyan, et al.
Published: (2023)

From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs
by: Cao, Jialun, et al.
Published: (2025)

A Certified Proof Checker for Deep Neural Network Verification in Imandra
by: Desmartin, Remi, et al.
Published: (2024)

Can Proof Assistants Verify Multi-Agent Systems?
by: Mendez, Julian Alfredo, et al.
Published: (2025)

Evaluating LLMs in the Context of a Functional Programming Course: A Comprehensive Study
by: Zhang, Yihan, et al.
Published: (2026)

APPL: A Prompt Programming Language for Harmonious Integration of Programs and Large Language Model Prompts
by: Dong, Honghua, et al.
Published: (2024)

Can LLMs Enable Verification in Mainstream Programming?
by: Shefer, Aleksandr, et al.
Published: (2025)

TypyBench: Evaluating LLM Type Inference for Untyped Python Repositories
by: Dong, Honghua, et al.
Published: (2025)

Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis
by: Wei, Anjiang, et al.
Published: (2025)

CatCode: A Comprehensive Evaluation Framework for LLMs On the Mixture of Code and Text
by: Lin, Zhenru, et al.
Published: (2024)

OSVBench: Benchmarking LLMs on Specification Generation Tasks for Operating System Verification
by: Li, Shangyu, et al.
Published: (2025)

Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification
by: Xu, Xu, et al.
Published: (2025)

ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations
by: Gu, Alex, et al.
Published: (2025)

FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
by: Ravi, Nikil, et al.
Published: (2026)

Towards Formal Verification of LLM-Generated Code from Natural Language Prompts
by: Councilman, Aaron, et al.
Published: (2025)

A Problem-Oriented Perspective and Anchor Verification for Code Optimization
by: Ye, Tong, et al.
Published: (2024)

CodeV: Empowering LLMs with HDL Generation through Multi-Level Summarization
by: Zhao, Yang, et al.
Published: (2024)

Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
by: Chakraborty, Saikat, et al.
Published: (2024)

Enhancing Programming Education with ChatGPT: A Case Study on Student Perceptions and Interactions in a Python Course
by: Ma, Boxaun, et al.
Published: (2024)

Ranking LLM-Generated Loop Invariants for Program Verification
by: Chakraborty, Saikat, et al.
Published: (2023)

Grammar-Based Code Representation: Is It a Worthy Pursuit for LLMs?
by: Liang, Qingyuan, et al.
Published: (2025)

RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation
by: Zhong, Sicheng, et al.
Published: (2025)

dafny-annotator: AI-Assisted Verification of Dafny Programs
by: Poesia, Gabriel, et al.
Published: (2024)

LLMs versus the Halting Problem: Characterizing Program Termination Reasoning
by: Sultan, Oren, et al.
Published: (2026)

AutoCode: LLMs as Problem Setters for Competitive Programming
by: Zhou, Shang, et al.
Published: (2025)

From Tool Calling to Symbolic Thinking: LLMs in a Persistent Lisp Metaprogramming Loop
by: de la Torre, Jordi
Published: (2025)

ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving
by: Thakur, Amitayush, et al.
Published: (2025)

LLMs as Meta-Reviewers' Assistants: A Case Study
by: Hossain, Eftekhar, et al.
Published: (2024)

Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification
by: Kasibatla, Saketh Ram, et al.
Published: (2024)

MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data
by: Huang, Yinya, et al.
Published: (2024)

LLMs Lean on Priors, Not Programming Language Semantics
by: Thimmaiah, Aditya, et al.
Published: (2025)

Improving LLM Code Reasoning via Semantic Equivalence Self-Play with Formal Verification
by: Barone, Antonio Valerio Miceli, et al.
Published: (2026)

$τ^2$-Bench: Evaluating Conversational Agents in a Dual-Control Environment
by: Barres, Victor, et al.
Published: (2025)

Crosscoding Through Time: Tracking Emergence & Consolidation Of Linguistic Representations Throughout LLM Pretraining
by: Bayazit, Deniz, et al.
Published: (2025)

Analyzing the Effectiveness of Large Language Models on Text-to-SQL Synthesis
by: Roberson, Richard, et al.
Published: (2024)

Traversal Verification for Speculative Tree Decoding
by: Weng, Yepeng, et al.
Published: (2025)

Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference
by: Le-Cong, Thanh, et al.
Published: (2025)

Chatting with Logs: An exploratory study on Finetuning LLMs for LogQL
by: Seshagiri, Vishwanath, et al.
Published: (2024)