method Max(a: int, b: int) returns (m: int) ensures m >= a && m >= b ensures m == a || m == b { if a >= b { m := a; } else { m := b; } } predicate Sorted(s: seq<int>) { forall i, j :: 0 <= i < j < |s| ==> s[i] <= s[j] } method BinarySearch(a: array<int>, key: int) returns (index: int) requires Sorted(a[..]) ensures 0 <= index ==> a[index] == key ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != key { var lo, hi := 0, a.Length; while lo < hi invariant 0 <= lo <= hi { var mid := (lo + hi) / 2; if a[mid] < key { lo := mid + 1; } else if key < a[mid] { hi := mid; } else { return mid; } } return -1; } lemma MaxCommutative(a: int, b: int) ensures Max(a, b) == Max(b, a) { }

fn verify(x: &State) -> bool { x.balance >= 0 && x.locked <= x.balance } #[requires(n > 0)] #[ensures(ret >= n)] fn next_pow2(n: u64) -> u64 { let mut p = 1; while p < n { p <<= 1; } p } (declare-const x Int) (declare-const y Int) (assert (> x 0)) (assert (= (+ x y) 10)) (check-sat) ; sat (get-model) ; (define-fun x () Int 3) ; (define-fun y () Int 7) (assert (forall ((a Int) (b Int)) (=> (and (> a 0) (> b 0)) (> (+ a b) 0)))) (check-sat) ; unsat impl Repair for Patch { fn verify(&self) -> Outcome { if self.tests_pass() && self.no_regression() { Outcome::Plausible } else { Outcome::Rejected } } }

Automated Repair of Programs from Large Language Models

Published in ICSE 2023 (Research Track), 2023

This paper studies how the output of large language models can be automatically repaired, combining LLM-based code generation with automated program repair techniques.

Recommended citation: Z. Fan, X. Gao, M. Mirchev, A. Roychoudhury, S. H. Tan. (2023). "Automated Repair of Programs from Large Language Models." Proceedings of the 45th International Conference on Software Engineering (ICSE), Research Track.

Share on

Twitter Facebook LinkedIn

Martin Mirchev

Share on