형식과 비형식의 가교: LLM 시대의 DSL 설계

2025-06-17

이 글에서는 DSL과 LLM의 교차점에서 새로운 방향을 탐구합니다. 바로 LLM 기반 코딩 워크플로우와 원활하게 통합되는 DSL을 설계하는 것입니다. 저자는 LLM을 사용하여 스크립트를 생성한 경험을 자세히 설명하며, LLM이 '연결 코드' 생성에 탁월함을 발견했습니다. 즉, 자연어 설명을 기반으로 보일러플레이트 코드를 생성하지만 복잡한 로직은 수동으로 코딩해야 합니다. 이 경험을 통해 LLM 지원 워크플로우를 DSL 자체에 어떻게 통합할 수 있는지에 대한 중요한 질문이 제기됩니다. 최종 목표는 형식적인 코드와 비형식적인 자연어 사양 간의 격차를 메우는 것이며, DSL의 형식 분석을 기반으로 자연어 사양을 자동으로 생성하는 것이 가능할 것입니다.

더 보기
개발

수학적 증명의 시각화: Lean Blueprints의 통찰

2025-05-11

Lean Blueprints는 수학자들이 증명을 공식화하는 데 사용하는 청사진 방법에서 영감을 받은 프로젝트 계획 도구로, 증명 과정에 대한 독창적인 통찰력을 제공합니다. 노드가 정의, 보조정리, 정리 등을 나타내고 색상이 상태를 나타내는(녹색: 증명됨, 파란색: 진술되었지만 증명되지 않음, 검정색: 미작성) 그래프를 사용합니다. Lean 프로젝트(예: Terrence Tao의 PFR 추측 공식화)의 버전 관리를 추적함으로써 증명의 진화를 시각화하고 수학자들의 작업 방식과 그들을 지원하는 도구를 구축하는 데 도움이 되는 데이터를 제공할 수 있습니다. 이 시각화는 수학적 증명의 구성 방법에 대한 이전에는 숨겨져 있던 통찰력을 제공합니다.

더 보기
개발 공식 증명