Duality theory in linear optimization and its extensions -- formally verified

이 논문은 Lean 4 를 사용하여 선형 순서체에서 파카스 (Farkas) 와 유사한 정리들을 형식적으로 증명하고, 일부 계수가 '무한대' 값을 가질 수 있는 경우로 선형 최적화의 쌍대성 이론을 확장합니다.

핵심

이 논문은 **"수학적 진리를 컴퓨터가 직접 검증한 선형 최적화 (Linear Optimization) 의 새로운 세계"**에 대한 이야기입니다.

마치 "수학의 법칙을 컴퓨터 코드로 직접 짠 뒤, 그 코드가 절대 틀릴 수 없음을 증명해낸" 프로젝트라고 생각하시면 됩니다. 저자들은 'Lean 4'라는 컴퓨터 증명 도구를 사용하여, 수백 년간 이어져 온 선형 계획법 (Linear Programming) 의 핵심 이론들을 다시 한번 완벽하게 검증하고, 여기에 **'무한대 (Infinity)'**라는 새로운 개념을 추가했습니다.

이 복잡한 내용을 일상적인 비유로 쉽게 설명해 드리겠습니다.

---

1. 배경: "요리하기"와 "제약 조건" (선형 계획법이란?)

우리가 매일 하는 결정들, 예를 들어 **"가장 싸게 먹으면서 영양을 챙기는 점심 메뉴를 고르는 문제"**를 생각해 봅시다.

• 목표: 돈을 가장 적게 쓰자 (비용 최소화).
• 제약 조건: 단백질은 30g 이상, 칼로리는 700kcal 이상.
• 재료: 쌀과 렌틸콩.

이 문제는 수학적으로 방정식과 부등식으로 표현할 수 있습니다. 이때 중요한 질문은 **"이런 조건을 만족하는 해 (해결책) 가 정말 존재할까?"**입니다.

