論文の概要: FormalRx: Rectify and eXamine Semantic Failures in Autoformalization
- arxiv url: http://arxiv.org/abs/2607.04655v1
- Date: Mon, 06 Jul 2026 04:20:06 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-07 22:26:30.035879
- Title: FormalRx: Rectify and eXamine Semantic Failures in Autoformalization
- Title（参考訳）: FormalRx: オートフォーマル化におけるrectifyとeXamineセマンティック障害
- Abstract要約: FormalRxは、オートフォーマル化のための総合的な診断評価フレームワークである。
自動形式評価をブラックボックスの判断から行動可能なフィードバックに変換する。
我々は56,287個のNL-FLペアでトレーニングされた診断モデルFormalRx-8Bでフレームワークをインスタンス化する。
最初のきめ細かい診断ベンチマークとしてFormalRx-Testをリリースしました。
- 参考スコア（独自算出の注目度）: 20.257622307895108
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: The veracious semantic alignment in autoformalization is significant for formal mathematical reasoning. However, existing evaluations provide only opaque binary verdicts or scalar scores, offering no interpretable insight into where or why translations fail. This opacity severely limits both human understanding and automated system improvement. To bridge this gap, we introduce FormalRx, a comprehensive diagnostic evaluation framework that transforms autoformalization assessment from black-box judgments into actionable feedback. At its core is SCI Error Taxonomy, a hierarchical classification scheme decomposing autoformalization errors into 28 distinct categories with strict priority ordering. Building on this taxonomy, FormalRx provides four critical diagnostic capabilities: alignment verdicts, error categorization, error localization, and correction. We instantiate the framework with a diagnostic model FormalRx-8B, trained on 56,287 NL-FL pairs with fine-grained diagnostic annotations, and release FormalRx-Test as the first fine-grained diagnostic benchmark. FormalRx-8B achieves F1-scores of 0.88 (verdict) and 0.71 (categorization), along with accuracies of 0.75 (localization) and 0.73 (correction), substantially outperforming both general-purpose LLMs and specialized baselines. By connecting evaluation with actionable insights, FormalRx enables systematic diagnosis and improvement of autoformalization systems.
- Abstract（参考訳）: 自己形式化における妥当なセマンティックアライメントは、形式的な数学的推論において重要である。
しかし、既存の評価は不透明な二分判定やスカラースコアのみを提供しており、翻訳がどこで失敗したのか、なぜ失敗したのかを理解できない。
この不透明さは、人間の理解と自動システム改善の両方を著しく制限します。
このギャップを埋めるために,ブラックボックスの判断から行動可能なフィードバックへと自己形式化評価を変換する総合的な診断評価フレームワークであるFormalRxを導入する。
SCI誤り分類(SCI Error Taxonomy)は、自己形式化エラーを厳格に優先順位付けした28のカテゴリに分解する階層的な分類体系である。
この分類に基づいて、FormalRxはアライメント検証、エラー分類、エラーローカライゼーション、修正の4つの重要な診断機能を提供する。
診断モデルFormalRx-8Bを用いてフレームワークをインスタンス化し、56,287個のNL-FLペアに詳細な診断アノテーションを付与し、最初の詳細な診断ベンチマークとしてFormalRx-Testをリリースする。
フォーマルRx-8Bは0.88(予測)と0.71(分類)のF1スコアと0.75(局所化)と0.73(補正)を達成し、汎用LLMと特殊ベースラインの両方を大幅に上回っている。
動作可能な洞察と評価を結びつけることで、FormalRxは、オートフォーマル化システムの体系的な診断と改善を可能にします。
関連論文リスト
- Evaluating the Semantic Specificity of Representation Steering in Language Models [11.464730765998555]
局所表現ステアリングは、大きな言語モデルにおける推論病理の修正に広く用いられている。
標準的なベンチマーク評価は、表面上のラベルオーバーライドによって簡単に騙され、推論回路の修理を誤った印象を与える。
論文 参考訳（メタデータ） (2026-08-29T20:31:32Z) - Evaluating Multi-Turn Multimodal Diagnostic Reasoning on Challenging Real-World Clinical Cases [59.5328455571863]
ClinMM-Benchは、これまでで最大のマルチターンマルチモーダル臨床診断評価ベンチマークである。
実際の患者は1,089件、医療画像は3,760件、専門は8件。
プロプライエタリモデルでは診断精度が最も高かったが、正確な診断の割合は限られていた。
論文 参考訳（メタデータ） (2026-07-28T16:19:03Z) - SAAG: Structured Agent Assessment and Grounding [13.62148061055744]
本稿では,エージェント呼び出し評価を3段階に分解するケースケード診断フレームワークを提案する。
このフレームワークは,5,10,15エージェントのレジストリサイズにまたがって,Glaiveの関数呼び出しデータセットから得られたベンチマークで評価する。
論文 参考訳（メタデータ） (2026-04-30T19:33:58Z) - A Multi-Stage Validation Framework for Trustworthy Large-scale Clinical Information Extraction using Large Language Models [1.9110728489340625]
大規模言語モデル(LLM)は、非構造化の健康記録から臨床的に意味のある情報を抽出する約束を示す。
LLMに基づく臨床情報抽出のための多段階検証フレームワークを提案する。
919,783名の臨床ノートから11種類の物質分類で診断された物質使用障害の抽出に本枠組みを適用した。
論文 参考訳（メタデータ） (2026-04-07T16:23:52Z) - An Explainable Vision-Language Model Framework with Adaptive PID-Tversky Loss for Lumbar Spinal Stenosis Diagnosis [1.2871968485402088]
既存の視覚言語モデルは、臨床セグメント化データセットでよく見られる極端なクラス不均衡に対処できない。
本稿では、これらの制限を克服するために、エンドツーエンドの説明可能な視覚言語モデルフレームワークを提案する。
診断精度は90.69%,マクロ平均Diceスコアは0.9512,CIDErスコアは92.80%であった。
論文 参考訳（メタデータ） (2026-04-02T20:18:35Z) - Clinical Cognition Alignment for Gastrointestinal Diagnosis with Multimodal LLMs [63.535652574541764]
MLLM(Multimodal Large Language Models)は医用画像解析において顕著な可能性を示した。
消化器内視鏡におけるそれらの応用は、現在、2つの重要な限界によって妨げられている。
本稿では,これらの課題に対処する新しい臨床認知アライメント(CogAlign)フレームワークを提案する。
論文 参考訳（メタデータ） (2026-03-21T07:47:37Z) - Agentic Cognitive Profiling: Realigning Automated Alzheimer's Disease Detection with Clinical Construct Validity [66.94391219005291]
本稿では,臨床プロトコルロジックによる自動スクリーニングを実現するエージェント認知プロファイリング(ACP)を提案する。
我々の設計の中心は、すべての定量化を決定論的関数呼び出しに委譲することで、測定から意味的理解を分離することである。
ACPは、タスク試験で90.5%のスコアマッチ率、AD予測で85.3%の精度を達成し、一般的な基準を上回っている。
論文 参考訳（メタデータ） (2026-03-18T06:15:35Z) - Guideline-Grounded Evidence Accumulation for High-Stakes Agent Verification [60.18369393468405]
既存の検証器は通常、ドメイン知識の欠如と限られた校正のために性能が劣る。
GLEANは専門家によって計算されたプロトコルをトラジェクトリインフォームされ、よく校正された正当性信号にコンパイルする。
我々は,MIMIC-IVデータセットから得られた3つの疾患の薬物的臨床診断でGLEANを実証的に検証した。
論文 参考訳（メタデータ） (2026-03-03T09:36:43Z) - Modeling Expert AI Diagnostic Alignment via Immutable Inference Snapshots [1.0499611180329804]
初期モデル推論と専門家補正の遷移は、構造化信号としてはほとんど分析されない。
本稿では,AI生成画像に基づくレポートを不変な推論状態として保存する診断アライメントフレームワークを提案する。
論文 参考訳（メタデータ） (2026-02-26T13:11:58Z) - ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
本稿では,意味的整合性評価を自己形式化プロセスに統合する反射的自己形式化手法を提案する。
これにより、モデルが形式的なステートメントを反復的に生成し、セマンティックな忠実さを評価し、自己修正された特定エラーを発生させることができる。
実験の結果、ReFormは最強のベースラインに対して平均22.6ポイントの改善を達成した。
論文 参考訳（メタデータ） (2025-10-28T16:22:54Z) - From Scores to Steps: Diagnosing and Improving LLM Performance in Evidence-Based Medical Calculations [45.414878840652115]
大規模言語モデル(LLM)は医療ベンチマークで有望な性能を示した。
しかし、医学的な計算を行う能力は未熟であり、評価も不十分である。
本研究は,臨床信頼性を重視した医療計算評価を再考する。
論文 参考訳（メタデータ） (2025-09-20T09:10:26Z) - Learning to diagnose cirrhosis from radiological and histological labels
with joint self and weakly-supervised pretraining strategies [62.840338941861134]
そこで本稿では, 放射線学者が注釈付けした大規模データセットからの転写学習を活用して, 小さい付加データセットで利用できる組織学的スコアを予測することを提案する。
我々は,肝硬変の予測を改善するために,異なる事前訓練法,すなわち弱い指導法と自己指導法を比較した。
この方法は、METAVIRスコアのベースライン分類を上回り、AUCが0.84、バランスの取れた精度が0.75に達する。
論文 参考訳（メタデータ） (2023-02-16T17:06:23Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。