Disproving Program Equivalence with LLMs

• URL: http://arxiv.org/abs/2502.18473v1
• Date: Wed, 05 Feb 2025 12:54:17 GMT
• Title: Disproving Program Equivalence with LLMs
• Authors: Miltiadis Allamanis, Pengcheng Yin,
• Abstract summary: This work introduces ProbeGen, a whitebox method that takes two or more executable pieces of code and searches for counterexamples to their equivalence.<n>We demonstrate that ProbeGen disproves 18% of samples considered equivalent to the ground truth by the benchmark-provided unit tests.<n>Using ProbeGen, we can semantically cluster LLM samples for semantic self-consistency, improving pass@1 by 10%.
• Score: 22.047880121762013
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: To evaluate large language models (LLMs) for code, research has used manually created unit test-based benchmarks. However, these tests are often inadequate, missing corner cases and other implementation-specific oddities. This work introduces ProbeGen, a whitebox method that takes two or more executable pieces of code and searches for counterexamples to their equivalence. Comparing code semantics requires a deep understanding of code. We demonstrate that LLMs with execution feedback perform well at this task. In a common code synthesis benchmark, ProbeGen disproves 18% of samples considered equivalent to the ground truth by the benchmark-provided unit tests. Additionally, using ProbeGen, we can semantically cluster LLM samples for semantic self-consistency, improving pass@1 by 10% by unifying syntactically distinct but semantically similar samples.

Related papers

• HyClone: Bridging LLM Understanding and Dynamic Execution for Semantic Code Clone Detection [3.2167919219391474]
  Code clone detection is a critical task in software engineering, aimed at identifying duplicated or similar code fragments within or across software systems.<n>Recent advances in large language models (LLMs) have shown promise in understanding code semantics.<n>We propose a novel two-stage framework that combines LLM-based screening with execution-based validation for detecting semantic clones in Python programs.
  arXiv  Detail & Related papers  (2025-08-02T13:11:56Z)
• CLEVER: A Curated Benchmark for Formally Verified Code Generation [57.476483009565044]
  $rm Csmall LEVER$ is a high-quality, curated benchmark of 161 problems for end-to-end verified code generation in Lean.<n>Each problem consists of (1) the task of generating a specification that matches a held-out ground-truth specification, and (2) the task of generating a Lean implementation that provably satisfies this specification.
  arXiv  Detail & Related papers  (2025-05-20T05:15:47Z)
• Scoring Verifiers: Evaluating Synthetic Verification for Code and Reasoning [59.25951947621526]
  We propose an approach which can transform existing coding benchmarks into scoring and ranking datasets to evaluate the effectiveness of synthetic verifiers. We release four new benchmarks (HE-R, HE-R+, MBPP-R, and MBPP-R+), and analyzed synthetic verification methods with standard, reasoning-based, and reward-based LLMs. Our experiments show that reasoning can significantly improve test case generation and that scaling the number of test cases enhances the verification accuracy.
  arXiv  Detail & Related papers  (2025-02-19T15:32:11Z)
• EquiBench: Benchmarking Large Language Models' Understanding of Program Semantics via Equivalence Checking [55.81461218284736]
  EquiBench is a new benchmark for evaluating large language models (LLMs)<n>It determines whether two programs produce identical outputs for all possible inputs.<n>We evaluate 19 state-of-the-art LLMs and find that the best accuracies are 63.8% and 76.2%, only modestly above the 50% random baseline.
  arXiv  Detail & Related papers  (2025-02-18T02:54:25Z)
• Evaluating and Aligning CodeLLMs on Human Preference [42.26173776584043]
  We present a rigorous human-curated benchmark CodeArena to emulate the complexity and diversity of real-world coding tasks.<n>We also propose a diverse synthetic instruction corpus SynCode-Instruct to verify the effectiveness of the large-scale synthetic instruction fine-tuning.<n>The results find performance differences between execution-based benchmarks and CodeArena.
  arXiv  Detail & Related papers  (2024-12-06T17:40:38Z)
• Commit0: Library Generation from Scratch [77.38414688148006]
  Commit0 is a benchmark that challenges AI agents to write libraries from scratch.<n>Agents are provided with a specification document outlining the library's API as well as a suite of interactive unit tests.<n> Commit0 also offers an interactive environment where models receive static analysis and execution feedback on the code they generate.
  arXiv  Detail & Related papers  (2024-12-02T18:11:30Z)
