arXiv CSopen access

Teaching Code LLMs to Reason with Intermediate Formal Specifications

arXiv:2607.04232v1 [cs.SE] 5 Jul 2026

Teaching Code LLMs to Reason with Intermediate Formal Specifications Minh Le-Anh

Cuong Chi Le

Tien N. Nguyen

FPT Software AI Center Hanoi Univ. of Science and Tech. Hanoi, Vietnam [email protected]

University of Texas at Dallas Texas, USA [email protected]

University of Texas at Dallas Texas, USA [email protected]

Abstract—Unlike natural-language specifications, executable formal specifications provide machine-checkable constraints for verifying, debugging, and repairing code. However, writing such specifications is labor-intensive, and existing LLM-based methods mainly infer whole-program pre/postconditions, missing the intermediate semantic commitments that programmers rely on when reasoning about an algorithm. Our study further shows that prompting current CodeLLMs often produces executable assertions that are syntactically invalid, trivial, or too weak to reject behavior-changing faults. In this paper, we study executable checkpoint specification generation, where assertions are inserted at meaningful internal program points to describe expected intermediate states. We introduce S PEC C ODER, a verificationguided CodeLLM training framework that learns from validated reference programs, behavior-changing mutants, and multi-turn specification-refinement traces. S PEC C ODER selects specifications that hold on correct executions while rejecting faulty executions, turning specifications from passive annotations into executable evidence. To evaluate this setting, we introduce HumanExec, a benchmark built from recent Codeforces competitiveprogramming problems with test suites, reference solutions, and human buggy submissions, supporting three tasks: specification generation, program correctness checking, and program repair. Experiments on HumanExec show that S PEC C ODER substantially improves checkpoint-specification quality over base CodeLLMs. Across Qwen2.5-Coder models, S PEC C ODER improves inline-specification correctness by up to 55.8%, completeness by up to 358.1%, and executable assertion validity by up to 26.6%. These gains further translate to downstream correctness reasoning and repair, showing that executable checkpoints provide fine-grained evidence for reliable verification.

I. I NTRODUCTION Formal specifications are symbolic constraints that describe expected program behavior and can be checked against executions [1], [2]. When a specification is written as an assertion, it becomes directly executable: the assertion can be evaluated on concrete program traces and used as feedback for verification, testing, debugging, and repair. Instead of only asking whether a program produces the correct final output, executable specifications can expose whether the program satisfies the properties needed to reach that output correctly. Recent advances in Large Language Models (LLMs) have transformed software development. However, the hallucination and semantic unreliability of LLM-generated code have shifted the focus of software engineering research from merely generating code to a more fundamental question: how can we

verify that generated code is correct and aligned with user intent, and how can we help repair it when it is not? Program specifications provide an important vehicle for this goal. They make the intended behavior explicit and can serve as oracles for checking, explaining, and correcting generated implementations. Unfortunately, manually writing high-quality formal specifications for LLM-generated code is labor-intensive and requires substantial programming and verification expertise. This creates a clear need for automated techniques that can generate executable formal specifications. Recent research has shown that LLMs can generate program specifications for a given implementation, including postconditions and natural-language correctness conditions [3]. For example, NL2Postcond [3] and SpecMind [4] infer postconditions from source code. HoarePrompt [5] uses naturallanguage state conditions for correctness reasoning, and SpecRover [6] extracts code intent to support repair. They demonstrate the value of specification-like reasoning, but their intermediate signals are not directly executable assertions. First, most existing approaches derive specifications at a coarse granularity. Approaches such as NL2Postcond and SpecRover primarily focus on preconditions or postconditions for an entire method or program. End-to-end specifications are useful because they summarize boundary behavior: what must hold before execution and what should hold after the program terminates. However, they do not expose whether the main algorithm is correct at each internal step that could ensure the final correctness. In practice, developers rarely reason about non-trivial programs only through final outputs. Instead, they decompose a program into meaningful computation steps and check local semantic commitments: after preprocessing, an array should have a certain structure; after a loop iteration, an invariant should hold; etc. Whole-program postconditions often miss these internal obligations, making them insufficient for fine-grained verification, diagnosis, and repair. Second, some LLM-based approaches can produce intermediate reasoning conditions, but these conditions are often expressed in natural language. For example, HoarePrompt-style reasoning can describe reachable program states at intermediate points, helping an LLM reason about correctness. However, natural-language specifications are difficult to execute directly. They may be useful for explanation or human inspection, but

they provide limited support for fully automated workflows that require machine-checkable feedback, such as trace-based consistency checking, test-time assertion validation, fault localization, and automated program repair. These limitations motivate a richer view of specification for LLM-generated code. Unlike prior work that treats specifications mainly as final summaries or textual reasoning aids, our goal is to teach models to produce the executable intermediate specifications that are validated by execution and selected for their ability to reject faulty behaviors.

1 2 3 4 5 6

def merge_intervals(intervals): # BUG: intervals should be sorted by start point, # but this implementation sorts by end point. # Example input: [[10,20], [1,100]] # Sorting by end keeps [10,20] before [1,100], so the start points are not sorted. intervals.sort(key=lambda p: p[1])

7 8 9 10

# Natural-language spec at the checkpoint: # "The intervals should be sorted before merging." # This is readable, but cannot be checked automatically.

11 12 13 14

# Executable checkpoint specification: assert all(intervals[i][0] <= intervals[i+1][0] for i in range(len(intervals) - 1))

15

{Pre} S0 {Step1 } S1 · · · {Stepn } Sn {Post}.

16 17 18

merged = [] for start, end in intervals: if not merged or merged[-1][1] < start: merged.append([start, end]) else: merged[-1][1] = max(merged[-1][1], end)

In this paper, we focus on assertion-style executable formal 19 specifications: Boolean predicates inserted into source code 20 21 and evaluated over concrete runtime states. Such specifications 22 still describe the boundary behavior of the code, but they 23 return merged are executable constraints. The intermediate formal checkFig. 1. Natural-language versus Executable Checkpoint Specification point specifications describe the semantic states reached by important algorithmic steps. Given a program, these checkeration, consistency checking between program intent and point specifications are executable assertions placed inside the implementation, and program repair. source code, so they can verify not only the final answer but also the path by which the program reaches it. II. M OTIVATION Toward this goal, our preliminary study shows that LLMs do not produce high-quality specifications in the intermediate A. Limitations of Natural-Language Specifications for Autocheckpoints for a given program. A final postcondition mainly mated Verification Natural-language specifications are widely used in recent requires understanding the desired output behavior of the whole program, whereas a checkpoint specification requires LLM-based verification and program-repair methods because understanding the internal algorithm, identifying meaningful they are easy to generate, read, and communicate to developprogram points, and expressing properties that should hold ers [5]. For example, an LLM can describe an intermediate at those points. Thus, checkpoint specification generation state with a sentence such as “the list should be sorted before demands a deeper form of step-by-step program reasoning. merging”. Such descriptions are useful for human inspection The gap exposed by our study suggests that current code and can guide an LLM’s reasoning about code. However, the key limitation is that natural-language specifiLLMs may produce plausible final conditions while still lacking robust understanding of intermediate program execu- cations are not executable. Unlike formal assertion-style spection. Moreover, they often produce trivial assertions, or weak ifications, they do not define precise Boolean conditions over conditions that are valid but provide little help for verification. concrete program states. Therefore, they cannot be directly We introduce S PEC C ODER, a specification-aware training checked against execution traces. Fig. 1 illustrates this with a simplified interval-merging proframework that teaches code LLMs to generate executable checkpoint specifications for a given program. S PEC C ODER gram. The natural-language checkpoint states that the intervals constructs training data from correct programs, synthesized should be sorted before merging. This description is readable, mutants, and specification-refinement traces, then trains mod- but it cannot be evaluated automatically. If the implementation els to produce interleaved code-and-specification outputs. The accidentally sorts intervals by their end point instead of their resulting specifications are executable assertions that can be start point, an automated system cannot directly detect the evaluated on program traces for correctness. The trained/fine- violation. In contrast, the executable assertion at line 13 tuned model supports the annotation setting (specification directly checks the required intermediate state on the concrete generation): given a program, it inserts executable checkpoint runtime value of intervals. Natural-language specifications can also be vague or inspecifications. This paper makes the following contributions: complete. For example, an LLM may state that “the current • A verification-guided training framework that uses reference programs, validated mutants, and specification-refinement interval has been handled correctly” or “the merged list is traces to produce specification-aware supervision for LLMs. updated properly.” These statements sound plausible, but they do not specify what must hold over program variables, such as • HumanExec, an execution-based benchmark for assessing specification generation on tasks with human-written buggy whether the intervals are ordered, or whether the last interval contains the maximum end point seen so far. code, measuring both correctness and completeness. This limitation weakens downstream automation. In pro• We empirically study the usefulness of specification-aware training in three downstream applications: specification gen- gram verification, a natural-language specification cannot be

