論文の概要: A Trust Ledger and an Execution Check for CPG-Based C-to-Lean 4 Autoformalization: Separating Declined from Silently Incorrect Translations
- arxiv url: http://arxiv.org/abs/2609.38237v1
- Date: Mon, 28 Sep 2026 23:26:12 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-01 18:57:26.413985
- Title: A Trust Ledger and an Execution Check for CPG-Based C-to-Lean 4 Autoformalization: Separating Declined from Silently Incorrect Translations
- Title（参考訳）: CPG-based C-to-Lean 4 AutoformalizationのためのTrust LedgerとExecution Check----------------------------------------------------------------------------------------------- ------------
- Abstract要約: ほとんどの自動形式化作業では、トランスレータが処理を拒んだコードと、トランスレータが誤って翻訳したコードという、2つの異なる障害モードを混同した単一の集合的成功率が報告されている。
我々は,Cソースを3階層の正当性(ホールフリー,コールクローズド,ダイナミックホールリスク)の下で,小さなLean4コアセマンティクスに変換する決定論的コードプロパティグラフ(CPG)ベースのエクスポート器を提案する。
- 参考スコア（独自算出の注目度）: 0.7239110701286596
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Verifying large C codebases requires translating them into formally checkable semantics, but most autoformalization work reports a single aggregate success rate that conflates two different failure modes: code the translator declined to handle and code the translator translated incorrectly. We present a deterministic code-property-graph (CPG)-based exporter that translates C source into a small Lean~4 core semantics under a three-tier correctness discipline: hole-free, call-closed, and dynamic-hole-risk, that keeps these modes distinct. Applied to a re-export of the SQLite source tree (8{,}602 functions, over 1.5~million AST nodes), the exporter translates 5{,}222 functions (60.7\%) hole-free, of which only 2{,}134 (24.8\%) are call-closed, a $2.4\times$ gap a single rate would hide. Both figures are reported in a full per-construct trust ledger rather than a single score. Our main contribution is methodological: a protocol for separating constructs that are fundamentally unresolvable by whole-program static analysis (such as public API boundaries) from constructs that only look that way. For example, we retracted our own ``impossible'' classification of function-pointer/vtable dispatch after tracing a concrete counterexample in the target codebase. Separately, a search for ``more holes closed'' surfaced a latent silent-wrong-answer bug: a translation that succeeded with an incorrect result rather than declining, a failure mode we argue is more dangerous than any hole, and one a hole-count-only evaluation would never surface.
- Abstract（参考訳）: 大規模なCコードベースの検証には、形式的にチェック可能なセマンティクスに変換する必要があるが、ほとんどの自動形式化作業では、2つの異なる障害モードを混同した単一の集合的成功率を報告している。
我々は、Cソースを3階層の正当性(ホールフリー、コールクローズド、ダイナミックホールリスク)の規律の下で、Cソースを小さなLean~4コアセマンティクスに変換する決定論的コードプロパティグラフ(CPG)ベースのエクスポート器を提案する。
SQLiteソースツリーの再エクスポート(8{,}602関数、1.5~mm ASTノード以上)では、5{,}222関数 (60.7\%) のホールフリーを変換し、2{,}134 (24.8\%) のみがコールクローズされ、1回のレートで2.4\times$ギャップが隠される。
どちらの数字も、単一のスコアではなく、構成単位の信頼台帳に報告されている。
私たちの主なコントリビューションは方法論的です – プログラミング言語全体の静的解析(パブリックAPI境界など)によって,基本的に解決不可能なコンストラクトを,そのようにしか見えないコンストラクトから分離するためのプロトコルです。
例えば、ターゲットコードベースで具体的な反例をトレースした後、関数ポインター/vtableディスパッチの ``impossible'' の独自の分類を削除しました。
第二に、'more hole closed''を検索すると、潜伏した無声で答えるバグが浮上した: 減少よりも間違った結果で成功した翻訳、私たちが主張する失敗モードは、どの穴よりも危険であり、ホール数のみの評価は決して現れない。
関連論文リスト
- Calibrating Interpretability Instruments Before Trusting Their Verdicts [1.0829694003408499]
Causal氏は、大きな言語モデル(LLM)の内部は測定にかかっていると主張している。
これらの測定は、エラーではなく可算数を返す特定の診断可能な方法で失敗する。
このノートは、拒絶と道徳的表現に関する因果的解釈可能性プログラムの6つの失敗を文書化している。
論文 参考訳（メタデータ） (2026-09-13T19:37:02Z) - Boundary-Mutation Testing for Pattern-Based Secret Detection: A Rule-Level Method and Cross-Scanner Evaluation [0.0]
パターンベースシークレットスキャナにおける境界突然変異試験
3つのスキャナー(43ルールのオープンソーススキャナ、Gitleaks 8.21.2、TruffleHog 3.82.13)がテストされている。
論文 参考訳（メタデータ） (2026-09-02T13:41:50Z) - IndicQE-APE: A Benchmark for Quality Estimation and Automatic Post-Editing for Indic Languages [77.88427845181154]
我々はWMT 2020-2024の共有タスクの系統を、英語のリソースを拡張してインディクシーに集約する:9つの方向対に対して126,754ドルのインスタンス。
セグメントレベルのQEでは,LSMが6つ,COMETが3つ,APEでは3つのシステムをベンチマークした。
論文 参考訳（メタデータ） (2026-08-17T09:50:52Z) - Fantastic Adaptive Taxonomies and How to Use Them [100.20614173157708]
AdaMASTは、実行トレースをコンパクトでエビデンスに基づく障害分類に変換する。
コードには手書きのコードはなく、人間による注釈もない。
エージェント・システム・サーチでは、失敗候補の分類コード診断が自由形式より優れている。
論文 参考訳（メタデータ） (2026-07-17T17:41:16Z) - ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers [77.95933562142014]
ITPEvalは、4つの主要なIPP間で自動形式証明翻訳を評価するための最初のベンチマークである。
itpevalは、状態が分離されたウォームバックエンドを備えた、統合されたマルチITP認証インフラストラクチャです。
論文 参考訳（メタデータ） (2026-07-07T22:05:55Z) - What Accuracy and Gradient Cosine Miss: Evaluating Feedback Alignment via Scale Stability, Reference Validity, and Depth Utility [48.10132234701036]
本稿では,3つのチェック(スケール安定性,参照妥当性,深度ユーティリティ)に基づく診断評価プロトコルを提案する。
複数のアーキテクチャや手法にまたがって、我々のプロトコルは広い校正マージンを持つ全ての障害を識別する。
論文 参考訳（メタデータ） (2026-06-19T06:04:17Z) - Hierarchical Certified Semantic Commitment for Byzantine-Resilient LLM-Agent Collaboration [30.310793549183117]
本稿では,BFTにインスパイアされたプロトコルH-CSC(Hierarchical Certified Semantic Commitment)を紹介する。
H-CSCはBFT対応バケット(0.31から2.04度)に低角偏差でコミットし、意図したようにBFTを超えるラウンド(n3f+1)の100%を中止する。
論文 参考訳（メタデータ） (2026-06-05T14:35:58Z) - Constraint-Guided Multi-Agent Decompilation for Executable Binary Recovery [47.704311990064554]
脱コンパイルは、セキュリティ分析、マルウェアのリバースエンジニアリング、レガシーソフトウェアメンテナンスに不可欠である。
マルチレベル制約誘導型デコンパイル(MCGD)により,デコンパイルされたコードを再実行可能なソースに変換するマルチエージェントフレームワークを提案する。
本フレームワークは,84～97%の再実行性を実現し,28～89ポイントのベースラインデコンパイラ出力を改善した。
論文 参考訳（メタデータ） (2026-04-27T01:28:11Z) - LLM-Driven Multi-step Translation from C to Rust using Static Analysis [27.122409727034192]
レガシー言語で書かれたソフトウェアをCからRustなどのモダン言語に翻訳することは、メモリ安全性を改善する上で大きなメリットがある。
LLM駆動型C-to-Rustゼロショット変換ツールであるSACTORを2段階の翻訳手法を用いて提案する。
SACTORは、既存の方法と比較して、より自然でRustに準拠した翻訳を生成する。
論文 参考訳（メタデータ） (2025-03-16T14:05:26Z) - LM-Critic: Language Models for Unsupervised Grammatical Error Correction [128.9174409251852]
文を文法的に判断する LM-Critic の定義において,事前訓練された言語モデル (LM) の活用法を示す。
このLM-Critic と BIFI と、ラベルなし文の集合を併用して、現実的な非文法的/文法的ペアをブートストラップし、修正子を訓練する。
論文 参考訳（メタデータ） (2021-09-14T17:06:43Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。