Dynamic Formal Systems
Truth by construction
The DFS lab is the main research division at Unusupicious. We bridge formal constructions of the world and it's physical substrate. Trying to close the gap between logic and the unsayable.
Main developppement product
AUFBAU
A typed prefix-parsing engine for constrained decoding.
The systems is named after Carnap's Der logische Aufbau der Welt. In the same way he tried to built the whole world on a rather small set of construction rules, AUFBAU makes the wager that LLMs guided by a correct-by-construction constraint layer. From a dynamically loaded typed grammar it constructs, token by token, only the continuations that keep a partial syntax tree well-formed and well-typed.
In the technical sense, its a prefix parser for a subset of attribute grammars.
The model interface lives in Proposition 7, where we use an oracle interface in the generation loop that allows us to verify if a token is a valid continuation of the current input. Validity is not only syntactic derivability but also semantic correctess.
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)
?B
AUFBAU grammar file format. Install with pip install aufbau-rs and get started with your own grammar files.
Research Focus
What the lab works on
Some of our areas of interest.
Constrained generation
We are buiding not only an engine but also a genealized theory of completability in context dependent languages. At the frontier between abstract semantics and concrete applications.
Proofs and Programs
Applying computer science techniques to logical reasoning, trying to discover the computational basis of intelligence.
Physical formalisms
Implementing physical dimensional analysis inside rust's type system with the SLUT crate. Used in simulations and scientific computing.
Meta-typed grammars
Making the meta-est theory of typed grammars.
Regex derivatives
Brzozowski derivatives for prefix validation: decide in one step whether a partial string can still complete to a match.
Interaction Nets and Computation graphs
Developpping a compute substrate for ML that uses parralelizable interaction nets.
State of affairs
What we've been doing
Work on the formal core
We welcome researchers, contributors, and the formally curious.