ForTress: Bringing Assurance and Determinism for LLM-Driven Fortran-to-Python Translation
Qinrun Dai, Ruitong Liu, Chien-Wei Huang, Guanhong Tao, Guannan Wei, Yueqi Chen
cs.SE
Oct 15, 2026 · v1
TL;DR
Mechanizes Fortran and Python semantics in Lean and kernel-checks LLM-generated soundness proofs and refutations for Fortran-to-Python translation rules.
Abstract
Modernizing mature scientific software from Fortran to Python can improve accessibility and integration with modern computing tools, but manual rewriting is expensive. Large language models (LLMs) make translation more practical, yet generated code can pass regression tests while violating source-language semantics, and contextual corrections may not persist across subsequent translations. We present ForTress, which solidifies recurring LLM translation decisions into guarded executable rules for deterministic reuse and provides semantic assurance for a non-trivial subset of these rules. Its LLM-assisted auditing process expresses universally quantified preservation obligations over mechanized Fortran and Python semantics in Lean. Human experts review semantic fidelity and correspondence with production rules, and Lean's kernel checks proofs and refutations under explicit assumptions. These audit records expose the conditions either supporting correctness or identifying failure cases. We evaluate ForTress on 17 benchmarks from 15 scientific software spanning diverse domains. The translated programs achieve bitwise-identical with native Fortran on all evaluated tests under the recorded execution and initialization configurations. Against these software, ForTress accumulates 193 executable rules and 188 audit records, of which 121 have checked soundness proofs, including 31 established after counterexample-guided refinement. Cross-software reuse exceeds 90% for 14 of the 15 software. Even with additional assurance and determinism, the LLM usage cost is 44.2% lower than direct LLM translation.
Problem
LLM-driven Fortran-to-Python translation can pass regression tests while violating source semantics, for example ANINT versus np.round on tie values. Corrections recorded in context or as skills are not reliably reused in later translations.
Approach
ForTress turns recurring LLM translation decisions into guarded executable rules that a deterministic translator applies, with differential execution against native Fortran. An LLM-assisted auditor states universally quantified semantic-preservation obligations over Fortran and Python semantics mechanized in Lean, then proposes proofs or counterexample refutations. Lean's kernel checks these, and human experts review model fidelity and how well each obligation matches its rule. Refutations and counterexamples feed back into rule refinement.
Results
Across 17 benchmarks from 15 scientific codes, the translated Python is bitwise identical to native Fortran on all evaluated tests under the recorded configurations. ForTress accumulated 193 rules, 42 Lean modules and 188 audit records; 121 records have checked soundness proofs, 31 of them obtained after counterexample-guided refinement. Cross-software rule reuse exceeds 90% for 14 of the 15 codes, and LLM cost is 44.2% lower than direct LLM translation.
