論文の概要: CUTECat: Concolic Execution for Computational Law

• arxiv url: http://arxiv.org/abs/2410.18212v1
• Date: Wed, 23 Oct 2024 18:30:23 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-10-25 12:50:25.287692
• Title: CUTECat: Concolic Execution for Computational Law
• Title（参考訳）: CUTECat: 計算法に関する訴訟執行
• Authors: Pierre Goutagny, Aymeric Fromherz, Raphaël Monat,
• Abstract要約: コンコリック実行ツール内でのデフォルトロジックの処理方法を示し、Catalaのコンテキストで私たちのアプローチを実装します。 我々は、フランス住宅給付のカタラ実施と米国税法第132条を評価した。
• 参考スコア（独自算出の注目度）: 1.1077637528502942
• License:
• Abstract: Many legal computations, including the amount of tax owed by a citizen, whether they are eligible to social benefits, or the wages due to civil state servants, are specified by computational laws. Their application, however, is performed by expert computer programs intended to faithfully transcribe the law into computer code. Bugs in these programs can lead to dramatic societal impact, e.g., paying employees incorrect amounts, or not awarding benefits to families in need. To address this issue, we consider concolic unit testing, a combination of concrete execution with SMT-based symbolic execution, and propose CUTECat, a concolic execution tool targeting implementations of computational laws. Such laws typically follow a pattern where a base case is later refined by many exceptions in following law articles, a pattern that can be formally modeled using default logic. We show how to handle default logic inside a concolic execution tool, and implement our approach in the context of Catala, a recent domain-specific language tailored to implement computational laws. We evaluate CUTECat on several programs, including the Catala implementation of the French housing benefits and Section 132 of the US tax code. We show that CUTECat can successfully generate hundreds of thousands of testcases covering all branches of these bodies of law. Through several heuristics, we improve CUTECat's scalability and usability, making the testcases understandable by lawyers and programmers alike. We believe CUTECat thus paves the way for the use of formal methods during legislative processes.
• Abstract（参考訳）: 市民が負う税の額、社会給付の資格、公務員による賃金などを含む多くの法的な計算は、計算法によって規定されている。 しかし、それらのアプリケーションは、法律を忠実にコンピュータコードに書き起こそうとする専門家のコンピュータプログラムによって実行される。 これらのプログラムのバグは、例えば、従業員に不適切な金額を支払ったり、必要な家族に利益を与えないといった、劇的な社会的影響をもたらす可能性がある。 この問題に対処するために,具体的な実行とSMTに基づくシンボリック実行の組み合わせであるコンコリック単体テストを検討し,計算法則の実装をターゲットとしたコンコリック実行ツールであるCUTECatを提案する。 このような法則は通常、基本ケースが後に多くの例外によって洗練されるパターンに従うが、これはデフォルトの論理を使って形式的にモデル化できるパターンである。 コンコリック実行ツール内でのデフォルトロジックの処理方法を示し、計算法則を実装するのに適した最近のドメイン固有言語である Catala のコンテキストで、我々のアプローチを実装します。 我々はCUTECatを、フランス住宅給付のカタラ実施や米国税法第132条など、いくつかのプログラムで評価する。 CUTECatは、これらの法律の全ての分野をカバーする何十万ものテストケースを正常に生成できることを示す。 いくつかのヒューリスティックスを通じて、私たちはCUTECatのスケーラビリティとユーザビリティを改善し、弁護士やプログラマが理解できるテストケースを作りました。 我々は、CUTECatが立法過程における形式的手法の活用の道を開くと信じている。

関連論文リスト

• Bayesian scaling laws for in-context learning [72.17734205418502]
  In-context Learning(ICL)は、言語モデルをトレーニング更新なしで複雑なタスクを実行するための強力なテクニックである。 我々は、ICCがベイズ学習者を近似し、ICCのための新しいベイズスケーリング法則のファミリーを開発することを示す。
  論文  参考訳（メタデータ） (2024-10-21T21:45:22Z)
• NExT: Teaching Large Language Models to Reason about Code Execution [50.93581376646064]
  大規模言語モデル(LLM)のコードは通常、プログラムの表面テキスト形式に基づいて訓練される。 NExTは,プログラムの実行トレースを検査し,実行時の動作を判断する手法である。
  論文  参考訳（メタデータ） (2024-04-23T01:46:32Z)
