About
One program, many domains: novelty, diversity, and verification
I’m a postdoctoral researcher at Microsoft Research NYC. My work sits at the intersection of generative modeling, human‑AI interaction, and formal methods. Across creative domains (music, poetry, identity) and technical domains (code and verification), I focus on a single question: How do we generate many valid possibilities—and let humans steer them—while retaining guarantees when they matter?
Diversity, novelty, and anti‑homogenization: keep the set of “good answers” broad rather than collapsing to the mean.
Steering interfaces and “counter‑egos”: systems that amplify decisions instead of replacing the decision‑maker.
Structure, constraints, and verification: when reliability matters, make it explicit and checkable.
If you’re looking for a one‑liner: I work on distribution design under constraints—for art, for code, and for systems that people can trust.
Research Program
A common toolkit: constraints/specifications → many valid candidates → human steering
The distribution, not just the best guess
Many deployed systems optimize for a single “best” output, which can inadvertently encourage homogenization and reduce user agency. I instead treat generation as set construction: define what counts as valid, produce a diverse set of valid candidates, and expose controllable levers so people can navigate the space.
Option Space
Diversity & novelty as first‑class objectives
I build evaluation metrics and generation methods that resist collapse to a statistical mean, especially in settings where innovation, exploration, and perspective matter.
- Generative collisions / novelty metrics for text and structured outputs
- Sampling and search that produces many high‑quality alternatives, not one answer
- Diversity‑aware objectives aligned with real user goals
Control
Steering without erasing the human
I focus on controllability that feels human‑meaningful: compositional levers, identity‑grounded distributions, and collaborations that treat AI as a “counter‑ego,” not a replacement.
- Identity → distributions (HAI‑GEN @ IUI Workshops)
- Compositional steering for music transformers
- Creative tooling that preserves authorship and intent
Guarantees
Constraints, structure, and verification
When outputs must satisfy hard rules—musical form, program semantics, safety constraints—explicit structure and formal methods become the backbone of trustworthy generation.
- Relational‑constraint generative modeling (NeurIPS 2022)
- Program‑synthesis‑guided generative modeling (ICML 2019)
- LLM‑assisted verification tooling: generate and check artifacts, not just text
Work
Methods, systems, and public scholarship
MethodRelational‑Constraint Generation
Global coherence with checkable structure
Generative models for sequence data that obey relational constraints—useful when “locally good” isn’t enough and outputs must satisfy global structure.
MethodProgram‑Synthesis‑Guided Generation
Latent structure discovered by synthesis
Using program synthesis to discover and enforce latent structure, making generation more interpretable and controllable.
MethodCompositional Steering
Control without changing model parameters
Steering music transformer generation by composing controllable mechanisms, keeping the model’s capabilities while adding user levers.
SystemAI for Creativity
Essays and public‑facing projects on identity, authorship, and the future of creative work with generative systems.
SystemIdentity → Generative Distributions
From statements of self to usable creative option spaces
Methods for turning individual identity statements into “desirable” artistic distributions—supporting exploration rather than prescribing a single style.
DemosMusic Generation Experiments
Practical demonstrations of controllable music generation: tools that help musicians iterate, explore, and keep authorship.
FeaturedJuGeo — Judgment Geometry
Novelty, diversity, and verification in one system · thehalleyyoung.github.io/jugeo
Proof‑carrying Python verification via sheaf‑theoretic judgment geometry. Multi‑channel evidence (solver proofs, runtime witnesses, AI proposals) with trust accounting and cohomological obstruction analysis.
- AI‑generated proofs as first‑class evidence alongside Z3 and Lean
- Diverse evidence channels: many valid perspectives per judgment, not a single proof term
- 960+ modules, 93 Lean proofs, 13 decidable SMT fragments
Selected Publications
Unified by controllability, structure, and the production of many valid candidates
Across venues, the through‑line is consistent: make the implicit structure explicit, generate a set of valid candidates, and give people meaningful control over which region of the space they explore.
Shows how identity statements can be converted into usable, steerable distributions—supporting exploration and agency rather than prescribing a single “correct” output.
Develops methods for measuring and enforcing global coherence in generated sequences, maintaining both local quality and structural integrity.
Introduces steering mechanisms that add user control without retraining or parameter manipulation, preserving model capabilities while expanding controllability.
Uses program synthesis to discover latent structure that can guide generation, laying groundwork for interpretable and controllable generative modeling.
Experience
Roles spanning controllable generation, creative AI, and reliable systems
Microsoft Research, NYC
Postdoctoral Researcher
Developing algorithms and evaluation methods for diverse, steerable generation and for reliability‑oriented tooling that connects LLMs to checkable artifacts.
Google Brain / Magenta
Research Intern
Built controllable generative music models and tooling focused on user agency, avoiding both de‑agentification and homogenization.
Riffit
Software Engineer / Researcher
Research in automated music production for therapeutic purposes, resulting in a patent.
University of Pennsylvania
Teaching Assistant
TA for Graduate AI; Head TA for Graduate Applied ML. Emphasized both technical rigor and real‑world impacts of deployment.
Education
PhD in Computer Science
University of Pennsylvania
Research on controllable generative models and structure‑aware generation (including neurosymbolic approaches). Chateaubriand Fellow.
B.A. magna cum laude, Computer Science
New York University
Selected honors include the Faculty Memorial Prize and the Computer Science Prize for Outstanding Performance in Computer Science.
B.A. Candidate
University of Chicago
Awarded the Lilian Gertrude Selz Prize.
Skills
Programming Languages
Research Areas
Contact
Reach out for collaboration, speaking, or advising
© 2025–2026 Halley Young • Last updated March 2026