AI RESEARCH
Rethinking Supervision Granularity: Segment-Level Learning for LLM-Based Theorem Proving
arXiv CS.AI
•
ArXi:2605.11905v1 Announce Type: new Automated theorem proving with large language models in Lean 4 is commonly approached through either step-level tactic prediction with tree search or whole-proof generation. These two paradigms represent opposite granularities for constructing supervised