• Chain of Code: Reasoning with a Language Model-Augmented Code Emulator [115.16975276693267]
  我々は、LMコード駆動推論を改善するシンプルながら驚くほど効果的な拡張であるChain of Codeを提案する。 キーとなるアイデアは、プログラム内のセマンティックなサブタスクを、インタープリタが明示的にキャッチできるフレキシブルな擬似コードとしてフォーマットすることを、LMに促すことである。
  論文  参考訳（メタデータ） (2023-12-07T17:51:43Z)
• 'Put the Car on the Stand': SMT-based Oracles for Investigating Decisions [4.170056099990699]
  最小限の仮定の下では、自動推論はアルゴリズムの振る舞いを厳格に問うことができることを示す。 我々は、検証やレビューボードなどの説明責任プロセスを、非現実的な論理探索や抽象リファインメントループとしてモデル化する。 われわれのフレームワークを実装し、その実用性を実証的な自動車事故のシナリオで実証する。
  論文  参考訳（メタデータ） (2023-05-09T19:23:47Z)
• LEVER: Learning to Verify Language-to-Code Generation with Execution [64.36459105535]
  本稿では,プログラムの実行結果の検証を学習することで,言語からコードへの生成を改善するシンプルな手法であるLEVERを提案する。 具体的には、LLMからサンプリングされたプログラムが、自然言語入力、プログラム自体とその実行結果に基づいて正しいか否かを判定するために、検証者を訓練する。 LEVER はベースコード LLMs (4.6% から 10.9% まで) を継続的に改善し、それらすべてに対して新しい最先端の結果を得る。
  論文  参考訳（メタデータ） (2023-02-16T18:23:22Z)
• CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives (full version) [12.790826917588575]
  暗号は例外であり、多くのパフォーマンスクリティカルなルーチンがアセンブリで直接書かれてきた。 CryptOptは、GCCやClangが生成するものよりもはるかに高速なアセンブリコードに高レベルの暗号関数プログラムを専門とする、最初のコンパイルパイプラインである。 形式検証の面では、FiatOptフレームワーク(関数型プログラムをCライクなIRコードに変換する)に接続し、新たに公式に認証されたプログラム等価チェッカーで拡張する。
  論文  参考訳（メタデータ） (2022-11-19T11:07:39Z)
• Law Informs Code: A Legal Informatics Approach to Aligning Artificial Intelligence with Humans [0.0]
  法的な解釈と法的な解釈は、不透明な人間の価値を妥当な指令に変換する計算エンジンを形成する。 論理インフォームズ・コード(Law Informs Code)は、複雑な計算法的なプロセスを捉え、それらをAIに埋め込む研究課題である。
  論文  参考訳（メタデータ） (2022-09-14T00:49:09Z)
• The Dangers of Computational Law and Cybersecurity; Perspectives from Engineering and the AI Act [1.332091725929965]
  計算法は、しばらくの間予測されていた社会において役割を担ってきた。 本稿では,既知の課題を概観し,設計から物理領域まで,さまざまなレベルで議論する。 計算法則がグローバルに機能するために必要な3つの勧告を提示する。
  論文  参考訳（メタデータ） (2022-07-01T09:42:11Z)
• Metamorphic Testing and Debugging of Tax Preparation Software [2.185694185279913]
  我々はケーススタディのためのオープンソース税作成ソフトウェアに焦点をあてる。 我々は,納税ソフトの正しさを体系的に検証するランダム化テストケース生成戦略を開発した。
  論文  参考訳（メタデータ） (2022-05-10T16:10:10Z)
• Natural Language to Code Translation with Execution [82.52142893010563]
  実行結果-プログラム選択のための最小ベイズリスク復号化。 そこで本研究では,自然言語からコードへのタスクにおいて,事前訓練されたコードモデルの性能を向上することを示す。
  論文  参考訳（メタデータ） (2022-04-25T06:06:08Z)
• ReACC: A Retrieval-Augmented Code Completion Framework [53.49707123661763]
  本稿では,語彙のコピーと類似したセマンティクスを持つコード参照の両方を検索により活用する検索拡張コード補完フレームワークを提案する。 我々は,Python および Java プログラミング言語のコード補完タスクにおけるアプローチを評価し,CodeXGLUE ベンチマークで最先端のパフォーマンスを実現する。
  論文  参考訳（メタデータ） (2022-03-15T08:25:08Z)

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

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