Cover Image

SubgoalXL: Subgoal-based Expert Learning for Theorem Proving

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Zhao, Xueliang, Zheng, Lin, Bo, Haige, Hu, Changran, Thakker, Urmish, Kong, Lingpeng
Format:	Preprint
Published:	2024
Subjects:	Machine Learning Artificial Intelligence Computation and Language Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

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

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

Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Proving
by: Cao, Chuxue, et al.
Published: (2025)

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

APEX-Searcher: Refining Credit Assignment with Subgoaling for Agentic Retrieval-Augmented Generation
by: Chen, Kun, et al.
Published: (2026)

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

Partial Label Learning for Automated Theorem Proving
by: Zombori, Zsolt, et al.
Published: (2025)

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

LLMs Know What to Drop: Self-Attention Guided KV Cache Eviction for Efficient Long-Context Inference
by: Wang, Guangtao, et al.
Published: (2025)

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

Training Domain Draft Models for Speculative Decoding: Best Practices and Insights
by: Hong, Fenglu, et al.
Published: (2025)

FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory
by: Yang, Xiao-Wen, et al.
Published: (2025)

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

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

Scaling Reasoning without Attention
by: Zhao, Xueliang, et al.
Published: (2025)

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

SambaLingo: Teaching Large Language Models New Languages
by: Csaki, Zoltan, et al.
Published: (2024)

3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes
by: Lamont, Sean, et al.
Published: (2024)

DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition
by: Ren, Z. Z., et al.
Published: (2025)

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

Agentic Proving for Program Verification
by: Sosso, Alessandro, et al.
Published: (2026)

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

Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code
by: Florath, Andreas
Published: (2024)

Investigating the Impact and Student Perceptions of Guided Parsons Problems for Learning Logic with Subgoals
by: Tithi, Sutapa Dey, et al.
Published: (2025)

BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving
by: Lamont, Sean, et al.
Published: (2024)

Automated Theorem Proving for Prolog Verification
by: Mesnard, Fred, et al.
Published: (2026)

PromptCoT: Synthesizing Olympiad-level Problems for Mathematical Reasoning in Large Language Models
by: Zhao, Xueliang, et al.
Published: (2025)

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

Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean
by: Song, Peiyang, et al.
Published: (2024)

Learning from Relevant Subgoals in Successful Dialogs using Iterative Training for Task-oriented Dialog Systems
by: Kaiser, Magdalena, et al.
Published: (2024)

Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method
by: Vishwakarma, Rahul, et al.
Published: (2023)

Defining implication relation for classical logic
by: Fu, Li
Published: (2013)

From Width-Based Model Checking to Width-Based Automated Theorem Proving
by: Oliveira, Mateus de Oliveira, et al.
Published: (2022)

MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving
by: Li, Jinzheng, et al.
Published: (2026)

Subgoal-Guided Policy Heuristic Search with Learned Subgoals
by: Tuero, Jake, et al.
Published: (2025)

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

Logical Negation Augmenting and Debiasing for Prompt-based Methods
by: Li, Yitian, et al.
Published: (2024)

Question Answering with LLMs and Learning from Answer Sets
by: Borroto, Manuel, et al.
Published: (2025)

EXPLORER: Exploration-guided Reasoning for Textual Reinforcement Learning
by: Basu, Kinjal, et al.
Published: (2024)

Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving
by: An, Chenyang, et al.
Published: (2024)