PaperlayerView exact revision on arXiv

Source-linked AI summary

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

arXiv:2610.22528v1cs.SE

TL;DR

LLM-driven Fortran-to-Python translation can be expensive to perform manually, and generated code may violate source semantics while corrections fail to persist. ForTress turns recurring decisions into executable rules and audits a subset with Lean; it achieved bitwise agreement across evaluated tests, high cross-software reuse, and lower LLM usage costs than direct translation.

  • Problem

    Manual modernization of mature scientific software is expensive, while LLM translations may violate source semantics and contextual corrections are not guaranteed to persist.

    Source: §1 · p. 1, §2 · p. 3

  • Method

    ForTress converts recurring translation decisions into executable rules for deterministic reuse and uses Lean to check semantic-preservation proofs and counterexample-based refutations.

    Source: §1 · p. 2

  • Results

    Across 17 benchmarks from 15 software, outputs were bitwise-identical to native Fortran on all evaluated tests; reuse exceeded 90% for 14 of 15 software, and LLM usage costs were 44.2% lower than direct translation.

    Source: §8 · p. 24

  • Takeaways & Limitations

    Audit proofs cover modeled instances satisfying their premises, while refutations identify modeled counterexamples and guide rule repair.

    Source: §1 · p. 2

    Bitwise agreement is limited to the recorded compiler, runtime, optimization, library, hardware, execution, and initialization configurations; formal results also depend on modeled semantics and their correspondence with production rules.

    Source: §6 · p. 22

Abstract

from arXiv · show

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.

1 Introduction

ForTress addresses semantic errors and unreliable persistence in LLM translations by turning recurring decisions into reusable executable rules and auditing a subset against mechanized semantics. Across scientific software benchmarks, the translated programs matched native Fortran bitwise under recorded configurations.

1 Introduction

  • LLM translations can pass regression tests while violating source semantics, and corrections recorded in context or skills are not guaranteed to persist.Execution-based validation establishes agreement only for the finite inputs tested.Source: §1 · pp. 1–2
  • ForTress converts recurring LLM translation decisions into executable rules for deterministic reuse and uses Lean to check preservation claims for a nontrivial subset.The proof attempts cover all source instances and inputs satisfying stated applicability conditions; failed attempts can prompt counterexample-guided refinement.Source: §1 · p. 2
  • 17 benchmarks across 15 software yielded Python outputs bitwise-identical to native Fortran on all evaluated tests under recorded execution and initialization configurations.The benchmarks reached 1,015 subprograms covering 105,631 lines of Fortran.Source: §1 · p. 2
  • 193 executable rules and 188 audit records accumulated; 121 records had checked soundness proofs, including 31 established after counterexample-guided refinement.The audit set also included 42 Lean modules.Source: §1 · p. 2
  • 14 of 15 software exceeded 90% reuse, and ForTress’s $960 LLM usage cost was 44.2% lower than the direct LLM baseline’s $1,721.The cost comparison includes additional assurance and determinism.Source: §1 · p. 2
  • Human experts review semantic fidelity and rule–obligation correspondence, while Lean’s kernel checks proofs and refutations under stated assumptions.The modeled definitions and preservation claims are initially generated with LLM assistance and are not trusted as generated.Source: §1 · pp. 2–3

2 Motivating Example

The ANINT example shows how a plausible Fortran-to-Python translation can diverge at halfway values, with consequences for scientific calculations. ForTress makes translation rules reusable and uses Lean audits to refute an incorrect rule and verify a repair against modeled semantics.

2 Motivating Example

  • ANINT rounds halfway cases away from zero, unlike Python’s np.round; in Quantum ESPRESSO, the divergence changed all three dipole components from −4 to 4.Ordinary inputs can agree, making the mismatch difficult to detect through testing.Source: §2 · p. 3
  • Documenting a corrected translation in context or a reusable skill does not enforce its consistent application across later translation sites.Context can be lost over long translation horizons, while stochastic generation provides no guarantee.Source: §2 · p. 3
  • Lean checks preservation obligations for modeled instances, while LLM-generated refutations identify counterexamples that can guide repair.A soundness obligation requires a source operation and its target helper to preserve the relation between already-related arguments and expressions.Source: §2 · pp. 4–5
  • ForTress dispatches a source construct to an executable target-language rule; for ANINT, the repaired helper truncates the input and adjusts away from zero when the fractional magnitude reaches one half.The original helper simply returns np.round(x).Source: §2 · pp. 4–5, Figure 2 · p. 4
  • At input 5/2, a Lean-checked refutation shows the original rule unsound: Fortran returns 3 while the modeled Python rounding returns 2.The Fortran and Python rounding semantics are defined independently.Source: §2 · p. 5
  • The repaired rounding core is equivalent to the modeled Fortran rounding semantics for every real input, not only the motivating example.Lean discharges the preservation obligation using an established equivalence lemma.Source: §2 · p. 5

3 ForTress Approach

