We present Trellis: an autoformalization system that leverages LLM agents in a deterministically constrained workflow to enforce incremental progress in Lean autoformalization tasks through iterative refinement of natural language proofs. Our approach is motivated by the common mathematician's notion of what it means to have a rigorous proof in the first place: namely, that it would be routine to elaborate any part of the proof in further detail. The result is a system which aims to achieve reliable autoformalization on a modest budget and with generalist agents, with specialization to autoformalization coming not from any task-specific agent training but instead from a meaning-of-rigor inspired workflow enforced by process semantics. We link to an end-to-end Lean formalization of a recent Ramsey theory breakthrough produced by the process.

翻译：摘要：我们提出Trellis：一种自动形式化系统，该系统在确定性约束的工作流中利用LLM agent，通过自然语言证明的迭代细化，在Lean自动形式化任务中强制实现渐进式进展。我们的方法基于数学家关于何为严谨证明的普遍观念：即能够例行公事地阐述证明的任何部分，提供更详细的细节。该系统旨在以适度的预算和通用agent实现可靠的自动形式化，其针对自动形式化的专门化并非来自任何特定任务的agent训练，而是源自一种受“严谨性含义”启发、由过程语义学强制执行的工作流。我们通过该流程链接了近期拉姆齐理论突破的端到端Lean形式化。