Imagen de Portada

Neural Theorem Proving for Verification Conditions: A Real-World Benchmark

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Xu, Qiyuan, Luan, Xiaokun, Wang, Renxi, Leang, Joshua Ong Jun, Wang, Peixin, Li, Haonan, Li, Wenda, Watt, Conrad
Formato:	Preprint
Publicado:	2026
Materias:	Artificial Intelligence Programming Languages Software Engineering I.2.3; F.4.1; I.2.5; I.2.7
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

Canonical for Automated Theorem Proving in Lean
por: Norman, Chase, et al.
Publicado: (2025)

Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4
por: Aniva, Leni, et al.
Publicado: (2024)

Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification
por: Thompson, Kyle, et al.
Publicado: (2024)

A Sequent Calculus for General Inductive Definitions
por: Eede, Robbe Van den, et al.
Publicado: (2026)

SPARQL in N3: SPARQL CONSTRUCT as a rule language for the Semantic Web (Extended Version)
por: Arndt, Dörthe, et al.
Publicado: (2025)

Integration of Contextual Descriptors in Ontology Alignment for Enrichment of Semantic Correspondence
por: Manziuk, Eduard, et al.
Publicado: (2024)

Understanding Syllogistic Reasoning in LLMs from Formal and Natural Language Perspectives
por: Poddar, Aheli, et al.
Publicado: (2025)

Proving Olympiad Algebraic Inequalities without Human Demonstrations
por: Wei, Chenrui, et al.
Publicado: (2024)

Grokking in the Wild: Data Augmentation for Real-World Multi-Hop Reasoning with Transformers
por: Abramov, Roman, et al.
Publicado: (2025)

TPTP World Infrastructure for Non-classical Logics
por: Steen, Alexander, et al.
Publicado: (2025)

An Explainable Collaborative Dialogue System using a Theory of Mind
por: Cohen, Philip R., et al.
Publicado: (2023)

A Coq-based Axiomatization of Tarski's Mereogeometry
por: Barlatier, Patrick, et al.
Publicado: (2025)

Quantum Abduction: A New Paradigm for Reasoning under Uncertainty
por: Pareschi, Remo
Publicado: (2025)

Formal Proofs as Structured Explanations: Proposing Several Tasks on Explainable Natural Language Inference
por: Abzianidze, Lasha
Publicado: (2023)

LLM-Assisted Formalization Enables Deterministic Detection of Statutory Inconsistency in the Internal Revenue Code
por: Yadamsuren, Borchuluun, et al.
Publicado: (2025)

MIRAGE: Scaling Test-Time Inference with Parallel Graph-Retrieval-Augmented Reasoning Chains
por: Wei, Kaiwen, et al.
Publicado: (2025)

Convolutional Model Trees
por: Armstrong, William Ward, et al.
Publicado: (2025)

Twitch: Learning Abstractions for Equational Theorem Proving
por: Axelrod, Guy, et al.
Publicado: (2026)

Cryptogenic stroke and migraine: using probabilistic independence and machine learning to uncover latent sources of disease from the electronic health record
por: Betts, Joshua W., et al.
Publicado: (2025)

Large Language Models Are Not Strong Abstract Reasoners
por: Gendron, Gaël, et al.
Publicado: (2023)

Enhancing Large Language Models through Neuro-Symbolic Integration and Ontological Reasoning
por: Vsevolodovna, Ruslan Idelfonso Magana, et al.
Publicado: (2025)

Liquid Amortization: Proving Amortized Complexity with LiquidHaskell (Functional Pearl)
por: van Brügge, Jan
Publicado: (2024)

Yanasse: Finding New Proofs from Deep Vision's Analogies, Part 1
por: Linhares, Alexandre
Publicado: (2026)

Logic.py: Bridging the Gap between LLMs and Constraint Solvers
por: Kesseli, Pascal, et al.
Publicado: (2025)

PC-SNN: Predictive Coding-based Local Hebbian Plasticity Learning in Spiking Neural Networks
por: Wang, Haidong, et al.
Publicado: (2022)

Complementarity, Augmentation, or Substitutivity? The Impact of Generative Artificial Intelligence on the U.S. Federal Workforce
por: Resh, William G., et al.
Publicado: (2025)

Development of Hybrid Artificial Intelligence Training on Real and Synthetic Data: Benchmark on Two Mixed Training Strategies
por: Wachter, Paul, et al.
Publicado: (2025)

From Scientific Texts to Verifiable Code: Automating the Process with Transformers
por: Wang, Changjie, et al.
Publicado: (2025)

By Their Fruits You Will Know Them: Comparing Formalizations of Law by the Decisions They Encode
por: Vernie, Julius, et al.
Publicado: (2026)

Evaluating the Architectural Reasoning Capabilities of LLM Provers via the Obfuscated Natural Number Game
por: Li, Lixing
Publicado: (2026)

Gyan: An Explainable Neuro-Symbolic Language Model
por: Srinivasan, Venkat, et al.
Publicado: (2026)

$ϕ^{\infty}$: Clause Purification, Embedding Realignment, and the Total Suppression of the Em Dash in Autoregressive Language Models
por: Kilictas, Bugra, et al.
Publicado: (2025)

Mechanized HOL Reasoning in Set Theory
por: Guilloud, Simon, et al.
Publicado: (2024)

Incomplete Descriptions and Qualified Definiteness
por: Więckowski, Bartosz
Publicado: (2024)

Term Orders for Optimistic Lambda-Superposition
por: Bentkamp, Alexander, et al.
Publicado: (2025)

Metric Equational Theories
por: Mardare, Radu, et al.
Publicado: (2025)

Implementing Dependent Type Theory Inhabitation and Unification
por: Norman, Chase, et al.
Publicado: (2026)

Seeing Is No Longer Believing: Frontier Image Generation Models, Synthetic Visual Evidence, and Real-World Risk
por: Wu, Shuai, et al.
Publicado: (2026)

Exponential Resolution Lower Bounds for Weak Pigeonhole Principle and Perfect Matching Formulas over Sparse Graphs
por: de Rezende, Susanna F., et al.
Publicado: (2019)

Active Inference for an Intelligent Agent in Autonomous Reconnaissance Missions
por: Schubert, Johan, et al.
Publicado: (2025)