ForTress converts recurring Fortran-to-Python decisions into reusable executable rules and combines execution testing with Lean-based auditing and human review. Its workflow feeds unsupported sites, test failures, and audit refutations back into rule and model refinement.

3 ForTress Approach

  • ForTress iteratively generates and revises executable rules, translates covered code deterministically, and feeds unsupported sites, test failures, and audit refutations back to the Rule-Generator.The Translator and Executor do not invoke LLMs.Source: §3 · pp. 5–6

3.1 Rule-Generator, Translator, and Executor

  • Rules pair a Fortran source pattern and applicability guard with a Python emission, and uncovered constructs are reported rather than translated speculatively.The guard limits the scope in which the emission is claimed to be correct.Source: §3.1 · pp. 6–7
  • The Executor uses differential and in-situ execution to compare translated Python with native Fortran, including intermediate traces and shared state.Unexercised routines and instrumentation sites are reported as uncovered, not passing.Source: §3.1 · p. 7

3.2 Auditor and Human-Expert

  • Audited guarantees cover only source-defined executions within the modeled fragments, and the current Lean semantics model arithmetic rather than exact IEEE 754 behavior.The preservation claim is forward, not a bidirectional equivalence between the full languages.Source: §3.2 · p. 8, Figure 4 · p. 8
  • The Auditor checks universally quantified preservation obligations in Lean, while experts review semantic fidelity and correspondence between obligations and production rules.A checked proof covers modeled instances satisfying the guard and premises; a checked counterexample can refute the claim.Source: §3.2 · pp. 7–9

3.3 Implementation

  • The prototype combines fparser and Lean 4 with Mathlib 4.34.0 and comprises approximately 50,000 lines of Python.The Auditor traces obligations to production rules and records proof status, assumptions, applicability conditions, and review examples.Source: §3.3 · p. 9

4 LLM-Generated Components in ForTress

ForTress combines reusable executable translation rules with a six-layer Lean proof library linking modeled source and target semantics to rule and whole-kernel preservation claims.

4.1 Executable Rule Library

  • The executable library contains 193 rules: 176 language or numerical transformations and 17 environment or extension-interface rules.Its largest category is precision and kind policy, followed by control flow and environment interfaces.Source: §4.1 · p. 9
  • Guarded emitters select translations by source facts; constant squares expand to multiplication, while runtime integer powers use a shared helper.The helper uses repeated squaring in gfortran’s multiplication order.Source: §4.1 · p. 10

4.2 Semantic Models and Proof Library

  • The proof library has 42 modules and 190 theorem declarations, which do not correspond one-to-one with executable rules or audit records.A guarded rule may need separate audit records, while a record may cover an emitter and helpers.Source: §4.2 · p. 11
  • Six layers build from separate language evaluators and execution models to cross-language relations over scalar values, arrays, and program states.Array relations account for shape, elements, and rebased indices.Source: §4.2 · pp. 11–13
  • Layer IV proves local rule-family contracts, while structural recursion composes those contracts for supported expressions.The integer-power proof covers defined cases for real bases and integer exponents.Source: §4.2 · p. 14
  • The statement theorem composes seven statement families into a forward simulation of terminating executions for the supported fragment.For SAXPY, the whole-kernel theorem covers every defined terminating execution admitted by the modeled semantics, under its stated premises.Source: §4.2 · pp. 14–15

5 Evaluation

Across 17 benchmarks from 15 scientific software systems, the evaluation examines translation effectiveness, rule assurance, and cross-software reuse. ForTress matches native Fortran on evaluated tests, its audits check many rule-preservation claims, and its reusable rules lower LLM cost.

5.1 Benchmarks and Research Questions

  • The evaluation uses purposively selected benchmarks with compilable Fortran sources and native drivers across diverse scientific domains, and frames questions around translation, assurance, and reuse.It covers 17 benchmarks from 15 software systems.Source: §5.1 · pp. 15–16

5.2 RQ1. Real-world Translation Effectiveness

  • Six reached routines were not translated because of data-transfer or application-state constraints, so ForTress retained their Fortran implementations and called them through f2py wrappers.The cases involve arrays of records, direct-access I/O on a connected unit, and nested records with private module state.Source: §5.2 · p. 16
  • ForTress achieved bitwise-identical results on evaluated tests, while direct LLM translation had seven failing routine calls and two benchmarks without reliable numerical agreement.ForTress translated 1,015 of 1,021 reached subprograms (99.4%); six routines remained in Fortran and were invoked through f2py wrappers.Source: §5.2 · pp. 16–17, Table 3 · p. 17

5.3 RQ2. Rule Assurance

  • Of 188 audit records, 121 (64.4%) have checked soundness proofs, including 31 after counterexample-guided refinement; 25 require extensions or contracts, and 42 remain unfinished.The 121 proofs include 80 under stated assumptions and 41 under additional applicability premises.Source: §5.3 · p. 18
  • For negative integer exponents, a counterexample exposed divergent Fortran and Python behavior, and Lean proved a repaired translation sound under operand-type and value-preservation premises.The repair uses _f_ipow to preserve Fortran integer exponentiation before conversion to real.Source: §5.3 · pp. 18–19

