論文の概要: SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization
- arxiv url: http://arxiv.org/abs/2608.29270v2
- Date: Wed, 02 Sep 2026 07:34:08 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-03 15:35:44.741174
- Title: SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization
- Title（参考訳）: SHADOWBENCH:オートフォーマライゼーションにおける意味的アライメントの信頼性の高い自動評価に向けて
- Abstract要約: SA-Passは、意図したステートメントを特徴づける*shadows*と呼ばれる補助的なステートメントを使用して、フォーマルなステートメントをテストする。
私たちはShadowBenchでSA-Passをインスタンス化しています。
- 参考スコア（独自算出の注目度）: 26.630769373757218
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Autoformalization translates informal mathematical theorems into code for proof assistants such as Lean. A central challenge is that current evaluation metrics can accept type-correct but misaligned statements or reject correct statements written in a different formulation. Inspired by Pass@$k$, we propose SA-Pass (*Semantic Alignment Pass*), which tests formal statements using auxiliary statements called *shadows* that characterize the intended statement. A generated statement receives full credit only when it compiles, implies each shadow (forward check), and is implied by their conjunction (backward check). We instantiate SA-Pass in ShadowBench, a Lean 4 full autoformalization benchmark of 178 postgraduate- to research-level problems spanning eight mathematical areas. Claude Code (Opus 4.8) with Numina-Lean-Agent reaches $61.8\%$ compile rate and $11.2\%$ SA-Pass. Across outputs generated by six agentic configurations, SA-Pass achieves $98.8\%$ binary agreement with expert judgments. An early version of ShadowBench served as the benchmark for Track 4 of the ICML 2026 AI4Math Challenge.
- Abstract（参考訳）: 自己形式化(Autoformalization)は、非公式な数学的定理をリーンのような証明アシスタントのコードに変換する。
主要な課題は、現在の評価メトリクスが型正しいが不一致のステートメントを受け入れたり、異なる定式化で書かれた正しいステートメントを拒否できることである。
Pass@$k$にヒントを得たSA-Pass(*Semantic Alignment Pass*)を提案する。
生成されたステートメントはコンパイル時にのみ完全なクレジットを受け取り、各シャドウ(フォワードチェック)を暗示し、それらの結合(バックワードチェック)によって暗示される。
私たちはShadowBenchでSA-Passをインスタンス化します。これはLean 4のフルオートフォーマル化ベンチマークで、178人の大学院生から8つの数学領域にわたる研究レベルの問題に対処しています。
Claude Code (Opus 4.8) with Numina-Lean-Agentはコンパイルレートが61.8\%、SA-Passが11.2\%である。
6つのエージェント構成によって生成されるアウトプット全体で、SA-Passは専門家の判断と980.8\%のバイナリ契約を達成している。
初期のバージョンのシャドウベンチはICML 2026 AI4Math Challengeのトラック4のベンチマークとして使用された。
関連論文リスト
- ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers [77.95933562142014]
ITPEvalは、4つの主要なIPP間で自動形式証明翻訳を評価するための最初のベンチマークである。
itpevalは、状態が分離されたウォームバックエンドを備えた、統合されたマルチITP認証インフラストラクチャです。
論文 参考訳（メタデータ） (2026-07-07T22:05:55Z) - Auto: The AGI Compiler [0.0]
Autoは、ライブエージェントの振る舞いを記録し、どの部分が秘密に決定論的かを測定し、それを検証プログラムや蒸留専門家に抽出し、認識バイナリを出力するコンパイラである。
我々は,「AGIコンパイラ」を狭義で実証可能な意味で使用し,新規体験を,未知の知識を計測しながら,永続的で検証された,ほぼ自由なスキルに自律的に変換するシステムを開発した。
論文 参考訳（メタデータ） (2026-07-05T23:09:24Z) - The Faithfulness Gap: Certifying Semantic Equivalence Between Natural-Language and Formal Mathematical Statements [0.0]
形式的なステートメントは、型チェックと証明が可能でありながら、意図した元とは異なる定理を符号化することができる。
emphBidirectional Provability Fingerprinting (bpf) を導入する。
我々は6つのサブフィールドにわたる制御ドリフトラベルを持つ2,183ドルのNL/Lean4ペアのベンチマークであるDreatbenchをリリースした。
論文 参考訳（メタデータ） (2026-06-15T10:45:59Z) - Skill-as-Pseudocode: Refactoring Skill Libraries to Pseudocode for LLM Agents [50.78646963535282]
Skill-as-Pseudocode (SaP) はマークダウンスキルライブラリの型付き擬似コードへの自動変換である。
1つ以上のスキルから引き出された類似の手続きパスのクラスタごとに、SaPは型付きコントラクトを抽出し、それを4チェック決定性検証器を通じてフィルタリングする。
プロモートされた契約は、復元された具体的なアクションテンプレートと共に書き直されたスキルスケルトンにインライン化され、エージェントは2つの補完的な信号を与える。
論文 参考訳（メタデータ） (2026-05-27T04:48:40Z) - Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems [100.24694338574402]
本稿では,インダクティブ・デダクティブ・シンセシス(IDS)について述べる。
IDSは約6.8時間で7/7を達成し、1仕様あたり106ドル、専門家の努力の約200倍、SOTAエージェントの約17%を達成している。
IDSはパフォーマンスフィードバックを同じループに組み込んでおり、検証されたシステムよりも最大3倍高速な実装を実現している。
論文 参考訳（メタデータ） (2026-05-22T00:05:36Z) - From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification [0.30915521808748864]
大規模な言語モデルは、自動化されたソフトウェア工学における約束を示すが、その正しさの保証は、誤ったコードや幻覚的なコードによってしばしば損なわれる。
NaturalLanguage2VerifiedCodeデータセット:60の複雑なアルゴリズム問題の集合を提供する。
7個のオープンウェイト LLM でランダムに選択された11個の問題集合をタイレッドプロンプト戦略を用いて評価した。
以上の結果から,コンテキストレスなプロンプトがほぼユニバーサルの失敗につながる一方で,構造的アンカーと反復的自己修復が劇的なパフォーマンスの転換を促進することが示唆された。
論文 参考訳（メタデータ） (2026-04-24T14:28:10Z) - PBLean: Pseudo-Boolean Proof Certificates for Lean 4 [27.126691338850254]
PBLean は VeriPB pseudo-Boolean (PB) 証明証明書をLean 4 にインポートする手法である。
リーンで完全証明され、コンパイルされたネイティブコードとして実行されるブールチェッカー関数。
我々のチェッカーは、カットプレーンや証明・バイ・コントラディション・サブプロテクションを含む全てのVeriPBカーネルルールをサポートしている。
論文 参考訳（メタデータ） (2026-02-09T14:13:30Z) - Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
Chain-of-Thoughtプロンプトは、大規模言語モデル(LLM)から推論能力を引き出すデファクトメソッドとなっている。
検出が極めて難しいCoTの幻覚を緩和するために、現在の方法は不透明なボックスとして機能し、彼らの判断に対する確認可能な証拠を提供しておらず、おそらくその効果を制限する。
任意のスコアを割り当てるのではなく、各推論ステップで形式数学言語Lean 4で数学的主張を明確にし、幻覚を識別するための公式な証明を提供しようとしている。
論文 参考訳（メタデータ） (2025-06-05T03:16:08Z) - APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning [16.8655558789989]
本稿では,自動定理証明のためのモデルに依存しないエージェントフレームワークであるAPOLLO (Automated PrOof repair viaLLM and Lean cOllaboration)を提案する。
エージェントのセットは、証明を分析し、シンタックスのエラーを修正し、リーンを使って証明の誤りを特定し、失敗するサブレムマを分離し、自動化されたソルバを利用し、残りの目標に対してLLMを呼び出す。
この結果から,LLM出力を目標としたコンパイラ誘導型修復は,効率と正確性の両方において劇的に向上することが示された。
論文 参考訳（メタデータ） (2025-05-09T03:38:31Z) - SolBench: A Dataset and Benchmark for Evaluating Functional Correctness in Solidity Code Completion and Repair [51.0686873716938]
コード補完モデルによって生成されたSolidityスマートコントラクトの機能的正しさを評価するベンチマークであるSolBenchを紹介する。
本稿では,スマートコントラクトの機能的正当性を検証するための検索拡張コード修復フレームワークを提案する。
その結果、コード修復と検索技術は、計算コストを削減しつつ、スマートコントラクト完了の正しさを効果的に向上することを示した。
論文 参考訳（メタデータ） (2025-03-03T01:55:20Z) - EquiBench: Benchmarking Large Language Models' Reasoning about Program Semantics via Equivalence Checking [58.15568681219339]
大規模言語モデル(LLM)を評価するための新しいベンチマークであるEquiBenchを紹介する。
このタスクは、プログラムのセマンティクスについて推論するモデルの能力を直接テストする。
19の最先端LCMを評価し、最も難しいカテゴリでは、最高の精度は63.8%と76.2%であり、50%のランダムベースラインよりわずかに高い。
論文 参考訳（メタデータ） (2025-02-18T02:54:25Z) - Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
我々は,2025年4月5日現在,数学問題の自動証明生成における最先端(最先端)性能を実現する,オープンソースの言語モデルであるGoedel-Proverを紹介した。
まず、自然言語の数学問題をNuminaデータセットからLean 4で等価な形式ステートメントに変換するためにLLMをトレーニングします。
次に,一連のプロデューサをトレーニングすることで,形式証明の大規模なデータセットを開発する。
最後に、Goedel-Pset-v1-solvedというデータセットを取得し、Goedel-Pset-v1から800K以上のステートメントの証明を含む。
論文 参考訳（メタデータ） (2025-02-11T15:27:35Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。