Fugu-MT 論文翻訳(概要): A machine-checked proof of the Dong-Yang classification of optimal (n,4) binary codes for BSCs

論文の概要: A machine-checked proof of the Dong-Yang classification of optimal (n,4) binary codes for BSCs

arxiv url: http://arxiv.org/abs/2609.10579v1
Date: Sat, 05 Sep 2026 07:36:38 GMT
ステータス: 翻訳完了
システム内更新日: 2026-09-11 23:53:35.069546
Title: A machine-checked proof of the Dong-Yang classification of optimal (n,4) binary codes for BSCs
Title（参考訳）: BSCに対する最適(n,4)二進符号のDong-Yang分類の機械チェックによる証明
Abstract要約: 我々は、二進対称チャネルに対する最適有限長$(n,4)$二進ブロック符号のドンとヤンの分類をLean4形式化する。正確性を確立するため、著者らはリーンの主要な定理文と受け入れられた公理を検証した。本稿では,AI生成の形式化に対する修正と単純化について論じるとともに,形式化時の論文に見られる相違点を記録する。
参考スコア（独自算出の注目度）: 7.827062001763223
License: http://creativecommons.org/licenses/by-nc-sa/4.0/
Abstract: We present a machine-checked Lean~4 formalization of Dong and Yang's classification of optimal finite-length $(n,4)$ binary block codes for binary symmetric channels. The formalization was developed mainly by feeding the paper's proofs to an AI tool. To establish correctness, the authors verified the main theorem statements in Lean and the accepted axioms. This note discusses the corrections and simplifications made to the AI-generated formalization, and records discrepancies found in the paper during the formalization. The Lean code is available at https://github.com/shhyang/n4code_lean.
Abstract（参考訳）: 機械チェックによるドンとヤンの最適有限長$(n,4)$バイナリブロック符号の定式化について述べる。この形式化は、主に論文の証明をAIツールに供給することによって開発された。正確性を確立するため、著者らはリーンの主要な定理文と受け入れられた公理を検証した。本稿では,AI生成の形式化に対する修正と単純化について論じるとともに,形式化時の論文に見られる相違点を記録する。 Leanコードはhttps://github.com/shhyang/n4code_lean.orgから入手できる。

関連論文リスト

Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics [20.90238876313568]
大きな言語モデル(LLM)は、人間の検出を避ける微妙なエラーを生成する。最近の傾向は、汎用LLMがリーンのために明確に調整されたより小さなモデルを上回っていることを示している。汎用LLMを用いたエージェントオートフォーマル化フレームワークを提案する。
論文参考訳（メタデータ） (2026-06-30T05:05:03Z)
LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
論文参考訳（メタデータ） (2026-06-02T08:16:42Z)
Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline [0.0]
我々は、ハイブリッドAI+Lean 4パイプラインとして、特許分析のための正式に検証されたフレームワークを提示します。 DAG被覆コア(Algorithm1b)は、有界マッチスコアが固定されると完全に機械検証される。クレームは、Lean 4でDAGとしてエンコードされ、強みを検証された完全な格子の要素と一致させ、信頼スコアは、証明された正しいモノトーン関数を通じて依存関係を通じて伝播する。
論文参考訳（メタデータ） (2026-04-20T22:02:57Z)
PBLean: Pseudo-Boolean Proof Certificates for Lean 4 [27.126691338850254]
PBLean は VeriPB pseudo-Boolean (PB) 証明証明書をLean 4 にインポートする手法である。リーンで完全証明され、コンパイルされたネイティブコードとして実行されるブールチェッカー関数。我々のチェッカーは、カットプレーンや証明・バイ・コントラディション・サブプロテクションを含む全てのVeriPBカーネルルールをサポートしている。
論文参考訳（メタデータ） (2026-02-09T14:13:30Z)
Statistical Learning Theory in Lean 4: Empirical Processes from Scratch [57.00315741159824]
本稿では,経験的プロセス理論に基づく統計学習理論(SLT)の総合的なLean 4形式化について述べる。エンドツーエンドの正式なインフラストラクチャは、最新のLean 4 Mathlibライブラリに欠けている内容を実装しています。この研究は再利用可能な形式基盤を確立し、機械学習理論の今後の発展への扉を開く。
論文参考訳（メタデータ） (2026-02-02T16:24:53Z)
Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification [49.506412445511934]
大きな言語モデル(LLM)は目覚ましい能力を示すが、その次は論理的不整合と報奨ハックを生み出す。本稿では,自然言語生成プロセスと形式的記号的検証を動的にインターリーブする形式論理検証誘導フレームワークを提案する。我々はこのフレームワークを,形式論理検証誘導制御による微調整とポリシー最適化の相乗効果を生かした,新しい2段階のトレーニングパイプラインを通じて運用する。
論文参考訳（メタデータ） (2026-01-30T07:01:25Z)
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)
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)
Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification [0.26763498831034044]
組込み戦術の力と既製の自動定理プローバーを利用するシステム内で使用される形式言語で全ての証明を生成するフレームワークを導入する。 LLMのトレーニングには2段階の微調整プロセスを使用し、まずSFTベースのトレーニングを使用して、モデルが構文的に正しいIsabelleコードを生成する。我々は,MiniF2F-testベンチマークとIsabelle証明アシスタントを用いてフレームワークを検証し,S3バケットアクセスポリシーコードの正当性を検証するためのユースケースを設計する。
論文参考訳（メタデータ） (2025-04-23T18:04:38Z)
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)
Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
論文参考訳（メタデータ） (2024-10-21T08:04:21Z)

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