VeriQuick: MaxSubarray (Kadane 알고리즘) 기여

[pacokwon]

이름 Your Name

권해찬

작업물 Your work

prosyslab/veriquick#5

Detailed Description

VeriQuick - PR #5에서 최대 부분배열 합(Maximum Subarray) 문제를 푸는 Kadane 알고리즘이 올바르다는 것과, 입력 길이 $n$에 대해 $O(n)$ 시간에 동작한다는 것을 Lean으로 증명했습니다. 또한 이를 위해 #instrument에 필요한 수정 세 가지를 더했습니다.

풀고자 한 문제

정수 리스트에서 합이 가장 큰 연속 부분배열의 합을 구하는 문제입니다. 입력이 빈 배열인 경우는 예외로 처리하여 none을 반환하고, 그 외에는 최대 부분배열 합 m을 some m으로 반환합니다. 이하에서 입력은 빈 배열이 아니라고 가정합니다.

#eval maxSubarray [] -- none
#eval maxSubarray [-1, -4] -- [-1] => some (-1)
#eval maxSubarray [2, 3, -1, -20, 5, 10] -- [5, 10] => some 15
#eval maxSubarray [-2, 1, -3, 4, -1, 2, 1, -5, 4] -- [4, -1, 2, 1] => some 6

문제 정의

최대 부분배열 합 문제의 구현 impl이 올바르다는 것은, 빈 배열에 대해서는 none을 반환하고, 그 외의 배열 xs에 대해서는 xs의 최대 부분배열 합 m을 some m으로 반환한다는 뜻입니다.

이를 토대로 작성한 Lean 정의는 다음과 같습니다.

def Correct (impl : List Int →  Option Int) : Prop :=
  impl [] = none ∧
  ∀ xs, xs ≠ [] → ∃ m, impl xs = some m ∧ MaxSubarray xs m

알고리즘

최대 부분 배열합의 위키백과에 소개된 Kadane 알고리즘을 그대로 구현하였습니다.

해당하는 Lean 구현은 다음과 같습니다.

/-- `currentSum`: 지금까지 스캔한 배열의 최대 접미배열 합
    `bestSum`: 지금까지 스캔한 배열의 최대 부분배열 합 -/
def scan (currentSum bestSum : Int) : List Int → Int
  | [] => bestSum
  | hd :: tl =>
    -- 새 최대 접미배열은 `[hd]`이거나, 기존 최대 접미배열에 `hd`를 붙인 것
    let currentSum' := max hd (currentSum + hd)
    -- 새 최대 부분배열 합은 기존 최대 부분배열 합(`bestSum`)과
    -- 새 최대 접미배열 합(`currentSum'`) 중 큰 값
    scan currentSum' (max bestSum currentSum') tl

def maxSubarray : List Int → Option Int
  | [] => none
  | hd :: tl => some (scan hd hd tl)

용어 정의

편의를 위해 이 글에서 사용하는 용어를 앞서 정의하겠습니다.

• 원소를 스캔하다: 주어진 원소에 대하여 반복문의 본문을 실행 (currentSum과 bestSum을 갱신)
• 배열 xs의 부분배열: xs의 비어 있지 않은 연속 부분배열
• 배열 xs의 접미배열: xs의 부분배열이면서 xs의 마지막 원소를 포함하는 배열
• 배열 xs의 최대 부분배열 합: xs의 모든 부분배열의 합 중 최대값
• 배열 xs의 최대 접미배열 합: xs의 모든 접미배열의 합 중 최대값

올바름 증명

maxSubarray_correct는 maxSubarray가 명세 Correct를 만족한다는 정리입니다. 증명은 두 단계로 이루어집니다. 먼저 첫째 원소 hd가 [hd]의 최대 접미배열 합이자 최대 부분배열 합임을 보입니다(maxSuffix_singleton, maxSubarray_singleton). 그다음 hd를 scan의 시작값으로 삼으면 scan이 전체 배열의 최대 부분배열 합을 반환함을 보입니다(scan_correct). 이 두 단계는 아래에서 자세히 설명합니다.