evaluated during execution. In consistency checking, it cannot provide an objective signal that an implementation violates the user intent. In program repair, it provides only weak feedback: the system may know that a final test failed, but not which intermediate semantic commitment was broken. In contrast, an executable checkpoint can expose the internal state where the computation first deviates from the intended behavior. This motivates executable checkpoint specifications: assertions placed at meaningful program points that can be validated on executions and used as reliable verification signals. B. Limitations of Code LLMs for Generating Reliable Formal Specifications Executable checkpoint specifications address the nonverifiability of natural-language descriptions, but generating them is substantially harder than generating free-form text. A model must identify meaningful program points, infer the intended semantics of the intermediate state, determine which variables are in scope, and express the property as a syntactically valid Boolean predicate. A generated assertion that refers to an unavailable variable, fails on the correct program, or states a tautology such as assert True cannot serve as a reliable verification signal. We thus examine whether base Code LLMs can generate reliable inline formal specifications through prompting alone. For each model, we prompt it to insert checkpoint assertions into correct programs and evaluate the generated assertions from three execution-based perspectives. Syntax measures whether the assertions are executable. Correctness measures whether they hold on correct executions. In our mutant-based evaluation, Completeness measures, operationally, whether they reject behavior-changing mutants that reach the same checkpoints and therefore provide useful verification signals. For example, for the program in Fig. 1, a prompted model may generate a syntactically valid but weak assertion such as assert len(intervals) >= 0, which holds on both correct and faulty executions. It may also generate an overly strong assertion such as checking that intervals are already nonoverlapping before the merge loop, which can fail on correct inputs. These illustrate why executable syntax alone is not sufficient: a useful checkpoint must be both valid for the intended computation and discriminative against faulty behavior. Table I shows that prompting alone is insufficient for reliable formal checkpoint specification generation. Although the models often produce syntactically executable assertions, their semantic quality remains limited. For example, Qwen2.5Coder-32B achieves 0.89 syntax validity, but only 0.63 correctness and 0.26 completeness. This indicates that many generated assertions either fail on correct executions or hold on correct executions, yet are too weak to reject buggy variants. These results reveal a key challenge: executable assertions are not useful merely because they are well formed. They must also capture semantic properties that are valid for the intended computation and discriminative against faulty behavior. LLMs often miss this balance, producing assertions that are invalid, overly specific, tautological, or unrelated to the algorithmic

TABLE I F ORMAL SPECIFICATION QUALITY OF BASE MODELS BEFORE FINE - TUNING .

Model

Syntax ↑

Correctness ↑

Completeness ↑

Qwen2.5-Coder-7B Qwen2.5-Coder-14B Qwen2.5-Coder-32B

0.8272 0.7900 0.8989

0.2772 0.5226 0.6313

0.1707 0.1989 0.2604

state. This motivates a verification-guided training approach, where candidate assertions are refined using execution feedback and chosen for both correctness and discriminative power. C. Key Idea These observations suggest that checkpoint specification generation should not be treated as a purely textual generation problem. A useful checkpoint must be validated on correct executions and challenged against faulty executions. This motivates our key idea to turn specification generation into verification-guided learning. Instead of treating an assertion as useful because it appears plausible to an LLM, we evaluate candidate assertions through execution. A checkpoint specification is useful only when it satisfies two properties: it should hold on correct executions, and it should reject faulty executions that reach the same checkpoint. Given a programming problem x and an implementation y, checkpoint specification generation produces an annotated program ỹ, where assertions are inserted at internal program points. Each assertion s is a Boolean predicate over variables in scope at its insertion point. We evaluate these assertions on two execution populations: correct executions, where the assertions should hold, and mutant executions, where strong assertions should expose behavior-changing faults. This converts specification generation from a purely generative task into a feedback-driven process in which the quality of a specification can be checked by running the program. III. S PEC C ODER : A V ERIFICATION -BASED M ODEL A. Data Construction We present S PEC C ODER, a training framework for adapting CodeLLMs to generate executable checkpoint specifications. Given a programming problem and a program, S PEC C ODER constructs supervision from assertions that are validated by execution rather than accepted solely from LLM output. The pipeline consists of four stages. First, we select reliable reference programs from a LeetCode-style programming system by keeping only submissions that pass their available test suites. These executions provide the correct runtime states on which checkpoint assertions should hold. Second, we construct behavior-changing mutants from each reference program and retain only non-trivial mutants that pass at least one test and fail at least one test. These mutants provide controlled faulty executions, excluding equivalent variants and programs that are too broken to yield useful intermediate signals. Third, a teacher model generates checkpoint specifications through a multi-turn Explore–Submit process. At each turn,

1 Problem Selection

4 Training data

2 Mutant Generation Given <Problem Statement> and <Reference Program>, create <N> one-line mutants. Preserve syntax; change behavior.

Mutant 1: x = A'(x, y) Mutant 2: y = B'(y, z) Mutant 3: y = C'(x, y)

Problem Statement def func(x, y, z): x = A(x,y) if cond(y, z): y = B(y, z) else: y = C(x, y) x, z = D(x, z) return x, y, z

Reference Profram

Test Cases

def func(x, y, z): x = A(x,y) if cond(y, z): y = B'(y, z) else: y = C(x, y) x, z = D(x, z) return x, y, z

Execute on Tests

Specification Generation task

Keep mutants with ≥1 pass and ≥1 fail

User: Generate specifications for this program: <Problem Statement> <Reference Program> + (<Mutant>)

Mutant List

3 Multi-turn Specification Refinement Given <Problem Statement> and <Reference Program>, insert executable checkpoint assertions into the program. Explore candidate assertion and then Submit (using <Feedback>)

Explore/Submit

def func(x, y, z): x = A(x,y) # assert Spec_1 if cond(y, z): y = B(y, z) # assert Spec_2 else: y = C(x, y) # assert Spec_3 x, z = D(x, z) # assert Spec_4 return x, y, z

Response: <Annotated Program> = <Reference Program> + (<Mutant>) + <Specifications>

Execution Verifier Correctness ( > α)

Completeness (>β)

Code Generation task Pass

Fail

Feedback (Correctness, Completeness)

User: Generate code for this problem: <Problem Statement> Response: <Annotated Program> = <Reference Program> + <Specifications>

Fig. 2. Pipeline for mutant-guided checkpoint specification data construction.

candidate assertions are instrumented and executed on the reference program and retained mutants. The verifier reports syntax errors, unsafe assertions, unreachable checkpoints, assertion failures, and mutant-rejection evidence. A submitted annotated program is accepted only when its assertions satisfy the required correctness and completeness thresholds. Finally, the accepted annotated programs are converted into supervised fine-tuning examples for two tasks: inserting checkpoint specifications into an existing program and generating a complete specification-bearing solution from the problem statement. This ensures that the student model learns from checkpoint specifications that are reachable, executable, valid on reference executions, and challenged by behavior-changing mutants. Fig. 2 illustrates the data construction pipeline, and Algorithm 1 gives its procedural form. Starting from problems, submissions, and test suites, we select validated reference programs, generate behavior-changing mutants as controlled faulty executions, and use multi-turn specification refinement to synthesize executable checkpoint assertions. Candidate specifications are executed on both reference programs and retained mutants, and only annotated programs satisfying the correctness and completeness thresholds are kept for training. 1) Problem Selection and Reference Validation: Given a programming problem xi , we collect a human-written submission yi and its test suite Ti . To ensure that the constructed specifications are grounded in executions, we keep a sample only when two conditions are satisfied. First, the test suite must contain more than 30 tests, so that execution feedback covers more than a small number of examples. Second, the submission must pass all available tests: ∀t ∈ Ti , Exec(yi , t) = Pass. This step gives us a trusted reference implementation. The executions of yi define the correct runtime states on which checkpoint specifications should hold. The same reference program is also used as the base program for constructing behavior-changing mutants. All train/validation/test splits are performed at the problem level before mutant generation and specification refinement. Thus, mutants and annotated programs derived from a problem cannot appear in training. 2) Mutant Generation: After validating the reference program, we construct mutants to provide negative executions.

