Imagen de Portada

HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Hu, Jilin, Zhang, Jianyu, Zhao, Yongwang, Ringer, Talia
Formato:	Preprint
Publicado:	2025
Materias:	Formal Languages and Automata Theory Artificial Intelligence Software Engineering
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

Beyond Correctness: Exposing LLM-generated Logical Flaws in Reasoning via Multi-step Automated Theorem Proving
por: Zheng, Xinyi, et al.
Publicado: (2025)

AutoVerus: Automated Proof Generation for Rust Code
por: Yang, Chenyuan, et al.
Publicado: (2024)

Configuration Monitor Synthesis
por: Köhl, Maximilian A., et al.
Publicado: (2024)

TruncProof: A Guardrail for LLM-based JSON Generation under Token-Length Constraints
por: Kato, Yoshio, et al.
Publicado: (2026)

Ontology-Driven Model-to-Model Transformation of Workflow Specifications
por: Abreu, Francisco, et al.
Publicado: (2025)

ClarifySTL: An Interactive LLM Agent Framework for STL Transformation through Requirements Clarification
por: Fang, Yue, et al.
Publicado: (2026)

Automata Learning -- Expect Delays!
por: Dengler, Gabriel, et al.
Publicado: (2025)

A Language and Methodology based on Scenarios, Grammars and Views, for Administrative Business Processes Modelling
por: Ndadji, Milliam Maxime Zekeng, et al.
Publicado: (2020)

Once and for all: how to compose modules -- The composition calculus
por: Fettke, Peter, et al.
Publicado: (2024)

Complete FSM Testing Using Strong Separability
por: Hierons, Robert M., et al.
Publicado: (2025)

A Simple Trace Semantics for Asynchronous Sequence Diagrams
por: Faitelson, David, et al.
Publicado: (2025)

Semi-Automatic Extraction of Formal Models from Object Oriented Code
por: van Spaendonck, P. H. M.
Publicado: (2024)

Contract Based Program Models for Software Model Checking
por: Amilon, Jesper, et al.
Publicado: (2025)

Formal Analysis of the Contract Automata Runtime Environment with Uppaal: Modelling, Verification and Testing
por: Basile, Davide
Publicado: (2025)

Disjunction Composition of BDD Transition Systems for Model-Based Testing
por: Zameni, Tannaz, et al.
Publicado: (2026)

Twinning automata and regular expressions for string static analysis
por: Negrini, Luca, et al.
Publicado: (2020)

On the Marriage of Theory and Practice in Data-Aware Business Processes via Low-Code
por: Eldin, Ali Nour, et al.
Publicado: (2025)

Probabilistic Bisimulation for Parameterized Anonymity and Uniformity Verification
por: Hong, Chih-Duo, et al.
Publicado: (2025)

Developing controlled natural language for formal specification patterns using AI assistants
por: Garanina, Natalia, et al.
Publicado: (2025)

ModelWisdom: An Integrated Toolkit for TLA+ Model Visualization, Digest and Repair
por: Chen, Zhiyong, et al.
Publicado: (2026)

A Synthesis Method of Safe Rust Code Based on Pushdown Colored Petri Nets
por: Zhang, Kaiwen, et al.
Publicado: (2026)

Proving Properties of $φ$-Representations with the Walnut Theorem-Prover
por: Shallit, Jeffrey
Publicado: (2023)

SynCode: LLM Generation with Grammar Augmentation
por: Ugare, Shubham, et al.
Publicado: (2024)

Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods
por: Granberry, George, et al.
Publicado: (2024)

The 4/$δ$ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee
por: Dantas, PIerre, et al.
Publicado: (2025)

Automatic Traffic Scenario Conversion from OpenSCENARIO to CommonRoad
por: Lin, Yuanfei, et al.
Publicado: (2023)

Overview and Performance Evaluation of Supervisory Controller Synthesis with Eclipse ESCET v4.0
por: Hendriks, Dennis, et al.
Publicado: (2025)

Designing FSMs Specifications from Requirements with GPT 4.0
por: Timo, Omer Nguena, et al.
Publicado: (2026)

Executable Ontologies: Synthesizing Event Semantics with Dataflow Architecture
por: Boldachev, Aleksandr
Publicado: (2025)

On the Effectiveness of Large Language Models in Writing Alloy Formulas
por: Hong, Yang, et al.
Publicado: (2025)

Type-safe Monitoring of Parameterized Streams
por: Baumeister, Jan, et al.
Publicado: (2026)

Automated Formalization of Probabilistic Requirements from Structured Natural Language
por: Mavridou, Anastasia, et al.
Publicado: (2025)

Petri Nets-based Methods on Automatically Detecting for Concurrency Bugs in Rust Programs
por: Zhang, Kaiwen, et al.
Publicado: (2022)

Data-Flow-Based Normalization Generation Algorithm of R1CS for Zero-Knowledge Proof
por: Shi, Chenhao, et al.
Publicado: (2023)

VeruSAGE: A Study of Agent-Based Verification for Rust Systems
por: Yang, Chenyuan, et al.
Publicado: (2025)

A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification
por: Tihanyi, Norbert, et al.
Publicado: (2023)

Formally Verifying Noir Zero Knowledge Programs with NAVe
por: Antonino, Pedro, et al.
Publicado: (2026)

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

A SCADE Model Verification Method Based on B-Model Transformation
por: Hou, Xili, et al.
Publicado: (2025)

A Verification Methodology for Safety Assurance of Robotic Autonomous Systems
por: Adam, Mustafa, et al.
Publicado: (2025)