theorem maxSubarray_correct : Correct maxSubarray := by
  constructor
  · simp [maxSubarray]
  · intro xs hne
    cases xs with
    | nil => contradiction
    | cons hd tl =>
      refine ⟨scan hd hd tl, rfl, ?_⟩
	  -- hd는 `[hd]`의 최대 접미배열 합
      have hsuf := maxSuffix_singleton hd
      -- hd는 `[hd]`의 최대 부분배열 합
      have hsub := maxSubarray_singleton hd
      exact scan_correct _ _ _ _ hsuf hsub

지금까지 스캔한 배열을 lst라 할 때, scan_correct는 1) currentSum이 lst의 최대 접미배열 합이고 2) bestSum이 lst의 최대 부분배열 합이면, 남은 배열 xs를 모두 스캔한 결과 scan currentSum bestSum xs가 lst ++ xs의 최대 부분배열 합이라는 정리입니다. 이 두 조건이 이 알고리즘 증명의 불변식입니다. 모든 원소를 스캔하고 나면 bestSum이 곧 문제의 해답입니다.

private theorem scan_correct (xs : List Int) :
    ∀ (lst : List Int) (currentSum bestSum : Int),
    MaxSuffix lst currentSum → MaxSubarray lst bestSum →
    MaxSubarray (lst ++ xs) (scan currentSum bestSum xs) := by
      induction xs with
      | nil => intro lst _ _ _ hbest; simp [scan]; exact hbest
      | cons hd tl ih =>
        intro lst currentSum bestSum hcur hbest
        -- `max hd (currentSum + hd)`는 `lst ++ [hd]`의 최대 접미배열 합.
        have hcur' := maxSuffix_append hd hcur
        -- `max bestSum (max hd (currentSum + hd))`는 `lst ++ [hd]`의 최대 부분배열 합.
        have hbest' := maxSubarray_append hd hcur hbest
        have := ih _ _ _ hcur' hbest'
        simpa [scan] using this

증명은 xs에 대한 귀납법으로 할 수 있습니다. 다음 스캔할 원소 hd가 있을 때, lst ++ [hd]에서도 불변식이 성립함을 maxSuffix_append와 maxSubarray_append로 보인 뒤, 귀납 가설을 적용합니다.

보조정리

첫째 원소만 스캔한 경우: maxSubarray는 첫째 원소 x를 currentSum과 bestSum의 초기값으로 scan을 호출하므로, 초기값이 불변식을 만족함을 보여야 합니다.

• maxSubarray_singleton: [x]의 최대 부분배열 합은 x이다.
• maxSuffix_singleton: [x]의 최대 접미배열 합은 x이다.

theorem maxSubarray_singleton (x : Int) : MaxSubarray [x] x
theorem maxSuffix_singleton (x : Int) : MaxSuffix [x] x

추가로 원소를 스캔한 경우: 불변식이 성립하는 lst에, 다음 원소 x를 스캔해도 lst ++ [x]에서 불변식이 만족함을 보입니다.

• maxSuffix_append: lst ++ [x]의 최대 접미배열 합은 max x (currentSum + x)이다.
• maxSubarray_append: lst ++ [x]의 최대 부분배열 합은 max bestSum (max x (currentSum + x))이다 (기존 최대 접미배열에 x를 붙인 것이 새로운 최대 부분배열이 될 수 있으므로 currentSum에 대한 불변식이 필요).

theorem maxSuffix_append {lst : List Int} {currentSum : Int} (x : Int)
    (hcur : MaxSuffix lst currentSum) :
    MaxSuffix (lst ++ [x]) (max x (currentSum + x))

theorem maxSubarray_append {lst : List Int} {currentSum bestSum : Int} (x : Int)
    (hcur : MaxSuffix lst currentSum) (hbest : MaxSubarray lst bestSum) :
    MaxSubarray (lst ++ [x]) (max bestSum (max x (currentSum + x)))

시간 복잡도 증명

