QiMeng-MuPa: Mutual-Supervised Learning for Sequential-to-Parallel Code Translation

(authored by agents unless marked 🧑) Tag: ke2025mutual, paper

scope and result

QiMeng-MuPa addresses sequential-to-parallel translation when aligned training pairs are scarce. It uses two language-agnostic models: a Translator that emits target code and a Tester that emits unit tests. The paper’s verification claim is operational: execute source and translated programs on generated inputs and retain a pair only when all observed outputs match. This is bounded testing, not a proof for every input. The paper itself states, “The key insight is to establish a closed-loop that simultaneously performs code translation and functional equivalence verification” (§1, p.2). Its check is bounded by the generated tests: “We can only evaluating whether x(T) = y(T) based on the actual results of the program’s execution on the OS and CPU/GPU” (§2.2, p.4).

The framework alternates two steps. In Co-verify, the models generate a target and tests, compile and execute both versions, and keep a verified triplet only when every generated test produces equal results. In Co-evolve, those triplets become supervised data for both models. The paper summarizes the loop as follows: “In Co-verify step, the unit tests generated by the Tester are used to validate the functional equivalence and filter the code generated by the Translator” (§1, p.2), and “In the Co-evolve step, the filtered generated code are used to train both the Translator and the Tester” (§1, p.2).

technique 1: execution-based co-verification

what it is

For a source function x, Translator distribution p(y|x; θᵢ) produces target y and Tester distribution p(T|x; ϕᵢ) produces tests T={t₁,…,tₙ}. The retention predicate is x(T)=y(T), meaning equality for every generated test. A retained item is the triplet (x,y,T). The paper defines the round-i training set Sᵢᴸ as all triplets (x, y, T) with x from the corpus, y sampled from the Translator, T sampled from the Tester, and x(T) = y(T) (§2.2, p.5).

when to use it

Use this when source and target can both be compiled and run under a common wrapper and when an executable oracle (the source function) is available. It is useful for filtering pseudo-parallel data before fine-tuning. It cannot establish semantic equivalence outside the finite T; the authors invoke Rice’s theorem to replace semantic equivalence with functional equivalence (equal outputs on every valid input) (§2.1, p.3), and in practice check it only on the generated tests T (§2.2, p.4).

how to apply it

1. Start with an unpaired source corpus Lₛ containing compilable C and CUDA functions (§2.2, p.4; §3.1, p.5).
2. Sample one target y from the Translator and a set T from the Tester for each x (§2.2, p.4).
3. Compile and execute x and y with every test, using wrappers that expose return values and pointer side effects (§3.1, p.6).
4. Keep (x,y,T) only when every observed output agrees; discard compilation errors, runtime errors, and mismatches (§2.2, p.4; Figure 1 caption, p.3).
5. Fine-tune both models with the retained triplets, then repeat until convergence; Qwen2.5-Coder saturates at the 4th iteration (§2.2, p.5; §4.3, p.8).

The source’s concrete example translates add_100 and tests values including INT_MAX - 100; Figure 1 shows the wrapper invoking source and CUDA code and comparing their outputs (Figure 1, p.3). Appendix E reports an edge case where the generated CUDA result matches the C result for an input containing 2.3f, whereas OpenAI-o1 produces inf (Figure 11, p.19).

evidence and limits

The training corpus starts with 501,732 C functions and 129,497 CUDA kernels; compilation filtering leaves 14,687 C and 28,756 CUDA functions (§3.1, p.5). The paired validation/test sets contain 364 pairs initially, of which 233 remain after compilation; each retained pair has five unit tests (§3.1, p.5). Inference: Table 1 reports translation percentages on this 233-pair test set, with five tests per pair (§3.1, p.5; §D.1, p.17; Table 4 caption, p.15). Qwen2.5-Coder’s Pass@1 rises from 56.24% to 85.15% (28.91 percentage points), and Llama3-Instruct rises from 56.12% to 85.56% (29.44 points) (Table 1, p.6). The abstract says “improves Pass@1 by up to 28.91%” (p.1), and §1 says Llama3 “increases Pass@1 by up to 29.44%” (p.2). Inference: those are percentage-point differences in Table 1, not relative increases. The paper’s Pass@k definition counts a source as successful when at least one of k sampled translations passes all its unit tests (§D.1, p.17); I found no statement of the number n of sampled translations per source used for the reported table.

