Pith. sign in

REVIEW 2 cited by

The SyGuS Language Standard Version 2.1

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2312.06001 v1 pith:BMJPVU5A submitted 2023-12-10 cs.PL

Saswat Padhi , Elizabeth Polgreen , Mukund Raghothaman , Andrew Reynolds , Abhishek Udupa This is my paper · ORCID
classification cs.PL
keywords standardgivenproblemspecificationsyguscorrectnesslanguagecandidate
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original abstract

The classical formulation of the program-synthesis problem is to find a program that meets a correctness specification given as a logical formula. Syntax-guided synthesis (SyGuS) is a standardized format for specifying the correctness specification with a syntactic template that constrains the space of allowed implementations. The input to SyGuS consists of a background theory, a semantic correctness specification for the desired program given by a logical formula, and a syntactic set of candidate implementations given by a grammar. The computational problem then is to find an implementation from the set of candidate expressions that satisfies the specification in the given theory. The formulation of the problem builds on SMT-LIB. This document defines the SyGuS 2.1 standard, which is intended to be used as the standard input and output language for solvers targeting the syntax-guided synthesis problem. It borrows many concepts and language constructs from the standard format for Satisfiability Modulo Theories (SMT) solvers, the SMT-LIB 2.6 standard.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Recursive Program Synthesis from Sketches and Mixed-Quantifier Properties

    cs.LO 2026-01 conditional novelty 7.0 of 10

    Cataclyst synthesizes recursive programs from mixed-quantifier first-order specs by synthesizing Skolem witness functions alongside the target program and pruning candidates with counterexample-derived syntactic constraints.

  2. Online Prompt Selection for Program Synthesis

    cs.AI 2025-01 conditional novelty 6.0 of 10

    An online multi-armed bandit that selects among symbolic solvers and LLM-prompt combinations for program synthesis solves 37.2% more queries than the best single solver and reaches 96% of the virtual best solver's per...

Pith tools