Algorithm 1 Mutant-guided checkpoint specification data construction Require: Problems P, submissions, test suites, teacher model M , thresholds α, β, maximum turns K Ensure: Training data Dspec , Dcode 1: Dspec , Dcode ← ∅ 2: for all problem xi ∈ P do 3: collect candidate program yi and test suite Ti 4: if |Ti | ≤ 30 or yi does not pass all tests then 5: continue 6: generate one-line mutants from yi 7: keep mutants with ≥ 1 pass and ≥ 1 fail 8: deduplicate retained mutants to obtain Mi 9: F ← ∅, ỹi ← ∅ 10: for k = 1, . . . , K do 11: a ← M (xi , yi , F ) ▷ E XPLORE or S UBMIT 12: extract annotated program ŷi from a 13: execute ŷi on Ti and Mi 14: compute Corrij and Compij for all assertions 15: if a = S UBMIT and ACCEPT(Si , α, β) then 16: ỹi ← Filter(ŷi ) 17: break 18: update feedback F from execution results 19: if ỹi = ∅ then 20: continue 21: add (xi , yi ) → ỹi to Dspec 22: add annotated mutant examples (xi , m) → m̃ to Dspec 23: add xi → ỹi to Dcode 24: return Dspec , Dcode ACCEPT(Si , α, β) holds if every generated assertion is reached on the reference code and satisfies Corrij ≥ α, every assertion with an evaluable mutant set satisfies Compij ≥ β, and at least one assertion has a non-empty eligible mutant set.

For each executable statement in yi , we prompt an LLM to generate plausible one-line buggy replacements. The prompt asks for natural coding mistakes, such as using an incorrect condition, updating the wrong variable, calling an incorrect helper function, or omitting a necessary update. Each mutant must preserve syntax while changing program behavior. We run every generated mutant on the same test suite Ti . We keep only non-trivial mutants that pass at least one test and fail at least one test: 0 < #{t ∈ Ti | Exec(m, t) = Pass} < |Ti |. A mutant passing all tests is likely equivalent to the reference

program under the available tests, while a mutant that fails all tests is often too broken to provide useful intermediate signals. We also deduplicate mutants with the same pass/fail pattern over the test suite. The remaining mutants form the retained mutant pool Mi . They serve as controlled faulty executions: a useful checkpoint specification should hold on the reference program but reject at least some faulty executions. 3) Multi-turn Specification Refinement: Inspired by the multi-turn refinement strategy of SpecMind [4], we generate executable checkpoint specifications through a verificationguided Explore–Submit process. For each task i, the teacher model is given the problem statement xi , a validated reference implementation yi , the available functional tests Ti , and a pool of retained behavior-changing mutants Mi . The goal is to insert inline checkpoint specifications into yi while leaving the executable implementation unchanged. At each turn, the teacher either explores candidate checkpoints or submits an annotated program for acceptance. Regardless of the turn type, the verifier executes the candidate annotations on both the reference program and retained mutants, producing feedback on reachability, correctness, and mutant rejection. The difference is that an EXPLORE turn uses the feedback only to guide the next revision, while a SUBMIT turn additionally triggers the acceptance test against the predefined quality thresholds. The implementation code is required to remain byte-equivalent after removing assertion comments; turns that modify executable code or contain unsafe assertion expressions are rejected and regenerated. We first extract all assertion comments from the annotated program and instrument them as executable runtime checks. Each assertion is evaluated at its original program location by wrapping its Boolean expression in a trace function. This records both whether a checkpoint is reached and whether the assertion holds every time it is reached. Assertions that contain syntactic errors, refer to undefined state at runtime, or use unsafe operations such as mutation, I/O, randomness, or dynamic evaluation are treated as invalid feedback. a) Correctness: Correctness measures whether a generated checkpoint specification is valid on the reference implementation. Let Si = {si1 , . . . , sik } be the assertions extracted from a candidate annotated program. For assertion sij and test t ∈ Ti , let rijt be the number of times the checkpoint is reached during the reference execution, and let pijt be the number of those evaluations for which the assertion is true. The per-assertion correctness score is P 1[rijt > 0 ∧ pijt = rijt ] . Corrij = t∈Ti P t∈Ti 1[rijt > 0] If the assertion is not reached by any reference execution, we set Corrij = 0. Thus, an assertion is correct only when every reached evaluation on the reference implementation satisfies the predicate. We aggregate at the test level rather than the raw evaluation level so that a single long-running test with many repeated checkpoint evaluations does not dominate the correctness score.

b) Completeness: Completeness measures whether a correct checkpoint specification can expose faulty intermediate states in retained mutants. A checkpoint should only be expected to reject faults that can influence the state observed at that checkpoint. Therefore, we restrict completeness evaluation to eligible mutants whose changed line occurs before the checkpoint and whose execution can reach the checkpoint. We only evaluate a mutant against a checkpoint when the mutant is eligible for that checkpoint: the mutated source line must occur before the checkpoint, and the corresponding original line and checkpoint must co-reach on at least one reference execution. This prevents a checkpoint from being penalized for mutants that cannot causally affect or reach it. For assertion sij , let Eij ⊆ Mi be the eligible mutants that reach the checkpoint in at least one mutant execution. A mutant m ∈ Eij is rejected if sij fails on any reached execution of that mutant. The per-assertion completeness score is Compij =

#{m ∈ Eij : sij rejects m} . #Eij

When Eij is empty, no completeness claim is made for that assertion and is excluded from the averaged completeness score. The verifier reports per-assertion feedback after each turn, including reachability, correctness, mutant rejection counts, skipped mutants, and surviving mutants when available. The teacher uses this feedback to preserve reliable assertions, repair false or unreachable ones, and strengthen assertions that are correct but weak. The acceptance test is applied at the assertion level rather than only to an average score. This prevents a submitted program from being accepted because a few strong checkpoints compensate for invalid, unreachable, or weak ones. A submitted annotated program is accepted only if its assertions satisfy the quality thresholds. That is, every generated assertion must be reached on the reference implementation and satisfy Corrij ≥ α, and every assertion with an evaluable mutant set must satisfy Compij ≥ β, with at least one assertion receiving a non-vacuous completeness evaluation. In our implementation, the default thresholds are α = 1.0 and β = 0.9. If no submitted program satisfies these conditions within the maximum number of turns, the trajectory is marked unsuccessful and is not used as accepted specification supervision. 4) Training Data: Accepted annotated programs are converted into two supervised fine-tuning tasks: specification generation and code generation. a) Specification generation: This task teaches the model to insert executable checkpoint specifications into an existing program. The input contains the problem statement and a program pi , where pi can be either the validated reference program or a retained mutant: pi ∈ {yi } ∪ Mi . For the reference program, the target is the accepted annotated program ỹi . For a mutant, we construct the target m̃ by inserting the accepted checkpoint specifications at the corresponding program locations of the mutant, while preserving the mutant’s

