Formally verified AI
AUFBAU
A decoder enforcing semantic constraints on language models.
published
Agents forget the shape of a tool call, mistake the type of an in-context variable, or touch data they may not. AUFBAU rules that out while the model decodes.
Token by token, it builds continuations that keep a partial syntax tree well-formed and well-typed. The constraints are attributes you define on a context-free surface. They range from type constraints to relational rules between objects.
You give the model hard rules, and it cannot break them.
The safe-pruning proof is a paper proof of the rejection rules, not a mechanised proof of the code. Completion holds only for grammars that meet the paper's conditions. Nothing here says the output is true.
Variable(var) ::= Identifier[x]
BaseType ::= Identifier | '(' Type ')'
AtomicType ::= BaseType | '(' Type ')'
FunctionType ::= AtomicType '->' Type
Type ::= AtomicType | FunctionType
Lambda(lambda) ::= 'λ' Identifier[a] ':' Type[τ] '.' Expression[e]
AtomicExpression ::= Variable | '(' Expression ')' | Lambda
Application(app) ::= Expression[l] AtomicExpression[r]
Expression ::= AtomicExpression | Application
x ∈ Γ
----------- (var)
Γ(x)
Γ[a:τ] ⊢ e : ?B
--------------------------- (lambda)
τ → ?B
Γ ⊢ l : ?A → ?B, Γ ⊢ r : ?A
--------------------------------- (app)
?BSlides
