論文の概要: ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers

• arxiv url: http://arxiv.org/abs/2607.19407v1
• Date: Tue, 07 Jul 2026 22:05:55 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-08-02 22:55:38.924421
• Title: ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers
• Title（参考訳）: ITPEval: インタラクティブな定理プローバー間の形式的翻訳のベンチマーク
• Abstract要約: ITPEvalは、4つの主要なIPP間で自動形式証明翻訳を評価するための最初のベンチマークである。 itpevalは、状態が分離されたウォームバックエンドを備えた、統合されたマルチITP認証インフラストラクチャです。
• 参考スコア（独自算出の注目度）: 77.95933562142014
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal theorem proving has emerged as a frontier challenge for machine learning, yet the ecosystem is fragmented: proofs remain siloed across incompatible systems, limiting both training data for learning-based provers and the portability of verified results. We present ITPEval, the first benchmark for evaluating automated formal proof translation across four major ITPs (Lean 4, Rocq, Isabelle, and HOL Light), spanning two distinct logical foundations. Our benchmark comprises 1,560 source files and 6,848 theorems organized into a controlled tier of axiomatized files that isolates foundational translation difficulty, and an ecosystem tier drawn from real libraries that exposes API and proof-style mismatches. We release itpeval, a unified multi-ITP verification infrastructure with state-isolated warm backends that preserve per-artifact native checking semantics. We evaluate both statement and proof translation across five frontier and open-weight LLMs on 12 directed translation pairs: statement translation peaks at 29.1% pass@1 and proof translation at 10.5%; controlled theorems reach 29.7% proof pass@1 versus 5.2% for ecosystem-level translations, confirming that library mismatch is the dominant bottleneck. In addition to pass@k evaluation, a deterministic Lean 4 BEq check establishes equivalence for 54.0% of verified source-to-Lean 4 miniF2F statement translations, showing that native type-checking alone can substantially overestimate semantic fidelity; in an autoformalization/auto-informalization round-trip study, Rocq and HOL Light are easier formalization targets than Lean 4 and Isabelle, while multi-ITP context improves pooled Lean 4 success from 4.8% to 10.6%. Our benchmark, verification infrastructure, and evaluation pipelines are publicly released.
• Abstract（参考訳）: 形式的定理証明は、機械学習のフロンティアチャレンジとして現れているが、エコシステムは断片化されている。証明は互換性のないシステム間でサイロ化され、学習ベースのプローバーのトレーニングデータと、検証結果の可搬性の両方が制限されている。 我々は4つの主要なIPP(Lean 4、Rocq、Isabelle、HOL Light)にまたがる自動形式証明翻訳を評価するための最初のベンチマークであるITPEvalについて述べる。 ベンチマークでは,基本翻訳の難しさを分離する公理化ファイルの制御層と,APIと証明スタイルのミスマッチを公開する実際のライブラリから引き出されたエコシステム層とを,1,560のソースファイルと6,848の定理で構成した。 itpevalは、複数のITP認証インフラストラクチャで、ステートアイソレーションされたウォームバックエンドで、アーチファクトごとのネイティブチェックセマンティクスを保存する。 文翻訳ピークは29.1% pass@1、証明翻訳は10.5%; 制御された定理は29.7%の証明パス@1と生態系レベルの翻訳では5.2%に達し、図書館ミスマッチが主要なボトルネックであることを確認した。 Pass@kの評価に加えて、決定論的Lean 4 BEqチェックは、検証済みのソース対リーン4のMiniF2F文の変換の54.0%の等価性を確立し、ネイティブな型チェックだけで意味的忠実性を大幅に過大評価できることを示している。 ベンチマーク、検証インフラストラクチャ、評価パイプラインが公開されています。

関連論文リスト

• Counterfactual Benchmarking and Training for Factuality Consistency and Order-Robust Grounded Reasoning in LLMs over Heterogeneous Knowledge [21.86609553205461]
  大規模言語モデル(LLM)は、ユーザが提供する知識に基づく応答生成をますますサポートしている。 TKFQAは10,130の質問回答(QA)ペアをテーブル,テキスト,知識グラフ(KG)に接地した実数整合性ベンチマークである。 それぞれの例は明示的な反事実的推論チェーンから構築され、回答の正しさ、推論チェーンの精度、異なる入力順序に対するロバスト性などの共同評価を可能にする。
  論文  参考訳（メタデータ） (2026-08-08T00:46:32Z)