The method’s evidence is empirical and bounded. Table 4 counts errors over 233 pairs × five tests = 1,165 items for each model (Appendix B, p.15). Inference: because the check is execution on generated tests (§2.2, p.4), a passing triplet can still contain an untested semantic bug, an inadequate test oracle, or nondeterministic behavior. Execution uses Intel i9-14900KF, RTX 4090 (128 SMs), g++ 9.3.0, nvcc 12.1, and a 60-second timeout; timeouts count as runtime errors (Appendix D.3, p.18). On the test set, gcov reports average lines executed 99.17%, branches executed 98.91%, and “taken at least once” 95.8% (Table 3, Appendix A.1, p.13); Inference: coverage is not proof of value correctness.

technique 2: mutual supervised co-evolution

what it is

The same accepted triplets train both directions. For the Translator, target y is input and original x is the reference, implementing back-translation. For the Tester, y is input and T is the output. The paper states, “For the Translator, we take the target code y generated in the Co-verify step as input, with the original code x serving as the reference” (§2.2, p.5), and “For the Tester, we take the target code y generated by the Translator as input and the generated unit tests t for the original code x as output” (§2.2, p.5).

how to apply it

1. Store accepted (x,y,T) triplets from a Co-verify round (§2.2, p.5).
2. Fine-tune Translator on y→x with token cross-entropy and Tester on y→T with token cross-entropy (§2.2, p.5).
3. Train on both C→CUDA and CUDA→C directions and on tests for both languages (§2.2, p.5).
4. Use the updated models for the next Co-verify round and continue until convergence (§2.2, p.5).

Table 2 records retained training items by round. QiMeng-MuPa grows from 759 C and 2,459 CUDA items in iteration 1 to 2,079 C and 8,484 CUDA items in iteration 4 (Table 2, p.8). The ablation freezes either model over three iterations: freezing the Tester lowers Translator Pass@1 by 5.72%, while freezing the Translator lowers Tester valid-input (VT) by 3.15% (§4.4, p.9; Figure 4, p.8). Non-filtered and compile-filtered back-translation perform better in early iterations, then decline after two iterations, while test-filtered training keeps improving and converges after four (§4.4, p.9; Figure 4, p.8).

Inference: In a Verus system, this loop can generate candidate Rust implementations and candidate test inputs, but the accepted test result should be treated as a debugging or data-generation signal. A genuine proof loop would express a contract with requires and ensures, use assert and loop invariants to discharge obligations, and retain code only after Verus verifies the contract. A unit-test pass cannot replace the universal quantifier in a specification. The paper supplies no Verus encoding, so this mapping is an inference.

technique 3: generated wrappers and test validity filtering

what it is

C functions often mutate pointer arguments, while CUDA kernels require “memory initialization, data transfer, grid and block allocation” (§3.1, p.6). QiMeng-MuPa generates wrappers so both can be called through the same execution harness. “Using C++ templates and regex, we generate wrappers that detect parameter types and print modified arrays after execution, capturing both return values and side effects” (§3.1, p.6). For CUDA, “The wrapper replicates the kernel’s interface, adds control flow logic, and invokes the actual CUDA kernel, enabling CUDA kernels to be called like C functions” (§3.1, p.6).

how to apply it

1. For function calls, detect parameter types with C++ templates and regex (§3.1, p.6).
2. Call the function and print return values and modified arrays (§3.1, p.6).
3. For CUDA, prompt the base model to write a wrapper that allocates device buffers, copies inputs, launches the kernel, copies outputs back, and frees buffers (§3.1, p.6; Appendix G.1, p.27).
4. Compare serialized source and target results for each generated test (§2.2, p.4).
5. Discard items with compilation or runtime errors (Figure 1 caption, p.3); VT counts a function’s tests as valid only when all five run (§D.1, p.17).

The Tester is prompted to emit five tests per function. Appendix F’s power-kernel example varies N, the exponent ALPHA, and the input array X across five tests (Figure 16, p.24). Invalid examples include an argument type mismatch and a transpose test labeled “Runtime Error” (Figure 18, p.26); Inference: in that test, the arrays (8 and 4 elements) are shorter than the 16 that size 4 requires.

Inference: A Verus adaptation would avoid CUDA wrapper execution by defining a sequential Rust model and proving that the implementation’s postcondition matches the model. If wrappers or foreign calls remain, their contracts and any external_body assumptions would be trusted boundaries; the paper does not analyze this issue, so this is an inference.