executable code. The target assertions describe the intended intermediate semantics of the task, not the behavior of the buggy code. Thus, when m̃ is executed, some assertions may fail and expose the fault. The training example is the same program annotated with executable checkpoint specifications: (xi , pi ) → p̃i . b) Code generation: This task teaches the model to generate a specification-bearing solution directly from the problem statement. The input contains only the problem statement, and the output is the validated reference solution annotated with checkpoint specifications: xi → ỹi . The final training data is the union of the two task datasets: D = Dspec ∪ Dcode . B. Model Training S PEC C ODER is trained with supervised fine-tuning on the constructed instruction data. The training set contains two types of examples: specification-generation examples, where the model annotates a given program with executable checkpoint assertions, and code-generation examples, where the model generates a complete solution together with checkpoint assertions. The two tasks share the same goal: the response should be a program with intermediate specifications. All examples are formatted as instruction-response pairs. For specification generation, the instruction contains the problem statement and an input program; for code generation, the instruction contains only the problem statement. In both cases, the response is the final annotated program. We do not train the student model to reproduce the teacher’s exploration turns or verifier feedback. The multi-turn refinement process is used only to construct and filter high-quality supervision targets. With the training corpus D = Dspec ∪ Dcode , we optimize the standard autoregressive language-modeling objective over the target response: L(θ) = −

|o| X X

log pθ (oj | u, o<j ),

(u,o)∈D j=1

where u is the instruction input and o is the annotated-program response. At inference time, the trained model can be used in the specification-generation setting to insert checkpoint assertions into a given program. IV. H UMAN E XEC DATASET We introduce HumanExec, a benchmark for evaluating whether models can generate and use executable specifications in realistic programming tasks. HumanExec is collected from recent Codeforces problems and is kept separate from the LeetCode-style data used to construct S PEC C ODER’s training corpus. Each task contains a problem statement, input/output specification, reference solution, human-submitted buggy solutions, and an executable test suite. The buggy programs come from real human submissions rather than synthetic mutation rules. Thus, the benchmark captures common programming

mistakes in algorithm design, boundary handling, state updates, data-structure usage, and case analysis. This allows us to test if executable checkpoint specifications are useful beyond the synthetic mutants used during training-data construction. To make the benchmark suitable for semantic verification, we filter out shallow failures. We remove submissions that do not compile, use malformed input/output handling, or fail only due to immediate runtime errors. We retain bugs that execute normally but produce incorrect outputs on some tests, since these cases require reasoning about the intended algorithm rather than merely fixing syntax or crashes. We also validate each reference solution against the available test suite and keep only tasks whose reference program passes all tests. For a buggy submission, we retain only non-trivial incorrect programs that pass at least one test and fail at least one test. This ensures that the benchmark focuses on semantic deviations rather than equivalent solutions or completely broken code. HumanExec is aimed to measure both specification quality and downstream programming performance under a shared execution setting. It has a total of 150 tasks, each has 48– 279 test cases with mean=79.53 and median=70. The number of mutant per task is 150, with min=3, max=188, mean=53.19, and median=44. The difficulty level is from 800-2500 (CodeForces standard), with mean=1348, and median=1300. Specification generation. Given a problem statement and a reference solution, the model must insert executable checkpoint specifications at meaningful internal program points. This subtask evaluates whether generated assertions are executable, valid on correct executions, and discriminative against faulty executions from human-submitted buggy programs. Program repair. Given a problem statement and a humansubmitted buggy solution, the model must produce a repaired solution that passes the test suite. This subtask tests whether executable checkpoint specifications can provide useful local evidence for identifying and correcting semantic errors. Program correctness checking. Given a problem statement and a candidate solution, the model must determine whether the solution is correct. This subtask evaluates whether models can use specification to justify correctness or expose a bug, instead of relying only on surface-level code plausibility. V. E MPIRICAL E VALUATION We evaluate S PEC C ODER from different perspectives: whether it generates higher-quality executable checkpoint specifications for a given code, and whether these specifications improve downstream programming tasks. Our evaluation is centered around the following research questions: • RQ1: Specification Generation. Can S PEC C ODER generate more correct and discriminative checkpoint specifications than prompted base models for a given code? • RQ2: Program Correctness Checking. Can S PEC C ODER’s checkpoint specifications help models judge whether a candidate program is correct? • RQ3: Program Repair. Do executable checkpoint specifications improve code repair of buggy programs?

TABLE II S PECIFICATION - GENERATION QUALITY ON H UMAN E XEC . A BBREVIATIONS : C ORR . = CORRECTNESS ON CORRECT EXECUTIONS ; C OMP. = COMPLETENESS AGAINST BEHAVIOR - CHANGING MUTANTS ; %VALID = EXECUTABLE ASSERTION RATE .

Inline Checkpoint Specs

Model Corr. Qwen2.5-Coder-7B + SpecCoder

Postconditions

∆ Corr. Comp. ∆ Comp. %Valid ∆ Valid

Corr.

∆ Corr. Comp. ∆ Comp.

0.5358 0.5389

0.0% +0.6%

0.3161 0.6981

0.0% +120.8%

0.7900 1.0000

0.0% 0.5808 0.0% +26.6% 0.6477 +11.5%

0.1901 0.6643

0.0% +249.4%

0.8989 0.9973

0.0% 0.7697 0.0% +10.9% 0.9047 +17.5%

0.2394 0.4561

0.0% +90.5%

0.2794 0.0% 0.4353 +55.8%

0.1707 0.7820

0.0% +358.1%

0.8272 0.9028

0.0% +9.1%

Qwen2.5-Coder-14B 0.5227 0.0% + SpecCoder 0.6468 +23.7%

0.1989 0.7713

0.0% +287.8%

Qwen2.5-Coder-32B 0.6313 0.0% + SpecCoder 0.8098 +28.3%

0.2640 0.6843

0.0% +159.2%

1) Datasets: We use HumanExec as the primary benchmark for all three RQs. For RQ1, we evaluate specification generation on reference solutions. Generated assertions are executed on correct reference executions to measure validity and correctness, and are evaluated against faulty executions to measure discriminativeness. These faulty executions are obtained from human-submitted buggy solutions in HumanExec; if evaluation-only mutants are additionally used, they are generated only after the train/test split and are never used for training. For RQ2, we construct candidate programs from both reference solutions and human-submitted buggy solutions and ask models to predict if each candidate is correct. For RQ3, we use human-submitted buggy solutions as repair inputs and evaluate generated repairs against the HumanExec test suites. 2) Models: We evaluate representative LLMs from the Qwen2.5-Coder families: Qwen2.5-Coder-7B, Qwen2.5Coder-14B, Qwen2.5-Coder-32B. For each model, we compare the base instruction-tuned model with its S PEC C ODERtuned counterpart. All methods use the same decoding settings and evaluation test suites. A. RQ1: Specification Generation 1) Baselines: We compare S PEC C ODER against zero-shot specification generation, where the base instruction-tuned model directly annotates a given program with checkpoint specifications. This baseline tests whether prompting alone is sufficient to produce high-quality executable specifications from the same backbone model. 2) Metrics: We evaluate generated specifications using execution-based metrics. Validity measures the fraction of generated assertions that can be safely instrumented and executed, excluding assertions with syntax errors, out-of-scope variables, or unsafe operations. Correctness measures whether a reachable assertion holds on correct executions of the reference solution. Completeness measures, in an operational mutantbased sense, whether a correct assertion rejects behaviorchanging faulty executions that reach the same checkpoint. Completeness is measured using evaluation-only behaviorchanging mutants constructed from HumanExec reference solutions after the train/test split. These mutants are used only for evaluation and are not included in S PEC C ODER’s training data. Note that completeness captures discriminative power against

Fig. 3. Quality of generated checkpoint assertions.

