Image de couverture de livre

Towards Language Model Guided TLA+ Proof Automation

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Zhou, Yuhao, Tripakis, Stavros
Format:	Preprint
Publié:	2025
Sujets:	Logic in Computer Science
Accès en ligne:	Acceder al recurso
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Documents similaires

Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems
par: Zhou, Yuhao, et autres
Publié: (2023)

Can LLMs Perform Synthesis?
par: Egolf, Derek, et autres
Publié: (2026)

Accelerating Protocol Synthesis and Detecting Unrealizability with Interpretation Reduction
par: Egolf, Derek, et autres
Publié: (2025)

Recursive Program Synthesis from Sketches and Mixed-Quantifier Properties
par: Egolf, Derek, et autres
Publié: (2026)

Interactive Safety Verification of Distributed Protocols by Inductive Proof Decomposition
par: Schultz, William, et autres
Publié: (2024)

Efficient Synthesis of Symbolic Distributed Protocols by Sketching
par: Egolf, Derek, et autres
Publié: (2024)

Retrieval-Augmented TLAPS Proof Generation with Large Language Models
par: Zhou, Yuhao
Publié: (2025)

LTLGuard: Formalizing LTL Specifications with Compact Language Models and Lightweight Symbolic Reasoning
par: Andresel, Medina, et autres
Publié: (2026)

Proofs that Modify Proofs, 1/2
par: Towsner, Henry
Publié: (2025)

COBALT-TLA: A Neuro-Symbolic Verification Loop for Cross-Chain Bridge Vulnerability Discovery
par: Blain, Dominik
Publié: (2026)

Towards an Analysis of Proofs in Arithmetic
par: Leitsch, Alexander, et autres
Publié: (2025)

Automating Bitvector and Finite Field Equivalence Proofs in Lean
par: Pertseva, Elizaveta, et autres
Publié: (2026)

Finding Bugs in Short Proofs: The Metamathematics of Resolution Lower Bounds
par: Li, Jiawei, et autres
Publié: (2024)

The Proof Analysis Problem
par: Arteche, Noel, et autres
Publié: (2025)

Towards a Proof System for Probabilistic Dynamic Logic
par: Johnsen, Einar Broch, et autres
Publié: (2024)

Proof-theoretic Semantics for Second-order Logic
par: Gheorghiu, Alexander V., et autres
Publié: (2025)

Proof-theoretic Semantics for the Logic of Bunched Implications
par: Gu, Tao, et autres
Publié: (2023)

Proof-theoretic Semantics for First-order Logic
par: Gheorghiu, Alexander V.
Publié: (2024)

Cyclic Proofs for iGL via Corecursion
par: Miranda, Borja Sierra
Publié: (2023)

Proof Complexity of Linear Logics
par: Tabatabai, Amirhossein Akbar, et autres
Publié: (2026)

Proof-Theoretic Functional Completeness for the Connexive Logic C
par: Ayhan, Sara, et autres
Publié: (2025)

Proof Theory and Decision Procedures for Deontic STIT Logics
par: Lyon, Tim S., et autres
Publié: (2024)

Universal Proof Theory, TACL 2022 Lecture Notes
par: Iemhoff, Rosalie, et autres
Publié: (2023)

Large Language Model for OWL Proofs
par: Yang, Hui, et autres
Publié: (2026)

Proof complexity of positive branching programs
par: Das, Anupam, et autres
Publié: (2021)

On Automating Proofs of Multiplier Adder Trees using the RTL Books
par: Manjrekar, Mayank
Publié: (2025)

Proof-theoretic Semantics for Classical Propositional Logic with Assertion and Denial
par: Gheorghiu, Alexander V., et autres
Publié: (2025)

Universal Proof Theory: Semi-analytic Rules and Uniform Interpolation
par: Tabatabai, Amirhossein Akbar, et autres
Publié: (2018)

Universal Proof Theory: Semi-analytic Rules and Craig Interpolation
par: Tabatabai, Amirhossein Akbar, et autres
Publié: (2018)

Towards Automated Readable Proofs of Ruler and Compass Constructions
par: Marinković, Vesna, et autres
Publié: (2024)

Proof Identity and Categorical Models of BV
par: Acclavio, Matteo, et autres
Publié: (2026)

Cut elimination for Cyclic Proofs: A Case Study in Temporal Logic
par: Afshari, Bahareh, et autres
Publié: (2024)

The Constructive $μ$-calculus: Game Semantics and Non-Wellfounded Proof Systems
par: Pacheco, Leonardo
Publié: (2026)

Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic (Extended Abstract)
par: Gheorghiu, Alexander V., et autres
Publié: (2023)

From Proof-theoretic Validity to Base-extension Semantics for Intuitionistic Propositional Logic
par: Gheorghiu, Alexander V., et autres
Publié: (2022)

PROMISE: Proof Automation as Structural Imitation of Human Reasoning
par: Ahn, Youngjoo, et autres
Publié: (2026)

An Introduction to Categorical Proof Theory
par: Tabatabai, Amirhossein Akbar
Publié: (2024)

Categorical Proof-Theoretic Semantics
par: Pym, David, et autres
Publié: (2023)

Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language
par: Powell, Thomas
Publié: (2023)

Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents
par: Lyon, Tim S., et autres
Publié: (2024)