論文の概要: A Certificate-Producing Cascade for Equational Implication: The SAIR EQT2 Stage 2 Solver
- arxiv url: http://arxiv.org/abs/2609.00706v1
- Date: Tue, 01 Sep 2026 04:34:00 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-02 16:31:36.321805
- Title: A Certificate-Producing Cascade for Equational Implication: The SAIR EQT2 Stage 2 Solver
- Title（参考訳）: SAIR EQT2 Stage 2 Solver
- Authors: Haobo Ma, Wenlin Zhang, Manuel Israel Cázares,
- Abstract要約: SAIR Mathematics Distillation Challenge on Equational Theories では、あるマグマが別のマグマの同一性を意味するかどうかを解き明かす。
我々は,最も安価な第1カスケードとして構成された単一ファイル解決器を提案する。
その偽分岐は、構造化代数族上の係数テスト、有界有限モデル探索、明示的な中心群群証人、およびいくつかの無限キャリア証人を組み合わせたものである。
- 参考スコア（独自算出の注目度）: 3.8048003898069975
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: The SAIR Mathematics Distillation Challenge on Equational Theories asks a solver to classify whether one magma identity implies another and, for either verdict, to return a certificate accepted by a deterministic Lean judge. We present a single-file solver organized as a cheapest-first cascade. Its false branch combines coefficient tests over structured algebra families, bounded finite-model search, an explicit central-groupoid witness, and several infinite-carrier witnesses. Its true branch is a proof-producing ordered unit superposition procedure with Knuth-Bendix ordering, bidirectional demodulation, indexing, memoised substitution, and anytime size deepening. Search results remain outside the trusted base: successful derivations are replayed as small Lean terms, and countermodels are rechecked by the competition judge. The frozen solver is a 189,504-byte Python file with SHA-256 f2392533c9f4c03b.... In local runs through official judge revision 2848228, it produced accepted certificates for all 1,889 rows of the six public sets with no language-model calls. Separate measurements recorded full agreement on the 800 published Stage 1 evaluation-distribution problems, 100 accepted rows in the canonical Marathon manifest without tokens, and 200 accepted rows in the hosted playground. These are regression and playground measurements, not a leaderboard result and not evidence about a hidden set. All quantitative claims are tied to immutable result ledgers; the paper makes no completeness or comparative-superiority claim.
- Abstract（参考訳）: 等式理論に関するSAIR数学蒸留チャレンジ(SAIR Mathematics Distillation Challenge on Equational Theories)は、解法者に1つのマグマのアイデンティティが別のものを意味するかどうかを分類するよう求め、いずれの評決も、決定論的リーンの裁判官によって受け入れられた証明書を返すよう要求する。
我々は,最も安価な第1カスケードとして構成された単一ファイル解決器を提案する。
その偽分岐は、構造化代数族上の係数テスト、有界有限モデル探索、明示的な中心群群証人、およびいくつかの無限キャリア証人を組み合わせたものである。
真の分岐は、クヌース・ベンディクスの順序付け、双方向の復調、インデックス化、メモ置換、および任意のサイズの深化を伴う証明生成順序単位の重ね合わせ手順である。
成功する導出は小さなリーン用語として再生され、カウンターモデルは競争裁判官によって再検査されます。
凍結解凍器はSHA-256 f2392533c9f4c03bの189,504バイトのPythonファイルである。
地方では、公式の審査修正2848228を通じて、6つの公開集合の1,889行すべてに対して、言語モデルコールなしの認定証明書を作成した。
異なる測定では,800件のステージ1評価分布問題,トークンのない正準マラソンマニフェストにおける100行,ホストされた遊び場での200行が完全に一致した。
これらは回帰と遊び場の測定であり、リーダーボードの結果ではなく、隠れた集合の証拠ではない。
すべての量的クレームは不変な結果台帳に結びついている。
関連論文リスト
- AI Grinding for Fun and Cryptanalysis [0.0]
エージェントが人間のレビューの前に仮説を生成・テスト・精査する自律型暗号解析ワークフローを提案する。
まず、公開マップや入力表現は、構築が隠さなければならない関係を消去または公開する。
第2に、シミュレータ、エラー法則、パラメータ認証は、要求されたものと異なる分布を使用する。
論文 参考訳（メタデータ） (2026-08-22T14:37:46Z) - Capability Sheaves for Compositional Agent-Harness Repair: Controlled Quotients and a Real-Repository Stress Test [0.0]
エージェントハーネスは、検索、ルーティング、状態、証明、検証を組み合わせるが、ローカルに成功したコンポーネントは共有状態に異を唱えることがある。
我々は、この失敗を有限エンハンパビリティ層でモデル化する:ストークは型付き動作シグネチャを符号化し、制限マップは共有フィールドを保持し、受け入れられた実行は有用なグローバルセクションである。
20以上のタスククラスタで制御された実験では、生の状態がニュアンス変数である隠された内部メディエータが導入された。
次に、PatchFuseBenchのSWE-benchプールから分離した発見法について、20のリポジトリから160の課題、875の実際の候補パッチ、2,579のソースを意識した編集原子をテストした。
論文 参考訳（メタデータ） (2026-08-13T13:31:09Z) - Reasoning Shortcuts and Value Symmetries: What Symmetry Permits, Architecture Realizes, and Optimization Selects [10.012788934490084]
推論ショートカット(Reasoning shortcuts)は、意図しない概念を通じて正しい予測を生成するニューロシンボリックシステムの規則の解である。
竹村、井上、西野の最近のフレームワークは、値を許容する自己同型群を通してそれらを分析している。
まず, 評価した4つのベンチマークのどれにも記載されているように, フレームワークの主要な定義である共有置換が適用されないことを示す。
論文 参考訳（メタデータ） (2026-08-11T03:10:20Z) - Coding Agents as Test-Suite Auditors: Finding What Official Suites Miss While Approaching What They Catch [47.836680625916266]
テストスイート監査官として機能する市販のコーディングエージェントは、どちらも、公式スイートが見逃すものを公開するために、敵対的なテストスイートを構築します。
認証チェーンは、各エージェントフラッグされた申請が、公式の裁判官に頼らずに、真にバグだらけであるか否かを判定する。
Codeforceは、利用可能なオフィシャルスイートを持たない問題に対して、同じテストビルディングメソッドを使用して、テストされた入力予算毎に5つの再生ベースラインを導出する。
論文 参考訳（メタデータ） (2026-08-03T05:24:03Z) - Abliteration Is Not a Scalpel: Off-Target Effects of Refusal Removal on Decision Disposition Across Model Families [51.56484100374058]
放棄 — モデルの拒絶方向を重みから取り除く — は、一般的な"アンセンソルド"なオープンウェイトモデルの標準的なレシピである。
ディスポジションプローブとして21,600個の決定を不確実性の下で使用し、凍結パイプラインを通じて再生することにより、決定層モデルが唯一の変数となる。
3つのエフェクトは2つのファミリーにまたがって複製される(ゼロを除く週間クラスターCI)
4つ目の効果は符号を逆転する:同じ操作によりGemmaで読み取られた方が自信が弱まり、Qwenで読み取られたものがより多くなる(ファミリーCIは重複しない)。
論文 参考訳（メタデータ） (2026-07-19T22:27:00Z) - When LLMs Agree, Are They Right? Auditing Self-Consistency and Cross-Model Agreement as Confidence Signals [0.0]
LLM-as-judgeは、企業パイプラインでAIシステムを評価する上で、ますますデフォルトになっている。
判断者間の整合性、あるいはモデル自身のサンプルが正当性を示していることを示す。
大規模なクロスランナー研究において、合意がいつ有用なプロキシであるかを問う。
論文 参考訳（メタデータ） (2026-07-09T02:46:51Z) - Cherry-pick Override: Unsafe Directional Commitment in LLM Judges under Mixed Evidence [14.905172804386973]
我々は、検証生成とコミットメント承認を分離する外部コミットメント制御層を論じる。
我々はCCOを明示的なタスク契約で定義し、同一のデノミネータ診断プロトコルで報告する。
論文 参考訳（メタデータ） (2026-06-05T20:51:51Z) - Survive or Collapse: The Asymmetric Roles of Data Gating and Reward Grounding in Self-Play RL [76.45061154544568]
セルフプレイ強化学習は、言語モデルを独自の生成タスクで訓練し、人間ラベルなしでプロジェクタとソルバを共進化させる。
最近のシステムでは強い推理効果が報告されているが、崩壊と不安定性は広く観察され、理解されていない。
代わりに、自己プレイの安定性は、提案者生成タスクがトレーニングプールに入るかを判断するデータレベルゲートと、すでに認められたタスクに関するポリシーを更新する報酬信号の2つの異なるレバーによって管理されていると論じる。
論文 参考訳（メタデータ） (2026-05-21T09:19:23Z) - Distributional Energy-Based Models for Uncertainty-Aware Structured LLM Reasoning [40.342912574072024]
大規模言語モデルは、旅行計画やコードソリューションのような構造化されたアウトプットを生成する。
個々の推論ステップは正しく見えるが、アウトプット全体が予算に違反したり、テストケースに失敗したり、あるいは以前の推論に矛盾することがある。
構造化LCM出力の検証のための決定論的解析制約付き学習品質スコアラを提案する。
論文 参考訳（メタデータ） (2026-05-15T17:08:27Z) - Solving Inequality Proofs with Large Language Models [42.667163027148916]
不等式証明は様々な科学・数学分野において不可欠である。
これにより、大きな言語モデル(LLM)の需要が高まるフロンティアとなる。
我々は、Olympiadレベルの不平等を専門家が計算したデータセットであるIneqMathをリリースした。
論文 参考訳（メタデータ） (2025-06-09T16:43:38Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。