Autoformalization and Formally Verifiable AI
Motivation & Goal
Autoformalization (converting natural language content into verifiable formalization) is considered a promising way of learning general purpose reasoning1.
In sharp contrast, existing natural language-based LLMs lack reliable verification, e.g., there seems to be no free lunch for inference scaling2, which is believed to be able to boost LLMs’ reasoning capabilities, as the verifier (reliable training signals) is not perfect for most cases.
Formal verifiers are not only important for safeguarded AI3, but also for steering the AI development into a direction I call maximally math-seeking, which could be, hopefully, more human-friendly.
Formal verification is usually extremely hard to obtain, and recent progress in automated reasoning could potentially make this approach easier. However, existing LLMs cannot do genuine logical reasoning or self-verification on their own, and they should be viewed as universal approximate knowledge retrievers (e.g., trying to mimic the reasoning steps seen during training)4. Given the important role of formal verifiers, I’m exploring ways of scaling up them.
A more detailed blog post is here
Approaches
We are focusing on the following approaches (not necessarily exclusive):
- Deep reinforcement learning
- Generative model, e.g., diffusion LM, autoregressive LM
- Formal verification
Seeking Collaboration
- If you are a full-time researcher (familiar with formal verification, software engineering, or deep RL) and is interested to collaborate, I’d be very happy to chat.
- If you are a student (eager to learn formal verification, software engineering, and deep RL – better already familiar with one of these), I could host you as an intern. See this page
Credits
Since this is a big and ambitious project, I believe that it is important to assign the correct amount credits to each member. I carefully divide it into a series of mini-projects. Each member is encouraged to take a lead in one of them, and each mini-project would hopefully result in an independent paper; More importantly, these mini-projects will be merged as the project to solve a big problem.