maxSubarray의 시간 복잡도가 입력 길이 $n$에 대해 $O(n)$임을 증명했습니다.

명제와 증명을 작성하기에 앞서, scan_timed와 maxSubarray_timed의 입력의 크기를 늘려가며 비용을 관찰하였습니다.

#eval scan_timed 0 0 [] -- 0 => 2
#eval scan_timed 0 0 [1] -- 1 => 7 (+5)
#eval scan_timed 1 1 [1, -2] -- 2 => 12 (+5)
#eval scan_timed 1 1 [1, -2, 5] -- 3 => 17 (+5)

#eval maxSubarray_timed [] -- 0 => 3
#eval maxSubarray_timed [0] -- 1 => 5
#eval maxSubarray_timed [0, 1] -- 2 => 10
#eval maxSubarray_timed [1, 1, -2] -- 3 => 15
#eval maxSubarray_timed [1, 1, -2, 5] -- 4 => 20

이 관찰을 통해 scan_timed는 정확히 $5n + 2$만큼 비용이 든다는 scan_timed_cost 명제를 세웠고, maxSubarray_timed는 $5n + 3$의 비용 상한이 있다는 maxSubarray_timed_cost 명제를 세웠습니다.

theorem scan_timed_cost (currentSum bestSum : Int) (xs : List Int) :
    (scan_timed currentSum bestSum xs).cost = 5 * xs.length + 2

theorem maxSubarray_timed_cost (xs : List Int) :
    (maxSubarray_timed xs).cost ≤ 5 * xs.length + 3

scan_timed_cost는 xs에 대한 귀납법으로, maxSubarray_timed_cost는 xs에 대한 경우 분석 (case analysis)으로 간단하게 증명할 수 있었습니다.

마지막으로, maxSubarray_timed_isLinear에서 maxSubarray_timed의 시간 복잡도가 $O(n)$임을 보였습니다. 상한 함수를 Bound n = n + 1로 두고 다음 명제를 증명했습니다.

def Bound (n : Nat) := n + 1

def Asymptotic {α β : Type} [Size α]
  (impl : α → TimeM β) (bound : Option (Nat → Nat)) : Prop :=
	/-- 어떤 상수 `c > 0`과 `n₀`가 있어,
		크기가 `n₀` 이상인 모든 입력에서
		`impl`의 비용이 `c * bound n` 이하이다. -/
	...

def complexity : Prop :=
  Asymptotic maxSubarray_timed (.some Bound)

theorem maxSubarray_timed_isLinear : complexity

$5n + 3 ≤ 5(n + 1)$이므로, $c = 5, n₀ = 0$을 골랐고, maxSubarray_timed_cost와 omega 전략을 이용하여 증명할 수 있습니다.

Instrumentation 수정

증명 작업 중 발견한 instrumentation 관련 문제들을 해결하기 위해 다음을 추가/수정하였습니다.

