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

Shuo Xu, Jiakun Zhang, Junyu Lai +2

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…