論文の概要: Beyond LLM Judge: Mechanical Verification for Agentic Autoformalization

• arxiv url: http://arxiv.org/abs/2610.20573v1
• Date: Wed, 14 Oct 2026 17:54:48 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-15 21:06:16.289437
• Title: Beyond LLM Judge: Mechanical Verification for Agentic Autoformalization
• Title（参考訳）: LLM判決を超えて:エージェントオートフォーマライゼーションのための機械的検証
• Abstract要約: LLM-judgedの忠実性を超えて、リーンの形式化を検証する新しい方法を紹介します。 LLMに基づくセマンティックレビューとメカニカル数値と空き度チェックを組み合わせることで,チェック可能なフィードバックを提供する。 本稿では,NIST Digital Library of Mathematical Function (DLMF) の部分的な形式化であるFLMF (Formalized Library of Mathematical Function) の構築に本手法を適用した。
• 参考スコア（独自算出の注目度）: 0.6875312133832079
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We introduce a novel method for verifying Lean formalizations that goes beyond LLM-judged faithfulness. Unlike most verification methods, which rely on LLMs or trained models, our method combines LLM-based semantic review with mechanical numerical and vacuity checks, providing checkable feedback and detecting errors missed by LLM judges. We apply this method, along with our Extract-Verify-Proof autoformalization pipeline, to construct the Formalized Library of Mathematical Functions (FLMF), a partial formalization of the NIST Digital Library of Mathematical Functions (DLMF). On three labeled datasets, our method achieves the lowest accepted-error rate among the evaluated methods, measured as the fraction of incorrect statements accepted by the verification method. Expert review of the results also identifies translation and source defects in existing datasets. Code available at https://github.com/annamei1/FLMF-Ch7ErrFunc-Release.git.
• Abstract（参考訳）: LLM-judgedの忠実性を超えて、リーンの形式化を検証する新しい方法を紹介します。 LLMや訓練されたモデルに依存するほとんどの検証方法とは異なり、LLMに基づくセマンティックレビューと機械的数値と空き度チェックを組み合わせ、チェック可能なフィードバックを提供し、LLMの審査員が見逃した誤りを検出する。 本手法は,数式関数の形式化ライブラリ (FLMF) を構築するために,抽出-検証-証明自動形式化パイプラインとともに,NIST Digital Library of Mathematical Function (DLMF) の部分形式化を行う。 3つのラベル付きデータセットにおいて,提案手法は評価手法の中で最小のエラー率を達成し,検証手法が受け入れた誤り文の分数として測定した。 結果のエキスパートレビューでは、既存のデータセットの翻訳とソースの欠陥も確認されている。 コードはhttps://github.com/annamei1/FLMF-Ch7ErrFunc-Release.gitで公開されている。

関連論文リスト

• DiffuRank: Effective Document Reranking with Diffusion Language Models [71.16830004674513]
  拡散言語モデル(dLLM)に基づいて構築されたフレームワークであるDiffuRankを提案する。 dLLMは、左から右への順序に制約されないより柔軟なデコーディングと生成プロセスをサポートする。 モデルサイズが類似した自己回帰LDMに匹敵する性能を示す。
  論文  参考訳（メタデータ） (2026-02-13T02:18:14Z)
• Reasoning-CV: Fine-tuning Powerful Reasoning LLMs for Knowledge-Assisted Claim Verification [17.35114345065597]
  CoT(Chain-of-Thought)-Verifyパラダイムは、サブステートへの分解を必要とせず、検証段階を分離することなく、元の複雑クレームに対するCoT検証パスを生成する。 Reasoning-CVは既存のDecompose-Then-Verify法よりも優れた知識支援クレーム検証性能を示す。
  論文  参考訳（メタデータ） (2025-05-18T10:28:54Z)
