생성형 AI에다가 몇가지 정의와 공식을 때려넣으면
theorem과 proof까지 저절로 증명해내는 일이 생길지도 모른다는거임
그리고 그걸 인간이 해낸건지 AI가 해낸건지 숨기면 알수없다는거고
[일반] 수학계도 곧 AI에게 잠식당할거임
ㄹㄹ(175.125)
2024-01-20 09:45
추천 23
댓글 70
다른 게시글
-
수학과로서의 정체성이 생기기 시작하는 시기는 언제임? [7][일반] 익명(223.39) | 24.01.20추천 0
-
수학 6등급인데 [15][일반] 익명(175.209) | 24.01.19추천 0
-
정수론 문제풀다 생긴 궁금한점(디게 어렵고 쓸데없고 1줄요약있음) [2][대학교이상] 익명(118.235) | 24.01.19추천 0
-
PMA랑 김김계 차이 [3][일반] 익명(211.234) | 24.01.19추천 0
-
그 미식축구선수 수학자 [2][일반] 133(221.147) | 24.01.19추천 0
-
프렐리아 번역서 새책 어떰 [10][일반] 익명(223.39) | 24.01.19추천 0
-
수1 지수 [7][중고딩문제] 익명(223.39) | 24.01.19추천 0
-
해석개론 처음하는데 증명과정 피드백 부탁드립니다 [4][일반] 익명(175.121) | 24.01.19추천 0
-
수학 암기 vs 이해 [10][일반] 익명(106.241) | 24.01.19추천 2
-
급수가 한번에 이해가 안되는게 정상인가여 [3][중고딩문제] 익명(61.34) | 24.01.19추천 0
어 그래
뭐 얼마나 알고 하는 소리임? 학부생 따리면 웃음벨
수학 관련 갤러리에 와서 이딴글을 왜 적는지 잘 모르겠네. 역시 사람은 변하지 않는다.
ai에 대해 알기는 하고?
ai가 증명한 결과를 자세히 들여다보고 무슨 일이 일어났는지 해석하는건 여전히 사람의 몫임
요즘 바둑기사들이 알파고의 수들을 공부하는 것처럼, 수학자들이 신탁을 해석하듯이 AI의 증명을 공부하고 있을 생각하니까 소름 돋기는 하네요,,, ㅎㅎ
범용 수학 AI가 부조종사 역할부터 잘하면 다행이지.
10년만에 ai가 직업대체하는 분기점까지왓는데 너무 다들 회의적이네
최첨단 수학 문제를 알아서 풀어 주는 대화형 AI는 아직 없을걸.
Explainable ML이나 Automatic Reasoning은 아직 갈 길이 먼 듯. 또 LLM이 수학을 어처구니 없을 정도로 (기본적인 산수도) 못한다는 리포트도 본적있음.
> Prove that two sets A and B are equal to each other if and only if there exists a surjective function f : A → B that is also an identity function.
https://chat.openai.com/share/46a26c1a-aa9f-4a43-a50b-3f09e3c88755
챗GPT
3.5로 이 문제 풀게 하니까 제대로 답하긴 하네. 근데 어차피 이런 풀이도 사람이 검토해야 되는 거 알지?
검토는 컴퓨터가 훨씬 잘하지 않나요?
https://www.ams.org/journals/notices/202401/rnoti-p79.pdf
그건 첨부터 린(Lean) 같은 컴퓨터 언어로 수학 증명을 작성했을 때.
뭐 당연히 training set에 없을테니 지금은 안되겠지만, Output a proof of "..." in LEAN syntax 같은 prompt도 충분히 가능하죠
아직은 챗GPT 3.5와 4 모두 린 3와 린 4의 코드 구문 차이를 구별 못 해. 그리고 잘못된 구문을 고쳐도 증명이 틀렸고. 린 4로 재서술한 문제를 린 코파일럿(Lean Copilot)으로 풀려고 해도 증명을 완성하지 못해.
https://github.com/lean-dojo/LeanCopilot
지금 당장 된다는 건 당연히 아니고 (그냥 웹상에서 텍스트 긁어서 training한 건데, LEAN이 mainstream도 아니고 될리가 없겠지) 내가 말하고 싶었던 거는 사람이 "검토"할 이유는 없어보인다는 거임. "해석"이라면 몰라도. LEAN syntax의 proof를 query하고, 자동으로 검증할 수 있지 않겠냐는 거임. 아니면 처음부터 Retrieval-Augmented Generation 스타일로 접근해볼 수도 있겠고. 있을법하긴 한데, LEAN Copilot이라는 프로젝트가 실제로 있는지는 몰랐네ㅋㅋㅋㅋ 땡큐
> 내가 말하고 싶었던 거는 사람이 "검토"할 이유는 없어보인다는 거임.
음? 사람이 당연히 검토해야지. 헤더 맥베스 교수님이 검토해 보니, 알파지오메트리가 30문제 중에서 25문제를 푼 게 아니라, 32문제 중에서 21문제를 풀었다는데?
https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learning-for-Theorem-Proving/topic/AlphaGeometry/near/416337485
왜지? LEAN 프로젝트의 본질 중 하나가 검증을 인간 말고 컴퓨터에게 시키자는거 아님?
알파지오메트리 얘기를 사람이 검토해야하는 이유로 말한거라면, 서로 지금 얘기하는 게 아예 다른듯. 알파지오메트리는 output이 human-readable proof잖아. 그건 당연히 사람이 검토해야겠지. 내말은 애초에 AI에게 LEAN syntax로 된 증명을 요구하면 인간이 검증할 필요가 없다는거임.
아, 의사소통이 지금 살짝 잘 안된 거 같네. 컴퓨터 언어로 작성된 증명은 당연히 증명 검증기가 알아서 검증해 주지. 사람은 정리 증명 말고 정리 '진술'이 똑바로 쓰였는지만 검토하면 돼. 그런 뒤에 사람들이 그 증명을 '음미'하겠지. 하지만 알파지오메트리 같은 수학 AI가 형식 증명 말고 '자연 언어' 증명을 내놓을 때는 당연히 사람이 그 증명을 검토해야지. 그게 틀릴 수 있으니까.
> 근데 어차피 이런 풀이도 사람이 검토해야 되는 거 알지? '이런 풀이'는 '자연 언어로 쓰인 수학 증명'을 가리키는 거였어. 내가 공유한 챗GPT 3.5의 수학 풀이가 자연 언어로 쓰여 있잖아.
ㅇㅇㅇ 나도 같은 생각
ㅇㅇ 근데 그 문장의 의도가 "AI가 극도로 발전해도 '검토'라는 인간의 역할이 남아있다"라는 것처럼 읽혀서 해본 말임 ㅎㅎ
1. 형식 증명은 이미 한참 전부터 정리 검증기라는 컴퓨터 프로그램이 사람보다 훨씬 더 정확히 검증한다. (사실) 2. 인공 지능이 지금보다 발전해도, 그런 인공 지능이 내놓은 자연 언어 증명은 여전히 사람이 검토해야 할 것이다. (내 의견)
나의 주장: AI가 고도로 발전했는데 자연언어로 된 증명을 요청할 이유가 없다. 형식 증명을 요청하면 되기 때문. (만약 해석의 문제 때문에 자연언어로 된 증명을 요구하고 싶어 하는거라면, 형식 증명에 대한 자연언어 주석을 요구하면 될일임.) 그러므로 2번 진술은 별 의미가 없는 진술이다.
> AI가 고도로 발전했는데 자연언어로 된 증명을 요청할 이유가 없다. 이건 동의하지만, 인공 지능이 고도로 발전하지 않은 지금으로서는 비형식 증명만 생성하는 수학 인공 지능도 계속 개발될걸. 네가 말하는 수준의 인공 지능은 너무 먼 미래라고 생각한다.
학부 수준의 수학 공부를 해본 사람이라면 이런 말이 쉽게 나오지 않을텐데
정의가 주어져있을 때, 학부수준의 명제를 자동으로 증명해주는 것은 거의 10년 전에도 가능했던 것으로 알고 있습니다. 물론 당시에는 human-readable proof는 아니었구요. AlphaGeometry가 대단한 점은 "빠른" 시간 안에 human-readable한 증명을 주는 것인듯요. 예를 들어, AlphaGeometry 논문에서도 언급하고있는데, Tarski's axiom 기반으로 하는 방법론으로는 이틀 정도면 거의 임의의 평면기하 명제를 증명할 수 있다고 하네요.
내 말의 요점은 그게 아니었음. 학부 수학을 공부했다면 기본적인 수학적 지식을 갖고 있기 때문에 advanced한 분야들을 공부해 봤거나 대충 알아들을 수 있을 거고, 그러면 거기에서 얻어지는 결론들이 얼마나 심오한지 알 것임. 나도 딥러닝을 공부했지만 그냥 올림피아드 기하문제를 푸는 수준의(이건 사실상 주어진 문제에서 추가적인 도형들을 그리거나 이미 알려진 정리들을 적용해보거나 하는 방식을 통해 비교적 빠르게 해답에 접근할 수 있는 편임) 인공지능이 본문에서 말하는것처럼 빠른 시일 내에 수학의 최전선에서 직접 증명을 할 정도의 수준까지는 한참 멀었다는 것이 내 요지였음.
> 정의가 주어져있을 때, 학부수준의 명제를 자동으로 증명해주는 것은 거의 10년 전에도 가능했던 것으로 알고 있습니다. 학부 수준의 정수론, 위상 수학, 해석학 문제도 잘 푼다고 하나?
흠 미안 검색해도 잘 안나오는 것 보니 잘못된 정보인 것 같네. 10년 전 쯤에 automated theorem proving에 일가견이 있는 친구에게 들은 얘기인데, 내가 잘못 기억하거나 그 친구가 과장했거나...
지금도 학부 수준 간단한 명제조차 증명못하는데 뭔소리임
ㅇㅇ 그러네 미안미안
너 알파지오메트리 읽어보지도 않고 씨부리는거 들킴
그걸 특이점이라고 부름..
1. 정의가 주어져 있을 때 주어진 명제를 증명하는 것에 대해서는 어느 순간 컴퓨터가 인간을 넘어설 것이라는 데에 동의합니다. 지금 수준으로 봐서는 매우 오랜시간이 걸릴 것 같지만요.
2. 정의가 주어져 있을 때 컴퓨터가 “놀라운” 명제를 찾아서 증명하는 것에 대해서는 회의적입니다. 현재 머신러닝 패러다임은 데이터를 학습한 뒤에 “그럴듯한” 결과를 뱉는 방식입니다. 청출어람이 불가능한 구조죠. (한가지 예외로 강화학습이 있겠는데, 이 경우에도 “놀라움”을 평가하는 목적함수를 과연 정량화할 수 있을까요?) 그래서 ML에서 여러번의 거대한 혁신이 일어나지 않는 이상, 결국 수학자 뿐 아니라 모든 분야에서 일류는 살아남을 거라고 저는 생각합니다. 물론 아무도 관심 없는 세팅에서 살짝씩만 바꿔가며 붕어빵 찍듯이 논문 쓰는 삼류 수학자들은 필요 없게 되겠죠. (사실 이들이 필요 없는건 지금도 마찬가지... ㅎㅎ)
3. 더 나아가… AI가 정의를 할 수 있을까요? 정의는 일종의 세계관입니다. 가치판단의 영역이구요. 불가능이라고 말하기는 어렵지만, AI가 스스로 가치를 설정할 수 있게 되면 그 때부터는 AI가 아니라 사실상 하나의 생명으로 봐야하지 않을까요? 이런 맥락에서 결국 정의와 이론을 만드는 일류 수학자들은 건재할 것이라고 생각합니다. 한가지 생각해볼만한 지점은 Problem-solver보다는 Theory-builder들이 AI에게 대체당하기 더 어렵다는 것입니다. Theory-building이 더 고차원적이고 인간적인 활동이라는 것이겠죠.
당연히 ai가 수학 증명할 날은 옴 ㅇㅇ 중요한 질문은 그게 인간의 수학 이해에 도움이 되느냐 근데 증명 자동으로 해주는데 도움이 안될리는 없고 결국 사람이 읽고 이해해야 의미 있는것도 맞고 새로운 형태의 수학을 미래 사람들이 하고 있을듯
근데 그쯤이면 인간의 모든 지적활동이 ai로 대체된다는건데 음
인정하는데, 수학은 그래도 재미있어 !
최소 30년 이상 걸림
ㅋㅋㅋㅋ 여기 댓글 단 사람 중에 학계에서 3년 이상 연구한 박사 단 한명이라도 있을까 과연 존나 웃기네 진짜 ㅋㅋㅋ
알파지오메트리 제1저자가 다른 연구자들과 나눈 얘기를 볼 거면 아래로.
https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learning-for-Theorem-Proving/topic/AlphaGeometry/near/416600508
아니 여기에 남 얘기 말고 본인 생각 쓴 사람이 있겠냐고 연구인으로서
뭣도 모르는 애송이들이 어디서 주워듣고 남 얘기들 옮겨다가 왈가왈부 하는 게 웃음벨이라고 하는데 그걸 링크를 주네 내가 다 쪽팔린다
본문 내 글 아닌데 뭔 소리여
피아식별 잘해라 아군이다
ㅇㅇ 사랑해
미안하다. 아이피가 비슷해서 본문 글쓴이로 착각했네. 댓글은 삭제했음.
인용이라도 하는 애송이가 너처럼 비웃을 줄밖에 모르는 사람보단 나아 보이는데.
그리고 난 린 코파일럿이 예제 잘 푸는지 직접 확인한 결과를 언급했다고...
모르겠고 현장에서 연구하는 박사로서 내 의견 얘기한 거임. 물론 머신러닝 딥러닝 이용해서 수학적 문제 푸는 연구 활발히 진행되고 있는데, 무슨 수학계가 잠식 된다느니ㅋㅋㅋ 하는 터무니 없는 소리는 절대 할 단계 아님. 뭣도 모르면서 아는 체 망상질 하는 학부생 따리가 우스워서 단 댓글임.
아니 아무리 생각해도 적어도 본인이 제대로 된 연구랄 걸 한번이라도 해봐야 스스로 판단할 수 있는 거 아니냐고
> 모르겠고 댓글 내용 제대로 안 봤다고 시인한 셈. > 무슨 수학계가 잠식 된다느니ㅋㅋㅋ 하는 터무니 없는 소리는 절대 할 단계 아님. 당연하지.
> 아니 아무리 생각해도 적어도 본인이 제대로 된 연구랄 걸 한번이라도 해봐야 스스로 판단할 수 있는 거 아니냐고 그래. 우리가 인공 지능 특이점에 곧 도달할 거라고 사람들이 '성급하고 막연하게' 기대하게 된 건 인공 지능 연구 단체와 기업의 탓이 큰 거 같다.
슬프게도, "언젠간 인공 지능이 수학 정리를 사람보다 더 빠르고 정확히 증명할 겁니다."라고 단언하는 사람들이 이제 더 많아졌어.
다 동의해놓고 반박한 척 하는 건 뭐여. 침해 당하지 않을 인간의 일의 영역은 아직 확고하고 막연한 망상들 뿐인데 본문 제목대로 예언하듯 '수학계가 AI에 잠식될 것' 이라고 말하는 게 타당하다고?
성급하고 막연하게 개소리 떠들고 있다고 시인하면서 뭘 반박한 듯이 떠들고 있네
이 정도면 다 말한 것 같으니 여기서 끝내겠음
너 설마 내가 원글 글쓴이랑 같은 사람이라고 생각하는 거냐? 박사면 박사답게 맥락 좀 파악해라.
맥락을 보면 더 어이 없는데 왜 댓 단 거임? 동어 반복 코멘트 한 건가. 됐다 빠이
@175.121: 학부생들 망상에 왜 이렇게 화가 나셨어요 박사님... 애초에 디씨갤의 존재이유가 이런 잡담하는 광장 아님? 가시적인 결과만 논할거면 논문을 써서 arxiv에 올리겠지. 현장에서 연구하는 박사가 열을 내면 이번에 또 임용에 떨어진 스트레스를 수잘갤 와서 푸는 것처럼밖에 안보임
내가 디시하는 박산데? 으이? ㅋㅋㅋㅋ
ㅋㅋㅋㅋㅋㅋㅋ
Ood(out of distribution)이라 안됨 지금은 그림도 ood를 구별하니 마니 연구하는 수준인데 ood 내용까지 정확하게 학습해서 이해한다는건 좀..
특슬람 왔노
"It is an opinion, but I feel pretty confident that in a few years, AI will become not just an assistant, but better than humans at what professional mathematicians do today. And robustly better, so better at asking good questions, at solving them, at making definitions, categorizing them." (출처
https://www.youtube.com/watch?v=8DYF-ReeAtY
5분 30초부터)
나 고졸인데 특이점은 100년뒤에나 온다
5차 방정식의 일반해는 없지만 컴퓨터는 그걸 수치해로 풀어버린다는 사실이 놀랍지 않냐? AI도 마찬가지임, 더 이상 논리로 수학을 세우는것이 아니라 수치로 쌓아올려버리면 답도없음