Compiling by Proving: Language-Agnostic Automatic Optimization from Formal Semantics

• URL: http://arxiv.org/abs/2509.21793v1
• Date: Fri, 26 Sep 2025 02:49:08 GMT
• Title: Compiling by Proving: Language-Agnostic Automatic Optimization from Formal Semantics
• Authors: Jianhong Zhao, Everett Hildenbrandt, Juan Conejero, Yongwang Zhao,
• Abstract summary: We construct All-Path Reachability Proofs through symbolic execution and compiling their graph structure.<n>We consolidate many semantic rewrites into single rules while preserving correctness by construction.<n>We implement this as a language-agnostic extension to the K framework.
• Score: 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.

Related papers

• AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms [54.99368693313797]
  Existing benchmarks test only individual languages/tools, so the performance numbers are not directly comparable.<n>We address this gap with AlgoVeri, a benchmark that evaluates vericoding of $77$ classical algorithms in Dafny, Verus, and Lean.
  arXiv  Detail & Related papers  (2026-02-10T06:58:26Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGE decomposes verification into three interconnected domains: Code, Specifications, and Proofs.<n>We show that this approach substantially improves both accuracy and efficiency beyond standard error feedback methods.
  arXiv  Detail & Related papers  (2025-11-26T06:39:19Z)
• Understanding Accelerator Compilers via Performance Profiling [1.1841612917872066]
  Accelerator design languages (ADLs) are high-level languages that compile to hardware units.<n>We introduce Petal, a cycle-level tool for understanding how the compiler's decisions affect performance.<n>We show that Petal's cycle-level profiles can identify performance problems in existing designs.
  arXiv  Detail & Related papers  (2025-11-24T22:40:11Z)
• Correctness-Guaranteed Code Generation via Constrained Decoding [11.531496728670746]
  We present a constrained runtime decoding algorithm for generating semantically correct programs.<n>We show that our method can generate semantically correct programs conforming to any prescribed scripting API.<n>We further show that, with careful design, our semantic guarantees extend to correctness, as validated in the application of generating game mechanics for a roguelike video game.
  arXiv  Detail & Related papers  (2025-08-20T20:48:18Z)
• Fun with flags: How Compilers Break and Fix Constant-Time Code [0.0]
  We analyze how compiler optimizations break constant-time code.<n>Key insight is that a small set of passes are at the root of most leaks.<n>We propose an original and practical mitigation that requires no source code modification or custom compiler.
  arXiv  Detail & Related papers  (2025-07-08T15:52:17Z)
• Valida ISA Spec, version 1.0: A zk-Optimized Instruction Set Architecture [2.0790368408580138]
  The Valida instruction set architecture is designed for implementation in zkVMs to optimize for fast, efficient execution proving.<n>This specification intends to guide implementors of zkVMs and compiler toolchains for Valida.
  arXiv  Detail & Related papers  (2025-05-12T23:03:02Z)
• Compiler Optimization Testing Based on Optimization-Guided Equivalence Transformations [3.2987550056134873]
  We propose a metamorphic testing approach inspired by compiler optimizations.<n>Our approach first employs tailored code construction strategies to generate input programs that satisfy optimization conditions.<n>By comparing the outputs of pre- and post-transformation programs, this approach effectively identifies incorrect optimization bugs.
  arXiv  Detail & Related papers  (2025-04-06T01:37:57Z)
• COrAL: Order-Agnostic Language Modeling for Efficient Iterative Refinement [80.18490952057125]
  Iterative refinement has emerged as an effective paradigm for enhancing the capabilities of large language models (LLMs) on complex tasks. We propose Context-Wise Order-Agnostic Language Modeling (COrAL) to overcome these challenges. Our approach models multiple token dependencies within manageable context windows, enabling the model to perform iterative refinement internally.
  arXiv  Detail & Related papers  (2024-10-12T23:56:19Z)
• Self-Constructed Context Decompilation with Fined-grained Alignment Enhancement [43.2637367483626]
  Decompilation transforms compiled code back into a high-level programming language when source code is unavailable. Previous work has primarily focused on enhancing decompilation performance by increasing the scale of model parameters or training data for pre-training. By integrating these two methods, we achieved a Re-Executability performance improvement of approximately 3.90% on the Decompile-Eval benchmark, establishing a new state-of-the-art performance of 52.41%.
  arXiv  Detail & Related papers  (2024-06-25T02:37:53Z)
• Contrastive Instruction Tuning [61.97704869248903]
  We propose Contrastive Instruction Tuning to maximize the similarity between semantically equivalent instruction-instance pairs. Experiments on the PromptBench benchmark show that CoIN consistently improves LLMs' robustness to unseen instructions with variations across character, word, sentence, and semantic levels by an average of +2.5% in accuracy.
  arXiv  Detail & Related papers  (2024-02-17T00:09:32Z)
• Performance Embeddings: A Similarity-based Approach to Automatic Performance Optimization [71.69092462147292]
  Performance embeddings enable knowledge transfer of performance tuning between applications. We demonstrate this transfer tuning approach on case studies in deep neural networks, dense and sparse linear algebra compositions, and numerical weather prediction stencils.
  arXiv  Detail & Related papers  (2023-03-14T15:51:35Z)
• Learning Performance-Improving Code Edits [107.21538852090208]
  We introduce a framework for adapting large language models (LLMs) to high-level program optimization. First, we curate a dataset of performance-improving edits made by human programmers of over 77,000 competitive C++ programming submission pairs. For prompting, we propose retrieval-based few-shot prompting and chain-of-thought, and for finetuning, these include performance-conditioned generation and synthetic data augmentation based on self-play.
  arXiv  Detail & Related papers  (2023-02-15T18:59:21Z)
• ReACC: A Retrieval-Augmented Code Completion Framework [53.49707123661763]
  We propose a retrieval-augmented code completion framework, leveraging both lexical copying and referring to code with similar semantics by retrieval. We evaluate our approach in the code completion task in Python and Java programming languages, achieving a state-of-the-art performance on CodeXGLUE benchmark.
  arXiv  Detail & Related papers  (2022-03-15T08:25:08Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.