Designing a Random Number Generator for Coq: A Practical Solution for A Language Engineering Toolbox

Abstract

The proposed approach by the authors involves developing a novel random number generator in Coq that satisfies three specific requirements - user-friendliness, independence from external libraries, and producing an acceptable level of randomness. To achieve this, they are seeking assistance from Generative AI and recommending the use of either OpenAI Playground or GitHub Copilot to automatically generate code. Additionally, the authors have modified their random generation code to cater to a newly defined language vocabulary group in their language engineering toolbox.

Background

When learning programming languages such as Java and Python, it is common for users to take the built-in random number generator for granted and become accustomed to its availability. However, designing a truly random generation mechanism requires careful consideration of many theoretical factors. This may be why the Coq (an Interactive Theorem Prover, a Proof Assistant, and a Reasoner) community has chosen not to enforce an opinionated random number generator in their standard libraries.

However, there is a practical need for a random number generation solution that allows us to explore a diverse range of valid language sequences within our predefined language structures, as defined by modern type theories.

The random number generator could be particularly useful in developing a semantic toolbox that utilizes the "Manifest" pattern, mentioned in below post:

By applying randomness to this pattern, we can specify incomplete language sentences and then leverage the generator to generate random candidates, providing a preview of the pattern. This approach could significantly improve productivity in using language specifications to build sophisticated language use cases.

Our goal is to propose a new method for building a random number generator in Coq that meets three specific criteria:

• First, it should be easy to use, requiring just a few lines of code.
• Second, it should not depend on external libraries. While we have found it useful to leverage sharable online environments like https://coq.vercel.app/ in the past, this approach is limited by the need for standard libraries. If we develop our own package with the random number generator, we may not be able to share our code on these platforms unless we work with the provider to load our library. Therefore, we should not rely on external libraries.
• Third, the generator should produce a reasonable degree of randomness, if not ideal.

Solution

We are seeking help from Generative AI.

Previously, programming languages often required the use of heavy-weight libraries to support random number generation. However, with the arrival of GPT-3, we can now simplify the process by generate random numbers through proper prompts, at each scenario we need it. While this approach may not necessarily result in reusable code, the prompting mechanism itself can be reused.

This aligns with our objective of emphasizing interactivity within our language engineering toolbox. As such, it is sufficient for users to utilize the OpenAI playground (https://platform.openai.com/playground) or GitHub Copilot, regardless of which one they choose, when designing languages. This enables them to generate the necessary code on an as-needed basis.

By eliminating the dependency on libraries, this approach can facilitate collaboration by utilizing online Coq environments such as https://coq.vercel.app/scratchpad.html. These environments only load commonly used libraries, and adding additional libraries can be a cumbersome process that requires significant setup time. Thanks to the generative AI, we now have a resource that greatly reduces the friction involved in sharing our work with the wider community.

The current working code is limited to the concept group containing six concepts, including Intellectual_Property and ChatGPT. The randomized function is implemented using the tactic code blocks that begin with "Complete a tactic sequence" and end with "End_block".

Inductive Randomizer:=
?| rand(n:nat).

Inductive Concept:=
? Intellectual_Property
?| ChatGPT
?| Quantum_computing | generative_ai | ethical_bias | responsible_ai
.

Definition randomizer_concept(r: Randomizer): Concept.
? ?destruct r.?
(** Complete a tactic sequence to build the randomizer, using a size 6 *)
(** First, the following pose command refers to the size 6 *)
? ?pose (Nat.modulo n 6) as N'.
(** And then, in the following refine block, there is a match statement. It will have size 6 cases, between 0 and the size minus 1 which is 5. Between 0 and 5 inclusive *)
? ?refine ((fun(n:nat)=>match n with?
? ? ? | 0 => _| 1 => _| 2 => _| 3 => _| 4 => _| 5 => _
(** The final case is needed *)
? ? ? | _ => _
? ? ?end) N').?
(** And then, the starting window is 0 plus one which is 1, ending window is size 6. Create a random non-repeating sequence between 1 and 6 inclusive.? *)?
(** 3 6 1 2 4 5 *)
(** Now, construct the number of constructors equal to the size 6, using above numbers as parameters *)
constructor 3. constructor 6. constructor 1. constructor 2. constructor 4. constructor 5.?
(** Finally, the following conclude, and the 1 is fixed *)
let EN:= 1 in let N:=EN in constructor N.
(** End_block *)
(** Complete a tactic sequence to build the randomizer, using a size ? *)
Defined.?

        

Adapt the Random Generation Code to New Scenario

Suppose that we need a group of Nouns of Animals to equip with a random enumerator.

We start with

Inductive Randomizer:
?| rand(n:nat).

Inductive Animal:=
? Dog | Cat | Tiger
 | Deer | Bird | Rabbit
?| Bug | Snake | Elephant
.

Definition randomizer_animal(r: Randomizer): Animal.
? ?destruct r.?
(** Complete a tactic sequence to build the randomizer, using a size 9 *)
        

Please be aware that the size has been changed from 6 to 9. The function "randomizer_animal" will generate random items and is defined to take an index, which should be a natural number, and produce a random item from the "Animal" group.

One can use the https://platform.openai.com/playground to generate the code automatically. To do so, you will need to go to the first code, copy and paste the section from "(** Complete a tactic sequence..." to "... End_block *)" into the playground. Then, copy the new prompt, which is the comment where the size changed from 6 to 9. Finally, you can trigger the auto-completion, and GPT-3 will apply one-shot learning to generate the entire new code block for you.

Some Coding Best Practices

Please note that the prompts are arranged in line with the code within the comments, for example, (** ... *). Note the over abundance of the references between the natural language comments and the code logic.

Furthermore, in order for the prompts to be effective, it is important to ensure that the explanatory text comes first, followed by the Noun. (LLM predicts the next token based on previous seen text.) This will be a useful best practice for Generative Coding.

Summary

Historically, there were significant limitations that hindered our ability to move quickly, and one of those limitations was related to generating random numbers. The overly strict frameworks made it challenging and expensive to innovate. If we were to adhere to the old approach for developing random number generation, it would take several weeks of effort.

However, with the current use case, where we do not require perfection, we can utilize Generative AI to quickly provide solutions that are sufficiently good to bridge the gap.