the available faulty executions rather than logical completeness over all possible bugs. We report these metrics separately for inline checkpoint specifications and final postconditions. 3) Results: Table II summarizes the specificationgeneration results on HumanExec. Across the zero-shot base models, larger base models improve correctness and completeness, although validity is not strictly monotonic. Yet, their specifications remain limited. Qwen2.5-Coder-7B achieves only 0.2794 correctness and 0.1707 completeness, while Qwen2.5-Coder-14B improves correctness to 0.5227 but still obtains only 0.1989 completeness. The strongest base model, Qwen2.5-Coder-32B, further improves to 0.6313 correctness and 0.2640 completeness, yet its generated specifications are still far from reliably discriminative. These results indicate that scaling the base model helps, but prompting alone is insufficient for generating specifications that are both correct and useful for rejecting buggy executions. S PEC C ODER substantially improves inline checkpoint specification quality. With Qwen2.5-Coder-14B, S PEC C ODER increases correctness from 0.5227 to 0.6468 and completeness from 0.1989 to 0.7713, while reaching 1.0000 executable assertion validity. With Qwen2.5-Coder-32B, S PEC C ODER reaches 0.8098 correctness and 0.6843 completeness, compared with 0.6313 and 0.2640 for the corresponding base zero-shot model. Across the three tuned backbones, S PEC C ODER improves average inline correctness from 0.4778 to 0.6306, average inline completeness from 0.2112 to 0.7459, and average validity from 0.8387 to 0.9667. These gains

show that verification-guided fine-tuning teaches the model to generate checkpoint assertions that are not only syntactically executable, but also substantially more discriminative against behavior-changing mutants. The specifications from S PEC C ODER range from value constraints, ordering structure, loop progress, algorithm, data shape, and others. Figure 3 further explains the source of these gains. We measure Checkpoint Quality as the fraction of assertions reached by at least one test case, and Non-triviality as the fraction of assertions that reject at least one mutant. These metrics are useful because a model could generate assertions in locations where no faulty execution reaches or can be affected by them. Such assertions may be correct, but they do not provide evidence for discriminating correct behavior from faulty behavior. Across all three backbones, S PEC C ODER consistently improves both metrics: average checkpoint quality increases from 68.6% to 87.1%, while the non-trivial assertion rate increases from 39.3% to 83.4%. This shows that S PEC C ODER does not merely generate more executable assertions; it generates assertions that are more often exercised during execution and more likely to expose faulty intermediate states. The remaining results follow the same trend. For Qwen2.5Coder-7B, S PEC C ODER achieves 0.4353 correctness, 0.7820 completeness, and 0.9028 validity, improving over the corresponding zero-shot base model by 55.8%, 358.1%, and 9.1%, respectively. For postcondition specifications, S PEC C ODER achieves 0.6971 correctness and 0.6062 completeness on average, compared with 0.6288 correctness and 0.2485 completeness for zero-shot prompting. The postcondition results show that S PEC C ODER also improves final-state specifications, but the largest gains occur for inline checkpoint completeness. This suggests that verification-guided training is especially beneficial for the harder task of generating intermediate assertions that expose faulty internal states. Overall, the results indicate that executable checkpoint specifications require verification-guided training rather than direct prompting alone. 4) Does SpecCoder Internalize Checkpoint Specifications?: We further measure whether S PEC C ODER internalizes executable checkpoint specifications using 30 held-out validation problems from the dataset construction process. Each problem contains verified annotated specifications produced by our verification-guided refinement pipeline. For each assertion, we teacher-force the same annotated program under the base model and the corresponding S PEC C ODER model, and compute perplexity only over assertion tokens. Since both models score the same target assertions, lower perplexity indicates that the model assigns higher likelihood to the same specification. Fig. 4 shows that S PEC C ODER shifts the per-assertion perplexity distribution left across all three backbones, indicating higher confidence on the same executable assertions. Together with Table II, this suggests that it learns both the syntax and placement patterns of checkpoint specifications, rather than relying only on prompting-time instruction following. 5) Qualitative Analysis: Fig. 5 shows a representative example comparing zero-shot specification generation with S PEC C ODER. The original model does not generate specifi-

Fig. 4. ECDF of per-assertion perplexity on held-out inline checkpoint specifications. Each panel compares a base Qwen2.5-Coder model with its S PEC C ODER-tuned counterpart on the same assertion tokens.

cations in the required executable format; instead, it mainly inserts explanatory comments, such as describing that s accumulates digit sums or that t is a greatest common divisor. Even comments prefixed with “assert” are still naturallanguage descriptions rather than valid Boolean predicates. As a result, they cannot be directly instrumented or checked during execution. In contrast, S PEC C ODER generates executable checkpoint assertions over in-scope variables, such as s == 0 and N - 2 > 0, n == N and 2 <= i < N, and t > 0 and s % t == 0 and (N-2) % t == 0. These assertions are placed at meaningful internal program points and can be evaluated on runtime states, illustrating why S PEC C ODER improves both assertion validity and discriminative completeness. B. RQ2: Program Correctness Checking RQ2 evaluates whether checkpoint specifications help a model judge whether a candidate program is correct. This task is different from repair: the model must produce a correctness verdict and justification rather than a patch. 1) Baselines: We compare direct correctness checking from the problem statement and code against chain-of-thought prompting, HoarePrompt-style natural-language specification reasoning, and S PEC C ODER with executable assertion evidence. The S PEC C ODER classifier receives checkpoint specifications and, when applicable, violated-specification evidence. 2) Metrics: We report Matthews Correlation Coefficient (MCC), balanced accuracy, true negative rate, true positive rate, false negative rate, and false positive rate. MCC and balanced accuracy summarize overall classification quality under class imbalance, while FPR and FNR distinguish the risk of incorrectly accepting a buggy program from the risk of incorrectly rejecting a correct program. 3) Results: Table III reports correctness-checking results on H UMAN E XEC. Overall, executable checkpoint evidence improves correctness checking across model sizes. Compared with Vanilla, S PEC C ODER improves MCC from 0.236 to 0.307 for Qwen2.5-Coder-7B, from 0.283 to 0.384 for Qwen2.5-

Original Model N = int(input()) s = 0 # s is the sum of digits of N in all bases from 2 to N-1 def gcd(a, b): while(b): a, b = b, a%b return a # a is the greatest common divisor of the initial a and b for i in range(2, N): n = N # n is the current number to be converted to base i while(n>0): s += n%i # s accumulates the sum of digits of N in base i n = n//i # n is reduced by removing the last digit in base i # assert s is the accumulated sum of digits of N in bases from 2 to i t = gcd(s, N-2) # t is the greatest common divisor of s and (N-2) # assert t divides both s and (N-2) without remainder print(str(s//t)+"/"+str((N-2)//t)) # the output is the irreducible fraction of s/(N-2) # assert (s//t) and ((N-2)//t) are the numerator and denominator of the irreducible fraction

N = int(input()) # assert 3 <= N <= 1000 s = 0 # assert s == 0 and N - 2 > 0 and 3 <= N <= 1000

HoarePrompt

N = int(input()) s = 0

SpecCoder

def gcd(a, b): while(b): a, b = b, a%b #State: a is the GCD of the original a and b, and b is 0. return a #The program returns the GCD of the original a and b, which is stored in variable a.

def gcd(a, b): # assert a >= 0 and b >= 0 while(b): a, b = b, a%b # assert b == 0 and a >= 0 return a

for i in range(2, N): n = N while(n>0): s += n%i n = n//i t = gcd(s, N-2) print(str(s//t)+'/'+str((N-2)//t)) #State of the program right berfore the function call: a and b are integers such that 3 <= a <= 1000 and a <= b.

for i in range(2, N): n = N # assert n == N and 2 <= i < N and s >= 0 while(n>0): s += n%i n = n//i # assert n == 0 and i - 1 <= s <= (i - 1) * N # assert N - 2 <= s <= (N - 2) * N and s == sum(sum((N // (base ** k)) % base for k in range(N)) for base in range(2, N)) t = gcd(s, N-2) # assert t > 0 and s % t == 0 and (N-2) % t == 0 print(str(s//t)+"/"+str((N-2)//t))

Fig. 5. Qualitative comparison of specification generation TABLE III P ROGRAM CORRECTNESS - CHECKING PERFORMANCE ON H UMAN E XEC . A BBREVIATIONS : MCC = M ATTHEWS C ORRELATION C OEFFICIENT; ∆MCC = RELATIVE MCC IMPROVEMENT OVER VANILLA ; BA = BALANCED ACCURACY; TPR = T RUE P OSITIVE R ATE ; FNR = FALSE N EGATIVE R ATE ; FPR = FALSE P OSITIVE R ATE ; TNR = T RUE N EGATIVE R ATE .

