(자동) 형식화는 쉬워야 한다: 엄밀한 증명을 기술하기 위한 Trellis 프로세스 의미론

우리는 Trellis를 제시합니다. 이는 자연어 증명(natural language proofs)의 반복적인 정교화(iterative refinement)를 통해 Lean 자동 형식화(autoformalization) 작업에서 점진적인 진전을 강제하도록, 결정론적으로 제약된 워크플로(workflow) 내에서 LLM 에이전트(agents)를 활용하는 자동 형식화 시스템입니다. 우리의 접근 방식은 애초에 엄밀한 증명(rigorous proof)을 갖는다는 것이 무엇을 의미하는지에 대한 일반적인 수학자의 관념에서 동기를 얻었습니다. 즉, 증명의 어떤 부분이든 더 자세하게 상세히 기술하는 것이 일상적이어야 한다는 것입니다. 그 결과, 적은 비용과 범용 에이전트(generalist agents)를 사용하여 신뢰할 수 있는 자동 형식화를 달성하는 것을 목표로 하는 시스템이 탄생했습니다. 여기서 자동 형식화에 대한 전문화는 특정 작업에 특화된 에이전트 학습에서 오는 것이 아니라, 프로세스 의미론(process semantics)에 의해 강제되는 '엄밀함의 의미(meaning-of-rigor)'에서 영감을 받은 워크플로로부터 나옵니다. 우리는 이 프로세스를 통해 생성된 최근 Ramsey 이론(Ramsey theory)의 돌파구에 대한 엔드 투 엔드(end-to-end) Lean 형식화를 연결하여 보여줍니다.