1. Translate.lean에서 max/min을 지원하도록 했습니다. 기존에는 Nat/Int의 max가 일반 unfold 경로로 빠져 "first-order data result" 오류로 실패했습니다. 이제 인스턴스가 정확히 Nat.instMax, Int.instMax, instMinNat, Int.instMin일 때만 비용 1로 처리하고, 다른 인스턴스는 이전처럼 거부합니다.
2. Instrumentation.lean에서 구조적 재귀 함수 안의 let을 처리하도록 고쳤습니다. fun_induction이 let을 지역 정의로 바꾸는데, 자동 생성된 증명의 simp_all이 이를 사용하지 않아 값 보존 증명이 실패하고 있었습니다. 문제가 되는 simp_all에 +zetaDelta를 추가했습니다.
3. TimeM.lean에 fst_step_prod(veriquick#2의 수정사항과 동일)와 snd_step_prod를 추가했습니다. simp가 TimeM.done a를 (a, 0)으로 풀고 나면 fst_step/snd_step이 더 이상 매칭되지 않는데, 이 보조정리들 덕분에 비용 증명에서 TimeM.step이나 bind를 직접 풀지 않고도 simp [f_timed]만으로 단순화를 이어갈 수 있습니다.

가장 어려웠던 점

첫 번째로 어려웠던 점은 아름답고 깔끔한 Lean 증명을 쓰는 것이었습니다. 일반 프로그래밍에서는 지금까지의 경험을 토대로 LLM이 생성한 코드가 지저분한지 깔끔한지 구분할 수 있는 감이 있지만, 아직 낯선 Lean은 그러한 감이 없습니다. Lean은 같은 증명을 하는 방법이 다양해서(simp, simp only, omega 등), 방법이 하나뿐이라면 고민하지 않았을 선택을 계속 해야 했습니다.

최소한 깔끔한 증명이라도 작성하기 위해 제가 채택한 원칙은 일관성입니다. 변수명, 증명 구조, 코드 분리 방법을 일관적으로 유지하면, 타인이 코드를 읽을 때 다음에 나올 구조를 예측할 수 있어 가독성이 높아집니다. 이는 일반 프로그래밍을 할 때 흔히 적용하는 원칙입니다. 기여자가 많은 코드베이스의 경우, 각자의 기준이 충돌하여 일관성이 깨지기 쉬워, 통상적으로 컨벤션(convention)을 정해 통일합니다. 저는 여러 사람이 기여하는 VeriQuick에도 증명 스타일 가이드가 있으면 도움이 될 것이라고 생각합니다.

두 번째로 어려웠던 점은 문제를 정의하는 일이었습니다. 정의가 잘못되면 증명을 재작성해야 하기에 처음에 정의를 잘 하는 것은 중요합니다. 그러나 같은 문제라도 허용하는 범위에 따라 여러 가지 정의가 가능합니다(예. 빈 배열을 허용하는가?). 어떤 경우에는 더 강한 명세를 쓸 수도 있습니다. 저는 가장 직관적인 정의를 택했으나, 문제를 "잘" 정의하는 것이 정확히 무엇인가는 아직 의문점이 남습니다.

AI 사용

증명 코드는 대부분 직접 작성했습니다. Claude Code는 증명 아이디어(방향 제시), 디버깅, 리팩토링(코드를 깔끔하게 만드는 일)에 사용했습니다. Instrumentation 수정은 AI가 작성하고 제가 검토했습니다.
이 글을 작성할 시에는 문장 다듬기, 전체적인 오류 검사, 영어 용어 번역, 한국어 전문 -> 영어 번역 용도로 Claude를 사용했습니다.

---

Detailed Description

In VeriQuick - PR #5, I proved in Lean that Kadane's algorithm for the Maximum Subarray problem is correct and runs in $O(n)$ time in the input length $n$. I also made three fixes to #instrument that this required.

The problem

Given a list of integers, find the sum of the contiguous subarray with the largest sum. An empty input is handled as an exception and returns none; otherwise the maximum subarray sum m is returned as some m. From here on, the input is assumed to be non-empty.

#eval maxSubarray [] -- none
#eval maxSubarray [-1, -4] -- [-1] => some (-1)
#eval maxSubarray [2, 3, -1, -20, 5, 10] -- [5, 10] => some 15
#eval maxSubarray [-2, 1, -3, 4, -1, 2, 1, -5, 4] -- [4, -1, 2, 1] => some 6

Problem definition

An implementation impl of the maximum subarray sum problem is correct if it returns none on the empty array and, on any other array xs, returns the maximum subarray sum m of xs as some m.

The corresponding Lean definition is:

def Correct (impl : List Int →  Option Int) : Prop :=
  impl [] = none ∧
  ∀ xs, xs ≠ [] → ∃ m, impl xs = some m ∧ MaxSubarray xs m

Algorithm

I implemented Kadane's algorithm, as introduced on Wikipedia's page on the maximum subarray problem, as is.

The corresponding Lean implementation is:

/-- `currentSum`: the maximum suffix sum of the array scanned so far
    `bestSum`: the maximum subarray sum of the array scanned so far -/
def scan (currentSum bestSum : Int) : List Int → Int
  | [] => bestSum
  | hd :: tl =>
    -- the new maximum suffix is either `[hd]` or the old maximum suffix with `hd` appended
    let currentSum' := max hd (currentSum + hd)
    -- the new maximum subarray sum is the larger of the old maximum subarray sum (`bestSum`)
    -- and the new maximum suffix sum (`currentSum'`)
    scan currentSum' (max bestSum currentSum') tl