• Toward Automated Validation of Language Model Synthesized Test Cases using Semantic Entropy [0.5057850174013127]
  Modern Large Language Model (LLM)-based programming agents often rely on test execution feedback to refine their generated code.<n>This paper introduces VALTEST, a novel framework that leverages semantic entropy to automatically validate test cases generated by LLMs.<n>Experiments show that VALTEST boosts test validity by up to 29% and improves code generation performance, as evidenced by significant increases in pass@1 scores.
  arXiv  Detail & Related papers  (2024-11-13T00:07:32Z)
• Quasi-random Multi-Sample Inference for Large Language Models [1.647759094903376]
  Large language models (LLMs) are often equipped with multi-sample decoding strategies. Traditional text generation methods, such as beam search and sampling-based techniques, have notable limitations. This study explores the potential of arithmetic sampling, contrasting it with ancestral sampling.
  arXiv  Detail & Related papers  (2024-11-09T18:55:04Z)
• A test-free semantic mistakes localization framework in Neural Code Translation [32.5036379897325]
  We present EISP, a static analysis framework based on the Large Language Model (LLM) The framework generates a semantic mapping between source code and translated code. EISP connects each pair of sub-code fragments with fine-grained knowledge hints through an AI chain.
  arXiv  Detail & Related papers  (2024-10-30T08:53:33Z)
• SWT-Bench: Testing and Validating Real-World Bug-Fixes with Code Agents [10.730852617039451]
  We investigate the capability of LLM-based Code Agents to formalize user issues into test cases.<n>We propose a novel benchmark based on popular GitHub repositories, containing real-world issues, ground-truth bug-fixes, and golden tests.<n>We find that LLMs generally perform surprisingly well at generating relevant test cases, with Code Agents designed for code repair exceeding the performance of systems designed for test generation.
  arXiv  Detail & Related papers  (2024-06-18T14:54:37Z)
• Uncovering LLM-Generated Code: A Zero-Shot Synthetic Code Detector via Code Rewriting [78.48355455324688]
  We propose a novel zero-shot synthetic code detector based on the similarity between the original code and its LLM-rewritten variants.<n>Our results demonstrate a significant improvement over existing SOTA synthetic content detectors.
  arXiv  Detail & Related papers  (2024-05-25T08:57:28Z)
• Large Language Models as Test Case Generators: Performance Evaluation and Enhancement [3.5398126682962587]
  We study how well Large Language Models can generate high-quality test cases. We propose a multi-agent framework called emphTestChain that decouples the generation of test inputs and test outputs. Our results indicate that TestChain outperforms the baseline by a large margin.
  arXiv  Detail & Related papers  (2024-04-20T10:27:01Z)
• Code-Aware Prompting: A study of Coverage Guided Test Generation in Regression Setting using LLM [32.44432906540792]
  We present SymPrompt, a code-aware prompting strategy for large language models in test generation. SymPrompt enhances correct test generations by a factor of 5 and bolsters relative coverage by 26% for CodeGen2. Notably, when applied to GPT-4, SymPrompt improves coverage by over 2x compared to baseline prompting strategies.
  arXiv  Detail & Related papers  (2024-01-31T18:21:49Z)
• Not All Metrics Are Guilty: Improving NLG Evaluation by Diversifying References [123.39034752499076]
  Div-Ref is a method to enhance evaluation benchmarks by enriching the number of references. We conduct experiments to empirically demonstrate that diversifying the expression of reference can significantly enhance the correlation between automatic evaluation and human evaluation.
  arXiv  Detail & Related papers  (2023-05-24T11:53:29Z)
• LLMs as Factual Reasoners: Insights from Existing Benchmarks and Beyond [135.8013388183257]
  We propose a new protocol for inconsistency detection benchmark creation and implement it in a 10-domain benchmark called SummEdits. Most LLMs struggle on SummEdits, with performance close to random chance. The best-performing model, GPT-4, is still 8% below estimated human performance.
  arXiv  Detail & Related papers  (2023-05-23T21:50:06Z)
• CodeT: Code Generation with Generated Tests [49.622590050797236]
  We explore the use of pre-trained language models to automatically generate test cases. CodeT executes the code solutions using the generated test cases, and then chooses the best solution. We evaluate CodeT on five different pre-trained models with both HumanEval and MBPP benchmarks.
  arXiv  Detail & Related papers  (2022-07-21T10:18:37Z)

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.