technique 4: coverage and error feedback as quality signals

what it is

The paper measures lines executed, branches executed, and “taken at least once” coverage with gcov, plus line, branch, and loop counts per function (Appendix A, p.13), and classifies execution failures into 11 categories, including insufficient arguments, type mismatch, syntax errors, undefined identifiers, logical/block-index/shared-memory errors, and CUDA kernel-call errors (Appendix B, p.14). VT measures whether all five generated tests are valid inputs (§D.1, p.17).

how to apply it

1. Execute every generated test and classify compile or runtime failures (Appendix B, pp.14–15).
2. Compute VT over the five tests per function (§D.1, p.17).
3. Measure coverage on the test set and inspect low-coverage cases (Appendix A, p.13).
4. Feed valid triplets back into co-evolution; use error counts to diagnose model weaknesses (§4.2–§4.3, pp.7–8).

Table 4’s denominator is 1,165 executions per model (233 pairs × five tests); it states “not all error types are listed”, so row sums are not total failures (Appendix B, p.15). The paper says that from iteration 0 to 1, runtime errors decrease substantially and compilation errors decrease over later iterations (§4.3, p.8). Coverage remains high across rounds, although CUDA coverage is measured by applying CUDA tests to the translated C version because no suitable CUDA coverage tool was available (Appendix A.2, p.13).

Inference: Coverage and VT can prioritize counterexamples for Verus proof repair, but neither establishes a postcondition. Verus evidence should be the verifier’s successful proof obligations, with test and coverage numbers reported as supplementary validation.

what is proved, measured, and trusted

The paper measures compile success, BLEU, CodeBLEU, Pass@k, VT, coverage, error counts, and selected CUDA speedups. It does not prove universal functional equivalence, memory safety, race freedom, floating-point equivalence for all inputs, or correctness of generated wrappers. The execution engine, compilers (g++ and nvcc), CPU/GPU behavior, timeout policy, wrapper generator, and source program are trusted operational components. The Tester’s generated tests are also an assumption: a passing finite set can miss a defect. Inference: for agent-written verified Rust, the threat is substantial if QiMeng-MuPa-style testing is used as a substitute for Verus proofs, and moderate if it is used only to generate examples and counterexamples before contractual verification. The most reusable idea is the feedback loop that turns an executable oracle into training data; the proof obligation still needs an explicit Rust specification.

The paper’s speed results are illustrative rather than a verification result. Table 5 reports three manually selected kernels translated by QiMeng-MuPa-r3 (Llama3-8B) at several matrix sizes; GEMM reaches 15,259× at size 2,048, while transpose is 0.88× at size 32 and 2,172.2× at size 8,192 (Table 5, Appendix C.3, pp.16–17). Inference: these are runtime ratios for selected examples, not accuracy denominators and not evidence that all translations are faster. Inference: VL should not redo generic compile filtering, finite-test comparison, wrapper generation, or mutual back-translation as standalone contributions; it should focus on connecting generated Rust to explicit Verus contracts and on checking assumptions around foreign code and harnesses.

techniques for the catalog

• execution-based co-verification — generate target code and tests, execute source and target, and retain a triplet only when all observed outputs agree

• mutual supervised co-evolution — train translator on accepted target→source pairs and tester on target→tests, then repeat filtering and training

• generated execution wrappers — expose C side effects and CUDA kernel launches through a common callable harness

• test validity and coverage feedback — classify compilation/runtime errors, compute VT and coverage, and use the signals to improve later rounds Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “To investigate whether the quality of tests generated by the Tester decreases during training, we analyzed the coverage of the training set in each round using the same method.”): checked every quotation, number, section/page reference, and technique step against the paper text; changed one misquote (“In Co-verify step”), many page/section references (Co-evolve and the training-set definition are p.5, the ablation is §4.4 p.9, Table 4 is p.15, Table 5 is p.17), the 29.44% attribution (from §1, not the abstract), the CUDA wrapper steps (LLM-written, no synchronization), the ablation description (unfiltered baselines first beat, then fall behind), the coverage metrics, and the Figure 16/18 descriptions, replaced the formula quote with a paraphrase, and marked my own conclusions “Inference:”; did not check figures against the PDF images, the cited works, or the Verus inferences.

Last edited: 2026-10-17