5.4 RQ3. Rule Reusability

  • By the final donor-pool column, 14 of 15 software exceed 90% rule reuse and six reach 100%; COSP2 is the exception, ending at 89%.Reuse is measured against each test software’s observed rule types, not all 193 executable rules.Source: Figure 9 · p. 20, §5.4 · p. 20
  • ForTress cost $960 versus Direct LLM’s $1,721, 44.2% less, despite more request rounds; rule-based settings also use fewer expensive output and cache-write tokens.The cost comparison includes the shared preparation cost in each setting.Source: Figure 10 · p. 21, §5.4 · pp. 21–22

6 Threats to Validity

The reported evidence is bounded by evaluated branches, trajectories, constructs, software, execution configurations, and the modeled semantics; it does not establish generality beyond those conditions.

6 Threats to Validity

  • Results may not generalize to unexecuted branches, longer trajectories, or other language constructs; all evaluated systems supplied development examples.These examples limit conclusions about transfer to unseen software.Source: §6 · p. 22
  • The current rule library has no characterized upper bound on coverage or completeness guarantee, and six routines remained in Fortran due to data-transfer and application-state access limits.Planned runtime and interface templates remain unevaluated for effectiveness and generality.Source: §6 · p. 22
  • Bitwise agreement is limited to tested behaviors under recorded configurations, while formal results depend on modeled semantics and their correspondence with production rules.Configuration changes require renewed numerical validation; exact-arithmetic proofs alone do not establish IEEE floating-point equivalence.Source: §6 · p. 22

7 Related Work

Prior work addresses LLM translation, verified compilation and rewrites, and translation validation. ForTress instead audits reusable production translation rules through reviewed semantic obligations and Lean-checked proofs or refutations.

LLM-driven code translation

  • Prior LLM systems target translation coverage, generation quality, or validation of individual programs, while ForTress distills recurring transformations into executable rules.The cited approaches include neural translation, bug analysis, counterexample-guided repair, and repository-level translation.Source: §7 · p. 22

Verified compilation and verified rewrite rules

  • CompCert, XCert, Pyrosome [Jamner et al. 2025], and Alive establish or reuse correctness guarantees for compilers and rewrite rules.Alive can prove rules or produce counterexamples; ForTress keeps its audited rules as production Python translation logic rather than requiring a verified translator framework.Source: §7 · pp. 22–23

Translation validation and equivalence checking

  • Translation validation checks consistency for a particular source-to-target translation, with systems extending comparisons across differing control structures and down to machine code.The section notes that correctness of an idealized translation does not by itself establish correctness of its implementation.Source: §7 · p. 23

ForTress's distinction

  • ForTress audits reusable rules universally over modeled instances satisfying their premises; proofs establish preservation and refutations identify counterexamples.Applying either result to production depends on human-reviewed correspondence between language behavior, mechanized semantics, executable rules, and obligations.Source: §7 · p. 23

8 Conclusion

ForTress turns recurring LLM transformations into executable rules and uses Lean proofs to provide assurance and feedback. Across 17 benchmarks from 15 scientific software systems, it achieved bitwise agreement under recorded configurations, high cross-software reuse, and lower LLM usage costs.

8 Conclusion

  • ForTress converts recurring LLM-generated transformations into executable rules for deterministic reuse and adds Lean proofs as assurance and feedback.The approach's audit records cover a subset of rules.Source: §8 · pp. 23–24
  • Across 17 benchmarks from 15 systems, Python achieved bitwise agreement under recorded configurations; reuse exceeded 90% for 14/15, and LLM costs were 44.2% lower.The evaluation accumulated 193 executable rules and 188 audit records, including 121 checked soundness proofs and 31 established after counterexample-guided refinement.Source: §8 · p. 24

A Executable Rule Categories

The appendix groups registered executable rule definitions into categories.

A Executable Rule Categories

  • The registry contains 193 executable rule definitions across 29 categories, with the 18 smaller categories combined in the final entry.Source: Table A.1 · p. 28

B Lean Proof Categories

Table B.1 groups representative Lean proof declarations into preservation theorems, results requiring additional premises, and checked refutations.

B Lean Proof Categories

C Single-source Rule Coverage

Figure C.1 reports directional single-source coverage of observed translation-rule types across 15 software systems; self-comparisons are excluded.

C Single-source Rule Coverage

D Frequently Reused Translation Rules

Table D.1 lists per-software event counts for the ten most frequently observed registered translation rules, ordered by total frequency.

D Frequently Reused Translation Rules

  • The table covers the ten most frequently observed registered translation rules, ranked by total frequency.Source: Table D.1 · p. 29
  • Counts include rewritten, discarded, and rollback-marked emissions.CAM-SIMA combines its three cases, counting shared events once.Source: Table D.1 · p. 29
  • A zero indicates no captured matching event.Source: Table D.1 · p. 29
Loading 2610.22528v1…