2025-11-24T09:28:17.353555

Herb.jl: A Unifying Program Synthesis Library

Hinnerichs, Reid, de Jong et al.

Program synthesis -- the automatic generation of code given a specification -- is one of the most fundamental tasks in artificial intelligence (AI) and many programmers' dream. Numerous synthesizers have been developed to tackle program synthesis, manifesting different ideas to approach the exponentially growing program space. While numerous smart program synthesis tools exist, reusing and remixing previously developed methods is tedious and time-consuming. We propose Herb.jl, a unifying program synthesis library written in the Julia programming language, to address these issues. Since current methods rely on similar building blocks, we aim to modularize the underlying synthesis algorithm into communicating and fully extendable sub-compartments, allowing for straightforward reapplication of these modules. To demonstrate the benefits of using Herb.jl, we show three common use cases: 1. how to implement a simple problem and grammar, and how to solve it, 2. how to implement a previously developed synthesizer with just a few lines of code, and 3. how to run a synthesizer against a benchmark.

academic

Herb.jl: 統一プログラム合成ライブラリ

基本情報

論文ID: 2510.09726
タイトル: Herb.jl: A Unifying Program Synthesis Library
著者: Tilman Hinnerichs, Reuben Gardos Reid, Jaap de Jong, Bart Swinkels, Pamela Wochner, Nicolae Filat, Tudor Magurescu, Issa Hanou, Sebastijan Dumancic (Technische Universiteit Delft)
分類: cs.PL（プログラミング言語）、cs.AI（人工知能）、cs.SE（ソフトウェア工学）
発表時期: Journal of Machine Learning Research 10 (2025) 1-48、提出 10/25
論文リンク: https://arxiv.org/abs/2510.09726

概要

プログラム合成——与えられた仕様から自動的にコードを生成すること——は人工知能における最も基本的なタスクの一つであり、多くのプログラマーの夢でもあります。指数関数的に増加するプログラム空間に対処するための多くの知的なプログラム合成ツールが開発されてきましたが、既存の方法の再利用と再組み合わせは煩雑で時間がかかります。本論文では、これらの問題を解決するためにJulia プログラミング言語で記述された統一プログラム合成ライブラリであるHerb.jlを提案しています。既存の方法が類似した構成要素に依存しているため、著者らは基礎となる合成アルゴリズムを相互通信可能で完全に拡張可能なサブコンポーネントにモジュール化し、これらのモジュールの直接的な再適用を可能にすることを目指しています。

研究背景と動機

核心的な問題

プログラム合成分野は4つの主要な問題に直面しています：

ドメイン特異性：合成器の実装は通常、特定の言語向けに設計されており、新しい構文規則への適応が困難です
モジュール化の不足：同じ構成要素を容易に再利用できず、研究者は同じ考え方を繰り返し実装する必要があります
比較の困難さ：エンジニアリング上の選択肢の違いにより、方法の比較は実装品質の比較に陥りがちです
ベンチマークの再利用の困難さ：ベンチマークの構文規則の選択は暗黙的であることが多く、公正な比較に影響を与えます

研究動機

既存のプログラム合成方法は各自のドメインで優れた性能を示していますが、以下の制限があります：

実装が過度に特殊化されており、再利用性の計画が不足しています
プログラム合成分野全体にわたるモジュール化設計が不足しています
暗黙的な仮定と最適化により、方法の比較が困難になります
ベンチマークの構文規則定義が統一されていません

核心的な貢献

Herb.jlの提案：Julia言語で記述された新規の統一プログラム合成ライブラリ
モジュール化実装の実証：Herb.jlを使用して既存の合成器を容易に実装する方法を実証
標準化されたベンチマークの提供：標準ベンチマークを人間が読める拡張可能な形式で再実装
設計原則の総括：Herb.jlの指導設計原則を概説し、他の合成器実装の参考となる知見を提供

方法の詳細説明

タスク定義

プログラム合成問題は2つのコンポーネントで定義されます：

仕様（Specification）：ユーザーの意図を記述し、通常は入出力例を通じて表現されます
文法（Grammar）：対象言語を記述し、文脈自由導出規則で構成されます

アーキテクチャ設計

Herb.jlは階層的モジュール化アーキテクチャを採用し、以下の核心コンポーネントを含みます：

核心モジュール

HerbCore.jl：文法、プログラム、制約のインターフェースを定義
HerbSpecification.jl：問題仕様定義を処理
HerbGrammar.jl：プログラム構文構造を定義
HerbInterpret.jl：プログラムセマンティクスと評価を処理
HerbConstraints.jl：制約の定式化と伝播
HerbSearch.jl：探索方法と列挙技術

特殊モジュール

Herb.jl：全体的なラッパーモジュール
HerbBenchmarks.jl：標準ベンチマークセット
Garden.jl：既知の合成器の実装セット

技術的革新点

1. 構文とセマンティクスの分離

Herb.jlは構文とセマンティクスを明確に分離します：

プログラム列挙は純粋に構文に基づき、抽象構文木（AST）の更新を通じて完成
プログラムは仕様をチェックするために実行可能な式に変換
ユーザーは実行可能な式を提供するだけで、内部メカニズムを理解する必要がありません

2. 統一木構造

「統一木」という独自のデータ構造を導入：

類似した形状の操作は類似した形状のプログラムを生成
統一ノードは単一の操作ではなく、同じ形状の操作ドメインを記述
メモリ使用量を大幅に削減し、効率的な制約の適用と伝播をサポート

3. 列挙順序の最適化

2つの関数によってプログラム列挙順序を定義：

優先度関数：優先度キュー内の要素の優先度値を定義
導出ヒューリスティック：統一木内の要素ドメインの列挙順序を定義

実験設定

ユースケースの実証

ケース1：簡単な問題定義と解決

# 入出力仕様を定義
problem = Problem([
    IOExample(Dict(:x => 0), 1),
    IOExample(Dict(:x => 1), 3),
    IOExample(Dict(:x => 2), 5),
    IOExample(Dict(:x => 3), 7)
])

# 文法を定義
grammar = @cfgrammar begin
    Int = 1 | 2 | x
    Int = Int + Int
    Int = Int * Int
end

# 探索を実行
iterator = BFSIterator(grammar, :Int, max_depth=5)
solution, flag = synth(problem, iterator)

ケース2：Probeアルゴリズムの実装

Probeシンセサイザーを数行のコードで再実装する方法を実証：

最も可能性の高い優先探索イテレータ（MLFSIterator）の実装
確率計算関数の定義
Probeループロジックの実装

ケース3：ベンチマーク実行

using HerbBenchmarks
pairs = get_all_problem_grammar_pairs(PBE_SLIA_Track_2019)

solved_problems = 0
for (problem, grammar) in pairs
    solution = probe(grammar, :Start, problem; max_depth=5)
    if !isnothing(solution)
        solved_problems += 1
    end
end