• Ontology-Amplified Distillation and Contextuality Auditing for Sovereign Enterprise Language Models: A Combined Proof-of-Mechanism and Negative-Results Method Study [0.0]
  本稿では2つの関連するFAOS研究を1つのメカニズムと制御項目にまとめる。 まず, オントロジー増幅蒸留の低消費電力実験を報告する。 第2に,エンタープライズエージェントルーティングのためのコンテキスト性監査手法を統合する。
  論文  参考訳（メタデータ） (2026-07-11T15:42:40Z)
• Benchmarking Speech-to-Speech Translation Models [55.00303727199927]
  音声音声翻訳(S2ST)は急速に進歩しているが、オフライン評価には統一されたプロトコルが欠けている。 8次元にわたる46のメトリクスを統合するベンチマークフレームワークを導入する。 FLEURSとCVSSから1,248のモデル言語構成でデプロイする。
  論文  参考訳（メタデータ） (2026-06-02T07:01:33Z)
• Incentivizing Parametric Knowledge via Reinforcement Learning with Verifiable Rewards for Cross-Cultural Entity Translation [68.85147984815778]
  本稿では, EA-RLVR(Entity-Anchored Reinforcement Learning with Verifiable Rewards)を提案する。 EA-RLVRは、検証可能なエンティティレベルの報酬信号の監視をアンカーし、最適化を安定させるために軽量な構造ゲートを組み込む。 EA-RLVRをXC-Translate上で評価し、エンティティ翻訳精度とドメイン外一般化の両面で一貫した改善を観察する。
  論文  参考訳（メタデータ） (2026-04-18T07:15:43Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。 提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
  論文  参考訳（メタデータ） (2025-11-26T06:39:19Z)
• ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings [9.764411884491052]
  ProofBridgeは、NLの定理と証明を自動的にリーン4に翻訳するフレームワークです。 中心となるのは、NL と FL (NL-FL) の定理対を共有意味空間で整列する合同埋め込みモデルである。 我々の訓練は、NL-FL 対が意味論的に同値である場合に限り、この空間において NL-FL の定理が密接にマッピングされることを保証する。
  論文  参考訳（メタデータ） (2025-10-17T14:20:50Z)
• Advancing Natural Language Formalization to First Order Logic with Fine-tuned LLMs [0.0]
  予測可用性はパフォーマンスを15～20%向上させる。 モデルは特定の訓練をせずに、目に見えない論理的議論に一般化する。 構造論理の翻訳は堅牢であるが、述語抽出が主要なボトルネックとして現れる。
  論文  参考訳（メタデータ） (2025-09-26T13:30:50Z)
• Document Attribution: Examining Citation Relationships using Large Language Models [62.46146670035751]
  そこで本研究では,帰属を簡単なテキスト・エンタテインメント・タスクとみなすゼロショット・アプローチを提案する。 また,アトリビューションプロセスの強化におけるアテンションメカニズムの役割についても検討する。
  論文  参考訳（メタデータ） (2025-05-09T04:40:11Z)
• RustRepoTrans: Repository-level Code Translation Benchmark Targeting Rust [50.65321080814249]
  RustRepoTransは、インクリメンタル翻訳をターゲットにした、最初のリポジトリレベルのコンテキストコード変換ベンチマークである。 複雑な翻訳シナリオの制約を評価するために, 7つの代表的なLLMを評価し, それらの誤差を分析した。
  論文  参考訳（メタデータ） (2024-11-21T10:00:52Z)
• Herald: A Natural Language Annotated Lean 4 Dataset [15.42247133378869]
  本稿では,Mathlib4コーパス(形式言語Lean 4における数学の統一ライブラリ)を自然言語に翻訳するための新しいフレームワークを提案する。 私たちはこのパイプラインの結果をHeraldとしてMathlib4で発表します(階層とレトリバルベースのトランスレーショナルリーン)。 また,Heraldを微調整したHerald Translatorを提案する。
  論文  参考訳（メタデータ） (2024-10-09T10:11:24Z)
• Prosody in Cascade and Direct Speech-to-Text Translation: a case study on Korean Wh-Phrases [79.07111754406841]
  本研究は,韻律が重要な役割を果たす発話を明瞭にするための直接S2TTシステムの能力を評価するために,コントラスト評価を用いることを提案する。 本結果は,カスケード翻訳モデルよりも直接翻訳システムの価値を明確に示すものである。
  論文  参考訳（メタデータ） (2024-02-01T14:46:35Z)
• Leveraging Discourse Rewards for Document-Level Neural Machine Translation [46.006636555165414]
  我々は,2つの確立された談話指標である語彙凝集(LC)とコヒーレンス(COH)を明示的に最適化する学習手法を提案する。 私たちのトレーニングアプローチは、他の競争的アプローチよりも密集的で一貫性のあるドキュメント翻訳を実現することができました。
  論文  参考訳（メタデータ） (2020-10-08T02:26:22Z)

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

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