論文の概要: The Signal-Coverage Matrix: Stratifying Type and Semantic Errors in Statement Autoformalization
- arxiv url: http://arxiv.org/abs/2606.28013v1
- Date: Fri, 26 Jun 2026 12:15:12 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-29 18:24:25.482156
- Title: The Signal-Coverage Matrix: Stratifying Type and Semantic Errors in Statement Autoformalization
- Title（参考訳）: Signal-Coverage Matrix:ステートメントオートフォーマル化におけるストラテグタイプとセマンティックエラー
- Abstract要約: LLMオートフォーマル化の見出し型精度は2年間で$sim$53%から$sim$76%に上昇した。
本稿では,リーンエラボレータを横断する信号被覆行列を意味等価判断で提案する。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Headline type-correctness (TC\%) of LLM autoformalization has climbed from $\sim$53\% to $\sim$76\% in two years, yet this scalar conceals which errors each method resolves. We propose a signal-coverage matrix that crosses the Lean elaborator (pass/fail) with a semantic-equivalence judgment (equivalent/not), sorting every output into one of four cells: true success (TS), type-only (TO), semantic-only (SO), or both fail (BF). On ProofNet\# and MiniF2F-test with DeepSeek V4-Pro across Vanilla, Lean-Retry, Sample-Filter, and Stratified Autoformalization (SAF): (1) the +34 to +36 TS gain across the three elab-feedback methods is $\sim$64\% type-stratum recovery, with SO flat on net (87.5\% of original semantic errors rescued, 8 newly created). (2) The TO-to-TS rate is 23/61 for each method (Wilson 95\% CI [26.6\%, 50.3\%]), and this stratum-level recovery rate predicts $Δ$TS on held-out methods to within 2/186 and renders $Δ$TC linear in the Vanilla elab-fail rate across six (model, dataset) cells ($R^2=0.96$). (3) The two judges disagree by 26 to 37 pp on elab-feedback outputs (vs. 7 pp on Vanilla), with 30 to 56\% of symbolic-judge false negatives traceable to elaborator-forced rewrites. The persistent residual reduces to two gold-formalization errors. TC\% gains should be credited by which cell moved, not by the scalar alone.
- Abstract（参考訳）: LLMオートフォーマル化の見出し型補正(TC\%)は2年間で$\sim$53\%から$\sim$76\%に上昇しているが、このスカラーは各メソッドが解決するエラーを隠蔽している。
本稿では,Lean Elaborator(pass/fail)を意味等価判断(equivalent/not)で横断し,すべての出力を真の成功(TS),タイプオンリー(TO),セマンティックオンリー(SO),フェール(BF)の4つのセルのいずれかに分類する信号被覆行列を提案する。
ProofNet\#とMiniF2F-test with DeepSeek V4-Pro across Vanilla, Lean-Retry, Sample-Filter, and Stratified Autoformalization (SAF): 1) 3つのelab-feedbackメソッドにまたがる+34から+36 TSのゲインは、$\sim$64\%のタイプストラムリカバリであり、SOフラットがネット上にある(オリジナルのセマンティックエラーの87.5\%が新たに作成されている)。
2)TO-to-TSレートは各手法で23/61(Wilson 95\% CI [26.6\%, 50.3\%])であり、この成層レベルの回収率はホールドアウト法で$Δ$TSを2/186の範囲で予測し、バニラ・エラブ・フェイルレートで$Δ$TCを6(モデル,データセット)セル(R^2=0.96$)でレンダリングする(R^2=0.96$)。
(3) 2人の裁判官は、elab-feedback(vs. 7 pp on Vanilla)のアウトプットについて、elab-feedback(vs. 7 pp)について、elaborator-forced(elaborator-forced)にトレース可能な30-56\%のシンボリック・ジャッジ偽陰性について、26-37 ppで意見が一致しない。
残留残差は2つのゴールドホルマライゼーション誤差に減少する。
TC*%の利得は、スカラー単独ではなく、どの細胞が移動したかによって評価されるべきである。
関連論文リスト
- Controlled Reformulation Testing for Logical Consistency in Large Language Models [45.88028371034407]
制御改革試験(CRTBench)における350の質問族(総質問数1,750)のベンチマークを示す。
本研究では,大言語モデルにおいて,制御された再編成における一貫した回答を維持する能力について検討する。
これらの結果から,LLMにおける論理的推論の評価には精度だけでは不十分であることが示唆された。
論文 参考訳（メタデータ） (2026-07-16T03:30:28Z) - Efficient Visual Pointing for Embodied AI:Agent-Driven Data Synthesis, Cross-Block Attention, and Iterative Correction [55.11480729304395]
PointArena 2026は77.2%の精度でベンチマークで2位である。
ap proachは3つの障害モードをターゲットにしている。第一に、エージェント駆動のシンセシスは大きなセマンティクスとアンカー相対的な候補プールを構築する。
次に、determinis tic steerable-dataパイプラインは、認証された10,000サンプルのメインセットと、マスク、テンプレート、パス検証を使用するリザーブサンプルを生成する。
論文 参考訳（メタデータ） (2026-06-29T06:39:03Z) - Control-Plane Placement Shapes Forgetting: An Architectural Study of Agent Memory Across Thirteen System Configurations [1.2763567932588586]
ForgetEvalは1000ケースのテンプレート・スイートと385ケースの対向層(手作り+253 LLMのオラクル・バリデーション)
決定論的プリミティブは語彙的・時間的カテゴリーで十分だが、正準化に失敗する。
1000ケースのテンプレートスイートと385ケースの反対層であるForgetEvalを通じて、トレードオフを公開しています。
論文 参考訳（メタデータ） (2026-06-14T16:32:15Z) - Layer-Isolated Evaluation: Gating the Deterministic Scaffold of a Production LLM Agent with a No-LLM, Regression-Locked Test Harness [45.148328075418156]
デプロイされた注文エージェントは、階層の固定された分類に分解される。
純粋なスイートは、ロックされたスライス単位のベースラインに対して、すべての変更でCIで動作する。
制御されたレグレッションインジェクションにより、安全でない7つの層に一度に1つの層を分解し、検証する。
論文 参考訳（メタデータ） (2026-06-10T05:55:13Z) - Right Makes Might: Aligning Verified Hidden States Empowers RL Reasoning [55.264863369127774]
現在の方法では、それぞれの正しいロールアウトを単一の報酬ビットに減らし、隠れた状態間で共有される幾何学的構造を無視している。
本稿では,RLトレーニングにおけるアンカートークンにおける正ロールアウトの最終層を,トレーニングと推論の両方においてゼロオーバーヘッドで整列する補助損失関数Hidden-Alignを提案する。
8つの数学的推論ベンチマークでは、Hidden-AlignはDAPOベースラインの平均パス@1をQwen3-1.7B, 4B, 14Bで3.8, 6.2, 5.4ポイント改善し、3つのスケールで一貫したパス@kゲインを得る。
論文 参考訳（メタデータ） (2026-06-02T06:51:15Z) - RAIL Guard: Closing the Evaluation-to-Remediation Gap in Responsible AI for LLM Agents [0.0]
RAIL GuardはクローズドループによるAIパイプラインである。
繰り返し出力をアセスメント・リライト・リ評価ループで更新する。
SystemはオープンソースSDKとして利用できる。
論文 参考訳（メタデータ） (2026-05-28T21:23:49Z) - Step-wise Rubric Rewards for LLM Reasoning [72.17879367869503]
RLVR(Reinforcement Learning with Verifiable Rewards)は、大規模言語モデルの推論を改善するために広く使われている。
正しい回答の18.2%は間違っているが、肯定的な報酬がある。
6つの数学的推論ベンチマークで、SRaRはRaRの平均精度を3.57ポイント改善した。
論文 参考訳（メタデータ） (2026-05-17T07:08:14Z) - Distributional Energy-Based Models for Uncertainty-Aware Structured LLM Reasoning [40.342912574072024]
大規模言語モデルは、旅行計画やコードソリューションのような構造化されたアウトプットを生成する。
個々の推論ステップは正しく見えるが、アウトプット全体が予算に違反したり、テストケースに失敗したり、あるいは以前の推論に矛盾することがある。
構造化LCM出力の検証のための決定論的解析制約付き学習品質スコアラを提案する。
論文 参考訳（メタデータ） (2026-05-15T17:08:27Z) - ReFlect: An Effective Harness System for Complex Long-Horizon LLM Reasoning [5.523132953818281]
本稿では,LLM推論のためのシステムであるReFlectについて述べる。
6つの推論領域にまたがる制御された実験により、100個の監査された反射ブロックのうち90個の問題にフラグを付けない、プロンプトレベルの自己批判が公式テンプレートを生成することが示された。
我々のReFlectハーネスは, GPT-4o-miniで41%, Claude Sonnet 4.5で56%のタスク成功率を実現している。
論文 参考訳（メタデータ） (2026-05-07T06:29:34Z) - When Corrective Hints Hurt: Prompt Design in Reasoner-Guided Repair of LLM Overcaution on Entailed Negations under OWL~2~DL [10.675009214407185]
OWL2DL コンプライアンスクエリにおいて GPT-5.4 で再現可能なエラーパターンを報告した。
emphFunctionalProperty closure または class emphdisjointness' の下で、理性に満ちた答えが no''' である場合、モデルは「未知」を頻繁に答える。
論文 参考訳（メタデータ） (2026-04-25T18:11:01Z) - One Token Away from Collapse: The Fragility of Instruction-Tuned Helpfulness [12.183451602438753]
単純な語彙制約(句読解文字または共通単語の禁止)により、命令調整されたLLMが応答を崩壊させることを示す。
ベースモデルでは,同じ制約の下で,小さな,騒々しい,双方向的な効果を伴って,体系的な崩壊を示さないことを示す。
論文 参考訳（メタデータ） (2026-04-14T17:40:01Z) - Hide and Seek in Embedding Space: Geometry-based Steganography and Detection in Large Language Models [44.41218866933059]
微調整LDMは、ステガノグラフィーチャネルを介してプロンプトシークレットを出力に隠蔽的にエンコードすることができる。
任意の写像を埋め込み空間由来のものに置き換えることで、従来のスキームが100%回復可能であることを示す。
我々は、微調整によるステガノグラフィー攻撃を検出するには、従来のステガナシス以上のアプローチが必要であると論じる。
論文 参考訳（メタデータ） (2026-01-30T10:43:43Z) - Improved techniques for deterministic l2 robustness [63.34032156196848]
畳み込みニューラルネットワーク(CNN)を$l_2$ノルムの下で厳密な1-Lipschitz制約で訓練することは、対向的堅牢性、解釈可能な勾配、安定した訓練に有用である。
我々は,最後の線形層を1重層に置き換えることで,1-Lipschitz CNNのロバスト性を証明する手法を提案する。
我々は,CIFAR-10およびCIFAR-100における標準および証明可能な堅牢な精度の最先端化を図る。
論文 参考訳（メタデータ） (2022-11-15T19:10:12Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。