Imagen de Portada

Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Li, Guchan, Tian, Rui, Wang, Hongning
Formato:	Preprint
Publicado:	2026
Materias:	Machine Learning Artificial Intelligence Logic in Computer Science Programming Languages
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
por: Tsoukalas, George, et al.
Publicado: (2024)

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

ScenicProver: A Framework for Compositional Probabilistic Verification of Learning-Enabled Systems
por: Vin, Eric, et al.
Publicado: (2025)

REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning
por: Shen, Ziju, et al.
Publicado: (2025)

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

STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
por: Dong, Kefan, et al.
Publicado: (2025)

ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization
por: Ahuja, Riyaz, et al.
Publicado: (2026)

Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs
por: Zhang, Terry Jingchen, et al.
Publicado: (2025)

TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?
por: Taylor, Alexander K, et al.
Publicado: (2026)

DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
por: Xin, Huajian, et al.
Publicado: (2024)

Intent-aligned Formal Specification Synthesis via Traceable Refinement
por: Ye, Zhe, et al.
Publicado: (2026)

CLEVER: A Curated Benchmark for Formally Verified Code Generation
por: Thakur, Amitayush, et al.
Publicado: (2025)

Pragmatics of Formally Verified Yet Efficient Static Analysis, in particular for Formally Verified Compilers
por: Monniaux, David
Publicado: (2024)

Theorem Provers: One Size Fits All?
por: Oates, Harrison, et al.
Publicado: (2025)

Compiling High-Level Neural Network Specifications into VNN-LIB Queries
por: Daggitt, Matthew L., et al.
Publicado: (2024)

From Symbolic Tasks to Code Generation: Diversification Yields Better Task Performers
por: Zhang, Dylan, et al.
Publicado: (2024)

What are the Right Symmetries for Formal Theorem Proving?
por: Olejniczak, Krzysztof, et al.
Publicado: (2026)

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

Decidable By Construction: Design-Time Verification for Trustworthy AI
por: Haynes, Houston
Publicado: (2026)

Lattice Annotated Temporal (LAT) Logic for Non-Markovian Reasoning
por: Mukherji, Kaustuv, et al.
Publicado: (2025)

LeanAgent: Lifelong Learning for Formal Theorem Proving
por: Kumarappan, Adarsh, et al.
Publicado: (2024)

NLP Verification: Towards a General Methodology for Certifying Robustness
por: Casadio, Marco, et al.
Publicado: (2024)

A Neurosymbolic Approach to Natural Language Formalization and Verification
por: Bayless, Sam, et al.
Publicado: (2025)

SubgoalXL: Subgoal-based Expert Learning for Theorem Proving
por: Zhao, Xueliang, et al.
Publicado: (2024)

Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving
por: Rajaee, Sara, et al.
Publicado: (2025)

A Comprehensive Survey of the Lean 4 Theorem Prover: Architecture, Applications, and Advances
por: Tang, Xichen
Publicado: (2025)

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

VEL: A Formally Verified Reasoner for OWL2 EL Profile
por: Ileri, Atalay Mert, et al.
Publicado: (2024)

Relating Answer Set Programming and Many-sorted Logics for Formal Verification
por: Hansen, Zachary
Publicado: (2025)

Verifying Peephole Rewriting In SSA Compiler IRs
por: Bhat, Siddharth, et al.
Publicado: (2024)

Vibe Coding an LLM-powered Theorem Prover
por: Hou, Zhe
Publicado: (2026)

VeriThoughts: Enabling Automated Verilog Code Generation using Reasoning and Formal Verification
por: Yubeaton, Patrick, et al.
Publicado: (2025)

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

Proof Recommendation System for the HOL4 Theorem Prover
por: Dekhil, Nour, et al.
Publicado: (2024)

Elenchus: Generating Knowledge Bases from Prover-Skeptic Dialogues
por: Allen, Bradley P.
Publicado: (2026)

Boosting Few-Pixel Robustness Verification via Covering Verification Designs
por: Shapira, Yuval, et al.
Publicado: (2024)

VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search
por: Brandfonbrener, David, et al.
Publicado: (2024)

Towards Regulated Deep Learning
por: García-Camino, Andrés
Publicado: (2019)

VERINA: Benchmarking Verifiable Code Generation
por: Ye, Zhe, et al.
Publicado: (2025)

Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving
por: Liu, Qi, et al.
Publicado: (2025)