論文の概要: From Scientific Texts to Verifiable Code: Automating the Process with Transformers

• arxiv url: http://arxiv.org/abs/2501.05252v1
• Date: Thu, 09 Jan 2025 14:03:35 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-01-10 14:00:45.091854
• Title: From Scientific Texts to Verifiable Code: Automating the Process with Transformers
• Title（参考訳）: 科学的テキストから検証可能なコードへ:トランスフォーマーによるプロセスの自動化
• Authors: Changjie Wang, Mariano Scazzariello, Marco Chiesa,
• Abstract要約: トランスフォーマーは 研究論文を読めます 正式な証明を持つアルゴリズムを 提案し これらの証明を 検証可能なコードに翻訳します このアプローチは形式的検証の障壁を大幅に減らすことができると我々は主張する。
• 参考スコア（独自算出の注目度）: 2.536225150399618
• License:
• Abstract: Despite the vast body of research literature proposing algorithms with formal guarantees, the amount of verifiable code in today's systems remains minimal. This discrepancy stems from the inherent difficulty of verifying code, particularly due to the time-consuming nature and strict formalism of proof details that formal verification tools require. However, the emergence of transformers in Large Language Models presents a promising solution to this challenge. In this position paper, we believe that transformers have the potential to read research papers that propose algorithms with formal proofs and translate these proofs into verifiable code. We leverage transformers to first build a formal structure of the proof using the original text from the paper, and then to handle the tedious, low-level aspects of proofs that are often omitted by humans. We argue that this approach can significantly reduce the barrier to formal verification. The above idea of reading papers to write verifiable code opens new avenues for automating the verification of complex systems, enabling a future where formally verified algorithms from academic research can more seamlessly transition into real-world software systems, thereby improving code reliability and security.
• Abstract（参考訳）: 公式な保証付きアルゴリズムを提案する膨大な研究論文にもかかわらず、今日のシステムにおける検証可能なコードの量は最小限である。 この違いは、コード検証が本質的に困難であること、特に形式的な検証ツールが必要とする、時間を要する性質と証明の詳細の厳密な形式性に起因している。 しかし、大規模言語モデルにおけるトランスフォーマーの出現は、この課題に対する有望な解決策を示します。 本稿では,形式的証明を伴うアルゴリズムを提案し,それらの証明を検証可能なコードに変換する研究論文を,トランスフォーマーが読むことができると考えている。 トランスフォーマーを利用して、まず論文の原文を使って証明の形式的構造を構築し、次に人間によってしばしば省略される証明の退屈で低レベルな側面を扱う。 このアプローチは形式的検証の障壁を大幅に減らすことができると我々は主張する。 上記の検証可能なコードを書くための論文を読むというアイデアは、複雑なシステムの検証を自動化するための新たな道を開き、学術研究から公式に検証されたアルゴリズムが現実世界のソフトウェアシステムによりシームレスに移行し、コードの信頼性とセキュリティを向上させる未来を可能にします。

関連論文リスト

• Enhancing Code Consistency in AI Research with Large Language Models and Retrieval-Augmented Generation [0.0]
  本稿では,対応する研究論文に概説されたアルゴリズムと方法論に対するコード実装の検証を目的とした,新しいシステムを提案する。 本システムではRetrieval-Augmented Generationを用いて研究論文とコードベースの両方から関連する詳細を抽出し,続いてLarge Language Modelを用いた構造化比較を行った。
  論文  参考訳（メタデータ） (2025-02-02T00:35:42Z)
• VEL: A Formally Verified Reasoner for OWL2 EL Profile [0.0]
  VEL はマシンチェック可能な正当性証明を備えた公式な EL++ 推論器である。 本研究は,理論および実装レベルでの正確性を確保するために,推論アルゴリズムの機械化の必要性を実証するものである。
  論文  参考訳（メタデータ） (2024-12-11T19:17:28Z)
• AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement [25.80131224070207]
  生成したコードが正しいことを数学的に保証するために,形式検証を利用することを目標としている。 LLMによる正式な認証コードの生成は、トレーニングデータの不足と、形式的な証明の複雑さによって妨げられる。 我々は、公式に認証されたコード生成をブートストラップする自己改善フレームワークであるAlphaVerusを紹介した。
  論文  参考訳（メタデータ） (2024-12-09T03:22:35Z)
• Analogous Alignments: Digital "Formally" meets Analog [0.0]
  本稿では,デジタルブロックとアナログブロックを組み合わせた混合信号知的特性(IP)の実用的形式検証に着目する。 Digital and Analog Mixed-Signal (AMS)設計は、本質的に異なるが、形式的な検証設定でシームレスに統合される。
  論文  参考訳（メタデータ） (2024-09-23T13:38:31Z)
• Knowledge-Augmented Language Model Verification [68.6099592486075]
  最近の言語モデル(LM)は、パラメータに内在化された知識を持つテキストを生成する際、印象的な能力を示している。 本稿では,知識付加型LMの出力と知識を別個の検証器で検証することを提案する。 その結果,提案した検証器は,検索と生成の誤りを効果的に識別し,LMがより現実的に正しい出力を提供できることを示した。
  論文  参考訳（メタデータ） (2023-10-19T15:40:00Z)
• FacTool: Factuality Detection in Generative AI -- A Tool Augmented Framework for Multi-Task and Multi-Domain Scenarios [87.12753459582116]
  より広い範囲のタスクは、生成モデルによって処理されると、事実エラーを含むリスクが増大する。 大規模言語モデルにより生成されたテキストの事実誤りを検出するためのタスクおよびドメインに依存しないフレームワークであるFacToolを提案する。
  論文  参考訳（メタデータ） (2023-07-25T14:20:51Z)
• A Simple, Yet Effective Approach to Finding Biases in Code Generation [16.094062131137722]
  この研究は、現在のコード生成システムが、彼らの大きな言語モデルバックボーンから受け継がれた望ましくないバイアスを示すことを示している。 コーディング課題のモジュラー分解と解析を可能にする「影響ブロック」の概念を提案する。
  論文  参考訳（メタデータ） (2022-10-31T15:06:15Z)
• GERE: Generative Evidence Retrieval for Fact Verification [57.78768817972026]
  本稿では,ジェネレーション方式で証拠を検索する最初のシステムであるGEREを提案する。 FEVERデータセットの実験結果は、GEREが最先端のベースラインよりも大幅に改善されていることを示している。
  論文  参考訳（メタデータ） (2022-04-12T03:49:35Z)
• Synthetic Disinformation Attacks on Automated Fact Verification Systems [53.011635547834025]
  本研究では,2つのシミュレーション環境において,自動ファクトチェッカーの合成正反対証拠に対する感度について検討する。 これらのシステムでは,これらの攻撃に対して大幅な性能低下がみられた。 偽情報の発生源としての現代のNLGシステムの脅威の増大について論じる。
  論文  参考訳（メタデータ） (2022-02-18T19:01:01Z)
• Evidence-Aware Inferential Text Generation with Vector Quantised Variational AutoEncoder [104.25716317141321]
  本稿では,大規模なテキストコーパスからイベントの証拠を自動的に発見し,その証拠を利用して推論テキストの生成を導く手法を提案する。 このアプローチは、Event2MindとATOMICの両方のデータセットで最先端のパフォーマンスを提供します。
  論文  参考訳（メタデータ） (2020-06-15T02:59:52Z)
• Robustness Verification for Transformers [165.25112192811764]
  我々はトランスフォーマーのための最初のロバスト性検証アルゴリズムを開発した。 提案手法で計算したロバスト性境界は, 素粒子間境界伝播法で計算したロバスト性境界よりもかなり厳密である。 これらの境界はまた、感情分析における異なる単語の重要性を常に反映しているトランスフォーマーの解釈にも光を当てている。
  論文  参考訳（メタデータ） (2020-02-16T17:16:31Z)

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

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