論文の概要: Compiling by Proving: Language-Agnostic Automatic Optimization from Formal Semantics

• arxiv url: http://arxiv.org/abs/2509.21793v1
• Date: Fri, 26 Sep 2025 02:49:08 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-29 20:57:54.14095
• Title: Compiling by Proving: Language-Agnostic Automatic Optimization from Formal Semantics
• Title（参考訳）: 証明によるコンパイル:形式的意味論からの言語に依存しない自動最適化
• Authors: Jianhong Zhao, Everett Hildenbrandt, Juan Conejero, Yongwang Zhao,
• Abstract要約: シンボル実行とグラフ構造のコンパイルにより全パス到達可能性証明を構築する。 我々は、多くの意味的な書き直しを単一のルールに集約し、建設による正確性を維持します。 我々はこれを言語に依存しないKフレームワークの拡張として実装する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Verification proofs encode complete program behavior, yet we discard them after checking correctness. We present compiling by proving, a paradigm that transforms these proofs into optimized execution rules. By constructing All-Path Reachability Proofs through symbolic execution and compiling their graph structure, we consolidate many semantic rewrites into single rules while preserving correctness by construction. We implement this as a language-agnostic extension to the K framework. Evaluation demonstrates performance improvements across different compilation scopes: opcode-level optimizations show consistent speedups, while whole-program compilation achieves orders of magnitude greater performance gains.
• Abstract（参考訳）: 検証証明は完全なプログラム動作を符号化するが、正当性を確認した後に破棄する。 我々はこれらの証明を最適化された実行規則に変換するパラダイムである証明によるコンパイルを提案する。 シンボリックな実行を通じて全パス到達可能性証明を構築し,そのグラフ構造をコンパイルすることにより,構成による正確性を維持しつつ,多くの意味的書き直しを単一ルールに集約する。 我々はこれを言語に依存しないKフレームワークの拡張として実装する。 オペコードレベルの最適化は、一貫したスピードアップを示し、プログラム全体のコンパイルは、桁違いのパフォーマンス向上を達成する。

関連論文リスト

• Correctness-Guaranteed Code Generation via Constrained Decoding [11.531496728670746]
  本稿では,意味論的に正しいプログラムを生成するための制約付き実行時復号アルゴリズムを提案する。 提案手法は,任意の所定のスクリプティングAPIに従って,意味的に正しいプログラムを生成することができることを示す。 さらに、慎重に設計することで、我々のセマンティック保証が正当性にまで拡張され、ローグライクなビデオゲームにゲームメカニクスを発生させることで検証されることを示す。
  論文  参考訳（メタデータ） (2025-08-20T20:48:18Z)
• Fun with flags: How Compilers Break and Fix Constant-Time Code [0.0]
  コンパイラの最適化が定数時間コードをどのように壊すかを分析する。 キーとなる洞察は、パスの小さなセットが、ほとんどのリークの根元にあるということだ。 ソースコードの変更やカスタムコンパイラを必要としない,オリジナルかつ実践的な緩和を提案する。
  論文  参考訳（メタデータ） (2025-07-08T15:52:17Z)
• Valida ISA Spec, version 1.0: A zk-Optimized Instruction Set Architecture [2.0790368408580138]
  Valida命令セットアーキテクチャはzkVMの実装のために設計されており、高速で効率的な実行証明のために最適化されている。 この仕様は、Valida用のzkVMとコンパイラツールチェーンの実装をガイドすることを目的としている。
  論文  参考訳（メタデータ） (2025-05-12T23:03:02Z)
• Compiler Optimization Testing Based on Optimization-Guided Equivalence Transformations [3.2987550056134873]
  本稿では,コンパイラ最適化にインスパイアされたメタモルフィックテスト手法を提案する。 提案手法ではまず,最適化条件を満たす入力プログラムを生成するために,最適化されたコード構築戦略を用いる。 事前変換プログラムと後変換プログラムの出力を比較することで、不正な最適化バグを効果的に識別する。
  論文  参考訳（メタデータ） (2025-04-06T01:37:57Z)
• Self-Constructed Context Decompilation with Fined-grained Alignment Enhancement [43.2637367483626]
  逆コンパイルは、ソースコードが利用できない場合、コンパイルされたコードをハイレベルなプログラミング言語に変換する。 これまでの研究は主に、モデルパラメータのスケールや事前トレーニングのためのトレーニングデータを増やすことで、デコンパイル性能の向上に重点を置いてきた。 これら2つの手法を統合することで、Decompile-Evalベンチマークで約3.90%の再実行可能性向上を実現し、新しい最先端性能52.41%を確立した。
  論文  参考訳（メタデータ） (2024-06-25T02:37:53Z)
• Contrastive Instruction Tuning [61.97704869248903]
  意味論的に等価な命令-インスタンスペア間の類似性を最大化するために、コントラスト命令チューニングを提案する。 PromptBenchベンチマークの実験によると、CoINはLLMの頑健さを一貫して改善し、文字、単語、文、意味のレベルを平均して2.5%の精度で変化させる。
  論文  参考訳（メタデータ） (2024-02-17T00:09:32Z)
• Performance Embeddings: A Similarity-based Approach to Automatic Performance Optimization [71.69092462147292]
  パフォーマンス埋め込みは、アプリケーション間でパフォーマンスチューニングの知識伝達を可能にする。 本研究では, 深層ニューラルネットワーク, 密度およびスパース線形代数合成, および数値風速予測ステンシルのケーススタディにおいて, この伝達チューニング手法を実証する。
  論文  参考訳（メタデータ） (2023-03-14T15:51:35Z)
• Learning Performance-Improving Code Edits [107.21538852090208]
  本稿では,大規模言語モデル(LLM)を高レベルプログラム最適化に適用するためのフレームワークを提案する。 まず、競争力のある77,000以上のC++プログラミングサブミッションペアによる、人間のプログラマによるパフォーマンス改善編集のデータセットをキュレートする。 提案手法は,検索をベースとした少数ショットプロンプトとチェーン・オブ・シンクレットを提案し,その微調整には,自己再生に基づく性能条件付き生成と合成データ拡張が含まれる。
  論文  参考訳（メタデータ） (2023-02-15T18:59:21Z)
• ReACC: A Retrieval-Augmented Code Completion Framework [53.49707123661763]
  本稿では,語彙のコピーと類似したセマンティクスを持つコード参照の両方を検索により活用する検索拡張コード補完フレームワークを提案する。 我々は,Python および Java プログラミング言語のコード補完タスクにおけるアプローチを評価し,CodeXGLUE ベンチマークで最先端のパフォーマンスを実現する。
  論文  参考訳（メタデータ） (2022-03-15T08:25:08Z)

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

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