論文の概要: ForTress: Bringing Assurance and Determinism for LLM-Driven Fortran-to-Python Translation

• arxiv url: http://arxiv.org/abs/2610.22528v1
• Date: Thu, 15 Oct 2026 18:22:13 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-20 00:56:07.622705
• Title: ForTress: Bringing Assurance and Determinism for LLM-Driven Fortran-to-Python Translation
• Title（参考訳）: ForTress: LLM駆動のFortran-to-Python翻訳のための保証と決定性を実現する
• Abstract要約: 大規模な言語モデル(LLM)は、翻訳をより実用的なものにするが、生成されたコードは、ソースコードのセマンティクスに違反しながら回帰テストをパスすることができる。 本稿では,再帰的なLLM翻訳決定を,決定論的再利用のためのガード付き実行ルールに統一するForTressを提案する。
• 参考スコア（独自算出の注目度）: 8.557167755493085
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.
• Abstract（参考訳）: FortranからPythonへの成熟した科学ソフトウェアの近代化は、アクセシビリティを改善し、現代のコンピューティングツールとの統合を可能にするが、手書きの書き直しは高価である。 大規模な言語モデル(LLM)は、翻訳をより実用的なものにするが、生成されたコードは、ソースコードのセマンティクスに違反しながら回帰テストをパスすることができる。 本稿では,LLM翻訳の繰り返し決定を決定論的再利用のためのガード付き実行ルールに統一し,これらのルールの非自明なサブセットに対するセマンティックアシュアランスを提供するForTressを提案する。 LLMによる監査プロセスは、リーンにおける機械化されたFortranとPythonのセマンティクスに対する普遍的に定量化された保存義務を表現している。 人間の専門家は、セマンティックな忠実さと生産ルールとの対応をレビューし、Leanのカーネルは明示的な前提の下で証明と反証をチェックします。 これらの監査記録は、正確性をサポートするか、障害ケースを特定するかのいずれかの条件を公開する。 さまざまな領域にまたがる15の科学ソフトウェアから17のベンチマークでForTressを評価した。 翻訳されたプログラムは、記録された実行および初期化設定の下で評価された全てのテストにおいて、ネイティブのFortranとビットワイズIDを得る。 これらのソフトウェアに対して、ForTressは193の実行可能なルールと188の監査記録を蓄積し、そのうち121は検査された音質証明を持っている。 ソフトウェア間の再利用は15ソフトウェア中14ソフトウェアで90%以上である。 追加の保証と決定性があるにもかかわらず、LLMの使用コストは直接のLLM翻訳よりも44.2%低い。

関連論文リスト

• Faithful Autoformalization of Natural Language Assertions [2.8921494813790094]
  Monty: アサーションのための自動形式化フレームワークを紹介します。 本手法は,新しい適合度測定値を用いたフィルタリング形式化に基づく。 提案手法は,LLMを用いてアサーションの翻訳を行う場合よりも,基礎的真理を確実に生成することを示す。
  論文  参考訳（メタデータ） (2026-07-14T22:12:14Z)
• Kaizen: Metamorphic Fuzzing and Differential Testing for LLM-Translated HPC Applications [2.4948485991003158]
  本稿では,OpenMP,OpenACC,Kokkos,SYCLに翻訳された大規模言語モデル(LLM)の正確性を評価するためのフレームワークを提案する。 カーネルレベルおよびフルプログラム粒度で3つの微調整LDMを用いて、16の科学応用のオン・トゥ・オープンMP翻訳を評価する。
  論文  参考訳（メタデータ） (2026-07-04T23:52:39Z)
• IFEvalCode: Controlled Code Generation [69.28317223249358]
  本稿では,Code LLMの命令追従能力を改善するために,前方および後方制約生成を提案する。 IFEvalCodeは、7つのプログラミング言語の1.6Kテストサンプルからなる多言語ベンチマークである。
  論文  参考訳（メタデータ） (2025-07-30T08:08:48Z)
• D-LiFT: Improving LLM-based Decompiler Backend via Code Quality-driven Fine-tuning [49.16469288280772]
  逆コンパイラは、バイナリから可読なソースコードを再構築する。 近年の進歩にもかかわらず、そのアウトプットは構文上の誤りや意味的な誤りに悩まされ、読みにくいままである。 大規模言語モデル (LLMs) の出現により、研究者は逆コンパイラ出力を洗練するためのLLMの可能性を探り始めた。 D-LIFTは、微調整強化学習を施した拡張逆コンパイラLLMパイプラインである。
  論文  参考訳（メタデータ） (2025-06-11T19:09:08Z)
• Enhancing LLMs in Long Code Translation through Instrumentation and Program State Alignment [0.0]
  コード翻訳は、機能を保ちながらプログラミング言語間でコードを変換することを目的としている。 大規模言語モデル(LLM)の最近の進歩はコード翻訳を改善しているが、課題は残る。
  論文  参考訳（メタデータ） (2025-04-02T13:55:29Z)
• ExeCoder: Empowering Large Language Models with Executability Representation for Code Translation [57.604506522287814]
  既存の大きな言語モデル(LLM)は、事前トレーニング中にのみコードのコンテキスト意味を学習する。 機能的セマンティクスや構文構造,変数依存性といった実行可能性表現を活用するために,ExeCoderを提案する。 ExeCoderは、既存のオープンソースコードLLMを10.88%以上、38.78%以上、27.44%以上、42.97%以上という、2つのメトリクスで、最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2025-01-30T16:18:52Z)
• Exploring and Unleashing the Power of Large Language Models in Automated Code Translation [40.25727029618665]
  本稿では,自動翻訳タスクのための多種多様なLLMと学習ベーストランスパイラについて検討する。 UniTrans は、様々な LLM に適用可能な統一コード翻訳フレームワークである。 最近の3つのLLMはUniTransでテストされており、いずれも大幅に改善されている。
  論文  参考訳（メタデータ） (2024-04-23T00:49:46Z)
• Assessing the Latent Automated Program Repair Capabilities of Large Language Models using Round-Trip Translation [44.3761164214368]
  RTT(Round-Trip Translation): あるプログラミング言語から別のプログラミング言語や自然言語にコードを翻訳する。 JavaにおけるRTT生成パッチの詳細な量的および定性的な分析を行う。 RTTはHumanEval-JavaベンチマークでGPT-4を用いた164のバグのうち100件に対して可塑性パッチを生成し,97件を手作業で評価した。
  論文  参考訳（メタデータ） (2024-01-15T22:36:31Z)
• LEVER: Learning to Verify Language-to-Code Generation with Execution [64.36459105535]
  本稿では,プログラムの実行結果の検証を学習することで,言語からコードへの生成を改善するシンプルな手法であるLEVERを提案する。 具体的には、LLMからサンプリングされたプログラムが、自然言語入力、プログラム自体とその実行結果に基づいて正しいか否かを判定するために、検証者を訓練する。 LEVER はベースコード LLMs (4.6% から 10.9% まで) を継続的に改善し、それらすべてに対して新しい最先端の結果を得る。
  論文  参考訳（メタデータ） (2023-02-16T18:23:22Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。