Building A Proof-Oriented Programmer That Is 64% Better Than GPT -4o Under Data Scarcity (2025)

Abstract: 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 the intricate reasoning process when performing proof-oriented programming. We present the first on synthetic data augmentation for project level proof oriented programming for both generation and repair. Our method addresses data scarcity by synthesizing basic proof-oriented programming problems for proficiency in that language; incorporating diverse coding data for reasoning capability elicitation and creating new proofs and repair data within existing repositories. This approach enables language models to both synthesize and repair proofs for function- and repository-level code. We show that our fine-tuned 14B parameter model, PoPilot, can exceed the performance of the models that outperforms GPT-4o in project-level proof-oriented programming by 64% relative margin, and can improve GPT-4o’s performance by 54% by repairing its outputs over GPT-4o’s self-repair.

## introduction in an era where software vulnerabilities can risk tremendous damages foot_0 and compromise national security 2 , ensuring the correctness and safety has become an urgent priority. proof-oriented programming integrates formal verification into software development, enabling mathematically rigorous correctness guarantees. proof-oriented programming languages such as f* @xcite and dafny(microsoft, 2024a) support this paradigm by providing expressive type systems and precise specification mechanisms. these capabilities enable static verification of program correctness without the need for extensive test suites or runtime execution. these languages like f* allow developers to write programs alongside formal proofs, providing strong guarantees about functional correctness and security properties, and famous realworld systems including firefox, the linux kernel, tezos blockchain, and azure cloud have employed formally verified components.however, despite decades of research, the adoption of prooforiented programming remains limited due to the high cost of proof construction and the steep learning curve of formal methods. on the other hand, the rapid advancements in large language models (llms) have transformed many areas of software development @xcite @xcite @xcite @xcite . yet, applying llms to prooforiented programming presents fundamental challenges @xcite . proof-oriented programming is highly distinct from conventional coding paradigms, demanding complex formal reasoning of program semantics over long contexts, which current models struggle with @xcite . a major bottleneck is extreme data scarcity, which manifests in two key ways: (1) a lack of diverse, high-quality corpora in prooforiented programming languages such as f* to teach the model the syntax and semantics of that language (f* constitutes of only 0.002% in stack-v2 @xcite ), and (2) an absence of large-scale project-level verification data, which involves highly complex and context-dependent formal reasoning. as a result, even state-of-the-art lms fail to generalize effectively to proof construction and verification tasks @xcite . in this work, we introduce a data-centric posttraining recipe designed to bridge the gap between general-purpose coding llms and repository-level proof-oriented programming in f*. we systematically address data scarcity and adaptation challenges through three key strategies: following the recipe above, we transform llms into specialized verification assistants capable of both synthesis and repair for proof-oriented programming, which we call popilot. popilot is the first project-level formal verification specialist llm trained on synthetic instruction-tuning data. notably, strategies 2 and 3 require generating problems using existing language models that has limited knowledge and low accuracy on f*. however, we could leverage f* solver to obtain data with correctness guarantee for generation tasks, and retrieve error messages to craft repair datasets 3 our experiments demonstrate that popilot demonstrates strong capacities to perform proof-oriented programming on a project level, leading to a remarkable margin of 64% over gpt-4o and can boost 3 the correctness can be determined by running the solver without test cases as in conventional programming languages. gpt-4o's performance to 54% by repairing a randomly chosen failed attempt. ## background formal verification is a process of examining the correctness of the operation of software programs by mathematical proof @xcite . f* is an smt-solver based proof-oriented language that enables convenient verification through execution by f* compiler. however, f*, like many other languages used for formal proofs (verified rust, rocq(coq), lean etc.), are comparatively low resource. the popular open coding data corpus stack-v2 @xcite containing over 3b files in 600+ programming and markup languages, f* has only 29.6k entries (less than 0.002%), much fewer than common programming languages like python (80.6m entries, 2.95%), java (223m entries, 8.17%). this scarcity implies both the lack of knowledge of the off-the-shelf pre-trained checkpoints and the insufficiency of existing resources to further train the model. additionally, f* is a dependently-typed language, where type definitions depend on values. this allows for more precise specification of program properties and invariants but also introduces complexity due to the need for intricate computations to determine type equality and detailed type reasoning @xcite . programmers also often need to go back and forth while writing f* code. therefore, enhancing the model's ability to repair code is crucial for both iterative improvement of automatic proof synthesis and better assistance to human programmers. in reality, the challenge of proof-oriented programming is further exacerbated by the crossrepository dependencies of the code. prooforiented programming often spans multiple repositories, especially in the large-scale formal verification of software systems, where the project contains different components relying on verifying properties from other repositories. this introduces huge challenges in dependency and environment management, as the proofs account for resolving inter-repository specification and module openings beyond the single repository @xcite . this property, together with the typedependent nature of the programming language, makes the task difficult to learn for model and even human expertise. problem synthesis new problemsolution pairs existing type declaration & proofs in-file context related types and definitions verify verified new type declaration & proof training data erroneous proofs & error messages repair data + llm solve llm repair existing data augmented data llm create problem synthesis loop repair loop ## function-level dataset collection in this section, we describe how we synthesize diverse function-level programming tasks from existing open-source code snippets. we focus on three types of tasks: natural language to code tasks, proof-oriented code completion tasks, and code repair tasks. to evaluate the generated data, we rely on f*'s feature to automatically verify code correctness via execution. in addition, the dataset is diversified by incorporating instruction-tuning data from other languages. ## project-level dataset synthesis in this section, we describe how we synthesize more project-level proof generation problems from existing repositories. project-level verification involves generating or repairing proofs for definitions embedded within complete verification repositories, where correctness depends not only on local function logic but also on broader module-level context-including previously established lemmas, type invariants, module imports, and shared assumptions. our goal is to generate new problemsolution pairs based on existing programming contexts where the problem consists of a type declaration, and the solution is the correct f* definition (a proof) that satisfies the given type declaration (see examples in b). ## function-level experiments we present our experiments on the function-level synthetic data mixtures in this section. ## project-level proof synthesis in this section, we present the experiments on project-level proof synthesis tasks. develop a best training corpus. we detail the training set-up for popilot in a.3. ## conclusion in this work, we propose a synthetic data recipe for instruction-tuning code language models to become proficient proof-oriented programmers in f* under extreme data scarcity. by synthesizing functionlevel f*, diversifying with other programming languages and tasks and generating new verification tasks on a repository level, we build a powerful popilot that outperforms powerful language models, even gpt-4o with only 14b parameter. we further show that popilot can work together with existing code lms to improve their proof-oriented programming capabilities by large margins. more broadly, we present a variable path for low-resource programming languages and verification tools, lowering the barrier to adopting formal verification in real-world software development. limitations this work focuses on the programming language of f*, but did not experiment with other languages due to their lack of wellestablished evaluation suite. c.2 repair prompt example you are tasked with f* code generation. you will be given a type declaration, and an incorrect student solution. you need to produce a correct solution. ## type declaration: val clienthelloextension_e_session _ticket_clens: ll.clens clienthelloextension_ e_session_ticket sessionticket 1. write the definition that satisfies the above type. 2. start the definition with ``l et clienthelloextension _e_session_ticket_clens ```. 3. only write in f* code. 4. add end token after completing the definition. ## already opened files and delared modules open mitls.parsers.sessionticket open prims open fstar.bytes open mitls.parsers open fstar.pervasives open fstar ## related types and definitions val newsessionticketextension_clens' _session_ticket: ll.clens newsessionticketextension newsessionticketextension_e_default let newsessionticketextension_clens' _session_ticket : ll.clens newsessionticketextension @xmath0.clens_dsum_payload newsessionticketextension_sum (ll.known (known_extensiontype_as_enum_key session_ticket)) val newsessionticketextension_clens' _client_certificate_type: ll.clens newsessionticketextension newsessionticketextension_e_default let newsessionticketextension_clens' _client_certificate_type : ll.clens newsessionticketextension @xmath1.clens_dsum_payload newsessionticketextension_sum (ll.known (known_extension type_as_enum_key client_certificate_type)) ## student solution @@ student f* code ```fstar open fstar open prims open fstar.pervasives open mitls.parsers open mitls.parsers open fstar.bytes module @xmath2.uint8 module @xmath3.uint16 module @xmath4.uint32 module @xmath5.uint64 module @xmath6.spec.base module @xmath7.slow.base module @xmath8.slow.base module @xmath9.spec.allintegers module @xmath10.low.base module @xmath11.list.tot module @xmath12.buffer module @xmath13.bytes module @xmath14.hyperstack module @xmath15.hyperstack.st open mitls.parsers.sessionticket open mitls.parsers. clienthelloextension_e_session_ticket #push-options "--initial_fuel 2 --max_fuel 8 --initial_ifuel 1 --max_ifuel 2 --smtencoding.elim_box false --smtencoding.nl_arith_repr boxwrap --smtencoding.l_arith_repr boxwrap --smtencoding.valid_intro true --smtencoding.valid_elim false --z3rlimit 5 --z3rlimit_factor 1 --z3seed 0" #restart-solver val clienthelloextension_e _session_ticket_clens :ll.clens clienthelloextension_e_session_ticket // error range start -line 27 sessionticket // error range end -line 27 let clienthelloextension_e _session_ticket_clens :ll.clens @xmath16.@xmath17; ll.@xmath18: clienthelloextension_e_session_ticket) -> (x <: sessionticket)) } @@ error message -expected type "type"; but "ll.clens sessionticket" has type "t2: type -> type" -expected type "type"; but "ll.clens sessionticket" has type "t2: type0 -> type" -expected type "ll.clens sessionticket"; but "ll.mkclens (fun _ -> l_true) (fun x -> x <: sessionticket)" has type "ll.clens clienthelloextension_e_session_ticket sessionticket" -expected type "ll.clens clienthelloextension_e_session_ticket sessionticket"; but "ll.mkclens (fun _ -> l_true) (fun x -> x <: sessionticket) <: ll.clens sessionticket" has type "ll.clens sessionticket" write your response below. c.3 new definition prompt example you are tasked with generating f* code. you will be given some premises, opened modules and some example type declarations and definitions. your goal is to write a different type declaration and a corresponding definition that satisfies the type declaration. you can use the information provided in the following sections to help you construct the new type declaration and definition. here's how you can use each section: possibly useful premises: this section lists modules, types, or functions that might be helpful. consider incorporating them into your definition if appropriate. already opened files and declared modules: the modules listed here are already opened in the context. you can use definitions from these modules directly without needing to prefix them with the module name. example type declarations and definitions: this shows some examples of how a definition satisfying a similar type declaration can be written. each example is delimited using "```". use this as a reference for the structure and style, but do not use the examples definitions in your answer.