論文の概要: Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization

• arxiv url: http://arxiv.org/abs/2609.39228v1
• Date: Wed, 30 Sep 2026 08:02:51 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-01 18:57:27.421708
• Title: Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization
• Title（参考訳）: Fyan: 文書レベルの形式化のためのセマンティック監査による人間-AIのハーネス
• Abstract要約: FYANは仕様、検証計画、論理的レビュー、リーン実証の構築、知識のキュレーション、検証にまたがるエンドツーエンドのワークフローをコーディネートする。 中心的なコンポーネントはエビデンスに基づくセマンティック監査(semantic auditing)であり、形式的なステートメントが彼らの非公式な仕様を忠実に保持するかどうかを評価する。 FYANはまた、通常の微分方程式の数値解析のための9,355行のリーンライブラリODENumLibも開発した。
• 参考スコア（独自算出の注目度）: 10.295359122542969
• License: http://creativecommons.org/licenses/by/4.0/
• 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 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.
• Abstract（参考訳）: 文書レベルの数学的形式化のための人間型AIハーネスであるFYANを提案する。 FYANは、定理を独立して扱うのではなく、仕様、証明計画、論理的レビュー、リーン実証の構築、知識のキュレーション、検証にまたがるエンドツーエンドのワークフローを調整し、独立した監督と人的指導をサポートする。 中心的な構成要素はエビデンスに基づくセマンティック監査(semantic auditing)であり、形式的なステートメントが彼らの非公式な仕様を忠実に保持するかどうかを評価する。 言語モデルは、局所的な対応、欠落、スコープ、論理的関係に関する構造化されたエビデンスを構築し、決定論的検証者は、このエビデンスをチェックし、再現可能な判断を生成する。 実体的だが許容できる偏差が受け入れられると、FYANは公式な文をソース対応の解釈に接続する明示的な証明-転送義務を必要とする。 同じモデル(DeepSeek-V4.1-Flash)でFYANは、厳密なリーンチェックの下で143のフォーマルTCS定理の86を一般エージェントハーネスの69に対して証明し、自然言語による証明スコアを0.501から0.851に引き上げる。 ConsistencyCheckでは、そのセマンティック監査は、ソースに対して検証されたラベル(0.777 vs. 0.636)と元のラベル(0.873 vs. 0.820)の両方で、直接LLM判事よりも一貫性のないステートメントをキャッチし、特定の仮説、結論、スコープに報告するそれぞれのミスマッチをローカライズする。 FYANはまた、通常の微分方程式の数値解析のための9,355行のリーンライブラリODENumLibも開発した。

関連論文リスト

• Truth for Believable AI: Expressed Doubt, Provenance, and Belief Revision as an Engineerable Stance [0.0]
  定型言語モデル上での動作層として,不確実性,先入観を意識したアサーション,明示的信念のリビジョンを実装できるかどうかを検証した。 合成モデルとQwen2.5-0.5B-インストラクタを用いて,機械的に評価したマルチセッションベンチマークを用いて評価を行った。
  論文  参考訳（メタデータ） (2026-09-22T11:34:53Z)
• FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence [9.041607777624504]
  FaithSieveは、自然言語の数学的証明を詳細に評価するためのリーン支援フレームワークである。 証明段階を局所的推論単位に分解し、型付き証明義務を抽出し、検証する。 350-problemのOlympiadデータセットでは、GPT-5.4バックボーンを使用したFaithSieveは81.43%の正確なファーストエラー精度を実現している。
  論文  参考訳（メタデータ） (2026-08-26T18:43:30Z)
• Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization [10.775710068605006]
  本稿では,評価問題とボトルネック帰属問題の両方として,忠実な文の形式化について検討する。 ツール拡張されたエージェントは89.5%のコンパイルに到達したが、コンセンサスの忠実度は60.5%に過ぎず、29.0ポイントのコンパイルパスを持つが、コンセンサスに反するギャップを露呈する。
  論文  参考訳（メタデータ） (2026-06-30T00:27:53Z)
• Decodable but Not Faithful: Coupling Natural-Language Rationales to Programmatic Verifiers [0.7212939068975618]
  言語モデルはそれらの予測に対して妥当な有理性を生成することができるが、これらの説明はモデルの内部的推論を忠実に表すものではないかもしれない。 本稿では,インラインクレームを推論トレースに挿入するフレームワークである検証器結合推論を提案し,プログラム的検証器出力を予測するための補助整合ヘッドを訓練する。 整合性トレーニングは、検証情報を合理性表現から復調可能にしますが、復調性は忠実な生成を保証しません。
  論文  参考訳（メタデータ） (2026-06-19T18:37:24Z)
• Faithful Autoformalization via Roundtrip Verification and Repair [0.4403025166321017]
  そこで本研究では,地平線アノテーションを必要としないラウンドトリップ検証手法を提案する。 2つの形式化が一致するとき、これは忠実な形式化の証拠となる。 我々はClaude Opus 4.6 と GPT-5.2 を用いて150のトラフィックルールに対するアプローチを評価した。
  論文  参考訳（メタデータ） (2026-04-27T22:26:01Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• Logical Satisfiability of Counterfactuals for Faithful Explanations in NLI [60.142926537264714]
  本稿では, 忠実度スルー・カウンタファクトの方法論について紹介する。 これは、説明に表される論理述語に基づいて、反実仮説を生成する。 そして、そのモデルが表現された論理と反ファクトの予測が一致しているかどうかを評価する。
  論文  参考訳（メタデータ） (2022-05-25T03:40:59Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。