• To Err Is Human; To Annotate, SILICON? Reducing Measurement Error in LLM Annotation [11.470318058523466]
  大規模言語モデル(LLM)は、人間のアノテーションに代わる費用対効果の高いスケーラブルな代替を約束する。 LLMアノテーションから測定誤差を体系的に低減するSILICON手法を開発した。 この証拠は,各エラー源の削減が必要であり,SILICONは管理研究において厳密なアノテーションをサポートしていることを示唆している。
  論文  参考訳（メタデータ） (2024-12-19T02:21:41Z)
• Evaluating the Correctness of Inference Patterns Used by LLMs for Judgment [53.17596274334017]
  我々は,LLMの詳細な推論パターンの正確さを,その正しい出力の裏側で評価した。 実験により、言語生成結果が正しそうであっても、LLMが法的な判断に用いた推論パターンのかなりの部分は、誤解を招く論理や無関係な論理を表す可能性があることが示された。
  論文  参考訳（メタデータ） (2024-10-06T08:33:39Z)
• Large Language Models for Anomaly Detection in Computational Workflows: from Supervised Fine-Tuning to In-Context Learning [9.601067780210006]
  本稿では,大規模言語モデル(LLM)を用いて,複雑なデータパターンの学習能力を活用することにより,ワークフローの異常検出を行う。 教師付き微調整 (SFT) では, 文分類のためのラベル付きデータに基づいて事前学習したLCMを微調整し, 異常を識別する。
  論文  参考訳（メタデータ） (2024-07-24T16:33:04Z)
• Exploring Automatic Cryptographic API Misuse Detection in the Era of LLMs [60.32717556756674]
  本稿では,暗号誤用の検出において,大規模言語モデルを評価するための体系的評価フレームワークを提案する。 11,940個のLCM生成レポートを詳細に分析したところ、LSMに固有の不安定性は、報告の半数以上が偽陽性になる可能性があることがわかった。 最適化されたアプローチは、従来の手法を超え、確立されたベンチマークでこれまで知られていなかった誤用を明らかにすることで、90%近い顕著な検出率を達成する。
  論文  参考訳（メタデータ） (2024-07-23T15:31:26Z)
• Through the Thicket: A Study of Number-Oriented LLMs derived from Random Forest Models [0.0]
  大規模言語モデル (LLM) はテキスト処理において例外的な性能を示した。 本稿では,ランダムフォレスト(RF)アンサンブルからの知識伝達を用いたLLMの学習手法を提案する。 我々は、細調整のためのアウトプットを生成し、その決定を分類し、説明するモデルの能力を高めます。
  論文  参考訳（メタデータ） (2024-06-07T13:31:51Z)
• $\forall$uto$\exists$val: Autonomous Assessment of LLMs in Formal Synthesis and Interpretation Tasks [21.12437562185667]
  本稿では,形式構文を自然言語に翻訳する際のLLM評価のスケールアップ手法を提案する。 我々は、文脈自由文法(CFG)を用いて、その場で配布外のデータセットを生成する。 我々はまた、このパラダイムの実現可能性と拡張性を示すために、複数のSOTAクローズドおよびオープンソースLCMの評価を行う。
  論文  参考訳（メタデータ） (2024-03-27T08:08:00Z)
• Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
  本稿では,大規模言語モデル (LLM) 生成応答の事実性に注釈を付けるための総合的なエンドツーエンドソリューションを提案する。 オープンドメインの文書レベルの事実性ベンチマークを,クレーム,文,文書の3段階の粒度で構築する。 予備実験によると、FacTool、FactScore、Perplexityは虚偽の主張を識別するのに苦労している。
  論文  参考訳（メタデータ） (2023-11-15T14:41:57Z)
• ReEval: Automatic Hallucination Evaluation for Retrieval-Augmented Large Language Models via Transferable Adversarial Attacks [91.55895047448249]
  本稿では,LLMベースのフレームワークであるReEvalについて述べる。 本稿では、ChatGPTを用いてReEvalを実装し、2つの人気のあるオープンドメインQAデータセットのバリエーションを評価する。 我々の生成したデータは人間可読であり、大きな言語モデルで幻覚を引き起こすのに役立ちます。
  論文  参考訳（メタデータ） (2023-10-19T06:37:32Z)

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

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