Image de couverture de livre

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

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Bayazıt, Barış, Li, Yao, Si, Xujie
Format:	Preprint
Publié:	2025
Sujets:	Programming Languages Artificial Intelligence
Accès en ligne:	Acceder al recurso
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Documents similaires

Towards Repository-Level Program Verification with Large Language Models
par: Zhong, Si Cheng, et autres
Publié: (2025)

Code Repair with LLMs gives an Exploration-Exploitation Tradeoff
par: Tang, Hao, et autres
Publié: (2024)

Chronosymbolic Learning: Efficient CHC Solving with Symbolic Reasoning and Inductive Learning
par: Luo, Ziyan, et autres
Publié: (2023)

From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs
par: Cao, Jialun, et autres
Publié: (2025)

A Certified Proof Checker for Deep Neural Network Verification in Imandra
par: Desmartin, Remi, et autres
Publié: (2024)

Can Proof Assistants Verify Multi-Agent Systems?
par: Mendez, Julian Alfredo, et autres
Publié: (2025)

Evaluating LLMs in the Context of a Functional Programming Course: A Comprehensive Study
par: Zhang, Yihan, et autres
Publié: (2026)

APPL: A Prompt Programming Language for Harmonious Integration of Programs and Large Language Model Prompts
par: Dong, Honghua, et autres
Publié: (2024)

Can LLMs Enable Verification in Mainstream Programming?
par: Shefer, Aleksandr, et autres
Publié: (2025)

TypyBench: Evaluating LLM Type Inference for Untyped Python Repositories
par: Dong, Honghua, et autres
Publié: (2025)

Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis
par: Wei, Anjiang, et autres
Publié: (2025)

CatCode: A Comprehensive Evaluation Framework for LLMs On the Mixture of Code and Text
par: Lin, Zhenru, et autres
Publié: (2024)

OSVBench: Benchmarking LLMs on Specification Generation Tasks for Operating System Verification
par: Li, Shangyu, et autres
Publié: (2025)

Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification
par: Xu, Xu, et autres
Publié: (2025)

ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations
par: Gu, Alex, et autres
Publié: (2025)

FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
par: Ravi, Nikil, et autres
Publié: (2026)

Towards Formal Verification of LLM-Generated Code from Natural Language Prompts
par: Councilman, Aaron, et autres
Publié: (2025)

A Problem-Oriented Perspective and Anchor Verification for Code Optimization
par: Ye, Tong, et autres
Publié: (2024)

CodeV: Empowering LLMs with HDL Generation through Multi-Level Summarization
par: Zhao, Yang, et autres
Publié: (2024)

Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
par: Chakraborty, Saikat, et autres
Publié: (2024)

Enhancing Programming Education with ChatGPT: A Case Study on Student Perceptions and Interactions in a Python Course
par: Ma, Boxaun, et autres
Publié: (2024)

Ranking LLM-Generated Loop Invariants for Program Verification
par: Chakraborty, Saikat, et autres
Publié: (2023)

Grammar-Based Code Representation: Is It a Worthy Pursuit for LLMs?
par: Liang, Qingyuan, et autres
Publié: (2025)

RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation
par: Zhong, Sicheng, et autres
Publié: (2025)

dafny-annotator: AI-Assisted Verification of Dafny Programs
par: Poesia, Gabriel, et autres
Publié: (2024)

LLMs versus the Halting Problem: Characterizing Program Termination Reasoning
par: Sultan, Oren, et autres
Publié: (2026)

AutoCode: LLMs as Problem Setters for Competitive Programming
par: Zhou, Shang, et autres
Publié: (2025)

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

ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving
par: Thakur, Amitayush, et autres
Publié: (2025)

LLMs as Meta-Reviewers' Assistants: A Case Study
par: Hossain, Eftekhar, et autres
Publié: (2024)

Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification
par: Kasibatla, Saketh Ram, et autres
Publié: (2024)

MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data
par: Huang, Yinya, et autres
Publié: (2024)

LLMs Lean on Priors, Not Programming Language Semantics
par: Thimmaiah, Aditya, et autres
Publié: (2025)

Improving LLM Code Reasoning via Semantic Equivalence Self-Play with Formal Verification
par: Barone, Antonio Valerio Miceli, et autres
Publié: (2026)

$τ^2$-Bench: Evaluating Conversational Agents in a Dual-Control Environment
par: Barres, Victor, et autres
Publié: (2025)

Crosscoding Through Time: Tracking Emergence & Consolidation Of Linguistic Representations Throughout LLM Pretraining
par: Bayazit, Deniz, et autres
Publié: (2025)

Analyzing the Effectiveness of Large Language Models on Text-to-SQL Synthesis
par: Roberson, Richard, et autres
Publié: (2024)

Traversal Verification for Speculative Tree Decoding
par: Weng, Yepeng, et autres
Publié: (2025)

Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference
par: Le-Cong, Thanh, et autres
Publié: (2025)

Chatting with Logs: An exploratory study on Finetuning LLMs for LogQL
par: Seshagiri, Vishwanath, et autres
Publié: (2024)