Frameworks
- LLM (In-context learning)
- AlphaGeometry (hybrid system)
- ? New Architecture
- ? (Finally) Neural Engine
2 - Auto-formalization
translate NL into FL less received than AI 4 theorem proving Argument: for semantic alignment, a better way to validate is just to do the proof Suggest: more unit tests(i..e examples) to improve redability of formalizaed artifact
3 - Scientific Verification
The ease of training AI to solve a task is proportional to how verifiable the task is
It might also be tempting to promote LLM autoformalization to other scientific fields, such as physics, chemistry, etc.
Q & A
- What is the middle language KELPS like
- it is a general syntax having a triple: “declaration, fact, query” for representing knowowledge
- with extensible libraries to deal with various theories
- What about autonomous theory discovery
- we need to first have a criteria of what is a good extension (of formal definitions …)
- this echos with the argument that definitions do not come alone, but need to be tested by whether theorems can be proved