Combining LLM Code Generation with Formal Specifications and Reactive Program Synthesis

• URL: http://arxiv.org/abs/2410.19736v1
• Date: Wed, 18 Sep 2024 15:59:06 GMT
• Title: Combining LLM Code Generation with Formal Specifications and Reactive Program Synthesis
• Authors: William Murphy, Nikolaus Holzer, Feitong Qiao, Leyi Cui, Raven Rothkopf, Nathan Koenig, Mark Santolucito,
• Abstract summary: Large Language Models (LLMs) struggle with accuracy and are unsuitable for high-risk applications. We introduce a solution that divides the code generation into two parts; one to be handled by an LLM and one to be handled by formal methods-based program synthesis.
• Score: 0.7580487359358722
• License:
• Abstract: In the past few years, Large Language Models (LLMs) have exploded in usefulness and popularity for code generation tasks. However, LLMs still struggle with accuracy and are unsuitable for high-risk applications without additional oversight and verification. In particular, they perform poorly at generating code for highly complex systems, especially with unusual or out-of-sample logic. For such systems, verifying the code generated by the LLM may take longer than writing it by hand. We introduce a solution that divides the code generation into two parts; one to be handled by an LLM and one to be handled by formal methods-based program synthesis. We develop a benchmark to test our solution and show that our method allows the pipeline to solve problems previously intractable for LLM code generation.

Related papers

• Automatic Generation of Benchmarks and Reliable LLM Judgment for Code Tasks [0.8274693573069442]
  This work introduces a methodology to generate and evaluate LaaJ implementations, utilizing an automatically generated benchmark. The benchmark is used both to develop and validate the LaaJs and to validate and test the LLM code related solution using the LaaJs. Our approach enables the creation of high quality code task solutions.
  arXiv  Detail & Related papers  (2024-10-28T14:34:36Z)
• zsLLMCode: An Effective Approach for Functional Code Embedding via LLM with Zero-Shot Learning [6.976968804436321]
  Large language models (LLMs) have the capability of zero-shot learning, which does not require training or fine-tuning. We propose zsLLMCode, a novel approach that generates functional code embeddings using LLMs.
  arXiv  Detail & Related papers  (2024-09-23T01:03:15Z)
• EPiC: Cost-effective Search-based Prompt Engineering of LLMs for Code Generation [8.009881267479189]
  Large Language Models (LLMs) have seen increasing use in various software development tasks, especially in code generation. We propose an alternative approach named Evolutionary Prompt Engineering for Code (EPiC) to evolve the original prompts toward better ones that produce high-quality code. Our evaluation against state-of-the-art (SOTA) LLM-based code generation models shows that EPiC outperforms all the baselines in terms of cost-effectiveness.
  arXiv  Detail & Related papers  (2024-08-20T21:15:36Z)
• What's Wrong with Your Code Generated by Large Language Models? An Extensive Study [80.18342600996601]
  Large language models (LLMs) produce code that is shorter yet more complicated as compared to canonical solutions. We develop a taxonomy of bugs for incorrect codes that includes three categories and 12 sub-categories, and analyze the root cause for common bug types. We propose a novel training-free iterative method that introduces self-critique, enabling LLMs to critique and correct their generated code based on bug types and compiler feedback.
  arXiv  Detail & Related papers  (2024-07-08T17:27:17Z)
• InfiBench: Evaluating the Question-Answering Capabilities of Code Large Language Models [56.723509505549536]
  InfiBench is the first large-scale freeform question-answering (QA) benchmark for code to our knowledge. It comprises 234 carefully selected high-quality Stack Overflow questions that span across 15 programming languages. We conduct a systematic evaluation for over 100 latest code LLMs on InfiBench, leading to a series of novel and insightful findings.
  arXiv  Detail & Related papers  (2024-03-11T02:06:30Z)
• StepCoder: Improve Code Generation with Reinforcement Learning from Compiler Feedback [58.20547418182074]
  We introduce StepCoder, a novel framework for code generation, consisting of two main components. CCCS addresses the exploration challenge by breaking the long sequences code generation task into a Curriculum of Code Completion Subtasks. FGO only optimize the model by masking the unexecuted code segments to provide Fine-Grained Optimization. Our method improves the ability to explore the output space and outperforms state-of-the-art approaches in corresponding benchmarks.
  arXiv  Detail & Related papers  (2024-02-02T13:14:31Z)
• If LLM Is the Wizard, Then Code Is the Wand: A Survey on How Code Empowers Large Language Models to Serve as Intelligent Agents [81.60906807941188]
  Large language models (LLMs) are trained on a combination of natural language and formal language (code) Code translates high-level goals into executable steps, featuring standard syntax, logical consistency, abstraction, and modularity.
  arXiv  Detail & Related papers  (2024-01-01T16:51:20Z)
• Function-constrained Program Synthesis [12.55507214959886]
  Large language models (LLMs) can generate code in real-time by drawing on all code available in a development environment. Current systems lack effective recovery methods, forcing users to iteratively re-prompt the model with modified prompts until a sufficient solution is reached. Our method constrains code-generation to an explicit function set and enabling recovery from failed attempts through automatically generated sub-functions.
  arXiv  Detail & Related papers  (2023-11-27T02:55:34Z)
• CodeChain: Towards Modular Code Generation Through Chain of Self-revisions with Representative Sub-modules [51.82044734879657]
  We propose CodeChain, a novel framework for inference that elicits modularized code generation through a chain of self-revisions. We find that CodeChain can significantly boost both modularity as well as correctness of the generated solutions, achieving relative pass@1 improvements of 35% on APPS and 76% on CodeContests.
  arXiv  Detail & Related papers  (2023-10-13T10:17:48Z)
• Test-Case-Driven Programming Understanding in Large Language Models for Better Code Generation [15.166827643436346]
  muFiX is a novel prompting technique to improve the code generation performance of large language models (LLMs) It first exploits test case analysis to obtain specification understanding and enables a self-improvement process. muFiX further fixes the specification understanding towards the direction reducing the gap between the provided understanding and the actual understanding.
  arXiv  Detail & Related papers  (2023-09-28T02:58:07Z)
• Inference with Reference: Lossless Acceleration of Large Language Models [97.04200102556551]
  LLMA is an accelerator to speed up Large Language Model (LLM) inference with references. It is motivated by the observation that there are abundant identical text spans between the decoding result by an LLM and the reference that is available in many real world scenarios.
  arXiv  Detail & Related papers  (2023-04-10T09:55:14Z)

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.