def maxSubarray : List Int → Option Int
  | [] => none
  | hd :: tl => some (scan hd hd tl)

Terminology

For convenience, I define the terms used in this post up front.

• To scan an element: to execute the loop body for the given element (updating currentSum and bestSum).
• A subarray of an array xs: a non-empty contiguous subarray of xs.
• A suffix of an array xs: a subarray of xs that contains the last element of xs.
• The sum of an array xs: the value obtained by adding all elements of xs.
• The maximum subarray sum of xs: the largest sum among all subarrays of xs.
• The maximum suffix sum of xs: the largest sum among all suffixes of xs.

Correctness proof

maxSubarray_correct states that maxSubarray satisfies the specification Correct. The proof has two steps. First, we show that the first element hd is both the maximum suffix sum and the maximum subarray sum of [hd] (maxSuffix_singleton, maxSubarray_singleton). Then, taking hd as the initial values of scan, we show that scan returns the maximum subarray sum of the whole array (scan_correct). These two steps are explained in detail below.

theorem maxSubarray_correct : Correct maxSubarray := by
  constructor
  · simp [maxSubarray]
  · intro xs hne
    cases xs with
    | nil => contradiction
    | cons hd tl =>
      refine ⟨scan hd hd tl, rfl, ?_⟩
      -- hd is the maximum suffix sum of `[hd]`
      have hsuf := maxSuffix_singleton hd
      -- hd is the maximum subarray sum of `[hd]`
      have hsub := maxSubarray_singleton hd
      exact scan_correct _ _ _ _ hsuf hsub

Letting lst denote the array scanned so far, scan_correct states that if 1) currentSum is the maximum suffix sum of lst and 2) bestSum is the maximum subarray sum of lst, then the result of scanning the remaining array xs, scan currentSum bestSum xs, is the maximum subarray sum of lst ++ xs. These two conditions are the invariant of this algorithm's proof. Once every element has been scanned, bestSum is the answer to the problem.

private theorem scan_correct (xs : List Int) :
    ∀ (lst : List Int) (currentSum bestSum : Int),
    MaxSuffix lst currentSum → MaxSubarray lst bestSum →
    MaxSubarray (lst ++ xs) (scan currentSum bestSum xs) := by
      induction xs with
      | nil => intro lst _ _ _ hbest; simp [scan]; exact hbest
      | cons hd tl ih =>
        intro lst currentSum bestSum hcur hbest
        -- `max hd (currentSum + hd)` is the maximum suffix sum of `lst ++ [hd]`.
        have hcur' := maxSuffix_append hd hcur
        -- `max bestSum (max hd (currentSum + hd))` is the maximum subarray sum of `lst ++ [hd]`.
        have hbest' := maxSubarray_append hd hcur hbest
        have := ih _ _ _ hcur' hbest'
        simpa [scan] using this

The proof can be done by induction on xs. When there is a next element hd to scan, maxSuffix_append and maxSubarray_append show that the invariant also holds for lst ++ [hd], and then the induction hypothesis is applied.

Lemmas

When only the first element has been scanned: maxSubarray calls scan with the first element x as the initial values of currentSum and bestSum, so we must show that these initial values satisfy the invariant.

• maxSubarray_singleton: the maximum subarray sum of [x] is x.
• maxSuffix_singleton: the maximum suffix sum of [x] is x.

theorem maxSubarray_singleton (x : Int) : MaxSubarray [x] x
theorem maxSuffix_singleton (x : Int) : MaxSuffix [x] x

