論文の概要: s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs

• arxiv url: http://arxiv.org/abs/2603.14628v1
• Date: Sun, 15 Mar 2026 21:55:59 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-03-17 16:19:35.924411
• Title: s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs
• Title（参考訳）: s2n-bignum-bench:LLMの低レベルコード推論評価のための実用的なベンチマーク
• Authors: Balaji Rao, John Harrison, Soonho Kong, Juneyoung Lee, Carlo Lipizzi,
• Abstract要約: s2n-bignumは、暗号化の高速なアセンブリルーチンを提供するためにAWSで使用されるライブラリである。 textits2n-bignum-bench では、正式な仕様を提供し、HOL Light で受け入れられる証明スクリプトを生成するよう LLM に依頼する。 このベンチマークは、競争数学を超えて証明された LLM ベースの定理を評価する上で、挑戦的で実用的なテストベッドを提供する。
• 参考スコア（独自算出の注目度）: 0.45671221781968324
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Neurosymbolic approaches leveraging Large Language Models (LLMs) with formal methods have recently achieved strong results on mathematics-oriented theorem-proving benchmarks. However, success on competition-style mathematics does not by itself demonstrate the ability to construct proofs about real-world implementations. We address this gap with a benchmark derived from an industrial cryptographic library whose assembly routines are already verified in HOL Light. s2n-bignum is a library used at AWS for providing fast assembly routines for cryptography, and its correctness is established by formal verification. The task of formally verifying this library has been a significant achievement for the Automated Reasoning Group. It involved two tasks: (1) precisely specifying the correct behavior of a program as a mathematical proposition, and (2) proving that the proposition is correct. In the case of s2n-bignum, both tasks were carried out by human experts. In \textit{s2n-bignum-bench}, we provide the formal specification and ask the LLM to generate a proof script that is accepted by HOL Light within a fixed proof-check timeout. To our knowledge, \textit{s2n-bignum-bench} is the first public benchmark focused on machine-checkable proof synthesis for industrial low-level cryptographic assembly routines in HOL Light. This benchmark provides a challenging and practically relevant testbed for evaluating LLM-based theorem proving beyond competition mathematics. The code to set up and use the benchmark is available here: \href{https://github.com/kings-crown/s2n-bignum-bench}{s2n-bignum-bench}.
• Abstract（参考訳）: 大規模言語モデル(LLM)を形式的手法で活用するニューロシンボリックアプローチは,最近数学指向の定理証明ベンチマークにおいて大きな成果を上げている。 しかし、競争スタイルの数学における成功は、それ自体が実世界の実装に関する証明を構築する能力を示すものではない。 このギャップを、HOL Lightですでにアセンブリルーチンが検証されている産業用暗号ライブラリから派生したベンチマークで解決する。 s2n-bignumは、暗号化のための高速なアセンブリルーチンを提供するためにAWSで使用されているライブラリであり、その正確性は正式な検証によって確立されている。 このライブラリを正式に検証する作業は、Automated Reasoning Groupにとって重要な成果となった。 1) プログラムの正しい振る舞いを数学的命題として正確に指定し、(2) 命題が正しいことを証明する。 s2n-bignumの場合、どちらのタスクも人間の専門家によって実行された。 textit{s2n-bignum-bench} では、正式な仕様を提供し、固定された証明チェックタイムアウト内で HOL Light で受け入れられる証明スクリプトを生成するよう LLM に要求する。 我々の知る限り、textit{s2n-bignum-bench}はHOL Lightにおける産業用低レベル暗号アセンブリーの機械チェック可能な証明合成に焦点を当てた最初の公開ベンチマークである。 このベンチマークは、競争数学を超えて証明された LLM ベースの定理を評価する上で、挑戦的で実用的なテストベッドを提供する。 ベンチマークの設定と使用のためのコードは以下の通りである。

関連論文リスト

• BrokenMath: A Benchmark for Sycophancy in Theorem Proving with LLMs [5.347237827669862]
  大規模言語モデル(LLM)におけるサイコファンティック行動を評価するための最初のベンチマークであるBrokenMathを紹介する。 我々は最先端のLCMとエージェントシステムの評価を行い、最も優れたモデルであるGPT-5を用いて、梅毒の29%の回答が得られた。
  論文  参考訳（メタデータ） (2025-10-06T11:41:46Z)
• CLEVER: A Curated Benchmark for Formally Verified Code Generation [53.5486188696892]
  $rm Csmall LEVER$は、リーンにおけるエンドツーエンドのコード生成のための161の問題を、高品質でキュレートしたベンチマークである。 それぞれの問題は、(1)堅実な仕様と一致する仕様を生成するタスク、(2)この仕様を確実に満足するリーン実装を生成するタスクで構成されています。
  論文  参考訳（メタデータ） (2025-05-20T05:15:47Z)
• 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)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)

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

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