:: Library Catalog

Cover Image

Saved in:

Bibliographic Details
Main Authors:	Xu, Qiyuan, Wang, Renxi, Wang, Peixin, Li, Haonan, Watt, Conrad
Format:	Preprint
Published:	2025
Subjects:	Programming Languages
Online Access:	https://arxiv.org/abs/2507.18885
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Neural Theorem Proving for Verification Conditions: A Real-World Benchmark
by: Xu, Qiyuan, et al.
Published: (2026)

Formalization of Differential Privacy in Isabelle/HOL
by: Sato, Tetsuya, et al.
Published: (2024)

IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL (Extended Version)
by: Griffin, Matt, et al.
Published: (2025)

Extending Isabelle/HOL's Code Generator with support for the Go programming language
by: Stübinger, Terru, et al.
Published: (2023)

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

Formalizing Pick's Theorem in Isabelle/HOL
by: Binder, Sage, et al.
Published: (2024)

Generically Automating Separation Logic by Functors, Homomorphisms and Modules
by: Xu, Qiyuan, et al.
Published: (2024)

Automated Discovery of Tactic Libraries for Interactive Theorem Proving
by: Xin, Yutong, et al.
Published: (2025)

Automated Theorem Proving for Prolog Verification
by: Mesnard, Fred, et al.
Published: (2026)

Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL
by: Bartl, Lukas, et al.
Published: (2025)

An In-Context Learning Agent for Formal Theorem-Proving
by: Thakur, Amitayush, et al.
Published: (2023)

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

Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification
by: Rao, Balaji, et al.
Published: (2025)

Brownian Motion in Isabelle/HOL
by: Laursen, Christian Pardillo, et al.
Published: (2024)

Linear Programming in Isabelle/HOL
by: Parsert, Julian
Published: (2024)

Formalizing MLTL Formula Progression in Isabelle/HOL
by: Kosaian, Katherine, et al.
Published: (2024)

Compiling by Proving: Language-Agnostic Automatic Optimization from Formal Semantics
by: Zhao, Jianhong, et al.
Published: (2025)

Mechanised Hypersafety Proofs about Structured Data: Extended Version
by: Gladshtein, Vladimir, et al.
Published: (2024)

Latent Idiom Recognition for a Minimalist Functional Array Language using Equality Saturation
by: Van der Cruysse, Jonathan, et al.
Published: (2023)

Verifying Numerical Methods with Isabelle/HOL
by: Bryant, Dustin, et al.
Published: (2025)

Complex Bounded Operators in Isabelle/HOL
by: Unruh, Dominique, et al.
Published: (2025)

Stalnaker's Epistemic Logic in Isabelle/HOL
by: Guzman, Laura P. Gamboa, et al.
Published: (2024)

Learning From Failure: Integrating Negative Examples when Fine-tuning Large Language Models as Agents
by: Wang, Renxi, et al.
Published: (2024)

Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving
by: Wang, Peixin, et al.
Published: (2023)

A Natural Formalized Proof Language
by: Xie, Lihan, et al.
Published: (2024)

Automating Equational Proofs in Dirac Notation
by: Xu, Yingte, et al.
Published: (2024)

Munkres' General Topology Autoformalized in Isabelle/HOL
by: Bryant, Dustin, et al.
Published: (2026)

(Dis)Proving Spectre Security with Speculation-Passing Style
by: Arranz-Olmos, Santiago, et al.
Published: (2025)

A Theorem-Proving-Based Evaluation of Neural Semantic Parsing
by: Funakura, Hayate, et al.
Published: (2025)

DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning
by: Zhang, Ziyin, et al.
Published: (2025)

Agentic Proof Automation: A Case Study
by: Xu, Yichen, et al.
Published: (2026)

Proving Functional Program Equivalence via Directed Lemma Synthesis
by: Sun, Yican, et al.
Published: (2024)

A Fixed Point Iteration Technique for Proving Correctness of Slicing for Probabilistic Programs
by: Amtoft, Torben, et al.
Published: (2024)

Proving Confluence in the Confluence Framework with CONFident
by: Gutiérrez, Raúl, et al.
Published: (2023)

RLMEval: Evaluating Research-Level Neural Theorem Proving
by: Poiroux, Auguste, et al.
Published: (2025)

Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar
by: Binder, Sage, et al.
Published: (2026)

Can Large Language Models Help Students Prove Software Correctness? An Experimental Study with Dafny
by: Carreira, Carolina, et al.
Published: (2025)

HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement
by: Hu, Jilin, et al.
Published: (2025)

Demystifying Instruction Mixing for Fine-tuning Large Language Models
by: Wang, Renxi, et al.
Published: (2023)

Benchmarking Testing in Automated Theorem Proving
by: Kim, Jongyoon, et al.
Published: (2026)