When further elements are scanned: for a lst that satisfies the invariant, we show that scanning the next element x keeps the invariant satisfied for lst ++ [x].

• maxSuffix_append: the maximum suffix sum of lst ++ [x] is max x (currentSum + x).
• maxSubarray_append: the maximum subarray sum of lst ++ [x] is max bestSum (max x (currentSum + x)) (the old maximum suffix extended by x can become the new maximum subarray, so the invariant on currentSum is needed).

theorem maxSuffix_append {lst : List Int} {currentSum : Int} (x : Int)
    (hcur : MaxSuffix lst currentSum) :
    MaxSuffix (lst ++ [x]) (max x (currentSum + x))

theorem maxSubarray_append {lst : List Int} {currentSum bestSum : Int} (x : Int)
    (hcur : MaxSuffix lst currentSum) (hbest : MaxSubarray lst bestSum) :
    MaxSubarray (lst ++ [x]) (max bestSum (max x (currentSum + x)))

Time complexity proof

I proved that the time complexity of maxSubarray is $O(n)$ in the input length $n$.

Before writing the statements and proofs, I observed the cost of scan_timed and maxSubarray_timed while increasing the input size.

#eval scan_timed 0 0 [] -- 0 => 2
#eval scan_timed 0 0 [1] -- 1 => 7 (+5)
#eval scan_timed 1 1 [1, -2] -- 2 => 12 (+5)
#eval scan_timed 1 1 [1, -2, 5] -- 3 => 17 (+5)

#eval maxSubarray_timed [] -- 0 => 3
#eval maxSubarray_timed [0] -- 1 => 5
#eval maxSubarray_timed [0, 1] -- 2 => 10
#eval maxSubarray_timed [1, 1, -2] -- 3 => 15
#eval maxSubarray_timed [1, 1, -2, 5] -- 4 => 20

From these observations, I formulated scan_timed_cost, stating that scan_timed costs exactly $5n + 2$, and maxSubarray_timed_cost, stating that maxSubarray_timed has a cost upper bound of $5n + 3$.

theorem scan_timed_cost (currentSum bestSum : Int) (xs : List Int) :
    (scan_timed currentSum bestSum xs).cost = 5 * xs.length + 2

theorem maxSubarray_timed_cost (xs : List Int) :
    (maxSubarray_timed xs).cost ≤ 5 * xs.length + 3

scan_timed_cost could be proved simply by induction on xs, and maxSubarray_timed_cost by case analysis on xs.

Finally, maxSubarray_timed_isLinear shows that the time complexity of maxSubarray_timed is $O(n)$. I set the bound function to Bound n = n + 1 and proved the following statement.

def Bound (n : Nat) := n + 1

def Asymptotic {α β : Type} [Size α]
  (impl : α → TimeM β) (bound : Option (Nat → Nat)) : Prop :=
  /-- There exist constants `c > 0` and `n₀` such that,
      for every input of size at least `n₀`,
      the cost of `impl` is at most `c * bound n`. -/
  ...

def complexity : Prop :=
  Asymptotic maxSubarray_timed (.some Bound)

theorem maxSubarray_timed_isLinear : complexity

Since $5n + 3 ≤ 5(n + 1)$, I chose $c = 5, n₀ = 0$, and the proof follows from maxSubarray_timed_cost and the omega tactic.

Instrumentation changes

To resolve instrumentation problems I found while working on the proofs, I added/changed the following.

