Trellis는 LLM 에이전트를 활용해 Lean 자동 형식화 작업을 수행하는 시스템입니다. 수학자가 생각하는 엄밀한 증명의 개념, 즉 세부 사항을 쉽게 보충할 수 있는 증명을 목표로 합니다. 일반적인 에이전트만으로 제한된 예산으로 안정적인 자동 형식화를 달성하는 것을 목표로 합니다.
Trellis는 단계적 개선을 위해 자연어 증명을 반복적으로 개선하는 결정론적 제약 워크플로우를 사용합니다. 형식화 과정은 수학자가 엄밀한 증명을 어떻게 생각하는지에 영감을 받아 프로세스 의미론으로 시행됩니다.
최근 Ramsey 이론의 돌파구를 공식화하는 데 사용된 전체 Lean 형식화에 대한 링크를 제공합니다.