Copper: Unifying Correctness and Performance Specification in Code Generation

• URL: http://arxiv.org/abs/2607.03130v1
• Date: Fri, 03 Jul 2026 09:19:34 GMT
• Title: Copper: Unifying Correctness and Performance Specification in Code Generation
• Abstract summary: We present Copper, a framework that combines formal verification with performance-aware specification.<n>Our approach integrates AI-driven code synthesis with formal verification tools, and automated performance profiling loops.
• Score: 1.799370552205315
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Generative AI has made remarkable progress in producing functionally correct code, yet ensuring both correctness and performance remains an open challenge. We present Copper, a framework that combines formal verification with performance-aware specification to generate code that is provably correct and efficiently executable. Our approach integrates AI-driven code synthesis with formal verification tools, and automated performance profiling loops. Evaluated on a diverse set of algorithmic and real-world programming tasks, Copper produces solutions that satisfy strict correctness guarantees while delivering significant improvements in runtime and memory efficiency compared to baseline AI-generated code. This work demonstrates that it is feasible to bridge the gap between trustworthiness and performance in AI-assisted programming, offering a practical pathway toward reliable, high-performance code generation.

Related papers

• WybeCoder: Verified Imperative Code Generation [22.401681809856896]
  WybeCoder is an agentic code verification framework.<n>It enables prove-as-you-generate development where code, invariants, and proofs co-evolve.
  arXiv  Detail & Related papers  (2026-03-31T00:06:44Z)
• Scaling Code-Assisted Chain-of-Thoughts and Instructions for Model Reasoning [65.20602712957725]
  Caco is a novel framework that automates the synthesis of high-quality, verifiable, and diverse instruction-CoT reasoning data.<n>Our work establishes a paradigm for building self-sustaining, trustworthy reasoning systems without human intervention.
  arXiv  Detail & Related papers  (2025-10-05T07:59:24Z)
• COMPASS: A Multi-Dimensional Benchmark for Evaluating Code Generation in Large Language Models [0.0]
  We introduce a comprehensive evaluation framework that assesses code generation across three dimensions: correctness, efficiency, and quality.<n>Our evaluation of three leading reasoning-enhanced models, Anthropic Claude Opus 4, Google Gemini 2.5 Pro, and OpenAI O4-Mini-High, reveals that models achieving high correctness scores do not necessarily produce efficient algorithms or maintainable code.
  arXiv  Detail & Related papers  (2025-08-19T11:55:07Z)
• CodeGrad: Integrating Multi-Step Verification with Gradient-Based LLM Refinement [12.792149709662874]
  CodeGrad introduces a principled framework that integrates rigorous verification techniques directly into an iterative generation loop.<n>It treats code as a differentiable variable, converting structured feedback and mathematical constraints into a textual pseudo-gradient.<n>We evaluate CodeGrad on the HumanEval, HumanEval+, and LiveCodeBench benchmarks.
  arXiv  Detail & Related papers  (2025-08-12T22:03:54Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  Code generation with large language models (LLMs) is increasingly adopted in production but fails to ensure code quality.<n>We propose REAL, a reinforcement learning framework that incentivizes LLMs to generate production-quality code.
  arXiv  Detail & Related papers  (2025-05-28T17:57:47Z)
• SolBench: A Dataset and Benchmark for Evaluating Functional Correctness in Solidity Code Completion and Repair [51.0686873716938]
  We introduce SolBench, a benchmark for evaluating the functional correctness of Solidity smart contracts generated by code completion models.<n>We propose a Retrieval-Augmented Code Repair framework to verify functional correctness of smart contracts.<n>Results show that code repair and retrieval techniques effectively enhance the correctness of smart contract completion while reducing computational costs.
  arXiv  Detail & Related papers  (2025-03-03T01:55:20Z)
• Learning to Solve and Verify: A Self-Play Framework for Code and Test Generation [69.62857948698436]
  Recent advances in large language models (LLMs) have improved their performance on coding benchmarks.<n>However, improvement is plateauing due to the exhaustion of readily available high-quality data.<n>We propose Sol-Ver, a self-play solver-verifier framework that jointly improves a single model's code and test generation capacity.
  arXiv  Detail & Related papers  (2025-02-20T18:32:19Z)
• LLM4EFFI: Leveraging Large Language Models to Enhance Code Efficiency and Correctness [38.399282089600284]
  Large Language Models (LLMs) have demonstrated impressive performance in code generation.<n>tool: ulineLarge ulineLanguage ulineModel for Code ulineEfficiency is a novel framework that enables LLMs to generate code that balances both efficiency and correctness.
  arXiv  Detail & Related papers  (2025-02-17T07:01:18Z)
• CodeDPO: Aligning Code Models with Self Generated and Verified Source Code [52.70310361822519]
  We propose CodeDPO, a framework that integrates preference learning into code generation to improve two key code preference factors: code correctness and efficiency.<n>CodeDPO employs a novel dataset construction method, utilizing a self-generation-and-validation mechanism that simultaneously generates and evaluates code and test cases.
  arXiv  Detail & Related papers  (2024-10-08T01:36:15Z)
• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  Large language models (LLMs) struggle with consistent and accurate reasoning. LLMs are trained primarily on correct solutions, reducing their ability to detect and learn from errors. We propose a novel collaborative method integrating Chain-of-Thought (CoT) and Program-of-Thought (PoT) solutions for verification.
  arXiv  Detail & Related papers  (2024-10-05T05:21:48Z)

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.