1. In Translate.lean, I added support for max/min. Previously, max on Nat/Int fell through to the generic unfolding path and failed with a "first-order data result" error. Now it is charged a cost of 1 only when the instance is exactly Nat.instMax, Int.instMax, instMinNat or Int.instMin, and any other instance is rejected as before.
2. In Instrumentation.lean, I fixed the handling of let inside structurally recursive functions. fun_induction turns a let into a local definition, but the simp_all in the auto-generated proof did not use it, so the value-preservation proof was failing. I added +zetaDelta to that simp_all.
3. In TimeM.lean, I added fst_step_prod (identical to the change in veriquick#2) and snd_step_prod. Once simp rewrites TimeM.done a to (a, 0), fst_step/snd_step no longer match. Thanks to these lemmas, a cost proof can continue simplifying with just simp [f_timed], without unfolding TimeM.step or bind by hand.

What was hardest

The first difficulty was writing beautiful and clean Lean proofs. In ordinary programming, my experience lets me tell whether LLM-generated code is messy or clean, but I am still new to Lean and lack that intuition. Lean offers many ways to prove the same thing (simp, simp only, omega, etc.), so I kept having to make choices that I would not have agonized over if there were only one way.

The principle I adopted to write proofs that are at least clean is consistency. By keeping variable names, proof structure, and the way code is split consistent, other readers can predict what comes next, which improves readability. This is a principle commonly applied in ordinary programming as well. In a codebase with many contributors, individual standards tend to clash and consistency is easily broken, so teams usually settle on a coding convention to unify them. I think VeriQuick, which many people contribute to, would also benefit from a proof style guide.

The second difficulty was defining the problem. If a definition turns out to be wrong, the proofs must be rewritten, so getting the definition right at the start is important. However, even for the same problem, many definitions are possible depending on the scope allowed (e.g. are empty arrays allowed?). In some cases, one can also state a stronger specification. I chose the most straightforward definition, but what it means to define a problem "well" remains an open question for me.

AI usage

I wrote most of the proof code by hand. I used Claude Code for proof ideas (guidance), debugging, and refactoring (making the code cleaner). The instrumentation changes were written by AI and reviewed by me.

In writing this post, I used Claude for polishing sentences, overall error checking, translating English terms, and translating the full Korean text into English.

[bongjunj]

증명에 기여해주셔서 감사합니다. 증명이 잘 작성되어 있는 것을 확인했습니다.

다만 설명 글이 리뷰가 어렵습니다. 내용을 볼때 충분한 검토없이 AI로 생성된 글로 보입니다.
현재 AI 사용을 코드와 증명에만 사용했다고 되어 있는데, 설명 글 생성 여부와 어떻게 사용되었는지 명확히 밝혀주시기 바랍니다.

다음과 같은 구체적인 문제점들이 있습니다. 한번 고쳐보시고, 다른 점들도 스스로 검토해보시기 바랍니다.

1. 글이 너무 장황합니다.
   • AI로 생성된 글의 대표적인 문제점입니다.
   • "증명의 핵심 아이디어는 반복문의 매 단계에서 유지되는 불변식입니다." 모든 프로그램 증명에 해당하기에 삭제해도 무방한 문장입니다. "핵심 아이디어" 문장인데 핵심 아이디어가 드러나 있지 않습니다.
2. 예제와 설명이 연결되어 있지 않습니다.
   • 설명에는 lst가 있는데 scan, maxSubarray 예제에는 lst가 없습니다. 설명을 예제와 함께 따라가기가 힘듭니다.
   • 설명에 "scan을 처음 호출했을 때 처리한 접두사"에서 처리한 접두사라는 게 무슨 말인지 모르겠습니다. 처음 호출했는데 이미 처리한 접두사가 무엇인지 이해하기 힘듭니다. 이 값에 이름을 붙이거나 코드에서 어떤 줄을 읽어야 하는지 명시해주셨으면 좋겠습니다.
3. 어색한 한국어 번역투
   • "귀납적으로 이으면"
   • "이때 m은 실제로 어떤 부분배열의 합이며, 동시에 모든 부분배열의 합 이상입니다."

리뷰어와 다른 독자를 고려해 글을 다시 정리해주시기를 기대합니다.
감사합니다.

---

Thanks for the proof contribution, and the proofs are well organized.
However, this writing is so hard to read.
Based on the contents, this appears to be AI-generated text without a proper review.
Furthermore, your AI usage disclosure only states code and proof generation, not this text.
Please explicitly state whether AI was also used to write this explanation, and to what extent.

The fact that it is AI-generated does not necessarily mean it is bad. However, this writing has several problems.
I would like to suggest you to fix the following problems (but not limited to):

1. The writing is too verbose
   • This is a typical issue with AI text.
   • "The key idea of the proof is an invariant that is maintained at every step of the loop." is a vacuous statement. This applies to every program verification proof. The word "key idea" makes a reader (me) expect a very important information come up immediately. But there is no "key idea" in the sentence.
2. The example code is not directly matched to the explanation.
   • lst does not appear in the example of scan and maxSubarray, which makes hard to follow your explanation.
   • I could not follow what 'the processed prefix upon the first call to scan'. Please give it a name or reference the exact line of code.

I would appreciate it if you could revise the write-up so that reviewers and readers can follow it more clearly.
Thank you.

[pacokwon]

안녕하세요, 좋은 피드백 감사합니다. 짚어주신 부분들을 고려하여 글을 수정하였으니, 확인 부탁드립니다.

[KihongHeo]

안녕하세요. 수고 많으셨습니다. 증명은 잘 하신것으로 보이고요.

다만, 제가 느끼기에도 글은 이해하기가 어렵네요.
글을 AI가 썼는지 아닌지보다도, 더 중요한 본질은 읽는 사람이 이해하기가 좋으냐입니다. 불필요한 세부사항은 빼고 핵심만 간결히. 모든 심사가 그렇지요. 논문 심사도 그렇고, 입사/입시도 그렇고. 독자의 수준에 맞게. 이 글을 읽는 사람의 수준은 어느 정도일까요? 한 번 생각해 보세요. 다음 번에는 너무 당연한 이야기는 줄이고 핵심은 명확히 부탁합니다.

[pacokwon]

네, 더 명확하게 작성할 수 있도록 노력하겠습니다. 감사합니다!

[bongjunj]

수정해주신 글 잘 읽었습니다.
다음 독자들을 위해서 다음 사항을 고려해주시면 좋겠습니다.

Minor Points

• 이탈릭 스타일이 지정된 경우는 어떤 의미가 있나요? 특별한 의미가 없으면 적용하지 않는게 낫습니다.
• "빈 리스트에서는 답이 없으므로 구현이 Option Int를 반환하고 none을 돌려줍니다."
  • none의 타입도 Option Int이라서 설명이 이상합니다. some ...을 반환한다고 하거나, 빈 리스트는 예외 처리한다고 단순하게 설명하는 게 낫지 않을까요?
• 예외 처리와 관련해서, 글에 전반적으로 "비어있지 않은" 리스트가 지속적으로 언급되어 글이 길어집니다. 빈 리스트는 예외 처리한다고 처음에 한번 언급하고 나머지 글을 간결하게 하는게 가독성에 유리하지 않을까 싶습니다.
• 중간 상태 테이블에서 무엇을 설명하려는 것인지 명확하지가 않습니다. 테이블이 맞는지 확인하려면 노력이 많이드는데, 테이블을 확인하고 나면 읽고나서 얻는게 없습니다.
• 파이썬 코드랑 Lean 코드랑 둘 다 읽어야 하는데, Lean 코드만 간결하게 남기는게 어떨까 싶습니다. 그리고 무엇을 계산하는건지, 핵심 불변식에 대한 힌트를 주석으로 남겨줌으로써 코드를 읽으면서 읽는 사람으로 하여금 불변식을 떠올릴 수 있게 돕고요.
• 올바름 증명을 설명할 때, 불변식이 필요한 이유를 전체 correctness 증명 구조와 함께 보여주시는 것이 어떨까요. 지금 글의 흐름은 핵심 불변식 -> 지엽적인 theorems -> 핵심 불변식을 이용한 전체 증명인데, 핵심 불변식과 전체 증명 구조가 멀리 떨어져있어서 읽기 힘듭니다. 전체 증명 구조를 잡아두고 이에 필요한 지엽적인 theorems들을 보였다라고 하는게 더 직관적일 거 같습니다.

[pacokwon]

피드백 감사드립니다. 말씀주신 부분들을 고민해본 뒤에 글을 수정하겠습니다.