Model

Qwen2.5-Coder-7B + SpecCoder Qwen2.5-Coder-14B + SpecCoder Qwen2.5-Coder-32B + SpecCoder

Correctness-Checking Metrics

Classifier MCC↑

∆MCC↑

Vanilla CoT HoarePrompt AssertChecker

0.236 0.211 0.310 0.307

Vanilla CoT HoarePrompt AssertChecker Vanilla CoT HoarePrompt AssertChecker

TNR↑ TPR↑

FNR↓

FPR↓

Input

Output

Total

0.0% 0.600 -10.71% 0.600 +30.94% 0.639 +29.75% 0.653

0.733 0.773 0.713 0.820

0.167 0.220 0.427 0.333

0.333 0.280 0.073 0.167

0.267 0.227 0.287 0.180

0.38 0.45 59.30 0.82

0.21 0.31 8.93 0.48

0.59 0.76 68.23 1.30

0.283 0.229 0.366 0.384

0.0% 0.633 -19.14% 0.613 +29.56% 0.680 +35.69% 0.680

0.900 0.840 0.887 0.887

0.233 0.273 0.293 0.253

0.267 0.227 0.207 0.247

0.100 0.160 0.113 0.113

0.38 0.45 53.01 0.91

0.22 0.38 10.47 0.34

0.60 0.83 63.58 1.25

0.394 0.248 0.455 0.493

0.0% 0.693 -36.97% 0.620 +15.69% 0.727 +25.15% 0.733

0.893 0.873 0.840 0.947

0.300 0.247 0.387 0.287

0.200 0.253 0.113 0.213

0.107 0.127 0.160 0.053

0.38 0.45 48.82 0.87

0.08 0.09 12.09 0.49

0.46 0.18 60.91 1.36

Coder-14B, and from 0.394 to 0.493 for Qwen2.5-Coder32B. Balanced accuracy follows the same trend: S PEC C ODER achieves 0.653, 0.680, and 0.733 across the three backbones, matching or exceeding the strongest baseline in each model group. In contrast, simple chain-of-thought prompting does not reliably improve correctness checking and even reduces MCC for all three backbones. This suggests that free-form reasoning alone is insufficient, while executable specification evidence gives the checker a more reliable signal. 4) Qualitative Analysis: Figure 5 also illustrates why executable checkpoint specifications provide stronger evidence for correctness checking than natural-language state reasoning. HoarePrompt generates readable state descriptions, such as explaining that a is the GCD of the original arguments or describing the state before a function call, but these descriptions are not executable and cannot be objectively checked against a candidate program. Some conditions also refer to implicit concepts such as “original” variable values, making them difficult to bind to concrete runtime states. By contrast, S PEC C ODER produces executable assertions that define concrete obligations over program variables, including initialization constraints, loop-state properties, accumulated digit-sum relations, and di-

BA↑

Tokens (Millions)

visibility checks after gcd. When a candidate program violates such an assertion, the checker receives localized, machinecheckable evidence of the semantic deviation, explaining the improved correctness-checking performance of S PEC C ODER. C. RQ3: Program Repair RQ3 evaluates whether executable checkpoint specifications help models repair human-written bugs. Given a buggy program, each method generates one or more candidate repairs under the AgentCoder backbone. We execute each candidate against the full test suite and measure whether the generated patch fixes the program. 1) Baselines: We introduce AssertRepair, an APR method that leverages assertion signals for program repair. Specifically, given a failing test input, AssertRepair executes the program and captures the assertion states, including violated checkpoint specifications. The resulting diagnostic evidence is then provided to the LLM to guide repair generation. Besides the vanilla baseline, we compare AssertRepair with state-of-the-art repair baselines based on natural-language specification signals. We adopt HoarePrompt (V), which uses programs annotated with HoarePrompt-generated specifications for repair, and SpecRover (V), a competitive-

TABLE IV P ROGRAM REPAIR PERFORMANCE ON H UMAN E XEC . A BBREVIATIONS : PASS @k REPORTS WHETHER AT LEAST ONE OF THE TOP -k GENERATED REPAIRS PASSES THE FULL TEST SUITE . APR REPORTS THE MEAN PASS RATE OVER GENERATED REPAIRS .

Model

Method

Pass@1 Pass@3 APR

Vanilla HoarePrompt SpecRover AssertRepair

0.089 0.099 0.132 0.140

0.157 0.111 0.151 0.190

0.447 0.511 0.580 0.514

Vanilla Qwen2.5-Coder-14B HoarePrompt SpecRover + SpecCoder AssertRepair

0.237 0.211 0.235 0.241

0.269 0.289 0.261 0.301

0.578 0.534 0.556 0.598

Vanilla Qwen2.5-Coder-32B HoarePrompt SpecRover + SpecCoder AssertRepair

0.261 0.272 0.279 0.283

0.301 0.358 0.338 0.333

0.615 0.587 0.610 0.622

Qwen2.5-Coder-7B + SpecCoder

programming variant of SpecRover. In contrast to these natural-language-specification baselines, AssertRepair uses executable checkpoint specifications and violated-assertion evidence. To ensure a fair comparison, all methods are allowed only a single repair attempt per turn. 2) Metrics: We report Pass@k, where k ∈ {1, 3}, measuring whether at least one of the top-k generated repairs passes all tests. We also report Average Pass Rate (APR). 3) Results: Table IV reports program repair results on H U MAN E XEC . Overall, executable checkpoint evidence improves

repair effectiveness, especially for the top-ranked generated repairs. S PEC C ODER achieves the best Pass@1 for all three backbones: 0.140 for Qwen2.5-Coder-7B, 0.241 for Qwen2.5Coder-14B, and 0.283 for Qwen2.5-Coder-32B. For Qwen2.5-Coder-14B and Qwen2.5-Coder-32B, S PEC C ODER achieves the highest APR, improving over Vanilla from 0.578 to 0.598 and from 0.615 to 0.622, respectively. These gains suggest that executable checkpoint specifications help the repair agent produce a larger fraction of passing patches, not only a better top candidate. Averaged across the three backbones, S PEC C ODER obtains an APR of 0.578, compared with 0.547 for Vanilla and 0.544 for HoarePrompt. Its average APR is close to SpecRover’s 0.582, while S PEC C ODER achieves stronger Pass@1 and Pass@3 on average. The results therefore suggest that executable checkpoint evidence is most effective at guiding the repair process toward correct high-ranked patches, while its effect on the entire candidate distribution depends on the strength of the underlying model. Overall, RQ3 shows that executable checkpoint specifications provide useful localized evidence for program repair. This evidence improves top-ranked repair success across all model sizes and improves average repair quality for the stronger 14B and 32B backbones.

VI. R ELATED W ORK a) Traditional specification inference: Dynamic approaches infer likely properties by observing executions [7], [1], [2], but their results depend heavily on the coverage and diversity of available tests. Static analyses [8], [9], [10], [11], [12] and abstract interpretation [13] often produce conservative or imprecise specifications due to over-approximation and false positives. Other approaches extract specifications from API documentation or code comments [14], [15], [16], [17], [18], [19], [20]. Data-mining techniques infer common API usage patterns from large codebases [21], [22], [23], including call pairs, sequences, and finite-state models [24], [25], [26], [27], [28], [29]. These methods are useful for API usage constraints, but they rarely infer executable postconditions [11]. b) Machine-learning and LLM-based specification generation: Recent machine-learning and LLM-based techniques have expanded automated specification and oracle generation. Some methods synthesize test oracles or unit tests [30], [31], [32], [33], [34], while others improve test generation and coverage [35], [36]. For example, AthenaTest [34] generates unit test inputs and oracles from the focal method implementation, TOGA [30] focuses on oracle generation, and TiCoder [33] uses LLMs to generate inputs/outputs from textual intent. Other work directly targets specifications. NL2Postcond [3] uses LLMs to infer postconditions from code and textual descriptions, and EvoSpex [37] applies evolutionary learning to infer functional input–output relationships. Recent efforts also explore property-based specifications: Vikram et al. [38] use LLMs to generate property-based tests, while Speculyzer [39] enumerates likely properties and candidate inputs to guide code generation. Beyond input–output properties, learningbased methods have been used to infer program invariants [40], [41], [42], [43]. In contrast, S PEC C ODER targets executable checkpoint specifications: assertions placed at meaningful internal program points and selected using execution feedback from correct programs and behavior-changing mutants. c) Specification-guided reasoning and repair.: LLMs have been used to produce specification-like reasoning for correctness checking and program repair. HoarePrompt [5] uses natural-language state conditions to support structural reasoning about program correctness. SpecRover [6] extracts natural-language code intent to guide agentic program repair, vet patches, and provide supporting evidence. These approaches show that specification-like signals can improve LLM-based reasoning, but their intermediate signals are primarily expressed in natural language and are not directly executable assertions. S PEC C ODER differs by training CodeLLMs to generate executable intermediate specifications that can be checked on concrete executions and used as verifiable evidence for specification generation, consistency checking, and repair. VII. C ONCLUSION We presented S PEC C ODER, a verification-guided framework for training CodeLLMs to generate executable checkpoint specifications. By learning from validated reference programs, behavior-changing mutants, and refinement traces,

