論文の概要: Trust the Spec, Not the Code - A Specification-First, AI-Assisted Case Study in Online Banking
- arxiv url: http://arxiv.org/abs/2609.07365v1
- Date: Mon, 07 Sep 2026 11:35:49 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-12 00:42:53.951118
- Title: Trust the Spec, Not the Code - A Specification-First, AI-Assisted Case Study in Online Banking
- Title（参考訳）: 仕様を信頼する - コードではなく - オンラインバンキングにおける仕様ファースト、AI支援ケーススタディ
- Abstract要約: 形式的な仕様は、早期エラー検出、明示的な不変性、設計による正しさを約束するが、その表記コストは主流の実践から遠ざかっている。
AIは推論と証明に十分な精度の中間仕様言語として機能する、と我々は主張する。
仕様は、著者、レビュー、証明、洗練の成果物となり、コードは再生可能な出力になる。
- 参考スコア（独自算出の注目度）: 1.6796354350132203
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Formal specification promises early error detection, explicit invariants, and correctness by design, yet its notational cost has kept it out of mainstream practice. We argue that AI removes much of that cost: natural language enriched with lightweight mathematics, written in \LaTeX, can serve as an intermediate specification language that is precise enough to reason over and prove, while a large language model (LLM) reviews it for ambiguity, drafts proofs, and generates the implementation. The specification becomes the artifact one authors, reviews, proves, and refines; the code becomes regenerable output. This paper is a follow-on to a prior study that established the discipline on an organizational-knowledge-growth simulation~\cite{predecessor2026}. Here we replicate the discipline in a different domain---an online-banking fund-transfer service---and extend it. The two domains share one spine: a conservation invariant (knowledge in the prior study, money here), which suggests the approach generalizes across domains. We contribute: (i) a second, independent case study of the method; (ii) a stress-test of the method on a richer problem---\emph{scheduled/recurring} transfers---whose generated code grows substantially while the invariant and its proof do not; (iii) an \emph{AI-proposed runtime coverage model} for invariants (``never violated $\neq$ covered''); and (iv) a Z formalization, including paired success/failure operation schemas and an invariant proved over the inductive set of all reachable configurations, together with an experiment in which the AI proposes the Z interfaces itself. We are explicit about the method's limits: the proofs and runtime checks live at the specification level and do not establish that the generated code refines the specification---that step is delegated to the AI. This is a case study, not a controlled experiment.
- Abstract（参考訳）: 形式的な仕様は、早期エラー検出、明示的な不変性、設計による正しさを約束するが、その表記コストは主流の実践から遠ざかっている。
ラテXで書かれた軽量な数学に富んだ自然言語は、推論と証明に十分正確な中間仕様言語として機能し、大きな言語モデル(LLM)は曖昧さをレビューし、証明をドラフトし、実装を生成する。
仕様は、著者、レビュー、証明、洗練の成果物となり、コードは再生可能な出力になる。
本稿では,組織-知識・成長シミュレーションの規律を確立した先行研究のフォローアップである。
ここでは、異なるドメイン — オンラインバンキングファンドのトランスファーサービス — で規律を再現し、それを拡張します。
2つの領域は1つのスピンを共有している: 保存不変量(以前の研究では、ここではお金)は、このアプローチが領域をまたいで一般化することを示唆している。
コントリビューション:
一 方法の独立した第二の事例研究
(ii) よりリッチな問題に対するメソッドのストレステスト---\emph{scheduled/recurring} 転送-- 生成したコードは、不変量とその証明がそうでない間に著しく増大する。
(iii)不変量に対する \emph{AI-proposed Runtime coverage model} (``never violated $\neq$ covered'') そして
(iv) 成功/失敗操作スキーマとすべての到達可能な構成の帰納的セットに対する不変性を含むZの形式化と、AIがZインターフェース自体を提案する実験。
証明と実行時チェックは仕様レベルで生きており、生成されたコードが仕様を洗練することを保証するものではない。
これはケーススタディで、制御された実験ではありません。
関連論文リスト
- Eigenius: A Typed Knowledge-Graph DBMS with Epistemic Stratification and Institution-Mediated Reasoning [0.0]
Eigeniusは、単一の前提に基づいて構築された知識グラフである。
これは、データ証明をサブシステムの境界を越えて再構成された特性ではなく、構造的不変量に変換する。
論文 参考訳（メタデータ） (2026-08-05T05:28:22Z) - A Formalization of the Mean-Field Derivation of the Vlasov Equation: AI-Assisted Lean Formalization as a Strategy Game [0.0]
我々は、数学者がAIシステムに指示することで、Lean 4証明アシスタントの研究結果を形式化し、そのアクティビティを形式化ゲームとしてフレーム化する。
目的は文書をリーンに変えることである。ゲームは開発がコンパイルされたときに勝利し、残念なことは含まない。マシンチェックは、目標定理がリーンの基本公理にのみ依存していることを示している。
ケーススタディは、ドブルシンの平均場経路を通した非線形ブラソフ方程式の正当性に対する完全で公理クリーンな定式化である。
論文 参考訳（メタデータ） (2026-07-09T23:17:54Z) - LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization [104.06650149974585]
信頼性の高い研究レベルのLean AutoformalizationのためのマルチエージェントハーネスであるLeanMarathonを紹介します。
4つのコントラクトスコープエージェントがこの青写真を構築し、監査し、証明し、修復する。
我々は4つのErds問題にまたがる最近の2つの研究論文でLeanMarathonを評価した。
論文 参考訳（メタデータ） (2026-06-03T20:09:39Z) - The Deterministic Horizon: Impossibility Results as Design Specifications for Trustworthy AI Systems [0.0]
この論文は、好奇心から不合理性の結果を設計規則に変える。
そのフラッグシップとなる結果は、アーキテクチャだけで設定された精度の高い天井を証明している。
同じ引数がサブフィールドにまたがって再キャストされる。
論文 参考訳（メタデータ） (2026-05-21T20:48:35Z) - DPrivBench: Benchmarking LLMs' Reasoning for Differential Privacy [50.73304874527716]
差分プライバシー(DP)は、データプライバシーを保護する幅広いアプリケーションを持っているが、DPアルゴリズムの設計と検証には専門家レベルの推論が必要である。
DPrivBenchは、各インスタンスが、ある関数やアルゴリズムが指定されたDP保証を満たすかどうかを問うベンチマークである。
実験によると、最強のモデルは教科書の仕組みをうまく扱えるが、全てのモデルは高度なアルゴリズムに苦しむ。
論文 参考訳（メタデータ） (2026-04-17T09:03:11Z) - The Specification as Quality Gate: Three Hypotheses on AI-Assisted Code Review [0.0]
AIが生成するコード品質の問題に対する業界の主要な反応は、AIレビュアーをデプロイすることだ。
本稿では,実行可能な仕様が存在しない場合,この応答は構造的に円形であると主張している。
論文 参考訳（メタデータ） (2026-03-26T11:59:05Z) - BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。
提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
論文 参考訳（メタデータ） (2025-11-26T06:39:19Z) - What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus [2.8003002159083237]
我々は,2つの言語で作業する8人の専門家から,詳細なソースコードテレメトリの収集と解析を行うユーザスタディを実施している。
その結果、専門家が証明開発プロセスで遭遇した重要な課題や証明についてどのように考えるかについて興味深い傾向とパターンが明らかになった。
我々はこれらの知見を,AI証明アシスタントのための具体的な設計指針に翻訳する。
論文 参考訳（メタデータ） (2025-08-01T22:16:30Z) - 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) - MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳（メタデータ） (2024-02-14T05:57:58Z) - Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。
NLProofSは仮説に基づいて関連するステップを生成することを学習する。
EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文 参考訳（メタデータ） (2022-05-25T02:22:30Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。