الملخص
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 accepted, FYAN requires an explicit proof-transfer obligation connecting the formal statement back to a source-facing interpretation. With the same model (DeepSeek-V4.1-Flash) in every stage, FYAN proves 86 of 143 FormalTCS theorems under a strict Lean check, against 69 for a general agent harness, and raises the natural-language proof score from 0.501 to 0.851. On ConsistencyCheck, its semantic audit catches more inconsistent statements than a direct LLM judge, both on labels verified against the source (recall 0.777 vs. 0.636) and on the original labels (0.873 vs. 0.820), and localizes each mismatch it reports to a specific hypothesis, conclusion, or scope. FYAN also built ODENumLib, a 9,355-line Lean library for the numerical analysis of ordinary differential equation.
الكلمات المفتاحية
الموضوع
بيانات النشر
- المجلة
- غير متاح
- وصول مفتوح
- وصول مفتوح أخضر
اقتبس هذه المقالة
APA 7
Zhao, W., Zou, Y., Ding, C., Wu, Y., Wang, X., Mao, Z., Zhang, L., & Luo, T. (2026). Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization. https://omanscience.com/ar/articles/fyan-a-human-ai-harness-with-semantic-auditing-for-document-level-formalization
MLA 9
Zhao, Wei, et al. "Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization." https://omanscience.com/ar/articles/fyan-a-human-ai-harness-with-semantic-auditing-for-document-level-formalization.
شيكاغو (المؤلف–التاريخ)
Zhao, Wei, Yangshuo Zou, Chengxiang Ding, Yifan Wu, Xuchuan Wang, Zimu Mao, Lei Zhang, and Tao Luo. 2026. "Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization." https://omanscience.com/ar/articles/fyan-a-human-ai-harness-with-semantic-auditing-for-document-level-formalization.
هارفارد
Zhao, W., Zou, Y., Ding, C., Wu, Y., Wang, X., Mao, Z., Zhang, L. and Luo, T. (2026) 'Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization', Available at: https://omanscience.com/ar/articles/fyan-a-human-ai-harness-with-semantic-auditing-for-document-level-formalization.
فانكوفر
Zhao W, Zou Y, Ding C, Wu Y, Wang X, Mao Z, et al. Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization. https://omanscience.com/ar/articles/fyan-a-human-ai-harness-with-semantic-auditing-for-document-level-formalization
IEEE
W. Zhao, Y. Zou, C. Ding, Y. Wu, X. Wang, Z. Mao, L. Zhang, and T. Luo, "Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization," https://omanscience.com/ar/articles/fyan-a-human-ai-harness-with-semantic-auditing-for-document-level-formalization.