5 Predicate Logic / 술어 논리 진술과 추론 규칙을 추가해서 확장한 명제 논리를 술어 논리라고 한다.
5.1 Quantifiers 정의. 기호 ∀은 "모두를 위해", "모두를 위해" 또는 "각자를 위해"라고 불립니다. 기호 ∃은 "어떤 것을 위해" 또는 "존재합니다"라고 불립니다.
5.2 Statements / 명제 정의. x가 임의의 변수이고 W가 x와 같은 유형의 식에 적용될 때 문에 평가되는 람다 식인 경우, (∀x, W(x))와 (∃x, W(x))는 모두 명제입니다.
5.3 Declarations / 선언 1. 변수(변수 선언) 로 선언 2. 상수(상수 선언) 로 선언 3. 임시적인 새로운 표기법으로 정의 4. 증명 시작 전에 주어진 전제 또는 전역적으로 선언된 전제에서 정리의 진술
5.4 Rules of Inference / 추론규칙 The rules of inference for these two quantifiers are as follows.
∀+ (Let s be arbitrary ⊢ W(s)) ⊢ (∀x, W(x)) ∀− (∀x, W(x)) ⊢ W(t) ∃+ W(t) ⊢ (∃x, W(x)) ∃− (∃x, W(x)) ⊢ For some constant c, W(c)
5.5 Equality / 동일성 등식/동일성 - 반사성 - A = B <-> B = A - 대체성 - A = B -> A+B = A + A = 2A
증명에서 전체에 대한 증명에서 많이 사용하는 For all (∀) 과 임의의 존재하는(∃) 에 대한 내용들이 나온다. 어떤 증명에서 해당하는 대상전체에 대한 증명어서는 "모든 x에 대해서" 라고 하고, 반례를 이용하여 증명하는 경우에 임의로 존재한다고 가정하는 "임의의 x"에 대해서라고 전개하는 경우에 사용된다. 소수의 무한성에 대한 유클리드의 증명에서 이것들을 생각할 수 있다.
소수(prime number)가 유한하다면, ∀ P_i 를 생각할 수 있고, 그 모든 수들을 곱하고 +1 을 하면 특정한 P를 만들수 있다. ∃P는 소수가 아니기 때문에, 1 과 자기 자신을 제외한 약수를 가져아 하지만, 모든 ∀ P_i 에 대해서 나누면 항상 1이 남기때문에 약수로 가질 수 없다. 그러므로, 처음 가정했던 유한성에 오류가 있고, 무한성이 증명되었다.
챕터 요약 (0. Introduction ~ 2. The Language of Mathematics)
0 Introduction 수학적 증명은 수학적인 사실을 결정하고 전달하기 위해서 필요한 객관성을 보여줄 수 있고 누구나 직접 확인해볼 수 있도록 한다. 이점이 공감대 형성에 도움을 줄 수 있다. 또한 공동작업을 위해서 필요한 가정, 용어, 사실에 대한 객관적인 출발점을 제공한다.
1 What is a proof? 증명은 어떤 명제가 객관적으로 옳은 이유를 설명하는 것이다. 이것을 위해서는 명제가 객관적으로 참임을 효과적인 방법을 통해서 설명하는 것이다.
형식적 증명 ( Formal proof) 과 전통적 증명(Traditional proof) - 형식적 증명: 기계로 검증이 가능하도록 엄정한 형식에 맞춰서 작성된 것 - 전통적 증명: 잘 정의된 방법들을 이용해서 지루하고 반복적인 부분을 제거한 것
1.1 Formal Proof Systems Definition 1. 형식적 증명은 명제들의 집합과 이것을 위한 추론 규칙(rules of inference)으로 구성된다.
Definition 2. 공리(axiom)은 증명이 필요하지 않는 추론 규칙들의 결론이다.
Definition 3. 어떤 명제가 증명가능하기 위해서는 그 명제가 선행된 명제(Q_1, ..., Q_n)들을 통한 결론이거나, 선행 명제로 필요한 명제들 (P_1, ... P_n)을 증명할 수 있을 때이다.
Definition 4. 선행하는 명제들이 없이 증명가능한 명제를 정리(theorem)이라고 한다.
Definition 5. 증명은 순차적으로 추론 규칙을 적용하여, 명제가 정리가 될 수 있음을 보이는 것이다.
1.2 Environments and Statements Environments serve two main purposes. - 특정한 가정이나 정의의 범위를 설정하고 알려주는 것. - ex) 이 증명에서 N 을 자연수의 집합으로 정의한다. - Notation. - 형식증명에서 P_1, ..., P_n 을 이용해서 Q를 증명할 수 있다면, 다음과 같이 표기합니다. - P_1, ..., P_n ⊢ Q - P_1, ..., P_n 은 증명에 대한 환경의 일부로 생각할 수 있고, 하위증명 혹은 명제(proposition)라고 합니다. - 여러 명제를 대상으로 확장 - P_1, ..., P_n ⊢ Q_1, ..., Q_m - ⊢ 의 왼쪽편인 P_1, ..., P_n 을 공리로서 가정한다면 , 오른쪽편인 Q_1, ..., Q_m 부분을 증명할 수 있다는 설명입니다.
2 The Language of Mathematics 2.1 Identifiers, Variables, and Constants - 수학에서 식별자(identifier)는 상수와 변수의 두 가지 종류가 있습니다. - 상수(constant) - 특정한 수학적인 대상을 지정하는 것 - ex) "π", ‘ln’, ‘cos’, ‘+’ - 변수(variable) - 특정한 유형의 값이 정해지지 않은 대상들의 이름 - ex) x, k, a, ...
2.2 Expressions and Statements - 단일 식별자는 기본문장(atomic expression)입니다. - 하나 이상의 식별자로 구성된 것을 복합문장(compound expression)이라고 합니다.
어떤 명제가 성립한다는 사실과 명제의 참, 거짓은 서로 독립적임.
2.3 Substitution and Lambda Expressions - Lambda Expressions - x 를 대상으로 하는 표현 E를 λx, E 형태로 기술 하는 방법
수학적 증명에서 사용하는 공리(axiom), 정리(theorem), 상수, 변수 같은 수학적인 용어와 개념들에 대한 간략한 설명이 나와 있는 부분이다.
6.1 Use Theorems as Rules of Inference 6.2 Substitute Logically Equivalent Expressions 6.3 Use Famous Logic Theorems Freely 6.4 Identify Certain Statements 6.5 Skip Some Logical Rules of Inference 6.6 Omit Most Premise Citations, Line Labels, and End-of-Subproof Symbols 6.7 Eliminate Extra Parentheses for Associative Binary Operators 6.8 Combine consecutive ∀+ rules 6.9 Use Transitive Chains! 6.10 Use Derived Rules of Inference
7 The Natural Numbers
7.1 The Peano Postulates 7.2 Strong Induction 7.3 Number Theory 7.4 Applications: Cardinal and Ordinal Numbers
8 Sequences
8.1 Finite and Infinite Sequences 8.2 Representations of Sequences 8.3 Reindexing 8.4 Recursive Definitions and Sequences
9 Integer, Rational, and Real Numbers
9.1 Notation 9.2 The Axioms for Real Numbers 9.3 Basic Properties of Real Numbers 9.4 Integers 9.5 Extending Definitions 9.6 Infinite Series and Decimal Representation
10 Sets, Functions, Numbers
10.1 Basic Definitions from Set theory 10.2 Shortcuts involving sets 10.3 Famous Sets of Numbers 10.4 Functions 10.5 Relations
11 Expository Proofs
11.1 Traditional Proofs 11.2 Specific Rules for Mathematical Writing 11.3 Notation 11.4 Syntax 11.5 Equations and Formulas 11.6 Writing Technique 11.7 Mathematical Typesetting
12 Combinatorial Proofs 12.1 Combinatorics 12.2 Combinatorical Collections and Expressions 12.3 Combinatorial Proofs 12.4 Combinatorial subtraction, division, and inequality
다른 강의 목차들을 참고하면, 많은 경우에 Set theory 에서 시작하는데, 이 강의에서는 증명 방법 자체에 대한 용어에 대한 부분으로 시작하고, 집합에 대한 내용은 후반부에 나온다. 다만, 수학적인 증명이 잘 보이는 기학학에 관련된 부분이 없는데, 이 부분을 보충하기 위해서, 기학학 정리와 관련된 문제들을 찾아서 같이 연결해서 살펴보려고 한다. 목표한 일정은 일주일에 한번정도 페이지를 정리해보려고 생각하는데, chapter 5 까지 내용을 정리해서 2~3회차로 정리하고, 6~12 까지는 한 chapter를 1~2회차로 정리할 생각이다. 여기에 기하학에 대한 내용들을 약간 보충하려고 한다. 전체 11~14회차로 정리할 수 있을 것으로 생각한다. 목표대로 진행한다면 8월까지 진행하면 마무리 할 수 있을 것 같다.
작년말에 등장한 OpenAI의 ChatGPT 이 세상에 가져온 영향이 크다. 많은 사람들이 AI 기술의 발달을 확인할 수 있었고, 단순한 지식의 축적과 요약에 있어서는 아주 뛰어난 성능을 보여줬다. GPT는 Generative Pre-trained Transformer 를 말하는데, LLM-Large Language Model-의 한가지이다. 내가 이해한 간략한 원리는 단어들 사이의 상관관계를 확률모델로 구현하는데, 아주 많은 자료 입력을 통해서 유의미한 상관관계에 따른 결과를 만들어 내는 것이다. 이것은 확률에 기반해서 결과를 만들어 내는 것이기 때문에, 논리적인 추론에 기반하여 만들어진 결과가 아니다. 언어로 기술된 내용들의 요약이나 결과 추출은 유의만한 결과를 보여주지만, 수학적인 내용에 서는 약점을 보인다.
수학적인 증명에서 어떤 명제는 참 혹은 거짓 중 하나가 된다. 증명과정은 참으로 확인된 내용들을 연결하여 완결된 증명을 한다. 중간에 확률이 개입하여 결과에 영향을 줄 수 있는 여지가 없다. 하지만, LLM의 학습을 위해서 사용하는 자료들에 포함된 수식을 식별하고 분리하는 어려움 한가지는 쉽게 예상해 볼 수 있다. 많은 수학 수식을 표현하기 위해 사용되는 것은 LaTex에 기초를 둔 TeX 문법을 적용한다. 이 표현은 처리를 거치기 전에는 수식의 형태가 나타나지 않는다. 하지만, 그런 내용은 학습과정에서 충분히 해결 가능하다고 하고, 아래 같은 경우를 생각해보자.
1+1 = 10, 2+2 = 11, 3+3 = 12, 4+4 = 13, ...
이런 수삭들이 있다고 하면, 일견 수학적으로 오류가 있다고 할 수도 있다. 하지만, 진법이라는 수학 개념을 적용한다면 모두 참인 명제이다. 이진법으로 계산하는 1+1=10 또한 맞으며, 4+4 = 13, 이것은 5진법으로 계산하면 맞는 얘기이다. 이런 모든 명제가 참으로서 훈련된다면, 어떤 수식 계산에서 = 가 나타났을 때 이러한 진법의 개념이 동반되지 않고 이전된다면 잘못된 명제 진행이 된다. 이런 문서들을 모두 배제할 수 없다. 이것도 수학의 일부분이며, 전산학의 기본은 0/1을 이용한 이진법에 기반하고 있고, 아날로그에 기반하는 회로라가 하면 multi-nary가 가능할 수 있다. 쉽게 생각해볼 수 있는 명제 하나를 얘기해보자.
- 삼각형의 내각의 합은 180이다.
이것은 "평면에서 한 직선과 평행하고 한점을 통과하는 직선의 유일성"에 기반한 명제이다. 이 공리를 배제한 비유클리드 기하학에서는 적용할 수 없는 명제이다. 즉, 수학적인 명제를 정확하게 정의하고 설명하기 위해서는 그 명제가 위치해 있는 그 영역에서만 적용할 수 있다는 것이다. 영역이 바뀌면, 기본 적인 명제들도 바뀌는 것이다. 그렇게 때문에, LLM에서 질문에 대한 답변은 다양한 영역에서 가장 비슷해보는 명제들을 엮어서 만들어 낸다. 하지만, 그 질문에 해당하는 영역에만 한정해서 답변을 만드는 것이 아니기 때문에 나오는 답변은 오류를 포함하고 있을 가능성이 높다. 실제 최근에 나온 LLM에서 수학문제 해결에 대한 결과는 다음에서 참고할 수 있다.
Model
MATH
MMLU-STEM
OCWCourses
GSM8k
Minerva
50.3%
75%
30.8%
78.5%
Published state of the art
6.9%
55%
-
74.4%
Minerva 540B significantly improves state-of-the-art performance on STEM evaluation datasets.
지식의 축적과 이해는 중요하다. 그렇지만 최근에 보이는 인공지능의 발전 방향을 생각하면 이런 수학적 엄밀한 증명방법을 익히고, 준비하는 것이 앞으로는 더 필요할 것으로 생각한다. 그래서, 여기에 관련된 내용들을 정리해보려고 한다.
엄밀한 수학적 증명을 배울 수 있는 방법을 찾아보면, 수업이나 교재가 많지 않다. 알려져 있는 증명 단계들을 따라하면서, 개인마다 논리적인 방법이나 과정을 배우는 방법이다. 실제로 수학적인 증명을 위해서는 영역마다 필요한 사전 지식들이 필요하다. Axiom - Theorem 들이 이런 것들이다. Euclid's Elements 경우도 정의(definition), 공리(axiom), 가정(postulate), 통념(common notion)에 기반하여 전체 명제들을 세우고 증명해 나간다. 이런 전체 과정에서 엄밀함을 만들어 가는 과정이 수학적 증명이라고 하겠다.
대학에서 수학을 전공하면 들어야 하거나 선택할 수 있는 수업들이 있기다. 아래의 두강의는 강의 노트를 확인 할 수 있는 수업들이다. 각 대학마다 비슷한 과목들이 있고, 그 내용을 소개하는 페이지들을 찾을 수 있을 것이다.
4면체 주사위 3개(A, B, C) 가 있고, 주사위의 각 면의 숫자는 1부터 10 사이의 숫자이다. 두 주사위를 던져서 높은 숫자가 많이 나오는 주사위가 이겼다고 할때, A > B > C > A 혹은 A < B < C < A 가 되는 조합이 있는지 판별하는 문제이다. 입력으로는 주사위 A, B의 숫자들이 주어진다.
주사위 C의 숫자들이 1 ~ 10 이고, 4개의 숫자를 선택할때 가능한 모든 조합 O(N^4)를 해도 10^4 이고, 주사위 2개를 비교해서 편정하는 경우도 4^2 이므로, 전체 계산량은 대략 10^5 정도로 가능하다. 중첩된 Loop 로 모든 경우를 비교하는 알고리즘으로 가능하다.
길이 N 인 두개의 배열 A, B 가 있고, 배열 A 를 버블정렬로 정렬하는 과정에서 배열 B 와 같은 경우가 있는지 확인하는 문제
입력
배열 크기 N 과 두 개의 크기 N 인 정수 배열 A, B
출력
정렬하는 과정에서 같은 경우가 있으면 1 , 없으면 0
입력 예
6
4 6 5 1 3 2
4 1 3 2 5 6
출력 예
1
제약조건
5 <= N <= 1e4, 1 <= a_i, b_i <= 1e9
문제 풀이
Brute force 를 적용하면 bubble sort - O(N^2) 이고, 한번 swap 을 할 때 마다 길이 N 인 두 배열을 비교한다면 추가로 O(N) 이 필요해서, 전체는 O(N^3) 이 되고, 필요시간이 길어져서, 제한시간안에 해결할 수 없다. ( N=10000 인 경우 O(N^3) 이면 1e12 정도의 계산이 필요하고, 보통 1e9 정도의 계산이 제한시간의 경계이다.)
먼저 확인할 것은 주어진 배열이 서로 순서만 다른 배열인지 아니면 내부에 값들이 다른 서로 다른 배열인지 구분해야 한다. 서로 다른 배열이라면, 정렬과정에서 같은 경우가 나올 수는 없다.
다음으로 순서만 서로 다른 배열이라고 하면 제일 앞에서부터 어디까지가 같은지 비교한 위치를 기록해서 그 이후 값들의 비교를 중심으로 비교하는 과정에서 중복을 줄일 수 있다. 앞에서부터 배열 A 와 배열 B 를 비교해서 일치하는 위치를 m_end로 기억한다. 배열 A를 정렬하는 과정에서 서로 바뀌는 위치를 k 라고 할 때, k < m_end 인 경우는 계속되는 정렬과정에서 원래 있던 값으로 돌아 갈 수 없으므로 실패가 된다. 또한 m_end < k 인 경우에는 배열 A 와 배열 B 를 비교하면서, 마지막 일치하는 위치 이후의 값들만 비교하고, 계속해서 m_end 값을 갱신해서, 추가적으로 비교해야 하는 경우를 줄 일 수 있다.
문자열 비교를 어떻게 할 것인가 하는 문제이다. 입력으로 주어진 3 x 3 퍼즐을 1 x 9 형태로 바꿔도 문제 풀이에 영향은 없다. char[9] 인 두개의 배열/vector를 만들어서 예상 답안과 실제 답안을 입력하고, 전체를 비교해서 같으면 Green 값에 반영한다. 다음은, 두 답안의 A~Z의 빈도를 확인해서, 잘못된 위치지만 있었는지 확인해서 Yellow 값에 반영한다. 다만, Green 에 반영된 결과를 두번 세지 않도록 해줘야 한다.
N을 만드는 곱할 수의 개수(n), 곱할 수들(n_1, ... , n_n) 열, M을 만드는 곱할 수의 개수(m), 곱할 수들 (m_1, ..., m_m)
출력
최대 공약수를 출력한다. 단, 최대 공약수가 1e9 보다 크다면 마지막 9자리만 출력한다.
입력 예
3
2 3 5
2
2 5
출력 예
10
제약조건
1 <= N, M <= 1000, 1 <= n_i, m_i <= 1e9
문제 풀이
곱해서 만들어지는 큰 수를 A, B 라고 할때, prime factorization 을 하면, A = p1^a1 x p2^a2 ... B = p1^b1 x p2^b2 ... 형태로 쓸 수 있고, 같은 소수가 있을 때 그중 거듭제곱이 낮은 것들을 골라서 모두 곱하면 최대 공약수가 된다. 이것을 위해서 곱해서 만들어지는 수들을 각각 소인수분해를 하고 그것을 map<int, int>에 저장한다. 나중에 하나를 기준으로 작은 것들을 골라서 곱하고 크기가 1e9과 비교해서 더 커지지 않는지 확인해서 출력한다. Modulo 연산은 곱셈에 닫혀 있으므로 곱하는 중간에 처리해도 결과 값은 달라지지 않는다.
for(map<int, int>::iterator it = f_n.begin(); it != f_n.end(); ++it)
{
int prime;
int power;
prime = it->first;
power = min(it->second, f_m[prime]);
// cout << prime << " " << power << "\n";
for(int i = 0; i<power; ++i)
{
ans *= prime;
if(ans >= MAX_F)
{
ans %= MAX_F;
flag = true;
}
}
}