論文の概要: Djinnlang: Higher-Level Programming by Unambiguous Specification with an LLM in the Compiler

• arxiv url: http://arxiv.org/abs/2609.23954v1
• Date: Mon, 21 Sep 2026 00:00:09 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-23 18:04:03.958974
• Title: Djinnlang: Higher-Level Programming by Unambiguous Specification with an LLM in the Compiler
• Title（参考訳）: Djinnlang: コンパイラのLLMによる曖昧な仕様による高レベルプログラミング
• Abstract要約: 我々は、この未来のために構築された高レベルな仕様言語であるDjinnlangを紹介します。 Djinnlangプログラムは仕様のみで構成されます。
• 参考スコア（独自算出の注目度）: 0.9600874183831257
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Programmers write formal specifications, and LLMs implement them, proving that each implementation matches its spec. Taken to its extreme, this makes specification languages the new programming languages. We argue that an unambiguity constraint is key: in addition to proving that its implementation satisfies the specification, the LLM must also prove that any other implementation satisfying it must produce the same outputs on the same inputs, i.e. that the relation formed by the constraints is deterministic. This leaves the LLM no leeway on program semantics: as with a conventional compiler, the generated code never needs to be read and can be regenerated from the spec at any time. Under this constraint and with a powerful LLM, the difference between a specification language and a programming language becomes essentially meaningless, and the LLM essentially becomes a part of the compiler toolchain. The arrangement doubles as a strong form of AI control: an untrusted model writes the code, yet its work is tightly checked by a verifier. To demonstrate that our LLM-in-the-compiler paradigm is feasible when supported by our unambiguity constraint, we present Djinnlang, a high-level specification language built for this future. A Djinnlang program consists only of specifications --- the programmer never writes executable code. In place of a traditional compiler, a symbolic translator lowers each spec to Dafny stubs and proof obligations, and a driver harness orchestrates an LLM that fills in implementations and proofs, all checked by the Dafny verifier. We evaluate our language and implementation on multiple examples and we show that it is self-hosting: an LLM can implement the Djinnlang translator from its specification and the reimplementation can verify itself.
• Abstract（参考訳）: プログラマは形式的な仕様を書き、LCMはそれを実装し、それぞれの実装が仕様と一致することを証明します。 極端なことに、これは仕様言語を新しいプログラミング言語にする。 実装が仕様を満たすことの証明に加えて、LCMは、同じ入力に対して同じ出力を生成する必要があること、すなわち、制約によって生成された関係が決定論的であることの証明も必要である。 従来のコンパイラと同様に、生成されたコードは読み取り不要で、いつでも仕様から再生できる。 この制約と強力なLLMでは、仕様言語とプログラミング言語の違いは本質的に意味のないものとなり、LLMは基本的にコンパイラツールチェーンの一部となる。 信頼できないモデルがコードを書き込むが、検証者によってその作業が厳密にチェックされる。 LLM-in-the-compilerパラダイムは、あいまいな制約によってサポートされた場合、実現可能であることを示すために、この未来のために構築された高レベルの仕様言語であるDjinnlangを紹介します。 Djinnlangプログラムは仕様のみで構成されます。 従来のコンパイラの代わりに、シンボリックトランスレータは各仕様をダフニースタブと証明義務に格下げし、ドライバーハーネスは実装と証明を埋めるLLMを編成し、すべてダフニー検証器でチェックする。 LLMはDjinnlangトランスレータを仕様から実装することができ、再実装は自身を検証できます。

関連論文リスト

• The Fools are Certain; the Wise are Doubtful: Exploring LLM Confidence in Code Completion [4.215010577170175]
  コードパープレキシティの測定により,コード生成時のLLM(Large Language Models)の信頼性を評価する。 強い型付け言語は動的型付け言語よりも難易度が低いことがわかった。 Perlは難易度が普遍的に高いが、Javaは低いように見える。
  論文  参考訳（メタデータ） (2025-08-22T06:51:13Z)
• IFEvalCode: Controlled Code Generation [69.28317223249358]
  本稿では,Code LLMの命令追従能力を改善するために,前方および後方制約生成を提案する。 IFEvalCodeは、7つのプログラミング言語の1.6Kテストサンプルからなる多言語ベンチマークである。
  論文  参考訳（メタデータ） (2025-07-30T08:08:48Z)
• Can LLMs Replace Humans During Code Chunking? [2.4056836012742]
  大規模言語モデル(LLM)は、特にコード理解と生成に関わるタスクにおいて、コンピュータ科学において重要なツールとなっている。 本稿では,ALC および MUMPS で記述されたレガシ行政コードの近代化における LLM の適用について検討する。
  論文  参考訳（メタデータ） (2025-06-24T13:02:35Z)
• Type-Constrained Code Generation with Language Models [51.03439021895432]
  本稿では,型システムを利用してコード生成を誘導する型制約デコード手法を提案する。 そこで本研究では,新しい接頭辞オートマトンと,在来型を探索する手法を開発し,LLM生成コードに適切な型付けを強制するための健全なアプローチを構築した。 提案手法は,コード合成,翻訳,修復作業において,コンパイルエラーを半分以上削減し,機能的正しさを著しく向上させる。
  論文  参考訳（メタデータ） (2025-04-12T15:03:00Z)
• ExeCoder: Empowering Large Language Models with Executability Representation for Code Translation [57.604506522287814]
  既存の大きな言語モデル(LLM)は、事前トレーニング中にのみコードのコンテキスト意味を学習する。 機能的セマンティクスや構文構造,変数依存性といった実行可能性表現を活用するために,ExeCoderを提案する。 ExeCoderは、既存のオープンソースコードLLMを10.88%以上、38.78%以上、27.44%以上、42.97%以上という、2つのメトリクスで、最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2025-01-30T16:18:52Z)
• InverseCoder: Self-improving Instruction-Tuned Code LLMs with Inverse-Instruct [43.7550233177368]
  本稿では、微調整されたオープンソースモデルを用いて、追加データを生成して命令調整データセットを拡張できるかどうかを考察する。 Inverse-Instructは、微調整 LLM を用いて、独自のトレーニングデータセットからコード応答の追加命令を生成するデータ拡張手法である。
  論文  参考訳（メタデータ） (2024-07-08T08:00:05Z)
• If LLM Is the Wizard, Then Code Is the Wand: A Survey on How Code Empowers Large Language Models to Serve as Intelligent Agents [81.60906807941188]
  大型言語モデル(LLM)は、自然言語と形式言語(コード)の組み合わせに基づいて訓練される コードは、標準構文、論理一貫性、抽象化、モジュール性を備えた高レベルの目標を実行可能なステップに変換する。
  論文  参考訳（メタデータ） (2024-01-01T16:51:20Z)

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

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