論文の概要: 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（参考訳）: 証明によるコンパイル:形式的意味論からの言語に依存しない自動最適化
• 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フレームワークの拡張として実装する。 オペコードレベルの最適化は、一貫したスピードアップを示し、プログラム全体のコンパイルは、桁違いのパフォーマンス向上を達成する。

関連論文リスト

• SEMBridge: Tagless-Final Program Semantics with Weakest-Precondition and Bounded-Checking Interpretations [0.8557392136621891]
  SEMBridgeは、同じ実行可能なオブジェクトプログラムから最も弱い条件と境界チェックの解釈を生成する。 Pythonプロトタイプは、割り当て、条件、仮定、アサーションを備えたループフリーな命令コアを実装している。
  論文  参考訳（メタデータ） (2026-05-29T18:00:06Z)
• Efficient Test-Time Inference via Deterministic Exploration of Truncated Decoding Trees [68.04613115686509]
  自己整合性は、複数の推論トレースを並列にサンプリングし、投票することで、推論時間のパフォーマンスを向上させる。 そこで本研究では,切り落された標本を伐採木として扱う決定論的復号法であるDLE(Distinct Leafion)を提案する。 DLEは高品質な推論トレースを調査し、数学、コーディング、一般的な推論タスクのパフォーマンスを向上させる。
  論文  参考訳（メタデータ） (2026-04-22T12:42:03Z)
• Superset Decompilation [7.989066784325648]
  decompilationはコンパイルの逆で、モジュラーパスのシーケンスとして構成できる。 我々はこれを、バイナリに関する事実を一元的にリレーショナルストアに導出するフレームワークである、証明誘導スーパーセットデコンパイル(PGSD)として定式化する。 Mandelは、宣言的なリバースエンジニアリングフレームワークとしてPGSDを実装しており、Linux ELFバイナリを35K行のRustとDatalogの粒度の中間表現を通じてC99に引き上げている。
  論文  参考訳（メタデータ） (2026-03-30T03:47:19Z)
• Conditional Execution of Transpiler Passes Based on Per-Script Feature Detection [0.0]
  本稿では,言語機能セットの正確な追跡と動的維持に基づいて,トランスパイラパスを条件付きで実行するコンパイラの改良を提案する。 大規模生産モノレポに対するこの改善の評価は、コンパイル時間とメモリ使用量を大幅に削減した。
  論文  参考訳（メタデータ） (2026-03-17T19:54:22Z)
• Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs [48.390500145598544]
  大型言語モデル (LLM) は形式定理の証明において大きな可能性を証明している。 我々は形式的検証において情報的構造を利用する: コンパイラが多様な証明の試みの広大な空間をマッピングする観察である。 我々は,この圧縮を利用して効率的な学習と証明探索を行う,学習と再定義のためのフレームワークを提案する。
  論文  参考訳（メタデータ） (2026-03-13T01:33:20Z)
• AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms [54.99368693313797]
  既存のベンチマークでは、個々の言語/ツールのみをテストするため、パフォーマンス番号は直接比較できない。 このギャップに対処するAlgoVeriは、Dafny、Verus、Leanで77ドルの古典的アルゴリズムのベリコーディングを評価するベンチマークです。
  論文  参考訳（メタデータ） (2026-02-10T06:58:26Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。 提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
  論文  参考訳（メタデータ） (2025-11-26T06:39:19Z)
• Understanding Accelerator Compilers via Performance Profiling [1.1841612917872066]
  アクセラレータ設計言語(ADL)は、ハードウェアユニットにコンパイルされるハイレベル言語である。 Petalは、コンパイラの判断がパフォーマンスにどのように影響するかを理解するための、サイクルレベルのツールです。 その結果,Petalのサイクルレベルのプロファイルは,既存の設計における性能問題を特定することができることがわかった。
  論文  参考訳（メタデータ） (2025-11-24T22:40:11Z)
• 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)
• COrAL: Order-Agnostic Language Modeling for Efficient Iterative Refinement [80.18490952057125]
  反復改良は、複雑なタスクにおける大規模言語モデル(LLM)の能力を高める効果的なパラダイムとして登場した。 我々はこれらの課題を克服するために、コンテキストワイズ順序非依存言語モデリング(COrAL)を提案する。 当社のアプローチでは、管理可能なコンテキストウィンドウ内で複数のトークン依存関係をモデル化しています。
  論文  参考訳（メタデータ） (2024-10-12T23:56:19Z)
• 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)

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

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