Buchumschlag

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

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Xu, Qiyuan, Luan, Xiaokun, Wang, Renxi, Leang, Joshua Ong Jun, Wang, Peixin, Li, Haonan, Li, Wenda, Watt, Conrad
Format:	Preprint
Veröffentlicht:	2026
Schlagworte:	Artificial Intelligence Programming Languages Software Engineering I.2.3; F.4.1; I.2.5; I.2.7
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

Canonical for Automated Theorem Proving in Lean
von: Norman, Chase, et al.
Veröffentlicht: (2025)

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

Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification
von: Thompson, Kyle, et al.
Veröffentlicht: (2024)

A Sequent Calculus for General Inductive Definitions
von: Eede, Robbe Van den, et al.
Veröffentlicht: (2026)

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

Integration of Contextual Descriptors in Ontology Alignment for Enrichment of Semantic Correspondence
von: Manziuk, Eduard, et al.
Veröffentlicht: (2024)

Understanding Syllogistic Reasoning in LLMs from Formal and Natural Language Perspectives
von: Poddar, Aheli, et al.
Veröffentlicht: (2025)

Proving Olympiad Algebraic Inequalities without Human Demonstrations
von: Wei, Chenrui, et al.
Veröffentlicht: (2024)

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

TPTP World Infrastructure for Non-classical Logics
von: Steen, Alexander, et al.
Veröffentlicht: (2025)

An Explainable Collaborative Dialogue System using a Theory of Mind
von: Cohen, Philip R., et al.
Veröffentlicht: (2023)

A Coq-based Axiomatization of Tarski's Mereogeometry
von: Barlatier, Patrick, et al.
Veröffentlicht: (2025)

Quantum Abduction: A New Paradigm for Reasoning under Uncertainty
von: Pareschi, Remo
Veröffentlicht: (2025)

Formal Proofs as Structured Explanations: Proposing Several Tasks on Explainable Natural Language Inference
von: Abzianidze, Lasha
Veröffentlicht: (2023)

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

MIRAGE: Scaling Test-Time Inference with Parallel Graph-Retrieval-Augmented Reasoning Chains
von: Wei, Kaiwen, et al.
Veröffentlicht: (2025)

Convolutional Model Trees
von: Armstrong, William Ward, et al.
Veröffentlicht: (2025)

Twitch: Learning Abstractions for Equational Theorem Proving
von: Axelrod, Guy, et al.
Veröffentlicht: (2026)

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

Large Language Models Are Not Strong Abstract Reasoners
von: Gendron, Gaël, et al.
Veröffentlicht: (2023)

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

Liquid Amortization: Proving Amortized Complexity with LiquidHaskell (Functional Pearl)
von: van Brügge, Jan
Veröffentlicht: (2024)

Yanasse: Finding New Proofs from Deep Vision's Analogies, Part 1
von: Linhares, Alexandre
Veröffentlicht: (2026)

Logic.py: Bridging the Gap between LLMs and Constraint Solvers
von: Kesseli, Pascal, et al.
Veröffentlicht: (2025)

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

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

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

From Scientific Texts to Verifiable Code: Automating the Process with Transformers
von: Wang, Changjie, et al.
Veröffentlicht: (2025)

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

Evaluating the Architectural Reasoning Capabilities of LLM Provers via the Obfuscated Natural Number Game
von: Li, Lixing
Veröffentlicht: (2026)

Gyan: An Explainable Neuro-Symbolic Language Model
von: Srinivasan, Venkat, et al.
Veröffentlicht: (2026)

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

Mechanized HOL Reasoning in Set Theory
von: Guilloud, Simon, et al.
Veröffentlicht: (2024)

Incomplete Descriptions and Qualified Definiteness
von: Więckowski, Bartosz
Veröffentlicht: (2024)

Term Orders for Optimistic Lambda-Superposition
von: Bentkamp, Alexander, et al.
Veröffentlicht: (2025)

Metric Equational Theories
von: Mardare, Radu, et al.
Veröffentlicht: (2025)

Implementing Dependent Type Theory Inhabitation and Unification
von: Norman, Chase, et al.
Veröffentlicht: (2026)

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

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

Active Inference for an Intelligent Agent in Autonomous Reconnaissance Missions
von: Schubert, Johan, et al.
Veröffentlicht: (2025)