論文の概要: GCD: Garbled, Corrected, Demonstrandum -- Fixing and Proving Go's Extended GCD Implementation

• arxiv url: http://arxiv.org/abs/2606.05796v2
• Date: Fri, 05 Jun 2026 02:47:18 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-08 14:33:29.320258
• Title: GCD: Garbled, Corrected, Demonstrandum -- Fixing and Proving Go's Extended GCD Implementation
• Title（参考訳）: GCD: Garbled, corrected, Demonstrandum -- Goの拡張GCD実装の修正と証明
• Authors: Linard Arquint,
• Abstract要約: Goの標準ライブラリの 'extendedGCD' 実装を検証する。 それぞれがアルゴリズムの不変性を破る2つの偏差を発見した。
• 参考スコア（独自算出の注目度）: 1.3311498879189612
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We verify the 'extendedGCD' implementation in Go's standard library ('crypto/internal/fips140/bigmod'), which plays a crucial role in the generation of RSA key pairs. Even though the Go implementation is supposedly a direct port from BoringSSL's implementation, we uncovered two deviations that each break the algorithm's invariants: (1) the Go implementation deviates in the way coefficients are updated, and (2) it permits a larger input domain. We address both deviations; the first by fixing the Go implementation, which results in an on average 24% speedup, and the second deviation by porting an existing proof for BoringSSL and extending it to cover the larger input domain. We prove correctness and termination of the fixed Go implementation using Gobra, a deductive program verifier for Go. Where necessary, we used Lean to prove key lemmata on non-linear arithmetic, which we import into Gobra. Our verification effort reveals three key insights: subtle bugs can slip into even well-reviewed code with surprising ease; formal verification is a powerful tool for uncovering them; and AI agents can facilitate the verification process by iteratively refining invariants and lemmata based on Gobra's error messages.
• Abstract（参考訳）: RSAキーペアの生成において重要な役割を果たすGoの標準ライブラリ('crypto/internal/fips140/bigmod')の'extendedGCD'実装を検証する。 Goの実装はBoringSSLの実装から直接移植されたものと思われるが、アルゴリズムの不変性を破る2つの逸脱を発見した。 ひとつはGoの実装の修正で、もうひとつは平均24%のスピードアップを実現し、もうひとつは既存のBoringSSLの証明を移植して、より大きな入力ドメインをカバーするように拡張したものです。 Goの演能的プログラム検証器であるGobraを用いて,Go実装の正当性と終了を証明した。 必要であれば、Leanを使って非線形算術のキーレマタを証明し、それをGobraにインポートしました。 微妙なバグは驚くほど簡単に精査されたコードに滑り込むことができ、形式的な検証はそれらを発見するための強力なツールであり、AIエージェントは、Gobraのエラーメッセージに基づいて不変量やレマタを反復的に修正することで、検証プロセスを促進することができます。

関連論文リスト

• Converted, Not Equivalent: Benchmarking Codebase Conversion via Observational Equivalence [56.25095230687242]
  コーディングエージェントは、しばしば自身のローカル検証ルーチンを過度に信頼し、表面チェックを満たすアーティファクトの成功を宣言する。 この問題は、事前評価が結果駆動である変換において特に深刻である。 ブラインド・コンバージョンは26.7-28.9%に達し、スペック・パスレートは91.1%まで上昇した。 このことは、失敗は限られた予算やバックボーンの強さよりも、契約ミスによる自己検証に起因していることを示唆している。
  論文  参考訳（メタデータ） (2026-05-27T19:57:15Z)
• Learning to Reason Efficiently with A* Post-Training [119.18396754931602]
  大規模言語モデルでは, A* 探索のガイダンスを用いて, 正確かつ効率的な証明を生成することができるかを検討する。 経験的に、1B--3B範囲のLlama-3.2モデルはA*ポストトレーニングの恩恵が大きいことが判明した。 より大きな探索空間では、不完全で訓練されたモデルの方が精度が高い。
  論文  参考訳（メタデータ） (2026-05-23T14:28:57Z)
• KVerus: Scalable and Resilient Formal Verification Proof Generation for Rust Code [15.778121969330476]
  我々は、VerusベースのRust検証のための検索拡張システムであるKVerusを紹介する。 KVerusは、コードメタデータ、レムマセマンティクス、ツールチェーン仕様の動的知識ベースを構築する。 複雑なファイル間の依存関係をナビゲートして証明を合成し、共通の進化的変化に直面した時に自動的に証明を修正することができる。
  論文  参考訳（メタデータ） (2026-05-05T14:50:24Z)
• Overcoming Joint Intractability with Lossless Hierarchical Speculative Decoding [58.92526489742584]
  我々は無益な無益な提案をする。 承認されたトークンの数を大幅に増加させる検証方法。 HSDは様々なモデルファミリやベンチマークの受け入れ率に一貫した改善をもたらすことを示す。
  論文  参考訳（メタデータ） (2026-01-09T11:10:29Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。 提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
  論文  参考訳（メタデータ） (2025-11-26T06:39:19Z)
• Less Greedy Equivalence Search [52.818153111470394]
  Greedy Equivalence Search (GES)は、観測データから因果探索を行うためのスコアベースのアルゴリズムである。 我々はGESの変種であるLose Greedy Equivalence Search (LGES)を開発した。
  論文  参考訳（メタデータ） (2025-06-27T15:39:48Z)
• Graph of Verification: Structured Verification of LLM Reasoning with Directed Acyclic Graphs [8.833716779340358]
  Graph of Verification (GoV)は、適応性と多粒性検証のための新しいフレームワークである。 GoVのコアイノベーションは、柔軟性のある"ノードブロック"アーキテクチャである。 GoVの適応的アプローチは、全体論的ベースラインと他の最先端の分解ベース手法の両方を著しく上回っている。
  論文  参考訳（メタデータ） (2025-06-14T13:46:03Z)
• VEL: A Formally Verified Reasoner for OWL2 EL Profile [0.0]
  VEL はマシンチェック可能な正当性証明を備えた公式な EL++ 推論器である。 本研究は,理論および実装レベルでの正確性を確保するために,推論アルゴリズムの機械化の必要性を実証するものである。
  論文  参考訳（メタデータ） (2024-12-11T19:17:28Z)

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

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