FormalAnswer - add logical rigor to AI responses with formal methods. It prompts the model to write a verifiable proof of the logic in its response using TLA+, Lean and/or Z3. This is tooling used by cryptographers, cloud infra eng, and mathematicians, so it has real-world legs.
The way the model uses the tools can be pretty inane though "Paris is the capital of France. Proof: Paris is not equal to France." If you prompt it properly, you do get usable outputs.
https://github.com/kig/formalanswer

No comments:
Post a Comment