2025
Building A Proof-Oriented Programmer That Is 64% Better Than GPT-4o Under Data Scarcity
ACL 2025finding
Existing LMs struggle with proof-oriented programming due to data scarcity, which manifest in two key ways: (1) a lack of sufficient corpora for proof-oriented programming languages such as F*, and (2) the absence of large-scale, project-level proof-oriented implementations that can teach the model…