딥러닝으로 증명하기(DL4TP) https://github.com/ZHAOYU-LI/dl4tp 1. DL4TP란 무엇인가? Welcome to our repository! This is a curated collection of resources related to deep learning for theorem proving. 수학 정리 증명(Theorem Proving) 분야는 오랫동안 사람이 작성한 논리 규칙 등에 기반해 발전해왔다. 하지만, 최근에는 대형 언어 모델(LLM)들이 빠르게 이 분야의
TCP와 UDP로 알아보는 네트워킹 우리는 대 인터넷의 시대에 살고 있다. 우리는 도서관에 가서 종이들을 뒤지는 대신 구글에 검색하고 ChatGPT와 말씨름을 벌인다. 친구와 같이 비디오 게임을 하기 위해 오락실으로 갈 이유도 없다. 각자의 집에서 원격으로 접속하면 되지 않는가? 혹자는 작금 인류사상 최고의 발명품으로 꼽는 이 인터넷은, 어떻게 작동하는 것일까? 이 질문의 답변은 너무나 방대하여 차마
레드스톤으로 이해하는 논리 회로 와 마인크래프트라니. Logicae에는 어울리지 않을 수 있다. 하지만, 마인크래프트의 레드스톤과 커맨드 영역 만큼은 Logicae에서 다뤄질 자격이 있다고 생각한다. (아님 말고) 레드스톤은 마인크래프트 세상 속에서 전기의 역할을 한다. 레드스톤을 이용하여 수많은 장치를 만들고 이용할 수 있다. 필자는 마인크래프트에서 레드스톤을 매우 높게 평가한다. 이 글에서는 레드스톤을 이용하여 만든 논리 회로에 대해 설명하겠다.
시간복잡도 백준같은 곳에서 알고리즘을 공부하다 보면 필연적으로 시간복잡도라는 개념을 한 번쯤은 보게 된다. 단순히 어떤 알고리즘의 시간복잡도가 \(\mathcal{O}(n^2)\)라는 것을 입력의 크기가 \(n\)일 때 최악의 경우에 실행 시간이 \(n^2\)에 비례한다는 것만 알아도 알고리즘 문제를 푸는 것에는 큰 영향이 없지만, 이 글에서는 시간복잡도의 수학적 정의에 대해서
시리즈 | Deep Learning - 3. 인공신경망의 동작 딥러닝 시리즈 2편에서 딥러닝의 기반이 되는 퍼셉트론과 인공신경망에 대해 다루었다. AND 게이트, OR 게이트, XOR 게이트 등 몇몇 예시를 통해 이러한 구조가 특정 작업들을 수행할 수 있음은 확인했지만, 구체적으로 어떻게 동작하는지, 이러한 구조가 일반화될 수 있는지에 대해서는 아직 다루지 않았다. 특히 중요한 것은, 앞선 2편에서 다룬 신경망 구조에서는 특정 작업을
CS - 뫼비우스 함수 Introduction 혹시 궁금해하는 사람을 위해 미리 말해두지만, 이 뫼비우스가 아니다. 이분이다. 이름 자체는 수학 함수의 대부분이 그렇듯이 만든 사람 이름 따온 별거 아닌 것 같지만, 그 효과만큼은 대단하다. 오늘은 뫼비우스 함수, 그리고 그것을 확장한 뫼비우스 반전 공식을 살펴보자. Before We Begin.. 시작하기 전에, 함수들이 어떻게 생겼는지 정도만 알아보고 가자. 뫼비우스