S PEC C ODER produces assertions that capture intermediate program states and can be checked during execution. Experiments on H UMAN E XEC show that these checkpoints improve specification quality and provide useful evidence for correctness checking and program repair, suggesting that executable intermediate specifications are a promising path toward more verifiable and repairable LLM-generated programs. VIII. DATA AVAILABILITY S TATEMENT All data and code are available at [44]. R EFERENCES [1] I. Beschastnikh, Y. Brun, S. Schneider, M. Sloan, and M. D. Ernst, “Leveraging existing instrumentation to automatically infer invariant-constrained models,” in Proceedings of the 19th Symposium on Foundations of Software Engineering, ser. ESEC/FSE ’11. ACM, 2011, pp. 267–277. [Online]. Available: http://doi.acm.org/10.1145/2025113.2025151 [2] M. D. Ernst, J. Cockrell, W. G. Griswold, and D. Notkin, “Dynamically discovering likely program invariants to support program evolution,” in Proceedings of the 21st International Conference on Software Engineering, ser. ICSE’99. ACM, 1999, pp. 213–224. [Online]. Available: http://doi.acm.org/10.1145/302405.302467 [3] M. Endres, S. Fakhoury, S. Chakraborty, and S. K. Lahiri, “Can large language models transform natural language intent into formal method postconditions?” Proc. ACM Softw. Eng., vol. 1, no. FSE, Jul. 2024. [Online]. Available: https://doi.org/10.1145/3660791 [4] C. C. Le, M. V. Pham, T. D. Vu, V. D. Cuong, P. N. Huy, P. N. Hoang, and T. N. Nguyen, “SpecMind: Cognitively inspired, interactive multi-turn framework for postcondition inference,” in Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), M. Liakata, V. P. Moreira, J. Zhang, and D. Jurgens, Eds. San Diego, California, United States: Association for Computational Linguistics, Jul. 2026, pp. 36 409–36 424. [Online]. Available: https://aclanthology.org/2026.acl-long.1687/ [5] D. S. Bouras, Y. Dai, T. Wang, Y. Xiong, and S. Mechtaev, “Hoareprompt: Structural reasoning about program correctness in natural language,” 2025. [Online]. Available: https://arxiv.org/abs/2503.19599 [6] H. Ruan, Y. Zhang, and A. Roychoudhury, “Specrover: Code intent extraction via llms,” in Proceedings of the IEEE/ACM 47th International Conference on Software Engineering, ser. ICSE ’25. IEEE Press, 2025, p. 963–974. [Online]. Available: https://doi.org/10.1109/ICSE55347.2025.00080 [7] G. Ammons, R. Bodı́k, and J. R. Larus, “Mining specifications,” in Proceedings of the 29th ACM SIGPLAN SIGACT Symposium on Principles of Programming Languages, ser. POPL ’02. ACM, 2002, pp. 4–16. [Online]. Available: http://doi.acm.org/10.1145/503272.503275 [8] S. Shoham, E. Yahav, S. Fink, and M. Pistoia, “Static specification mining using automata-based abstractions,” in Proceedings of the 2007 International Symposium on Software Testing and Analysis, ser. ISSTA ’07. New York, NY, USA: Association for Computing Machinery, 2007, p. 174–184. [Online]. Available: https://doi.org/10.1145/1273463.1273487 [9] D. Engler, D. Y. Chen, S. Hallem, A. Chou, and B. Chelf, “Bugs as deviant behavior: A general approach to inferring errors in systems code,” in Proceedings of the Eighteenth ACM Symposium on Operating Systems Principles, ser. SOSP’01. ACM, 2001, pp. 57–72. [Online]. Available: http://doi.acm.org/10.1145/502034.502041 [10] T. Kremenek, P. Twohey, G. Back, A. Ng, and D. Engler, “From uncertainty to belief: inferring the specification within,” in Proceedings of the 7th Symposium on Operating Systems Design and Implementation, ser. OSDI ’06. USA: USENIX Association, 2006, p. 161–176. [11] M. K. Ramanathan, A. Grama, and S. Jagannathan, “Static specification inference using predicate mining,” in Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation, ser. PLDI ’07. ACM, 2007, pp. 123–134. [Online]. Available: http://doi.acm.org/10.1145/1250734.1250749 [12] Y. Wei, C. A. Furia, N. Kazmin, and B. Meyer, “Inferring better contracts,” in Proceedings of the 33rd International Conference on Software Engineering, ser. ICSE ’11. ACM, 2011, pp. 191–200. [Online]. Available: http://doi.acm.org/10.1145/1985793.1985820

