딥러닝으로 증명하기(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)들이 빠르게 이 분야의 지형을 바꾸고 있다. 이런 배경 속에서 만들어진 DL4TP는 논문, 데이터셋, 튜토리얼, 작업 분류 등 연구에 필요한 자료들을 구조적으로 정리해 놓은 Git 레포지토리다. 이 레포지토리는 관련 연구를 시작하려는 사람들에게 큰 도움이 될 것이다.

2. DL4TP가 유용한 대상

DL4TP는 특히 다음 같은 사람들에게 실용적이다:

• ‘머신러닝 + 수학/형식증명’ 융합 분야를 처음 조사하는 학생/연구자
• 자동 증명을 직접 연구하거나 구현하려는 사람
• 증명 데이터셋 및 기존 접근법을 빠르게 탐색하고 싶은 사람

특히 프로젝트를 준비하는 입장에서 자료를 조사하기에 최적의 자료다.

3. DL4TP에서 눈여겨볼 핵심 논문 소개

아래는 DL4TP 중, 분야를 처음 접하는 사람이 반드시 참고하면 좋은 핵심 논문들이다:

1. First Experiments with Neural Translation of Informal to Formal Mathematics
   1. 이 논문은 비공식적인 LaTeX 형식의 수학 텍스트를 공식적인 Mizar 언어로 자동 번역하기 위해 딥러닝 신경망을 적용한 최초의 실험 연구이다.
2. Learning Alignment between Formal & Informal Mathematics
   1. 이 논문은 자연어로 된 비공식 수학 텍스트와 공식 수학 언어를 준지도 학습 방식으로 훈련하여, 자동 형식화하는 연구이다.
3. Autoformalization with Large Language Models
   1. 이 논문은 대규모 언어 모델(LLM)을 활용해 성능을 29.6%에서 35.2%로 향상시킬 수 있음을 입증한 연구이다.

4. DL4TP의 한계 & 앞으로의 과제

DL4TP는 매우 유용한 리소스 허브지만, 몇 가지 한계도 존재한다.

• 연구 논문 수는 많지만, "완전한 자동 증명 시스템" 수준의 안정성, 확장성은 여전히 미완성이다.
• 정리 증명기(Lean, HOL, Coq 등)마다 구조가 다르기 때문에 논문이 사용하는 체계가 제각각이며, 직접 사용할 때는 각 시스템의 제약을 이해해야 한다.
• 논문과 데이터셋 링크는 풍부하지만, '즉시 실행 가능한 통합 프레임워크' 형태는 아니라 사용자가 직접 환경 세팅과 실험 설계를 해야 한다.

즉, DL4TP는 연구 방향을 잡고 핵심 자료를 빠르게 찾기 위한 용도로 사용하면 이상적일 것이다.