Alvin Cheung and Sanjit A. Seshia

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2025-174

October 3, 2025

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2025/EECS-2025-174.pdf

Recent advances in large language models (LLMs) have achieved impressive performance on source-to-source code translation benchmarks, with potential applications ranging from enterprise code migration to safety-critical software modernization. Yet today’s evaluations remain shallow: test suites, syntactic matches, and heuristic similarity metrics conflate superficial success with true reliability. This gap is critical in high-assurance domains, where subtle errors can compromise security, safety, or maintainability. In this position paper, we argue that correctness, not just plausibility, must become the governing principle of LLM-based code translation. Specifically, we argue that principled definitions of correctness, grounded in formal methods and enforced through compositional reasoning, are essential for trustworthy code translation. We propose a layered view of correctness, encompassing top-level functional equivalence, internal contracts and invariants, and non-functional properties such as memory safety and timing guarantees. We highlight why LLMs alone cannot satisfy these obligations, and advocate for hybrid workflows where formal reasoning tools constrain, guide, and certify translation both during and after generation, which, we believe, offers a scalable path forward to translating realistic code bases. By embracing compositional specification, translation, and verification, we can turn LLMs from statistical translators into reliable collaborators. Finally, we outline the key open challenges, including cross-language reasoning, specification extraction, and correctness beyond functional equivalence, that must be solved to realize this vision.

---

BibTeX citation:

@techreport{Cheung:EECS-2025-174,
    Author= {Cheung, Alvin and Seshia, Sanjit A.},
    Title= {LLM-Based Code Translation Needs Formal Compositional Reasoning},
    Year= {2025},
    Month= {Oct},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2025/EECS-2025-174.html},
    Number= {UCB/EECS-2025-174},
    Abstract= {Recent advances in large language models (LLMs) have achieved impressive performance on source-to-source code translation benchmarks, with potential applications ranging from enterprise code migration to safety-critical software modernization. Yet today’s evaluations remain shallow: test suites, syntactic matches, and heuristic similarity metrics conflate superficial success with true reliability. This gap is critical in high-assurance domains, where subtle errors can compromise security, safety, or maintainability. In this position paper, we argue that correctness, not just plausibility, must become the governing principle of LLM-based code translation. Specifically, we argue that principled definitions of correctness, grounded in formal methods and enforced through compositional reasoning, are essential for trustworthy code translation. We propose a layered view of correctness, encompassing top-level functional equivalence, internal contracts and invariants, and non-functional properties such as memory safety and timing guarantees. We highlight why LLMs alone cannot satisfy these obligations, and advocate for hybrid workflows where formal reasoning tools constrain, guide, and certify translation both during and after generation, which, we believe, offers a scalable path forward to translating realistic code bases. By embracing compositional specification, translation, and verification, we can turn LLMs from statistical translators into reliable collaborators. Finally, we outline the key open challenges, including cross-language reasoning, specification extraction, and correctness beyond functional equivalence, that must be solved to realize this vision.},
}

EndNote citation:

%0 Report
%A Cheung, Alvin 
%A Seshia, Sanjit A. 
%T LLM-Based Code Translation Needs Formal Compositional Reasoning
%I EECS Department, University of California, Berkeley
%D 2025
%8 October 3
%@ UCB/EECS-2025-174
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2025/EECS-2025-174.html
%F Cheung:EECS-2025-174