Rethinking Supervision Granularity: Segment-Level Learning for LLM-Based Theorem Proving

arXiv:2605.11905v1 Announce Type: new Abstract: 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 training data: the former provides dense local signals but may fragment coherent proof processes, while the latter preserves global structure but requires complex end-to-end generation. In this pap