2. 핵심 이론: "파르카스 보조정리" (Farkas' Lemma)

이 논문에서 다루는 가장 유명한 정리는 파르카스 보조정리입니다. 이를 비유하자면 다음과 같습니다.

"어떤 요리 레시피 (조건) 를 만족하는 재료를 찾을 수 있을까?"

이 정리는 두 가지 상황 중 반드시 하나만 성립한다고 말합니다.

1. 성공: 조건을 만족하는 재료 조합 (해) 이 존재한다.
2. 실패: 조건을 만족하는 조합이 없다면, 우리는 "이 조건들은 서로 모순되어 0 < 0 과 같은 터무니없는 결론을 이끌어낸다"는 것을 증명할 수 있다.

즉, **"해가 없다면, 그 이유를 논리적으로 증명해낼 수 있다"**는 뜻입니다. 이는 수학적으로 매우 강력한 도구입니다.

3. 이 논문의 첫 번째 업적: "컴퓨터가 직접 증명했다"

기존에 수학자들은 이 정리를 종이와 펜으로 증명해 왔습니다. 하지만 저자들은 Lean 4라는 컴퓨터 프로그램을 사용하여 이 정리를 코드로 작성하고, 컴퓨터가 한 단계 한 단계 논리적 오류가 없음을 검증했습니다.

• 비유: 마치 "이 요리 레시피가 정말로 실패할 수 없는지, 인공지능이 모든 경우의 수를 돌려보며 100% 확신하게 만든 것"과 같습니다.
• 의미: 인간의 실수나 착각을 완전히 배제하고, 수학의 진리를 디지털로 영구적으로 보존한 것입니다.

4. 이 논문의 두 번째 업적: "무한대 (Infinity) 를 허용하다"

기존의 수학 이론은 숫자가 유한할 때만 작동했습니다. 하지만 현실 세계에는 **'절대 불가능한 조건'**이나 '무한히 비싼 가격' 같은 개념이 있습니다.

• 예시: "렌틸콩이 품절되어 구할 수 없다"거나 "렌틸콩 가격이 1 억 원이다"라고 가정해 봅시다.
• 기존 방식: 렌틸콩을 아예 목록에서 지우고 다시 문제를 풀어야 했습니다. (컴퓨터는 행렬 크기가 바뀌는 것을 싫어합니다.)
• 이 논문의 혁신: 렌틸콩 가격을 **'무한대 (∞)'**로 설정했습니다.
  • 컴퓨터는 "가격이 무한대라면, 최적의 해는 렌틸콩을 0 개 사야 한다"고 자연스럽게 계산합니다.
  • 마치 **"무한대라는 마법의 숫자"**를 추가해서, 품절된 재료를 목록에서 지우지 않고도 자연스럽게 처리할 수 있게 만든 것입니다.

저자들은 이 '확장된 실수 (Extended Reals)' 개념을 포함하여 파르카스 정리와 '쌍대성 (Duality)' 이론을 다시 증명했습니다.

5. 쌍대성 (Duality): "원래 문제와 거꾸로 된 문제"

선형 계획법에는 **원래 문제 (Primal)**와 **쌍대 문제 (Dual)**라는 두 가지 관점이 있습니다.

• 원래 문제: "최소 비용으로 영양을 챙기자."
• 쌍대 문제: "영양 성분의 '가상 가격 (Shadow Price)'을 계산하자."

이 두 문제의 최적값은 서로 연결되어 있습니다. 이 논문은 무한대가 포함된 상황에서도 이 두 값이 완벽하게 일치 (또는 부호만 반대) 함을 컴퓨터로 증명했습니다.

6. 왜 이것이 중요한가? (일상적인 의미)

이 연구는 단순히 수학 이론을 증명하는 것을 넘어, 복잡한 현실 문제를 더 유연하게 모델링할 수 있는 길을 열었습니다.

• 실제 적용: 공장에서 기계가 고장 나거나 (무한대 비용), 특정 자원이 절대 불가능한 경우 (무한대 제약) 를 수학 모델에 자연스럽게 포함시킬 수 있게 되었습니다.
• 신뢰성: 컴퓨터가 검증했기 때문에, 이 이론을 바탕으로 만든 알고리즘 (예: 물류 최적화, 금융 모델링) 은 논리적 오류가 없을 것이라고 믿을 수 있습니다.

요약

이 논문은 **"수학의 고전적인 법칙을 컴퓨터로 다시 검증하여, '무한대'라는 새로운 개념을 포함시켜 현실 세계의 더 복잡한 문제 (품절, 불가능한 조건 등) 를 자연스럽게 해결할 수 있는 틀을 만들었다"**는 이야기입니다.

마치 **"오래된 요리책에 '불가능'이라는 재료가 들어갈 때에도 요리법이 깨지지 않도록, 새로운 규칙을 추가하고 그 규칙이 완벽함을 컴퓨터로 확인한 것"**과 같습니다.

기술 요약

이 논문은 선형 최적화 (Linear Optimization) 의 쌍대성 이론 (Duality Theory) 과 그 확장을 Lean 4 형식 증명 언어를 사용하여 엄밀하게 증명하고 확장한 연구입니다. 저자 Martin Dvorak 과 Vladimir Kolmogorov 는 기존의 유한한 실수 계수를 가진 선형 부등식 시스템에 대한 페르카스 (Farkas) 보조정리 및 쌍대성 정리를 일반화하고, 계수에 '무한대' 값이 포함될 수 있는 확장된 선형 프로그래밍 (Extended Linear Programming) 에 대한 새로운 이론을 수립하여 형식화했습니다.

다음은 논문의 기술적 요약입니다.

1. 연구 문제 (Problem)

• 선형 부등식 시스템의 해 존재성: 주어진 선형 부등식 시스템이 해를 가지는지 여부는 부등식들의 선형 결합을 통해 모순 (예: $0 < 0$) 을 유도할 수 있는지 여부와 동치라는 페르카스 보조정리 (Farkas' Lemma) 와 같은 대안 정리 (Theorems of Alternatives) 가 최적화 분야에서 핵심적입니다.
• 기존 이론의 한계: 기존의 형식화 작업들은 주로 유한한 실수 (또는 유리수) 계수에 국한되어 있었습니다. 그러나 실제 최적화 문제 (특히 이산 최적화) 에서는 '강제 제약 (hard constraints)'을 모델링하기 위해 목적 함수나 제약 조건의 계수에 무한대 값을 사용하는 경우가 많습니다.
• 무한대 계수의 처리: 전통적인 선형 프로그래밍 (LP) 은 무한대 값을 허용하지 않으므로, 이러한 '강제 제약'을 다루기 위해 별도의 기법 (예: 매우 큰 상수 사용) 이 필요했습니다. 이는 수학적으로 우아하지 않으며, 형식 증명 시스템에서 행렬 크기의 동적 변경을 피하기 어렵게 만듭니다.
• 목표: 선형 순서체 (Linearly Ordered Field) 위에서 페르카스 유사 정리들을 일반화하고, 계수에 무한대 ($\top, \bot$) 를 허용하는 확장된 선형 프로그래밍에 대한 쌍대성 이론을 Lean 4 에서 엄밀하게 증명하는 것입니다.

2. 방법론 (Methodology)

• 형식 증명 도구: Lean 4 와 수학 라이브러리 Mathlib 를 사용했습니다. 모든 논증은 논리적 공리 (propext, Classical.choice, Quot.sound) 에서 출발하여 기계적으로 검증됩니다.
• 대수적 구조의 일반화:
  • Bartl 의 일반화: 가환성이 보장되지 않는 선형 순서 나눗셈환 (Linearly Ordered Division Ring) 과 모듈 (Module) 구조를 활용하여 페르카스 정리를 일반화했습니다. 이는 행렬이 아닌 선형 사상 (Linear Map) 과 모듈 간의 관계를 다룹니다.
  • 확장된 선형 순서체 ($F_\infty$): 기존 체 $F$에 음의 무한대 ($\bot$) 와 양의 무한대 ($\top$) 를 추가한 구조를 정의했습니다.
    • 연산 규칙: $\bot + \top = \bot$, $0 \cdot \bot = \bot$ 등 특수한 규칙을 도입하여 대수적 구조를 유지하면서도 무한대 연산을 처리합니다.
    • 주의점: $F_\infty$는 더 이상 체 (Field) 가 아니며, 군 (Group) 도 아니지만, 밀집된 선형 순서 아벨 모노이드 (Densely Linearly Ordered Abelian Monoid) 로서 작동합니다.
• 확장된 선형 프로그래밍 (Extended LP):
  • 제약 조건과 목적 함수에 $F_\infty$의 원소를 포함시킵니다.
  • 유효성 (Validity) 조건: 무한대 값이 혼재될 때 모순을 방지하기 위해 행렬 $A$와 벡터 $b, c$에 대해 6 가지 전제 조건 (예: 같은 행에 $\bot$과 $\top$이 공존하지 않음 등) 을 정의했습니다.
  • 쌍대성 정의: 원문제 (Primal) 와 쌍대문제 (Dual) 를 정의하고, 최적값이 정의될 수 있는 조건을 명시했습니다.

3. 주요 기여 (Key Contributions)

1. Lean 4 에 의한 페르카스 정리의 형식적 증명:
   • 기존에 알려진 Farkas 정리 (등식형, 부등식형) 를 선형 순서체 위에서 증명했습니다.
   • Bartl 의 일반화 (Theorem 1.4 - 1.6): Bartl 의 정리를 기반으로, 비가환 나눗셈환과 모듈 구조를 포함하는 가장 일반적인 형태의 페르카스 정리 (fintypeFarkasBartl) 를 증명했습니다. 이는 행렬을 넘어선 선형 사상과 모듈의 관점에서 정리를 재구성한 것입니다.
2. 무한대 계수를 허용하는 새로운 쌍대성 이론:
   • 확장된 페르카스 정리 (Extended Farkas, Theorem 1.8): 계수에 무한대가 포함된 경우에도 성립하는 새로운 대안 정리를 제시했습니다. 이 정리는 무한대 값의 특수한 연산 규칙 ($\bot + \top = \bot$ 등) 을 고려하여 조건을 세밀하게 조정했습니다.
   • 유효한 확장 LP 의 강한 쌍대성 (ValidELP.strongDuality, Theorem 1.11): 6 가지 유효성 조건을 만족하는 확장된 선형 프로그래밍에 대해, 원문제와 쌍대문제의 최적값이 서로 부호만 반대임을 ($P^\star = -D^\star$) 증명했습니다.
3. 실용적 예시 (Cheap Lunch Problem):
   • 쌀과 렌틸콩을 이용한 영양 문제 (Diet Problem) 를 예로 들어, 렌틸콩이 품절되었을 때 가격을 무한대 ($\top$) 로 설정하여 LP 를 수정하는 방식이 기존 수치적 근사법보다 수학적으로 더 우아하고 직접적인 해결책을 제공함을 보였습니다.

4. 주요 결과 (Results)

• 정리 1.1 - 1.3 (기존 정리): 선형 순서체에서의 등식/부등식 페르카스 정리와 표준 LP 의 강한 쌍대성 정리를 Lean 4 로 재증명했습니다.
• 정리 1.4 - 1.6 (Bartl 일반화): 선형 순서 나눗셈환과 모듈 구조를 활용한 가장 일반적인 페르카스 정리를 증명했습니다. 이는 행렬 표현에 국한되지 않는 더 추상적인 수학적 구조를 다룹니다.
• 정리 1.8 (확장된 페르카스): 무한대 계수를 가진 행렬과 벡터에 대해, 특정 전제 조건 하에서 해의 존재성과 모순 도출 사이의 대안 관계를 증명했습니다.
• 정리 1.11 (확장된 강한 쌍대성): 유효한 확장 LP 에 대해, 원문제와 쌍대문제의 최적값이 항상 정의되며 서로 부호가 반대임을 증명했습니다.
• 반례 분석 (Section 7): 확장된 페르카스 정리와 유효한 쌍대성 정리를 성립시키기 위해 필요한 전제 조건 (예: 행렬의 특정 행/열에 $\bot$과 $\top$이 공존하지 않아야 함 등) 이 필수적임을 반례를 통해 보였습니다. 조건 중 하나라도 생략되면 정리가 성립하지 않음을 확인했습니다.

5. 의의 및 결론 (Significance)

• 수학적 엄밀성: 선형 최적화의 핵심 이론인 쌍대성과 페르카스 정리를 컴퓨터가 검증할 수 있는 형식적 언어로 완벽하게 재구성했습니다. 이는 추후 다른 최적화 알고리즘의 검증이나 SMT 솔버 개발의 기초가 될 수 있습니다.
• 실용적 확장: '무한대' 계수를 허용하는 새로운 이론적 틀을 마련함으로써, 강제 제약 (Hard Constraints) 이 포함된 복잡한 최적화 문제를 수학적으로 더 자연스럽게 모델링할 수 있게 되었습니다. 이는 기존에 '매우 큰 상수'로 근사하던 방식의 한계를 극복합니다.
• Lean 4 및 Mathlib 활용: Lean 4 가 추상 대수학 (모듈, 링, 체) 과 선형 대수학을 다루는 데 매우 효과적임을 보여주었습니다. 특히 행렬 연산과 무한대 값 처리를 위한 커스텀 정의와 증명이 필요했지만, 이를 통해 형식 증명 도구의 능력을 확장했습니다.
• 향후 연구: 이 작업은 선형 프로그래밍의 이론적 기반을 강화하고, 무한대 값을 포함하는 최적화 문제의 자동화된 분석 및 검증에 새로운 길을 열었습니다.

요약하자면, 이 논문은 선형 최적화의 고전적인 이론을 현대적인 형식 증명 기술로 재검증했을 뿐만 아니라, 무한대 값을 포함하는 확장된 맥락에서 새로운 쌍대성 이론을 수립하여 수학의 엄밀성과 실용적 적용 가능성을 동시에 높인 중요한 연구입니다.