精选理由
Trellis 解决了自动形式化中可靠性与成本之间的平衡问题，做定理证明或形式化验证的开发者可以直接用这个工作流来生成 Lean 证明，值得关注其开源实现。
Trellis 是一个自动形式化系统，利用 LLM 智能体在确定性约束的工作流中，通过迭代优化自然语言证明，逐步推进 Lean 自动形式化任务。该系统受数学家对“严谨证明”的直觉启发——即证明的任何部分都可以被进一步详细阐述。Trellis 在有限预算下使用通用智能体实现了可靠的自动形式化，其专业化来自“严谨性”含义驱动的工作流，而非特定任务训练。论文还展示了该系统生成的 Ramsey 理论最新突破的端到端 Lean 形式化证明。
AI 翻译 · 中文
Trellis 是一个自动形式化系统，利用 LLM 智能体在确定性约束的工作流中，通过迭代优化自然语言证明，逐步推进 Lean 自动形式化任务。该系统受数学家对“严谨证明”的直觉启发——即证明的任何部分都可以被进一步详细阐述。Trellis 在有限预算下使用通用智能体实现了可靠的自动形式化，其专业化来自“严谨性”含义驱动的工作流，而非特定任务训练。论文还展示了该系统生成的 Ramsey 理论最新突破的端到端 Lean 形式化证明。
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 natura…