Buchumschlag

Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Rajaee, Sara, Pratik, Kumar, Cesa, Gabriele, Behboodi, Arash
Format:	Preprint
Veröffentlicht:	2025
Schlagworte:	Artificial Intelligence Computation and Language Machine Learning Logic in Computer Science
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4
von: Liu, Chengwu, et al.
Veröffentlicht: (2026)

SubgoalXL: Subgoal-based Expert Learning for Theorem Proving
von: Zhao, Xueliang, et al.
Veröffentlicht: (2024)

An In-Context Learning Agent for Formal Theorem-Proving
von: Thakur, Amitayush, et al.
Veröffentlicht: (2023)

Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Proving
von: Cao, Chuxue, et al.
Veröffentlicht: (2025)

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

Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving
von: Liu, Qi, et al.
Veröffentlicht: (2025)

ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving
von: Thakur, Amitayush, et al.
Veröffentlicht: (2025)

Partial Label Learning for Automated Theorem Proving
von: Zombori, Zsolt, et al.
Veröffentlicht: (2025)

What are the Right Symmetries for Formal Theorem Proving?
von: Olejniczak, Krzysztof, et al.
Veröffentlicht: (2026)

Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification
von: Rao, Balaji, et al.
Veröffentlicht: (2025)

BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving
von: Lamont, Sean, et al.
Veröffentlicht: (2024)

LeanAgent: Lifelong Learning for Formal Theorem Proving
von: Kumarappan, Adarsh, et al.
Veröffentlicht: (2024)

STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
von: Dong, Kefan, et al.
Veröffentlicht: (2025)

Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean
von: Song, Peiyang, et al.
Veröffentlicht: (2024)

Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method
von: Vishwakarma, Rahul, et al.
Veröffentlicht: (2023)

Automated Theorem Proving for Prolog Verification
von: Mesnard, Fred, et al.
Veröffentlicht: (2026)

MSC-180: A Benchmark for Automated Formal Theorem Proving from Mathematical Subject Classification
von: Li, Sirui, et al.
Veröffentlicht: (2025)

MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving
von: Li, Jinzheng, et al.
Veröffentlicht: (2026)

SATBench: Benchmarking LLMs' Logical Reasoning via Automated Puzzle Generation from SAT Formulas
von: Wei, Anjiang, et al.
Veröffentlicht: (2025)

Proving the Coding Interview: A Benchmark for Formally Verified Code Generation
von: Dougherty, Quinn, et al.
Veröffentlicht: (2025)

PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
von: Tsoukalas, George, et al.
Veröffentlicht: (2024)

3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes
von: Lamont, Sean, et al.
Veröffentlicht: (2024)

MathConstraint: Automated Generation of Verified Combinatorial Reasoning Instances for LLMs
von: Pati, Viresh, et al.
Veröffentlicht: (2026)

Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs
von: Li, Guchan, et al.
Veröffentlicht: (2026)

Logic-Parametric Neuro-Symbolic NLI: Controlling Logical Formalisms for Verifiable LLM Reasoning
von: Farjami, Ali, et al.
Veröffentlicht: (2026)

Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code
von: Florath, Andreas
Veröffentlicht: (2024)

Agentic Proving for Program Verification
von: Sosso, Alessandro, et al.
Veröffentlicht: (2026)

From Width-Based Model Checking to Width-Based Automated Theorem Proving
von: Oliveira, Mateus de Oliveira, et al.
Veröffentlicht: (2022)

An Automated Theorem Generator with Theoretical Foundation Based on Rectangular Standard Contradiction
von: Xu, Yang, et al.
Veröffentlicht: (2025)

A Neurosymbolic Approach to Loop Invariant Generation via Weakest Precondition Reasoning
von: King, Daragh, et al.
Veröffentlicht: (2025)

RLSF: Fine-tuning LLMs via Symbolic Feedback
von: Jha, Piyush, et al.
Veröffentlicht: (2024)

TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?
von: Taylor, Alexander K, et al.
Veröffentlicht: (2026)

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

LLM-ARC: Enhancing LLMs with an Automated Reasoning Critic
von: Kalyanpur, Aditya, et al.
Veröffentlicht: (2024)

Controlling Logical Collapse in LLMs via Algebraic Ontology Projection over F2
von: Miyashita, Hisashi, et al.
Veröffentlicht: (2026)

VERINA: Benchmarking Verifiable Code Generation
von: Ye, Zhe, et al.
Veröffentlicht: (2025)

Conflict-Aware Fusion: Mitigating Logic Inertia in Large Language Models via Structured Cognitive Priors
von: Bao, Qiming, et al.
Veröffentlicht: (2025)

Explainability by design: an experimental analysis of the legal coding process
von: Cristani, Matteo, et al.
Veröffentlicht: (2025)

VEL: A Formally Verified Reasoner for OWL2 EL Profile
von: Ileri, Atalay Mert, et al.
Veröffentlicht: (2024)

Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving
von: Liang, Zhenwen, et al.
Veröffentlicht: (2025)