論文の概要: IRONPROOF: COBOL-to-Python Transpilation with SMT-Based Equivalence Checking
- arxiv url: http://arxiv.org/abs/2610.11073v1
- Date: Thu, 08 Oct 2026 01:31:58 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-10 02:36:53.726299
- Title: IRONPROOF: COBOL-to-Python Transpilation with SMT-Based Equivalence Checking
- Title（参考訳）: IRONPROOF: SMTに基づく等価チェックによるCOBOL-to-Pythonトランスパイレーション
- Abstract要約: 現代語への翻訳はプログラムの計算方法を変えることができ、LLM翻訳は等価性の保証を持たない。
我々は、中間表現に解析し、Pythonを生成し、共有入力上でZ3式としてエンコードし、マシンチェック可能な等価証明書(UNSAT)または逆例(SAT)を出力するIRONPROOFを提案する。
2,345ファイル(GnuCOBOLテスト、NIST CCVS85、オープンソースコレクション、私たちが生成または書き込んだプログラム)では、782がチェックパスに入る。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Translating COBOL to a modern language can change what a program computes, and LLM translations carry no guarantee of equivalence. We present IRONPROOF, which parses COBOL into an intermediate representation, generates Python, encodes both as Z3 formulas over shared inputs, and emits either a machine-checkable equivalence certificate (UNSAT) or a counterexample (SAT). On 2,345 COBOL files (GnuCOBOL tests, NIST CCVS85, open-source collections, and programs we generated or wrote), 782 enter the checking path: 606 (77.5%) are proved equivalent, 101 are partially verified, none is refuted, and 75 fail inside our pipeline and stay in the denominator. On independently authored programs the rate is 52.6% (153 of 291), against 92.3% on programs we wrote. Of the 153 independent proofs, 37 cover a single execution of a program that reads input the encoder does not model, and across all 606 proofs only 14 quantify over an input that a proved output depends on. On two public business-application corpora (AWS CardDemo and IBM GenApp), the encoder models no program end to end. An April 2026 LLM-only baseline failed on 54 of 94 independently authored programs, counting translations our encoder could not verify. PIC-bounded overflow detection flags an out-of-range output in 22.1% of the programs it can analyze, an upper bound. An earlier confrontation with GnuCOBOL 3.2.0 found 24 of 49 executable independent proofs disagreeing with the runtime on a variable in the proof's domain. A proof establishes that the generated Python computes what our intermediate representation says the COBOL computes, not equivalence to a COBOL implementation.
- Abstract（参考訳）: COBOLを現代言語に翻訳すると、プログラムが計算したものが変わり、LLM翻訳は等価性の保証を持たない。
我々は、COBOLを中間表現に解析し、Pythonを生成し、共有入力上でZ3式としてエンコードし、マシンチェック可能な等価証明書(UNSAT)または逆例(SAT)を出力するIRONPROOFを提案する。
2,345 COBOLファイル(GnuCOBOLテスト、NIST CCVS85、オープンソースコレクション、私たちが生成または書き込んだプログラム)では、782がチェックパスに入る。
独立した認可プログラムでは52.6%(153対291対291対92.3%)であり、私たちが書いたプログラムでは92.3%である。
153個の独立した証明のうち37は、エンコーダがモデル化していない入力を読み込むプログラムの単一の実行をカバーし、証明された出力が依存する入力について、すべての606個の証明のうち14個しか定量化できない。
2つのパブリックビジネスアプリケーションコーパス(AWS CardDemoとIBM GenApp)では、エンコーダはプログラムをエンドツーエンドにモデル化しない。
2026年4月、LLMのみのベースラインが94の独立したプログラムのうち54で失敗し、エンコーダが検証できない翻訳を数えた。
PICバウンドオーバーフロー検出フラグは、解析可能なプログラムの22.1%でアウト・オブ・レンジ出力をフラグする。
以前のGnuCOBOL 3.2.0との対立により、49の独立した証明のうち24が証明領域の変数のランタイムと矛盾していることが分かった。
証明は、生成したPythonが、中間表現がCOBOLが計算したものを計算し、COBOLの実装と等価ではないことを証明します。
関連論文リスト
- Agentic Method for Deterministic Validation of Legacy Code Migration [0.0]
ロックスミスループ」は2つの実行環境を準備することで開始される。
ロックスミスループ」は入力モック上でワイトネス検索を行い、プログラムの分岐を貫き、その後パリティ保存突然変異が続く。
Locksmithは、入力検索高原を超えて、継続的にカバレッジを改善した。
論文 参考訳（メタデータ） (2026-07-30T14:25:23Z) - SEDCoT: Enhancing LLM-Based COBOL Code Translation via Symbolic Execution and Delta Debugging [49.898541267264115]
古い技術や疎結合なドキュメンテーション、開発者の引退などによって、メンテナンスはますます難しくなっている。
従来のルールベースのトランスコンパイラは、読み書きが難しい出力を出力する。
本稿では,新しいC言語翻訳フレームワークであるSEDCoTを提案する。
論文 参考訳（メタデータ） (2026-07-05T03:07:10Z) - COBOL-Coder: Domain-Adapted Large Language Models for COBOL Code Generation and Translation [10.733306714499067]
既存の大規模言語モデル(LLM)は、コードを正しく生成し翻訳するのに苦労する。
本稿では,コンパイラ誘導型検証とマルチステージ類似度に基づくフィルタリングを組み合わせた自動データキュレーションパイプラインを提案する。
Code-Coderは最大73.95パーセントのコンパイル成功率と49.33のPass-1 onEvalを実現している。
論文 参考訳（メタデータ） (2026-04-05T06:12:49Z) - COBOLAssist: Analyzing and Fixing Compilation Errors for LLM-Powered COBOL Code Generation [10.733306714499067]
本稿では,コンパイルエラーの問題を考察し,これらの問題に対処するための大規模言語モデル(LLM)を利用したフレームワークを提案する。
まず、LLM生成コードの一般的なコンパイルエラーを、不完全なコードエラー、構文エラー、型関連エラーの3つのグループに分類する。
論文 参考訳（メタデータ） (2026-04-05T05:51:54Z) - A Multi-Language Object-Oriented Programming Benchmark for Large Language Models [61.267115598083315]
35の既存ベンチマークの調査では、3つの大きな不均衡が明らかになった。
85.7%は単一のプログラミング言語に重点を置いている。
94.3%は関数レベルまたはステートメントレベルのタスクのみを対象としている。
80%以上は平均10件未満のテストケースを含む。
論文 参考訳（メタデータ） (2025-09-30T11:30:08Z) - Automated Validation of COBOL to Java Transformation [5.162381960073761]
我々は,Javaの等価性と翻訳の妥当性を検証するためのフレームワークとツールを提案する。
問題が発生した場合のコード修正や,改善のためのAIモデルへのフィードバックの提供にも役立ちます。
論文 参考訳（メタデータ） (2025-04-14T06:13:32Z) - Automated Testing of COBOL to Java Transformation [5.395038658302793]
我々はIBM Watsonx Code Assistant for Z (WCA4Z) [5] のテストフレームワークを開発した。
私たちのフレームワークはシンボリックな実行を使用して、外部呼び出しをモックし、それらをJUnitテストに変換して、翻訳されたJavaでセマンティックな等価性を検証します。
論文 参考訳（メタデータ） (2025-04-14T04:53:30Z) - EquiBench: Benchmarking Large Language Models' Reasoning about Program Semantics via Equivalence Checking [58.15568681219339]
大規模言語モデル(LLM)を評価するための新しいベンチマークであるEquiBenchを紹介する。
このタスクは、プログラムのセマンティクスについて推論するモデルの能力を直接テストする。
19の最先端LCMを評価し、最も難しいカテゴリでは、最高の精度は63.8%と76.2%であり、50%のランダムベースラインよりわずかに高い。
論文 参考訳（メタデータ） (2025-02-18T02:54:25Z) - CRUXEval-X: A Benchmark for Multilingual Code Reasoning, Understanding and Execution [50.1875460416205]
CRUXEVAL-Xコード推論ベンチマークには19のプログラミング言語が含まれている。
各言語に対して少なくとも600人の被験者で構成され、合計19Kのコンテンツ一貫性テストがある。
Pythonでのみトレーニングされたモデルでさえ、他の言語で34.4%のPass@1を達成することができる。
論文 参考訳（メタデータ） (2024-08-23T11:43:00Z) - Natural Language to Code Translation with Execution [82.52142893010563]
実行結果-プログラム選択のための最小ベイズリスク復号化。
そこで本研究では,自然言語からコードへのタスクにおいて,事前訓練されたコードモデルの性能を向上することを示す。
論文 参考訳（メタデータ） (2022-04-25T06:06:08Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。