[13] P. M. Cousot, R. Cousot, F. Logozzo, and M. Barnett, “An abstract interpretation framework for refactoring with application to extract methods with contracts,” in Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, ser. OOPSLA ’12. New York, NY, USA: Association for Computing Machinery, 2012, p. 213–232. [Online]. Available: https://doi.org/10.1145/2384616.2384633 [14] R. Pandita, X. Xiao, H. Zhong, T. Xie, S. Oney, and A. Paradkar, “Inferring method specifications from natural language api descriptions,” in Proceedings of the 34th International Conference on Software Engineering, ser. ICSE ’12. IEEE Press, 2012, p. 815–825. [15] L. Tan, D. Yuan, G. Krishna, and Y. Zhou, “/*icomment: bugs or bad comments?*/,” in Proceedings of Twenty-First ACM SIGOPS Symposium on Operating Systems Principles, ser. SOSP ’07. New York, NY, USA: Association for Computing Machinery, 2007, p. 145–158. [Online]. Available: https://doi.org/10.1145/1294261.1294276 [16] L. Tan, Y. Zhou, and Y. Padioleau, “acomment: mining annotations from comments and code to detect interrupt related concurrency bugs,” in Proceedings of the 33rd International Conference on Software Engineering, ser. ICSE ’11. New York, NY, USA: Association for Computing Machinery, 2011, p. 11–20. [Online]. Available: https://doi.org/10.1145/1985793.1985796 [17] S. H. Tan, D. Marinov, L. Tan, and G. T. Leavens, “@tcomment: Testing javadoc comments to detect comment-code inconsistencies,” in Proceedings of the 2012 IEEE Fifth International Conference on Software Testing, Verification and Validation, ser. ICST ’12. USA: IEEE Computer Society, 2012, p. 260–269. [Online]. Available: https://doi.org/10.1109/ICST.2012.106 [18] A. Blasi, A. Goffi, K. Kuznetsov, A. Gorla, M. D. Ernst, M. Pezzè, and S. D. Castellanos, “Translating code comments to procedure specifications,” in Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis, ser. ISSTA 2018. New York, NY, USA: Association for Computing Machinery, 2018, p. 242–253. [Online]. Available: https://doi.org/10.1145/3213846.3213872 [19] H. Zhong, L. Zhang, T. Xie, and H. Mei, “Inferring resource specifications from natural language api documentation,” in Proceedings of the 24th IEEE/ACM International Conference on Automated Software Engineering, ser. ASE ’09. USA: IEEE Computer Society, 2009, p. 307–318. [Online]. Available: https://doi.org/10.1109/ASE.2009.94 [20] Y. Zhou, R. Gu, T. Chen, Z. Huang, S. Panichella, and H. Gall, “Analyzing apis documentation and code to detect directive defects,” in 2017 IEEE/ACM 39th International Conference on Software Engineering (ICSE), 2017, pp. 27–37. [21] Z. Li and Y. Zhou, “Pr-miner: Automatically extracting implicit programming rules and detecting violations in large software code,” in Proceedings of the 13th Symposium on Foundations of Software Engineering, ser. ESEC/FSE-13. ACM, 2005, pp. 306–315. [Online]. Available: http://doi.acm.org/10.1145/1081706.1081755 [22] B. Livshits and T. Zimmermann, “Dynamine: finding common error patterns by mining software revision histories,” in Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, ser. ESEC/FSE-13. New York, NY, USA: Association for Computing Machinery, 2005, p. 296–305. [Online]. Available: https://doi.org/10.1145/1081706.1081754 [23] H. Zhong, T. Xie, L. Zhang, J. Pei, and H. Mei, “Mapo: Mining and recommending api usage patterns,” in Proceedings of the 23rd European Conference on ECOOP 2009 — Object-Oriented Programming. Springer-Verlag, 2009, pp. 318–343. [24] A. Wasylkowski, A. Zeller, and C. Lindig, “Detecting object usage anomalies,” in Proceedings of the Symposium on Foundations of Software Engineering, ser. ESEC-FSE ’07. ACM, 2007, pp. 35–44. [Online]. Available: http://doi.acm.org/10.1145/1287624.1287632 [25] C. C. Williams and J. K. Hollingsworth, “Automatic mining of source code repositories to improve bug finding techniques,” IEEE Trans. Softw. Eng., vol. 31, no. 6, pp. 466–480, 2005. [26] S. Thummalapenta and T. Xie, “Alattin: Mining alternative patterns for detecting neglected conditions,” in Proceedings of the 2009 IEEE/ACM International Conference on Automated Software Engineering, ser. ASE ’09. IEEE Computer Society, 2009, pp. 283–294. [Online]. Available: http://dx.doi.org/10.1109/ASE.2009.72 [27] T. T. Nguyen, H. A. Nguyen, N. H. Pham, J. M. Al-Kofahi, and T. N. Nguyen, “Graph-based mining of multiple object usage patterns,” in Proceedings of the Symposium on Foundations of Software Engineering,

ser. ESEC/FSE ’09. ACM, 2009, pp. 383–392. [Online]. Available: http://doi.acm.org/10.1145/1595696.1595767 [28] M. Pradel and T. R. Gross, “Automatic generation of object usage specifications from large method traces,” in Proceedings of the 2009 IEEE/ACM International Conference on Automated Software Engineering, ser. ASE ’09. IEEE Computer Society, 2009, pp. 371–382. [Online]. Available: http://dx.doi.org/10.1109/ASE.2009.60 [29] A. Wasylkowski and A. Zeller, “Mining temporal specifications from object usage,” in Proceedings of the 2009 IEEE/ACM International Conference on Automated Software Engineering, ser. ASE ’09. IEEE Computer Society, 2009, pp. 295–306. [Online]. Available: http://dx.doi.org/10.1109/ASE.2009.30 [30] E. Dinella, G. Ryan, T. Mytkowicz, and S. K. Lahiri, “Toga: a neural method for test oracle generation,” in Proceedings of the 44th International Conference on Software Engineering, ser. ICSE ’22. New York, NY, USA: Association for Computing Machinery, 2022, p. 2130–2141. [Online]. Available: https://doi.org/10.1145/3510003.3510141 [31] A. Mastropaolo, N. Cooper, D. N. Palacio, S. Scalabrino, D. Poshyvanyk, R. Oliveto, and G. Bavota, “Using transfer learning for coderelated tasks,” IEEE Transactions on Software Engineering, vol. 49, no. 4, pp. 1580–1598, 2023. [32] M. Tufano, D. Drain, A. Svyatkovskiy, and N. Sundaresan, “Generating accurate assert statements for unit test cases using pretrained transformers,” in Proceedings of the 3rd ACM/IEEE International Conference on Automation of Software Test, ser. AST ’22. New York, NY, USA: Association for Computing Machinery, 2022, p. 54–64. [Online]. Available: https://doi.org/10.1145/3524481.3527220 [33] S. K. Lahiri, S. Fakhoury, A. Naik, G. Sakkas, S. Chakraborty, M. Musuvathi, P. Choudhury, C. von Veh, J. P. Inala, C. Wang, and J. Gao, “Interactive code generation via test-driven user-intent formalization,” 2023. [Online]. Available: https://arxiv.org/abs/2208.05950 [34] M. Tufano, D. Drain, A. Svyatkovskiy, S. K. Deng, and N. Sundaresan, “Unit test case generation with transformers and focal context,” 2021. [Online]. Available: https://arxiv.org/abs/2009.05617 [35] C. Lemieux, J. P. Inala, S. K. Lahiri, and S. Sen, “Codamosa: Escaping coverage plateaus in test generation with pre-trained large language models,” in Proceedings of the 45th International Conference on Software Engineering, ser. ICSE ’23. IEEE Press, 2023, p. 919–931. [Online]. Available: https://doi.org/10.1109/ICSE48619.2023.00085 [36] J. Altmayer Pizzorno and E. D. Berger, “Coverup: Effective high coverage test generation for python,” Proc. ACM Softw. Eng., vol. 2, no. FSE, Jun. 2025. [Online]. Available: https://doi.org/10.1145/3729398 [37] F. Molina, P. Ponzio, N. Aguirre, and M. Frias, “Evospex: An evolutionary algorithm for learning postconditions,” in Proceedings of the 43rd International Conference on Software Engineering, ser. ICSE ’21. IEEE Press, 2021, p. 1223–1235. [Online]. Available: https://doi.org/10.1109/ICSE43902.2021.00112 [38] V. Vikram, C. Lemieux, J. Sunshine, and R. Padhye, “Can large language models write good property-based tests?” 2024. [Online]. Available: https://arxiv.org/abs/2307.04346 [39] W.-D. Li, D. Y. Key, and K. Ellis, “Toward trustworthy neural program synthesis,” in ICLR 2025 Third Workshop on Deep Learning for Code, 2025. [Online]. Available: https://openreview.net/forum?id=zC4Wjyu2Wu [40] P. Garg, D. Neider, P. Madhusudan, and D. Roth, “Learning invariants using decision trees and implication counterexamples,” in Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ser. POPL ’16. New York, NY, USA: Association for Computing Machinery, 2016, p. 499–512. [Online]. Available: https://doi.org/10.1145/2837614.2837664 [41] L. Laich, P. Bielik, and M. Vechev, “Guiding program synthesis by learning to generate examples,” in International Conference on Learning Representations, 2020. [Online]. Available: https://openreview.net/forum?id=BJl07ySKvS [42] J. Yao, G. Ryan, J. Wong, S. Jana, and R. Gu, “Learning nonlinear loop invariants with gated continuous logic networks,” in Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, ser. PLDI 2020. New York, NY, USA: Association for Computing Machinery, 2020, p. 106–120. [Online]. Available: https://doi.org/10.1145/3385412.3385986 [43] K. Pei, D. Bieber, K. Shi, C. Sutton, and P. Yin, “Can large language models reason about program invariants?” in Proceedings

of the 40th International Conference on Machine Learning, ser. Proceedings of Machine Learning Research, A. Krause, E. Brunskill, K. Cho, B. Engelhardt, S. Sabato, and J. Scarlett, Eds., vol. 202. PMLR, 23–29 Jul 2023, pp. 27 496–27 520. [Online]. Available: https://proceedings.mlr.press/v202/pei23a.html [44] [Online]. Available: https://speccoder.site