כתבה
arXiv cs.AI ·
FYAN: תיקון ואודיט סמנטי להפורמליזציה של תאורמות
Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization
FYAN היא תקינה-אי-אי של תאורמות, המשלבת תיקון ואודיט סמנטי. היא משתמשת ב-DeepSeek כדי להפורמליזר תאורמות ולבדוק את התיקונים. FYAN יכולה להפורמליזר 86 מ-143 התאורמות של FormalTCS.
תקציר מקורי באנגליתarXiv:2609.39228v1 Announce Type: new Abstract: We present FYAN, a human--AI harness for document-level mathematical formalization. Rather than treating theorems in isolation, FYAN coordinates an end-to-end workflow spanning specification, proof planning, logical review, Lean proof construction, knowledge curation, and validation, with support for independent supervision and human guidance. A central component is evidence-grounded semantic auditing, which assesses whether formal statements faithfully preserve their informal specifications. A language model constructs structured evidence over local correspondences, omissions, scope, and logical relations, while a deterministic validator checks this evidence and produces reproducible judgments. When a substantive but admissible deviation is
קרא במקור המקורי
arxiv.org
פתח כתבה מקורית